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(_).