1		% (c) 2009-2019 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		real
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		; assert(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(real).
155		predefined_type(number).
156		predefined_type(atom).
157		predefined_type(atomic).
158		predefined_type(list(_X)).
159		predefined_type(term(_F,_TL)).
160		predefined_type(vlist(_X)).
161		predefined_type(vterm(_F,_TL)).
162		predefined_type(ask(_T)).
163		predefined_type(call(_)).
164
165		/* ------------------------ */
166
167		:- public print_types/0.
168		print_types :- print_message(informational,'---------'),user_defined_type(Type,Descr),
169		print_message(informational,type(Type,Descr)),fail.
170		print_types :- print_message(informational,'---------').
171
172		/* ------------------------ */
173		/* legal_type_description/1 */
174		/* ------------------------ */
175
176		/* checks whether something is a legal type description */
177
178		check_types :- % print('% Checking user defined types: '),
179		user_defined_type(Type,Descr),
180		(legal_type_description(Descr) -> true %,(print(Type),print(' '))
181		; print_error('### Error in type definition:'), print_error(Type),
182		print_error(Descr)),
183		fail.
184		check_types :- % print('% Checking user defined types: '),
185		user_defined_type(Type,Descr), user_defined_type(Type,Descr2),
186		Descr \= Descr2,
187		print_error('### Multiple Definitions for type:'), print_error(Type),
188		fail.
189		check_types. % :- nl.
190
191		legal_type_description(X) :- var(X),!,fail.
192		legal_type_description(any) :- !.
193		legal_type_description(ground) :- !.
194		legal_type_description(nonground) :- !.
195		legal_type_description(var) :- !.
196		legal_type_description(nonvar) :- !.
197		legal_type_description(integer) :- !.
198		legal_type_description(real) :- !.
199		legal_type_description(number) :- !.
200		legal_type_description(atom) :- !.
201		legal_type_description(atomic) :- !.
202		legal_type_description(ask(_Type)) :- !.
203		legal_type_description(call(Call)) :- Call=Module:Pred,atomic(Module),atomic(Pred),!.
204		legal_type_description(list(Type)) :- !,
205		legal_type_description(Type).
206		legal_type_description(vlist(Type)) :- !,
207		legal_type_description(Type).
208		legal_type_description(term(Functor,TypeList)) :- !,
209		((length(TypeList,Arity),functor(T,Functor,Arity),
210		user_defined_type(T,_))
211		-> print_message(informational,'*** Warning: term also exists as type:'), print_message(informational,T)
212		; true
213		),
214		l_legal_type_description(TypeList).
215		legal_type_description(vterm(_Functor,TypeList)) :- !,
216		l_legal_type_description(TypeList).
217		legal_type_description((Type1 ; Type2)) :- !,
218		legal_type_description(Type1),!,legal_type_description(Type2).
219		legal_type_description(Type) :-
220		\+(predefined_type(Type)),
221		user_defined_type(Type,_Descr),!.
222		legal_type_description(type(Type)) :- !,print_error('### Illegal type descriptor: '),
223		print('### type/1 can only be used in type definitions'),
224		print_error(Type),fail.
225		legal_type_description(Type) :- print_error('### Illegal type descriptor: '),
226		print_error(Type),fail.
227
228		l_legal_type_description([]).
229		l_legal_type_description([Type1|Rest]) :-
230		legal_type_description(Type1),
231		l_legal_type_description(Rest).
232
233
234		/* ----------------- */
235		/* term_is_of_type/2 */
236		/* ----------------- */
237
238		type_check(Term,Type) :- %print_message(type_check(Term,Type)),
239		reset_type_error,
240		(term_is_of_type(Term,Type,yes)
241		-> \+(type_error_occurred)
242		; \+(type_error_occurred), print_type_error(Term,Type,yes,type_check),fail).
243
244
245		/* ----------------- */
246		/* term_is_of_type/3 */
247		/* ----------------- */
248
249		/* if the third argument is yes then an error message is printed if the
250		type check does not succeed and the call to term_is_of_type
251		will NEVER FAIL !! */
252		/* if the third argument is different from yes than no message will be printed
253		but the call will fail if the type check fails */
254
255		/* term_is_of_type(Term,Descr,PE) :-
256		print(tiot(Term,Descr)),nl,fail. */
257
258		term_is_of_type(Term,Descr,PrintErrMsg) :-
259		is_inf(Term),!,
260		print_inf_error(Term,Descr,PrintErrMsg),
261		read(_Cont).
262
263		term_is_of_type(_Term,any,_PrintErrMsg) :-
264		!. /* anything is of type any */
265		term_is_of_type(Term,ground,_PrintErrMsg) :-
266		ground(Term),!.
267		term_is_of_type(Term,nonground,_PrintErrMsg) :-
268		\+(ground(Term)),!.
269		term_is_of_type(Term,var,_PrintErrMsg) :-
270		var(Term),!.
271		term_is_of_type(Term,nonvar,_PrintErrMsg) :-
272		nonvar(Term),!.
273		term_is_of_type(Term,integer,_PrintErrMsg) :-
274		integer(Term),!.
275		term_is_of_type(Term,real,_PrintErrMsg) :-
276		float(Term),!.
277		term_is_of_type(Term,number,_PrintErrMsg) :-
278		number(Term),!.
279		term_is_of_type(Term,atom,_PrintErrMsg) :-
280		atom(Term),!.
281		term_is_of_type(Term,atomic,_PrintErrMsg) :-
282		atomic(Term),!.
283		term_is_of_type(Term,ask(Type),_PrintErrMsg) :-
284		!,
285		print('Type => '),print(Type),nl,
286		print('Term => '),print(Term),nl,
287		print('(y or n) =>'),read(UserChoice),
288		UserChoice=y.
289		term_is_of_type(Term,call(Module:Predicate),_PrintErrMsg) :-
290		functor(Call,Predicate,1),
291		arg(1,Call,Term),
292		call(Module:Call).
293		term_is_of_type(Term,list(Type),PrintErrMsg) :-
294		var(Term),!,
295		print_type_error(Term,list(Type),PrintErrMsg,term_is_of_type).
296		term_is_of_type([],list(_Type),_PrintErrMsg) :- !.
297		term_is_of_type([Head|Tail],list(Type),PrintErrMsg) :-
298		term_is_of_type(Head,Type,PrintErrMsg),!,
299		term_is_of_type(Tail,list(Type),yes).
300		term_is_of_type(Term,vlist(_Type),_PrintErrMsg) :-
301		var(Term),!. /* also to avoid modifying Term in the next 2 clauses */
302		term_is_of_type([],vlist(_Type),_PrintErrMsg) :- !.
303		term_is_of_type([Head|Tail],vlist(Type),PrintErrMsg) :-
304		term_is_of_type(Head,Type,PrintErrMsg),!,
305		term_is_of_type(Tail,vlist(Type),yes).
306		term_is_of_type(Term,term(Functor,ArgTypeList),PrintErrMsg) :-
307		var(Term),!,
308		print_type_error(Term,term(Functor,ArgTypeList),PrintErrMsg,term_is_of_type_var).
309		term_is_of_type(Term,term(Functor,ArgTypeList),_PrintErrMsg) :-
310		Term =.. [Functor|Args],!,
311		l_term_is_of_type(Args,ArgTypeList,yes), !.
312		term_is_of_type(Term,vterm(_Functor,_ArgTypeList),_PrintErrMsg) :-
313		var(Term),!. /* also to avoid modifying Term in the next clause */
314		term_is_of_type(Term,vterm(Functor,ArgTypeList),_PrintErrMsg) :-
315		Term =.. [Functor|Args],!,
316		l_term_is_of_type(Args,ArgTypeList,yes), !.
317		term_is_of_type(Term,Type,PrintErrMsg) :-
318		\+(predefined_type(Type)),
319		user_defined_type(Type,Descr), /* user defined type; we assume single definition exists */
320		!,
321		term_is_of_type(Term,Descr,PrintErrMsg).
322		term_is_of_type(Term,(Type1 ; Type2),PrintErrMsg) :-
323		(term_is_of_type(Term,Type1,no) -> true
324		; term_is_of_type(Term,Type2,PrintErrMsg)),
325		!.
326		term_is_of_type(Term,Type,PrintErrMsg) :-
327		print_type_error(Term,Type,PrintErrMsg,term_is_of_type_catchall).
328
329
330		l_term_is_of_type([],[],_PrintErrMsg).
331		l_term_is_of_type([Term1|Rest],[Type1|TypeList],PrintErrMsg) :-
332		term_is_of_type(Term1,Type1,PrintErrMsg),!,
333		l_term_is_of_type(Rest,TypeList,PrintErrMsg).
334
335		print_type_error(T,Type,_,PP) :-
336		(legal_type_description(Type) -> true
337		; print_error(pp(PP)),print_error(illegal_type(Type)),print_error(term(T))),
338		fail.
339		print_type_error(Term,Type,PrintErrMsg,PP) :- PrintErrMsg\=no, nl,
340		%print(err(Term,Type)),nl,nl,
341		print_error('### Type Error Occured! Type:'),print_error(Type),
342		print_error('### Term:'),safe_print_term(Term),nl,
343		print_error('### ProgramPoint:'),safe_print_term(PP),nl,
344		assert_type_error.
345
346
347		print_inf_error(Term,Type,PrintErrMsg) :- PrintErrMsg \= no, nl,
348		print_error('### Cyclic Term Error: Requested Type '),print_error(Type),
349		print_error('### Term: '),safe_print_term(Term),nl,
350		assert_type_error.
351
352		safe_print_term(X) :- var(X),!,print(X).
353		safe_print_term(X) :- is_inf(X),!,
354		X =.. [Func|Args],
355		print(Func),print('('),
356		l_safe_print(Args),
357		print(')').
358		safe_print_term(X) :- print(X).
359
360		l_safe_print([]).
361		l_safe_print([Term|T]) :-
362		(is_inf(Term)
363		-> (print('!CYCLIC!('),write_term(Term,[max_depth(3)]),print(')'))
364		; (print(Term))
365		),
366		((T=[]) -> true ; print(',') ),
367		l_safe_print(T).
368
369		:- dynamic type_error/1.
370		type_error(no).
371
372		assert_type_error :-
373		retract(type_error(_N)),fail.
374		assert_type_error :-
375		assert(type_error(yes)).
376
377
378		reset_type_error :-
379		retract(type_error(_N)),fail.
380		reset_type_error :-
381		assert(type_error(no)).
382
383		type_error_occurred :-
384		type_error(yes).
385
386
387
388		:- use_module(library(terms)).
389		is_inf(X) :- cyclic_term(X).
390
391		check_cyclic(X) :- cyclic_term(X),!,
392		print('### Cyclic Term : '), nl,
393		safe_print_term(X),nl,
394		fail.
395		check_cyclic(_).