1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | ||
6 | :- module(typechecker,[type_check/2, term_is_of_type/3, | |
7 | (type)/1, check_types/0, | |
8 | ground_check/1, debug_non_ground_term/1, | |
9 | check_cyclic/1]). | |
10 | ||
11 | ||
12 | /* ------------------------ */ | |
13 | /* TYPE CHECKER FOR PROLOG */ | |
14 | /* ------------------------ */ | |
15 | ||
16 | :- op(1150, fx, type). | |
17 | :- op(500,yfx,+-->). | |
18 | ||
19 | :- use_module(tools_printing, [print_error/1]). | |
20 | ||
21 | :- use_module(module_information). | |
22 | :- module_info(group,testing). | |
23 | :- module_info(description,'A very basic runtime type checker for Prolog.'). | |
24 | ||
25 | /* | |
26 | ============================================================================= | |
27 | Using the type checker: | |
28 | ============================================================================= | |
29 | ||
30 | 1) Built-in types: | |
31 | ||
32 | The following are built-in types: | |
33 | any | |
34 | ground | |
35 | nonground | |
36 | var | |
37 | nonvar | |
38 | integer | |
39 | float | |
40 | number | |
41 | atom | |
42 | atomic | |
43 | ask(Type) [ask user whether of type] | |
44 | call(Module:Predicate) [calls an external unary predicate to check the type] | |
45 | ||
46 | The following are built-in type constructors: | |
47 | list/1 -> list(TypeOfListElements) | |
48 | vlist/1 -> same as list/1 except that variables also match this type | |
49 | term/2 -> term(Functor,ListOfTypesForArguments) | |
50 | vterm/2 -> same as term/2 except that variables also match this type | |
51 | ||
52 | ============================================================================= | |
53 | ||
54 | 2) Defining your own types: | |
55 | ||
56 | just enter type/2 definitions for each type you want to use, like: | |
57 | ||
58 | type(program,list(clause)). | |
59 | type(clause,term(cl,[atom,list(atom)])). | |
60 | type(atom,any). | |
61 | ||
62 | You can also define your own type constructors: | |
63 | ||
64 | type(binary_tree(Type),term(null,[])). | |
65 | type(binary_tree(Type), | |
66 | term(tree,[binary_tree(Type),Type,binary_tree(Type)])). | |
67 | ||
68 | ============================================================================= | |
69 | ||
70 | 3) Type checking: | |
71 | ||
72 | Just call: | |
73 | term_is_of_type([1,2,3],list(integer)). | |
74 | term_is_of_type(tree(null,1,null),binary_tree(ground)). | |
75 | ||
76 | You can also call | |
77 | check_for_illegal_types. | |
78 | to test whether you have introduced some illegal type definitions | |
79 | (it might currently loop for badly defined types like "type(rec,rec)." ). | |
80 | ============================================================================= | |
81 | */ | |
82 | ||
83 | ground_check(X) :- (ground(X) -> true ; | |
84 | print_error('### Not ground: '), print_error(X),nl,debug_non_ground_term(X),fail). | |
85 | ||
86 | debug_non_ground_term(X) :- var(X),!, print('-> top level is variable: '), print(X),nl. | |
87 | debug_non_ground_term(X) :- debug_non_ground_term(X,[]). | |
88 | ||
89 | debug_non_ground_term(X,_) :- ground(X),!. | |
90 | debug_non_ground_term(X,T) :- X =.. [Fun|Args], l_debug_ng(Args,[Fun|T],1). | |
91 | ||
92 | l_debug_ng([],_,_). | |
93 | l_debug_ng([H|T],Hist,NrOfArg) :- | |
94 | (var(H) -> print('--> Arg #'), print(NrOfArg), print(' of '), print(Hist),nl ; debug_non_ground_term(H,Hist)), | |
95 | A1 is NrOfArg+1, | |
96 | l_debug_ng(T,Hist,A1). | |
97 | ||
98 | :- dynamic user_defined_type/2. | |
99 | % SHOULD NOT BE VOLATILE ! | |
100 | ||
101 | type(Type +--> Def) :- assert_user_type(Type,Def),!. | |
102 | type(Type = Def) :- assert_user_type(Type,Def),!. | |
103 | type(TD) :- print_error('### Illegal Type Declaration: '), print_error(TD),nl. | |
104 | ||
105 | ||
106 | assert_user_type(Type,Def) :- | |
107 | %print_message(add_type(Type,Def)), | |
108 | translate_type_def(Def,TranslatedDef,Type),!, | |
109 | (user_defined_type(Type,OldDef) | |
110 | -> (OldDef = TranslatedDef -> true | |
111 | ; print_error('### Type Clash for: '), print_error(Type), | |
112 | print_error(OldDef), print_error(TranslatedDef) | |
113 | ) | |
114 | ; (predefined_type(Type) | |
115 | -> print_error('### Trying to redefine built-in type: '), print_error(Type) | |
116 | ; assertz(user_defined_type(Type,TranslatedDef)) | |
117 | ) | |
118 | ). | |
119 | assert_user_type(Type,Def) :- | |
120 | print_error('### Could not translate type description for type:'), | |
121 | print_error(Type), print_error(Def). | |
122 | ||
123 | translate_type_def(X,any,_) :- var(X),!,print_error('### Variable Type !'). | |
124 | translate_type_def(call(Module:Call),call(Module:Call),_) :- !. | |
125 | translate_type_def(type(X),X,_) :- !. | |
126 | translate_type_def(list(X),list(TX),Cur) :- !, translate_type_def(X,TX,Cur). | |
127 | translate_type_def(vlist(X),vlist(TX),Cur) :- !, translate_type_def(X,TX,Cur). | |
128 | translate_type_def((X;Y),(TX;TY),Cur) :- !, | |
129 | translate_type_def(X,TX,Cur), translate_type_def(Y,TY,Cur). | |
130 | translate_type_def(term(F,A),term(F,TA),Cur) :- !, l_translate_type_def(A,TA,Cur). | |
131 | translate_type_def(vterm(F,A),vterm(F,TA),Cur) :- !, l_translate_type_def(A,TA,Cur). | |
132 | translate_type_def(X,X,CurType) :- (predefined_type(X) ; user_defined_type(X,_) ; X=CurType),!. | |
133 | translate_type_def(X,term(Fun,TArgs),Cur) :- nonvar(X), X =.. [Fun|Args], !, | |
134 | l_translate_type_def(Args,TArgs,Cur). | |
135 | translate_type_def(X,X,_) :- | |
136 | print_message(informational,'*** Forward type reference'), print_message(informational,X). | |
137 | ||
138 | l_translate_type_def([],[],_Cur). | |
139 | l_translate_type_def([A|T],[AT|TT],Cur) :- | |
140 | translate_type_def(A,AT,Cur), l_translate_type_def(T,TT,Cur). | |
141 | ||
142 | /* ----------------- */ | |
143 | /* predefined_type/1 */ | |
144 | /* ----------------- */ | |
145 | ||
146 | /* checks whether something is a predefined type */ | |
147 | ||
148 | predefined_type(any). | |
149 | predefined_type(ground). | |
150 | predefined_type(nonground). | |
151 | predefined_type(var). | |
152 | predefined_type(nonvar). | |
153 | predefined_type(integer). | |
154 | predefined_type(float). | |
155 | predefined_type(number). | |
156 | predefined_type(atom). | |
157 | predefined_type(atomic). | |
158 | predefined_type(simple). | |
159 | predefined_type(compound). | |
160 | predefined_type(mutable). | |
161 | predefined_type(list(_X)). | |
162 | predefined_type(term(_F,_TL)). | |
163 | predefined_type(vlist(_X)). | |
164 | predefined_type(vterm(_F,_TL)). | |
165 | predefined_type(ask(_T)). | |
166 | predefined_type(call(_)). | |
167 | ||
168 | /* ------------------------ */ | |
169 | ||
170 | :- public print_types/0. | |
171 | print_types :- print_message(informational,'---------'),user_defined_type(Type,Descr), | |
172 | print_message(informational,type(Type,Descr)),fail. | |
173 | print_types :- print_message(informational,'---------'). | |
174 | ||
175 | /* ------------------------ */ | |
176 | /* legal_type_description/1 */ | |
177 | /* ------------------------ */ | |
178 | ||
179 | /* checks whether something is a legal type description */ | |
180 | ||
181 | check_types :- % print('% Checking user defined types: '), | |
182 | user_defined_type(Type,Descr), | |
183 | (legal_type_description(Descr) -> true %,(print(Type),print(' ')) | |
184 | ; print_error('### Error in type definition:'), print_error(Type), | |
185 | print_error(Descr)), | |
186 | fail. | |
187 | check_types :- % print('% Checking user defined types: '), | |
188 | user_defined_type(Type,Descr), user_defined_type(Type,Descr2), | |
189 | Descr \= Descr2, | |
190 | print_error('### Multiple Definitions for type:'), print_error(Type), | |
191 | fail. | |
192 | check_types. % :- nl. | |
193 | ||
194 | legal_type_description(X) :- var(X),!,fail. | |
195 | legal_type_description(any) :- !. | |
196 | legal_type_description(ground) :- !. | |
197 | legal_type_description(nonground) :- !. | |
198 | legal_type_description(var) :- !. | |
199 | legal_type_description(nonvar) :- !. | |
200 | legal_type_description(integer) :- !. | |
201 | legal_type_description(float) :- !. | |
202 | legal_type_description(number) :- !. | |
203 | legal_type_description(atom) :- !. | |
204 | legal_type_description(atomic) :- !. | |
205 | legal_type_description(compound) :- !. | |
206 | legal_type_description(simple) :- !. | |
207 | legal_type_description(mutable) :- !. | |
208 | legal_type_description(ask(_Type)) :- !. | |
209 | legal_type_description(call(Call)) :- Call=Module:Pred,atomic(Module),atomic(Pred),!. | |
210 | legal_type_description(list(Type)) :- !, | |
211 | legal_type_description(Type). | |
212 | legal_type_description(vlist(Type)) :- !, | |
213 | legal_type_description(Type). | |
214 | legal_type_description(term(Functor,TypeList)) :- !, | |
215 | (length(TypeList,Arity),functor(T,Functor,Arity), | |
216 | user_defined_type(T,_) | |
217 | -> print_message(informational,'*** Warning: term also exists as type:'), print_message(informational,T) | |
218 | ; true | |
219 | ), | |
220 | l_legal_type_description(TypeList). | |
221 | legal_type_description(vterm(_Functor,TypeList)) :- !, | |
222 | l_legal_type_description(TypeList). | |
223 | legal_type_description((Type1 ; Type2)) :- !, | |
224 | legal_type_description(Type1),!,legal_type_description(Type2). | |
225 | legal_type_description(Type) :- | |
226 | \+(predefined_type(Type)), | |
227 | user_defined_type(Type,_Descr),!. | |
228 | legal_type_description(type(Type)) :- !,print_error('### Illegal type descriptor: '), | |
229 | print('### type/1 can only be used in type definitions'), | |
230 | print_error(Type),fail. | |
231 | legal_type_description(Type) :- print_error('### Illegal type descriptor: '), | |
232 | print_error(Type),fail. | |
233 | ||
234 | l_legal_type_description([]). | |
235 | l_legal_type_description([Type1|Rest]) :- | |
236 | legal_type_description(Type1), | |
237 | l_legal_type_description(Rest). | |
238 | ||
239 | ||
240 | /* ----------------- */ | |
241 | /* term_is_of_type/2 */ | |
242 | /* ----------------- */ | |
243 | ||
244 | type_check(Term,Type) :- %print_message(type_check(Term,Type)), | |
245 | reset_type_error, | |
246 | (term_is_of_type(Term,Type,yes) | |
247 | -> \+(type_error_occurred) | |
248 | ; \+(type_error_occurred), print_type_error(Term,Type,yes,type_check),fail). | |
249 | ||
250 | ||
251 | /* ----------------- */ | |
252 | /* term_is_of_type/3 */ | |
253 | /* ----------------- */ | |
254 | ||
255 | /* if the third argument is yes then an error message is printed if the | |
256 | type check does not succeed and the call to term_is_of_type | |
257 | will NEVER FAIL !! */ | |
258 | /* if the third argument is different from yes than no message will be printed | |
259 | but the call will fail if the type check fails */ | |
260 | ||
261 | /* term_is_of_type(Term,Descr,PE) :- | |
262 | print(tiot(Term,Descr)),nl,fail. */ | |
263 | ||
264 | term_is_of_type(Term,Descr,PrintErrMsg) :- | |
265 | is_inf(Term),!, | |
266 | print_inf_error(Term,Descr,PrintErrMsg), | |
267 | read(_Cont). | |
268 | ||
269 | % TODO: move second argument to first for indexing: | |
270 | term_is_of_type(_Term,any,_PrintErrMsg) :- | |
271 | !. /* anything is of type any */ | |
272 | term_is_of_type(Term,ground,_PrintErrMsg) :- | |
273 | ground(Term),!. | |
274 | term_is_of_type(Term,nonground,_PrintErrMsg) :- | |
275 | \+(ground(Term)),!. | |
276 | term_is_of_type(Term,var,_PrintErrMsg) :- | |
277 | var(Term),!. | |
278 | term_is_of_type(Term,nonvar,_PrintErrMsg) :- | |
279 | nonvar(Term),!. | |
280 | term_is_of_type(Term,integer,_PrintErrMsg) :- | |
281 | integer(Term),!. | |
282 | term_is_of_type(Term,float,_PrintErrMsg) :- | |
283 | float(Term),!. | |
284 | term_is_of_type(Term,number,_PrintErrMsg) :- | |
285 | number(Term),!. | |
286 | term_is_of_type(Term,atom,_PrintErrMsg) :- | |
287 | atom(Term),!. | |
288 | term_is_of_type(Term,atomic,_PrintErrMsg) :- | |
289 | atomic(Term),!. | |
290 | term_is_of_type(Term,compound,_PrintErrMsg) :- | |
291 | compound(Term),!. | |
292 | term_is_of_type(Term,simple,_PrintErrMsg) :- | |
293 | \+ compound(Term),!. | |
294 | term_is_of_type(Term,mutable,_PrintErrMsg) :- | |
295 | mutable(Term),!. | |
296 | term_is_of_type(Term,ask(Type),_PrintErrMsg) :- | |
297 | !, | |
298 | print('Type => '),print(Type),nl, | |
299 | print('Term => '),print(Term),nl, | |
300 | print('(y or n) =>'),read(UserChoice), | |
301 | UserChoice=y. | |
302 | term_is_of_type(Term,call(Module:Predicate),_PrintErrMsg) :- | |
303 | functor(Call,Predicate,1), | |
304 | arg(1,Call,Term), | |
305 | call(Module:Call). | |
306 | term_is_of_type(Term,list(Type),PrintErrMsg) :- | |
307 | var(Term),!, | |
308 | print_type_error(Term,list(Type),PrintErrMsg,term_is_of_type). | |
309 | term_is_of_type([],list(_Type),_PrintErrMsg) :- !. | |
310 | term_is_of_type([Head|Tail],list(Type),PrintErrMsg) :- | |
311 | term_is_of_type(Head,Type,PrintErrMsg),!, | |
312 | term_is_of_type(Tail,list(Type),yes). | |
313 | term_is_of_type(Term,vlist(_Type),_PrintErrMsg) :- | |
314 | var(Term),!. /* also to avoid modifying Term in the next 2 clauses */ | |
315 | term_is_of_type([],vlist(_Type),_PrintErrMsg) :- !. | |
316 | term_is_of_type([Head|Tail],vlist(Type),PrintErrMsg) :- | |
317 | term_is_of_type(Head,Type,PrintErrMsg),!, | |
318 | term_is_of_type(Tail,vlist(Type),yes). | |
319 | term_is_of_type(Term,term(Functor,ArgTypeList),PrintErrMsg) :- | |
320 | var(Term),!, | |
321 | print_type_error(Term,term(Functor,ArgTypeList),PrintErrMsg,term_is_of_type_var). | |
322 | term_is_of_type(Term,term(Functor,ArgTypeList),_PrintErrMsg) :- | |
323 | Term =.. [Functor|Args],!, | |
324 | l_term_is_of_type(Args,ArgTypeList,yes), !. | |
325 | term_is_of_type(Term,vterm(_Functor,_ArgTypeList),_PrintErrMsg) :- | |
326 | var(Term),!. /* also to avoid modifying Term in the next clause */ | |
327 | term_is_of_type(Term,vterm(Functor,ArgTypeList),_PrintErrMsg) :- | |
328 | Term =.. [Functor|Args],!, | |
329 | l_term_is_of_type(Args,ArgTypeList,yes), !. | |
330 | term_is_of_type(Term,Type,PrintErrMsg) :- | |
331 | \+(predefined_type(Type)), | |
332 | user_defined_type(Type,Descr), /* user defined type; we assume single definition exists */ | |
333 | !, | |
334 | term_is_of_type(Term,Descr,PrintErrMsg). | |
335 | term_is_of_type(Term,(Type1 ; Type2),PrintErrMsg) :- | |
336 | (term_is_of_type(Term,Type1,no) -> true | |
337 | ; term_is_of_type(Term,Type2,PrintErrMsg)), | |
338 | !. | |
339 | term_is_of_type(Term,Type,PrintErrMsg) :- | |
340 | print_type_error(Term,Type,PrintErrMsg,term_is_of_type_catchall). | |
341 | ||
342 | ||
343 | l_term_is_of_type([],[],_PrintErrMsg). | |
344 | l_term_is_of_type([Term1|Rest],[Type1|TypeList],PrintErrMsg) :- | |
345 | term_is_of_type(Term1,Type1,PrintErrMsg),!, | |
346 | l_term_is_of_type(Rest,TypeList,PrintErrMsg). | |
347 | ||
348 | print_type_error(T,Type,_,PP) :- | |
349 | (legal_type_description(Type) -> true | |
350 | ; print_error(pp(PP)),print_error(illegal_type(Type)),print_error(term(T))), | |
351 | fail. | |
352 | print_type_error(Term,Type,PrintErrMsg,PP) :- PrintErrMsg\=no, nl, | |
353 | %print(err(Term,Type)),nl,nl, | |
354 | print_error('### Type Error Occured! Type:'),print_error(Type), | |
355 | print_error('### Term:'),safe_print_term(Term),nl, | |
356 | print_error('### ProgramPoint:'),safe_print_term(PP),nl, | |
357 | assert_type_error. | |
358 | ||
359 | ||
360 | print_inf_error(Term,Type,PrintErrMsg) :- PrintErrMsg \= no, nl, | |
361 | print_error('### Cyclic Term Error: Requested Type '),print_error(Type), | |
362 | print_error('### Term: '),safe_print_term(Term),nl, | |
363 | assert_type_error. | |
364 | ||
365 | safe_print_term(X) :- var(X),!,print(X). | |
366 | safe_print_term(X) :- is_inf(X),!, | |
367 | X =.. [Func|Args], | |
368 | print(Func),print('('), | |
369 | l_safe_print(Args), | |
370 | print(')'). | |
371 | safe_print_term(X) :- print(X). | |
372 | ||
373 | l_safe_print([]). | |
374 | l_safe_print([Term|T]) :- | |
375 | (is_inf(Term) | |
376 | -> (print('!CYCLIC!('),write_term(Term,[max_depth(3)]),print(')')) | |
377 | ; (print(Term)) | |
378 | ), | |
379 | (T=[] -> true ; print(',') ), | |
380 | l_safe_print(T). | |
381 | ||
382 | :- dynamic type_error/1. | |
383 | type_error(no). | |
384 | ||
385 | assert_type_error :- | |
386 | retract(type_error(_N)),fail. | |
387 | assert_type_error :- | |
388 | assertz(type_error(yes)). | |
389 | ||
390 | ||
391 | reset_type_error :- | |
392 | retract(type_error(_N)),fail. | |
393 | reset_type_error :- | |
394 | assertz(type_error(no)). | |
395 | ||
396 | type_error_occurred :- | |
397 | type_error(yes). | |
398 | ||
399 | ||
400 | ||
401 | :- use_module(library(terms)). | |
402 | is_inf(X) :- cyclic_term(X). | |
403 | ||
404 | check_cyclic(X) :- cyclic_term(X),!, | |
405 | print('### Cyclic Term : '), nl, | |
406 | safe_print_term(X),nl, | |
407 | fail. | |
408 | check_cyclic(_). |