1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2% Hindley-Milner Type Checker for Prolog
3%
4% All authors agree to the licences of SWI-Prolog and YAP
5%
6% AUTHORS OF CODE:
7%	Tom Schrijvers
8%       Bart Demoen
9%	Markus Triska
12%
13% ACKNOWLEDGEMENTS:
14%	Ulrich Neumerkel for providing feedback
15%	Vitor Santos Costa
16%	Jose Santos
18%
19%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
20%
21% DOCUMENTATION
22%
23% Type Definitions
24% ----------------
25%
26% Define polymorphic algebraic data types like:
27%
28%	:- type pair(A,B)    	---> A - B.
29%	:- type list(T) 	---> [] ; [T|list(T)].
30%	:- type boolean    	---> true ;  false.
31%
32% (NOTE: the above types are predefined, as well as integer and float.)
33%
34% Type definitions can also be empty, e.g.
35%
36%	:- type an_empty_type.
37%
38% This means that the type is not inhabited by instantiated values. Only
39% logical variables are possible.
40%
41% Predicate Signatures
42% --------------------
43%
44% Predicates are given a signature like:
45%
46%	:- pred append(list(E), list(E), list(E)).
47%	:- pred not(boolean, boolean).
48%	:- pred lookup(list(pair(Key,Value)), Key, Value).
49%
50% Optionally, modes can be specified as well, by prefixing
51% the argument types with +, - or ?. For instance:
52%
53%	:- pred not(+boolean, -boolean).
54%
55% Note that the type checker fully ignores mode declarations. Hence,
56% mode declarations have not other purpose than to serve as documentation.
57% In particular, the validity of mode declarations is not verified.
58%
59% Interfacing Untyped Code
60% ------------------------
61%
62% 1) Calling typed code from untyped code (and the Prolog top-level)
63%    results in runtime type checks.
64%
65% 2) One may annotate calls to untyped predicates from within typed predicates:
66%
67%       :- pred concat(list(list(integer)),list(integer)).
68%
69%	concat(LL,L) :- flatten(LL,L) :: flatten(list(list(integer)),list(integer)).
70%
71%    which results in runtime type checking. The annotation is also used for static
72%    type checking of the code surrounding the annotated call.
73%
74%    A variant of the annotation is only used for static type checking, and does
75%    not result in runtime checks:
76%
77%	concat(LL,L) :- flatten(LL,L) :< flatten(list(list(integer)),list(integer)).
78%
79% 3) A second way is to provide a signature for untypable code with:
80%
81%	:- trust_pred sort(list(integer),list(integer)).
82%
83%    This signature is only into account when checking calls from
84%    typed code.
85%
86% Coping with Untypable Code
87% --------------------------
88%
89% Untypable code, e.g. using Prolog built-ins, may be encapsulated
90% in a trusted predicate. E.g.
91%
92%	:- trust_pred new_array(list(T),array(T)).
93%
94%	new_array(List,Array) :- Array =.. [array|List].
95%
96% No additional runtime checks are performed for trusted predicates.
97%
98% Similarly, untyped imported predicates may be given a type signature
99% with the trust_pred declaration.
100%
101%
102% Type Checker Options
103% --------------------
104%
105% Options can be passed to the type checker with the declaration
106%
107%	:- type_check_options(Options).
108%
109% where Options is a list containing zero or more of the following elements:
110%
111%	check(Flag) where Flag is on or off,
112%		to enable or disable the type checker
113%		enabled by default
114%
115%	runtime(Flag) where Flag is on or off,
116%		to enable or disable runtime type checking
117%		disabled by default
118%
119%	verbose(Flag) where Flag is on or off,
120%		to enable or disable printed summary at end of type checking
121%		enabled by default
122%
123%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
124%
125% CURRENT LIMITATIONS
126%
127%	* global namespace for types
128%	* runtime type checks are not exhaustive for (non-ground) polymorphic types
129%
130% TODO:
131%	* check uniqueness of defined types, e.g. list(T) not defined twice
132%	* check syntactic well-formedness of type definitions and declarations
133%	* add module awareness for predicates
134%	* add module awareness for types
135%	* take care with variables used in :: (also used for values / other annotations)
136%	* improve error messages with tc_stats(Errors,Total)
137%		- source location information
138%	  	- what the inconsistency is
139%	* support for more built-ins
140%	* higher-order types for meta-predicates
141%	* exported vs. hidden types
142%	* abstract types (hidden definition)
143%	* automatic inference of signatures
144%	* type classes
145%
146% CHANGES:
149%	* added statistics printing at end of type checking
150%	* fixed detection of less general types than signature
151%	* added error message for less polymorphic signature
152%	* added error message for duplicate predicate signature
153%	* added :< annotation, which is a variant of  the :: annotation,
154%	        where the semantics is not to include runtime assertions,
155%               but to simply trust the programmer.
156%	* added type pred/0 for goals
158%	* added type pred/1 and pred/2
159%	* addded call/1 and call/2 built-ins
160%	* improved error message for less polymorphic inferred types
161%	* support for built-in type `float'
169%	* added coercion predicate any_to_type/3
170%	* added coercion predicate type_to_any/2
171%	* normalize all types, also built-in ones
172%	* option to enable/disable type-checking
173%	* option to enable/disable runtime type checks
174%	* added empty type definitions
175%	* detect ambiguous use of numeric types
176%
177%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
178
179:- module(type_check,
180	  [ op(1150, fx, type)
181	  , op(1130, xfx, --->)
182	  , op(1150, fx, pred)
183	  , op(1150, fx, trust_pred)
184	  , op(500,yfx,::)
185	  , op(500,yfx,:<)
186	  , op(200, fy,?)
187	  ]).  188
189:- use_module(library(lists)).  190:- use_module(library(terms), [variant/2]).  191:- use_module(functor_constraint).  192:- use_module(library(apply_macros)).  193
194:- style_check(-singleton).  195
196:- op(1150, fx, type).  197:- op(1130, xfx, ---> ).  198:- op(1150, fx, pred).  199:- op(500,yfx,::).  200:- op(500,yfx,:<).  201
202:- multifile
203	user:term_expansion/2,
204	user:goal_expansion/2,
205	prolog:message/3,
206	constructor/4,
207	constructor_info/4,
208	signature/4,
209	trusted_predicate/1,
210	basic_normalize/2.  211
212:- dynamic
213	user:term_expansion/2,
214	user:goal_expansion/2,
215	signature/4,
216	constructor_info/4,
217	trusted_predicate/1,
218	basic_normalize/2.  219
220tc_version('\$Id: type_check.pl,v 1.52 2010-06-16 03:51:31 toms Exp \$').
221
222%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
223%% Type checker options {{{
224
225:- nb_setval(type_check_runtime,off).  226:- nb_setval(type_check,on).  227:- nb_setval(type_check_verbose,on).  228
229handle_options(List) :- maplist(handle_option,List).
230
231handle_option(verbose(Flag)) :- !, nb_setval(type_check_verbose,Flag).
232handle_option(runtime(Flag)) :- !, nb_setval(type_check_runtime,Flag).
233handle_option(check(Flag))   :- !, nb_setval(type_check,Flag).
234handle_option(Other)	     :- format('Unsupported type checker option `~w\'.\n',[Other]).
235
236
237type_checking_runtime :- nb_getval(type_check_runtime,on).
238type_checking_verbose :- nb_getval(type_check_verbose,on).
239type_checking         :- nb_getval(type_check,on).
240
241% }}}
242%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
243
244
245
246
247type_check_term(Term,ExpectedType,EnvIn,EnvOut) :-
248	normalize_type(ExpectedType,NormalExpectedType),
249	type_check_term_(Term,NormalExpectedType,EnvIn,EnvOut).
250
251type_check_term_(Term,ExpectedType,EnvIn,EnvOut) :-
252	var(Term), !,
253	( lookup_eq(EnvIn,Term,EnvType) ->
254		( equate_types(ExpectedType,EnvType) ->
255			true
256		;
257			term_type_error(Term,ExpectedType,EnvType)
258		),
259		EnvIn = EnvOut
260	;
261		EnvOut = [Term-ExpectedType|EnvIn]
262	).
263type_check_term_(Term,Type,EnvIn,EnvOut) :-
264	integer(Term), !,
265	numeric_type(Type),
266	EnvIn = EnvOut.
267	% ( equate_types(Type,integer) ->
268	%	EnvIn = EnvOut
269	% ;
270	%	term_type_error(Term,integer,Type)
271	% ).
272type_check_term_(Term,Type,EnvIn,EnvOut) :-
273	float(Term), !,
274	( equate_types(Type,float) ->
275		EnvIn = EnvOut
276	;
277		term_type_error(Term,float,Type)
278	).
279
280type_check_term_(Term,Type,EnvIn,EnvOut) :-
281	nonvar(Type),
282	functor(Type,pred,Arity),
283	!,
284	Type =.. [_|ArgTypes],
285	Term =.. [Functor|Args],
286	length(DummyArgs,Arity),
287	append(Args,DummyArgs,FullArgs),
288	Goal =.. [Functor|FullArgs],
289	pairup(DummyArgs,ArgTypes,ExtraEnv),
290	append(ExtraEnv,EnvIn,Env),
291	type_check_control(Goal,top,Env,EnvOut).
292
293type_check_term_(Term,Type,EnvIn,EnvOut) :-
294	Type == string, !,
295	( atom(Term) -> EnvIn = EnvOut
296	; term_type_error(Term,unknown_type,Type)
297	).
298
299type_check_term_(_Term,Type,EnvIn,EnvOut) :-
300	Type == any, !,
301	EnvIn = EnvOut.
302
303type_check_term_(Term,Type,EnvIn,EnvOut) :-
304	% constructor(Term,Type,EnvIn,EnvOut), !.
305	functor_constraint(Term,Type,Args,Types), !,
306	type_check_terms(Args,Types,EnvIn,EnvOut).
307
308type_check_term_(Term,Type,_EnvIn,_EnvOut) :-
309	term_type_error(Term,unknown_type,Type).
310
311type_check_terms([],[],Env,Env).
312type_check_terms([Term|Terms],[Type|Types],Env1,Env3) :-
313	type_check_term(Term,Type,Env1,Env2),
314	type_check_terms(Terms,Types,Env2,Env3).
315
316term_type_error(Term,ExpectedType,EnvType) :-
317	throw(error(type_error(Term,ExpectedType,EnvType))).
318
319%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
320
321constructor_clauses((A;B),Type) --> !,
322	constructor_clauses(A,Type),
323	constructor_clauses(B,Type).
324constructor_clauses(Constructor,Type) -->
325	{ functor(Constructor, Name, Arity),
326	  functor(Term, Name, Arity),
327	  Term        =.. [_|Args],
328	  Constructor =.. [_|Types],
329	  args_body(Args,Types,Body,EnvIn,EnvOut)
330	},
331	[ ( type_check:constructor(Term, ExpectedType, EnvIn, EnvOut) :-
332		( type_check:equate_types(ExpectedType,Type) ->
333			true
334		;
335			type_check:term_type_error(Term,ExpectedType,Type)
336		),
337		Body
338	  )
339	],
340	constructor_info_clause(Constructor,Type).
341
342constructor_info_clause(Constructor,Type) -->
343	{ functor(Constructor, Name, Arity),
344	  functor(Term, Name, Arity),
345	  Term        =.. [_|Args],
346	  Constructor =.. [_|Types],
347	  Clause = type_check:constructor_info(Term, Type, Args, Types)
348	},
349	[ Clause
350	].
351
352args_body([],[],true,Env,Env).
353args_body([Term|Terms],[Type|Types],(type_check:type_check_term(Term,Type,EnvIn,Env),Body),EnvIn,EnvOut) :-
354	args_body(Terms,Types,Body,Env,EnvOut).
355
356signature_clause(Signature, Clause) :-
357	( check_signature(Signature) ->
358		signature_clause_(Signature, Clause)
359	;
360		true
361	).
362
363
364signature_clause_(Signature,Clause) :-
365	functor(Signature,Name,Arity),
366	functor(Call,Name,Arity),
367	Call      =.. [_|Args],
368	Signature =.. [_|Types],
369	args_body(Args,Types,Body,EnvIn,EnvOut),
370	Clause =
371	( type_check:signature(Call,Types,EnvIn,EnvOut) :-
372		Body
373	).
374
375check_signature(Signature) :-
376	nonvar(Signature),
377	functor(Signature,Name,Arity),
378	functor(Prototype,Name,Arity),
379	( signature(Prototype,_,[],_) ->
380		duplicate_signature_error(Signature),
381		fail
382	;
383		true
384	).
385
386%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
387type_check_file(NClauses) :-
388	findall(Clause,retract(clause_to_check(Clause)),Clauses),
389	( type_checking ->
390		type_check_clauses(Clauses,Stats),
391		( type_checking_runtime ->
392			transform_clauses(Clauses,NClauses)
393		;
394			NClauses = Clauses
395		),
396		final_message(Stats)
397	;
398		NClauses = Clauses
399	).
400
401type_check_clauses(Clauses,Stats) :-
402	init_stats(Stats0),
403	type_check_clauses(Clauses,Stats0,Stats).
404
405type_check_clauses([],Stats,Stats).
406type_check_clauses([Clause|Clauses],Stats0,Stats) :-
407	catch(
408		( type_check_clause(Clause) ,
409		  inc_ok_stats(Stats0,Stats1)
410		)
411	     ,  error(type_error(_Term,_ExpType,_InfType))
412	     ,  ( %format('TYPE ERROR in clause: \n\n',[]),
413	  	  %portray_clause(Clause),
414		  inc_error_stats(Stats0,Stats1)
415		)
416	     ),
417	type_check_clauses(Clauses,Stats1,Stats).
418
419type_check_clause((:- _)) :- !,
420	true. % ignoring
423	( trusted_predicate(P/N) ->
424		true
425	;
427	).
430
432	Env0 = [],
433        /* check the head */
434        catch(
436		error(type_error(Term,Exp,Inf)),
438	),
439	/* check the body */
440	catch(
441	  	 type_check_control(Body,top,Env1,_Env2),
442		error(type_error(Term,Exp,Inf),Context),
444	),
446	InfSig =.. [Name|ArgTypes],
447	/* check for ambiguous types */
448	check_ambiguous_types(InfSig),
449	/* check whether Head is variant of signature */
450	functor(Prototype,Name,Arity),
451	signature(Prototype,ProtoTypes,Env0,_ProtoEnv),
452	( variant(ArgTypes, ProtoTypes) % JCAS: equivalent to  ArgTypes =@= ProtoTypes but does not require SWI.pl
453	 ->
454	  true
455	;
456	  DecSig =.. [Name|ProtoTypes],
457	  less_polymorphic_error((:- pred InfSig),
458	  			 (:- pred DecSig)),
459	  throw(type_error)
460	).
461
462filter([],_Pred,[]).
463filter([X|Xs],Pred,Result) :-
464	( call(Pred,X) ->
465		Result = [X|More],
466		filter(Xs,Pred,More)
467	;
468		filter(Xs,Pred,Result)
469	).
470
473	filter(TyVars,is_ambiguous_numeric_type,AmbTyVars),
474	( AmbTyVars == [] ->
475		true
476	;
479		write( '%------------------------------------------------------------------------------%'), nl,
480		format('TYPE ERROR: Ambiguous numeric types `~p\'.\n',[AmbTyVars1]),
482		format('            types should be one of `integer\' or `float\' \n',[]),
483		throw(type_error)
484	).
485
486
487% context ::=
488%	  top
489%	| lconj parent right
490%	| rconj parent left
491%	| ldisj parent right
492%	| rdisj parent left
493%	| cond  parent then
494%	| then  parent cond
495%	| once  parent
496%	| findall parent pattern result
497
498% env == list(pair(var-type))
499type_check_control(G,_Context,Env1,Env2) :- var(G), !,
500	type_check_term(G,(pred),Env1,Env2).
501
502type_check_control((G1,G2),Context,Env1,Env3) :- !,
503	type_check_control(G1,lconj(Context,G2),Env1,Env2),
504	type_check_control(G2,rconj(Context,G1),Env2,Env3).
505
506type_check_control((G1;G2),Context,Env1,Env3) :- !,
507	type_check_control(G1,ldisj(Context,G2),Env1,Env2),
508	type_check_control(G2,rdisj(Context,G1),Env2,Env3).
509
510type_check_control((G1 -> G2),Context,Env1,Env3) :- !,
511	type_check_control(G1,cond(Context,G2),Env1,Env2),
512	type_check_control(G2,then(Context,G1),Env2,Env3).
513
514type_check_control(once(G),Context,Env1,Env2) :- !,
515	type_check_control(G,once(Context),Env1,Env2).
516
517type_check_control(findall(Pattern,Goal,Result),Context,Env1,Env4) :- !,
518	type_check_control(Goal,findall(Context,Pattern,Result),Env1,Env2),
519	type_check_term(Pattern,Type,Env2,Env3),
520	type_check_term(Result,list(Type),Env3,Env4).
521
522type_check_control(Goal,Context,Env1,Env2) :-
523	catch(
524		( type_check_goal(Goal,Env1,Env2,Warnings,[]) ->
525			maplist(control_warning(context(Goal,Context)),Warnings)
526		;
527			term_type_error(?,?,?)
528		),
529		error(type_error(Term,ExpType,InfType)),
530		control_type_error(type_error(Term,ExpType,InfType),Goal,Context)
531	).
532
533control_type_error(Error,Goal,Context) :-
534	throw(error(Error,context(Goal,Context))).
535% }}}
536
537numeric_type(Type) :-
538	( nonvar(Type) ->
539		check_numeric_type(Type)
540	;
541		put_attr(Type,numeric_type,x)
542	).
543
544numeric_type:attr_unify_hook(_,Other) :-
545	( nonvar(Other) ->
546		check_numeric_type(Other)
547	;
548		put_attr(Other,numeric_type,_)
549	).
550
551check_numeric_type(integer) :- !.
552check_numeric_type(float) :- !.
553check_numeric_type(Other) :-
554	term_type_error(some_arithmetic_expression,a_numeric_type,Other).
555
556is_ambiguous_numeric_type(Type) :- var(Type), get_attr(Type,numeric_type,_).
557
558% type_check_goal(+goal,+env,-env,-warnings,+warnings_tail) {{{
559type_check_goal((X = Y),Env1,Env3,W,W) :- !,
560	type_check_term(X,Type,Env1,Env2),
561	type_check_term(Y,Type,Env2,Env3).
562type_check_goal((X \= Y),Env1,Env3,W,W) :- !,
563	type_check_term(X,Type,Env1,Env2),
564	type_check_term(Y,Type,Env2,Env3).
565type_check_goal((X == Y),Env1,Env3,W,W) :- !,
566	type_check_term(X,Type,Env1,Env2),
567	type_check_term(Y,Type,Env2,Env3).
568type_check_goal((X \== Y),Env1,Env3,W,W) :- !,
569	type_check_term(X,Type,Env1,Env2),
570	type_check_term(Y,Type,Env2,Env3).
571type_check_goal((X @< Y),Env1,Env3,W,W) :- !,
572	type_check_term(X,Type,Env1,Env2),
573	type_check_term(Y,Type,Env2,Env3).
574type_check_goal((X @> Y),Env1,Env3,W,W) :- !,
575	type_check_term(X,Type,Env1,Env2),
576	type_check_term(Y,Type,Env2,Env3).
577type_check_goal((X @>= Y),Env1,Env3,W,W) :- !,
578	type_check_term(X,Type,Env1,Env2),
579	type_check_term(Y,Type,Env2,Env3).
580type_check_goal((X @=< Y),Env1,Env3,W,W) :- !,
581	type_check_term(X,Type,Env1,Env2),
582	type_check_term(Y,Type,Env2,Env3).
583type_check_goal(copy_term(X,Y),Env1,Env3,W,W) :- !,
584	type_check_term(X,Type,Env1,Env2),
585	type_check_term(Y,Type,Env2,Env3).
586type_check_goal((X is Y),Env1,Env3,W,W) :- !,
587	numeric_type(Type),
588	type_check_term(X,Type,Env1,Env2),
589	type_check_expression(Y,Type,Env2,Env3).
590type_check_goal((X > Y),Env1,Env3,W,W) :- !,
591	numeric_type(Type),
592	type_check_expression(X,Type,Env1,Env2),
593	type_check_expression(Y,Type,Env2,Env3).
594type_check_goal((X < Y),Env1,Env3,W,W) :- !,
595	numeric_type(Type),
596	type_check_expression(X,Type,Env1,Env2),
597	type_check_expression(Y,Type,Env2,Env3).
598type_check_goal((X =< Y),Env1,Env3,W,W) :- !,
599	numeric_type(Type),
600	type_check_expression(X,Type,Env1,Env2),
601	type_check_expression(Y,Type,Env2,Env3).
602type_check_goal((X >= Y),Env1,Env3,W,W) :- !,
603	numeric_type(Type),
604	type_check_expression(X,Type,Env1,Env2),
605	type_check_expression(Y,Type,Env2,Env3).
606type_check_goal((X =:= Y),Env1,Env3,W,W) :- !,
607	numeric_type(Type),
608	type_check_expression(X,Type,Env1,Env2),
609	type_check_expression(Y,Type,Env2,Env3).
610type_check_goal((X =\= Y),Env1,Env3,W,W) :- !,
611	numeric_type(Type),
612	type_check_expression(X,Type,Env1,Env2),
613	type_check_expression(Y,Type,Env2,Env3).
614
615type_check_goal(arg(I,_,_),Env1,Env2,W,W) :- !,
616	type_check_term(I,integer,Env1,Env2).
617type_check_goal(functor(Term,Functor,I),Env1,Env3,W,W) :- !,
618	type_check_term(I,integer,Env1,Env2),
619	( nonvar(I) -> I >= 0 ; true ),
620	type_check_term(Term,Type,Env2,Env3),
621	( nonvar(Functor) ->
622		atomic(Functor),
623		( nonvar(I), nonvar(Type) ->
624			functor(Dummy,Functor,I),
625			constructor(Dummy,Type,[],_Env)
626		;
627			true
628		)
629	;
630		true % ignore functor
631	).
632type_check_goal(integer(I),Env1,Env2,W,W) :- !,
633	type_check_term(I,integer,Env1,Env2).
634type_check_goal(float(I),Env1,Env2,W,W) :- !,
635	type_check_term(I,float,Env1,Env2).
636
637type_check_goal(true,Env1,Env2,W,W) :- !, Env1 = Env2.
638type_check_goal(fail,Env1,Env2,W,W) :- !, Env1 = Env2.
639type_check_goal(!,Env1,Env2,W,W) :- !, Env1 = Env2.
640type_check_goal(abort,Env1,Env2,W,W) :- !, Env1 = Env2.
641
642type_check_goal(writeln(Term),Env1,Env2,W,W) :- !, type_check_term(Term,_Type,Env1,Env2).
643type_check_goal(format(_,_),Env1,Env2,W,W) :- !, Env1 = Env2.
644
645type_check_goal(var(Term),Env1,Env2,W,W) :- !, type_check_term(Term,_Type,Env1,Env2).
646type_check_goal(nonvar(Term),Env1,Env2,W,W) :- !, type_check_term(Term,_Type,Env1,Env2).
647type_check_goal(ground(Term),Env1,Env2,W,W) :- !, type_check_term(Term,_Type,Env1,Env2).
648
649type_check_goal(atom_chars(A1,A2),Env1,Env3,W,W) :- !,
650	type_check_term(A1,string,Env1,Env2),
651	type_check_term(A2,list(string),Env2,Env3).
652type_check_goal(atom_concat(A1,A2,A3),Env1,Env4,W,W) :- !,
653	type_check_term(A1,string,Env1,Env2),
654	type_check_term(A2,string,Env2,Env3),
655	type_check_term(A3,string,Env3,Env4).
656type_check_goal(atom_length(A1,A2),Env1,Env3,W,W) :- !,
657	type_check_term(A1,string,Env1,Env2),
658	type_check_term(A2,integer,Env2,Env3).
659type_check_goal(concat_atom(A1,A2),Env1,Env3,W,W) :- !,
660	type_check_term(A1,list(string),Env1,Env2),
661	type_check_term(A2,string,Env2,Env3).
662type_check_goal(get_char(A1),Env1,Env2,W,W) :- !,
663	type_check_term(A1,string,Env1,Env2).
664
665type_check_goal(throw(_),Env1,Env2,W,W) :- !, Env1 = Env2.
666type_check_goal(catch(Goal,_,Handler),Env1,Env3,W1,W3) :- !,
667	type_check_goal(Goal,Env1,Env2,W1,W2),
668	type_check_goal(Handler,Env2,Env3,W2,W3).
669
670
671type_check_goal(call(Goal),Env1,Env2,W,W) :- !,
672	type_check_term(Goal,(pred),Env1,Env2).
673
674type_check_goal(call(Goal,Arg),Env1,Env3,W,W) :- !,
675	type_check_term(Goal,pred(Type),Env1,Env2),
676	type_check_term(Arg, Type,      Env2,Env3).
677
678type_check_goal(call(Goal,Arg1,Arg2),Env1,Env4,W,W) :- !,
679	type_check_term(Goal,pred(Type1,Type2),Env1,Env2),
680	type_check_term(Arg1,Type1,            Env2,Env3),
681	type_check_term(Arg2,Type2,            Env3,Env4).
682
683type_check_goal(Goal :: Signature, Env1, Env3,W,W) :- !,
684	/* first take into account the predicate signatures
685	   if one exists 				    */
686	( participating_predicate(Goal) ->
687		signature(Goal,_,Env1,Env2)
688	;
689		Env2 = Env1
690	),
691	functor(Goal,F,A),
692	functor(Signature,F,A),
693	Goal      =.. [_|Args],
694	Signature =.. [_|Types],
695	type_check_terms(Args,Types,Env2,Env3).
696type_check_goal(Goal :< Signature, Env1, Env3,W,W) :- !,
697	/* first take into account the predicate signatures
698	   if one exists 				    */
699	( participating_predicate(Goal) ->
700		signature(Goal,_,Env1,Env2)
701	;
702		Env2 = Env1
703	),
704	functor(Goal,F,A),
705	functor(Signature,F,A),
706	Goal      =.. [_|Args],
707	Signature =.. [_|Types],
708	type_check_terms(Args,Types,Env2,Env3).
709
710type_check_goal(type_to_any(A1,A2),Env1,Env3,W,W) :- !,
711	type_check_term(A1,_Type,Env1,Env2),
712	type_check_term(A2,any,Env2,Env3).
713
714type_check_goal(any_to_type(A1,A2,Type),Env1,Env3,W,W) :- !,
715	type_check_term(A1,any,Env1,Env2),
716	type_check_term(A2,Type,Env2,Env3).
717
718type_check_goal(Goal,Env1,Env2,W,W) :-
719	participating_predicate(Goal), !,
720	signature(Goal,_,Env1,Env2).
721
722type_check_goal(Goal,Env1,Env2,W,RW) :-
723	/* all other predicates are simply ignored */
724	Warning = unknown_predicate_call(Goal),
725 	W = [Warning|RW],
726	Env1 = Env2.
727% }}}
728
729% type_check_expression(+expression,+type,+env,-env) {{{
730type_check_expression(Exp,Type,Env1,Env2) :-
731	var(Exp), !,
732	type_check_term(Exp,Type,Env1,Env2).
733type_check_expression(random,Type,Env1,Env1) :- !,  % NOTE: only supported by Yap
734	equate_types(Type,float).
735type_check_expression((-Exp),Type,Env1,Env2) :- !,
736	type_check_expression(Exp,Type,Env1,Env2).
737type_check_expression((\Exp),Type,Env1,Env2) :- !,
738	equate_types(Type,integer),
739	type_check_expression(Exp,Type,Env1,Env2).
740type_check_expression(abs(Exp),Type,Env1,Env2) :- !,
741	type_check_expression(Exp,Type,Env1,Env2).
742type_check_expression(log(Exp),Type,Env1,Env2) :- !,
743	equate_types(Type,float),
744	type_check_expression(Exp,Type,Env1,Env2).
745type_check_expression(float(Exp),Type,Env1,Env2) :- !,
746	equate_types(Type,float), % explicit conversion from integer to float
747	type_check_expression(Exp,integer,Env1,Env2).
748type_check_expression(integer(Exp),Type,Env1,Env2) :- !,
749	equate_types(Type,integer), % explicit conversion from float to integer
750	type_check_expression(Exp,float,Env1,Env2).
751type_check_expression(sign(Exp),Type,Env1,Env2) :- !,
752	type_check_expression(Exp,Type,Env1,Env2).
753type_check_expression((Exp1+Exp2),Type,Env1,Env3) :- !,
754	type_check_expression(Exp1,Type,Env1,Env2),
755	type_check_expression(Exp2,Type,Env2,Env3).
756type_check_expression((Exp1-Exp2),Type,Env1,Env3) :- !,
757	type_check_expression(Exp1,Type,Env1,Env2),
758	type_check_expression(Exp2,Type,Env2,Env3).
759type_check_expression((Exp1*Exp2),Type,Env1,Env3) :- !,
760	type_check_expression(Exp1,Type,Env1,Env2),
761	type_check_expression(Exp2,Type,Env2,Env3).
762type_check_expression((Exp1/Exp2),Type,Env1,Env3) :- !,
763	equate_types(Type,float),
764	type_check_expression(Exp1,Type,Env1,Env2),
765	type_check_expression(Exp2,Type,Env2,Env3).
766type_check_expression((Exp1//Exp2),Type,Env1,Env3) :- !,
767	equate_types(Type,integer),
768	type_check_expression(Exp1,Type,Env1,Env2),
769	type_check_expression(Exp2,Type,Env2,Env3).
770type_check_expression((Exp1**Exp2),Type,Env1,Env3) :- !,
771	equate_types(Type,float),
772	type_check_expression(Exp1,Type,Env1,Env2),
773	type_check_expression(Exp2,Type,Env2,Env3).
774type_check_expression((Exp1 mod Exp2),Type,Env1,Env3) :- !,
775	equate_types(Type,integer),
776	type_check_expression(Exp1,Type,Env1,Env2),
777	type_check_expression(Exp2,Type,Env2,Env3).
778type_check_expression(min(Exp1,Exp2),Type,Env1,Env3) :- !,
779	type_check_expression(Exp1,Type,Env1,Env2),
780	type_check_expression(Exp2,Type,Env2,Env3).
781type_check_expression(max(Exp1,Exp2),Type,Env1,Env3) :- !,
782	type_check_expression(Exp1,Type,Env1,Env2),
783	type_check_expression(Exp2,Type,Env2,Env3).
784type_check_expression((Exp1 >> Exp2),Type,Env1,Env3) :- !,
785	equate_types(Type,integer),
786	type_check_expression(Exp1,Type,Env1,Env2),
787	type_check_expression(Exp2,Type,Env2,Env3).
788type_check_expression((Exp1 << Exp2),Type,Env1,Env3) :- !,
789	equate_types(Type,integer),
790	type_check_expression(Exp1,Type,Env1,Env2),
791	type_check_expression(Exp2,Type,Env2,Env3).
792type_check_expression((Exp1 /\ Exp2),Type,Env1,Env3) :- !,
793	equate_types(Type,integer),
794	type_check_expression(Exp1,Type,Env1,Env2),
795	type_check_expression(Exp2,Type,Env2,Env3).
796type_check_expression((Exp1 \/ Exp2),Type,Env1,Env3) :- !,
797	equate_types(Type,integer),
798	type_check_expression(Exp1,Type,Env1,Env2),
799	type_check_expression(Exp2,Type,Env2,Env3).
800type_check_expression(Exp,Type,Env1,Env2) :-
801	/* catch all */
802	type_check_term(Exp,Type,Env1,Env2).
803% }}}
804
805unify_args([],[],Env,Env).
806unify_args([X|Xs],[Y|Ys],Env1,Env3) :-
807	type_check_goal((X = Y), Env1, Env2,_,[]),
808	unify_args(Xs,Ys,Env2,Env3).
809
810%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
811% ERROR MESSAGES
812
814	write( '%------------------------------------------------------------------------------%'), nl,
815	format('TYPE ERROR: expected type `~w\' for term `~w\'\n',[ExpType,Term]),
816	format('           inferred type `~w\'\n',[InfType]),
819        term_type_error(Term,ExpType,InfType).
820
821less_polymorphic_error(InfSig,DecSig) :-
822	copy_term_nat(InfSig,InfSig1),
823	copy_term_nat(DecSig,DecSig1),
824	numbervars(InfSig1,0,_),
825	numbervars(DecSig1,0,_),
826	write( '%------------------------------------------------------------------------------%'), nl,
827	format('TYPE ERROR: Inferred signature is less polymorphic than declared signature.\n',[]),
828	format('            inferred signature `~p\'\n',[InfSig1]),
829	format('            declared signature `~p\'\n',[DecSig1]).
830
831duplicate_signature_error(Signature) :-
832	write( '%------------------------------------------------------------------------------%'), nl,
833	format('TYPE ERROR: Predicate already has a signature.\n',[]),
834	format('            duplicate signature `~w\'\n',[Signature]),
835	format('            Ignoring duplicate signature.\n',[]).
836
839	format('TYPE ERROR: expected type `~w\' for term `~w\'\n',[ExpType,Term]),
840	format('            inferred type `~w\'\n',[InfType]),
841	format('\tin goal:\n\t\t ~w\n\tin clause:\n',[Source]),
842	assemble_marked_body(Context,'HERE'(Source),MarkedBody),
844        term_type_error(Term,ExpType,InfType).
845
846control_warning(Context,Warning) :-
847	control_warning_(Warning,Context).
848
849control_warning_(unknown_predicate_call(Call),context(Source,Context)) :-
850	format('% TYPE WARNING: call to unknown predicate `~w\'\n',[Call]),
851	format('%     Possible Fixes: - add type annotation `::\' to call\n',[]),
852	format('%                     - replace with call to other predicate\n',[]),
853	assemble_marked_body(Context,'HERE'(Source),MarkedBody),
854	portray_clause(('...' :- MarkedBody)).
855
856prolog:message(error(type_error(Term,ExpectedType,InferredType))) -->
857	[ '\n\tTYPE ERROR: expected type `~w\' for term `~w\'\n' - [ExpectedType, Term],
858	  '\t            inferred type `~w\'\n' - [InferredType]
859	].
860% }}}
861
862% assemble_marked_body(+context,+goal,-goal) {{{
863assemble_marked_body(top,Acc,Body) :- Body = Acc.
864assemble_marked_body(lconj(Context,Right),Acc,Body) :-
865	assemble_marked_body(Context,(Acc,Right),Body).
866assemble_marked_body(rconj(Context,Left),Acc,Body) :-
867	assemble_marked_body(Context,(Left,Acc),Body).
868assemble_marked_body(ldisj(Context,Right),Acc,Body) :-
869	assemble_marked_body(Context,(Acc;Right),Body).
870assemble_marked_body(rdisj(Context,Left),Acc,Body) :-
871	assemble_marked_body(Context,(Left;Acc),Body).
872assemble_marked_body(cond(Context,Then),Acc,Body) :-
873	assemble_marked_body(Context,(Acc->Then),Body).
874assemble_marked_body(then(Context,Cond),Acc,Body) :-
875	assemble_marked_body(Context,(Cond->Acc),Body).
876assemble_marked_body(once(Context),Acc,Body) :-
877	assemble_marked_body(Context,once(Acc),Body).
878assemble_marked_body(findall(Context,Pattern,Result),Acc,Body) :-
879	assemble_marked_body(Context,findall(Pattern,Acc,Result),Body).
880% }}}
881%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
882% Transform clauses: 	{{{
883%
884% 	p(T1,...,Tn) :- B.
885%
886% becomes:
887%
888%	p(X1,...,Xn) :- CHECKS, p'(X1,...,Xn).	(* one for each predicate *)
889%
890%	p'(T1,...,Tn) :- B'.
891%
892% where all calls to type safe predicates have been replaced in B to get B'
893
894transform_clauses(Clauses,NClauses) :-
895	wrappers(Clauses,NClauses).
896
897wrappers(Clauses,NClauses) :-
898	findall(FA,(member(Clause,Clauses), only_check_participating_clauses(Clause,FA)),FAs0),
899	sort(FAs0,FAs),
900	maplist(wrapper_clause,FAs,WrapperClauses),
901	maplist(tc_clause,Clauses,TcClauses),
902	append(WrapperClauses,TcClauses,NClauses).
903
904% PORTRAY_CLAUSE bug?
905%
907% p(_, _) :-
908%         signature(p(_, _)).
909
910wrapper_clause(F/A,Clause) :-
914
917	tc_body(Body,TcBody).
920
923	atom_concat('\$tc_',F,NF),
925
926tc_body(Var,TcBody) :- var(Var), !, TcBody = Var.
927tc_body((G1,G2),TcBody) :- !,
928	TcBody = (TcG1,TcG2),
929	tc_body(G1,TcG1),
930	tc_body(G2,TcG2).
931tc_body((G1;G2),TcBody) :- !,
932	TcBody = (TcG1;TcG2),
933	tc_body(G1,TcG1),
934	tc_body(G2,TcG2).
935tc_body((G1->G2),TcBody) :- !,
936	TcBody = (TcG1 -> TcG2),
937	tc_body(G1,TcG1),
938	tc_body(G2,TcG2).
939tc_body(Body, TcBody) :-
940	participating_predicate(Body), !,
942tc_body(Body, TcBody) :-
943	TcBody = Body.
944% }}}
945%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
946
947only_check_participating_clauses(_) :-
948	\+ type_checking, !, fail.
949
950only_check_participating_clauses(Clause) :-
951	only_check_participating_clauses(Clause,_).
952
953only_check_participating_clauses((:- _),_) :- !, fail.
956	FA = F / A,
960	FA = F / A,
962
965	functor(Test,Name,Arity),
966 	signature(Test,_,[],_).
967%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
968basic_normalize_clause(Alias,Type,Clause) :-
969	Clause = type_check:basic_normalize(Alias,Type).
970
971normalize_type(Type0,Type2) :-
972	( nonvar(Type0), basic_normalize(Type0,Type1) ->
973		normalize_type(Type1,Type2)
974	;
975		Type2 = Type0
976	).
977
978equate_types(Type1,Type2) :-
979	( nonvar(Type1), nonvar(Type2) ->
980		normalize_type(Type1,NType1),
981		normalize_type(Type2,NType2),
982		functor(NType1,Functor,Arity),
983		functor(NType2,Functor,Arity),
984		NType1 =.. [_|Args1],
985		NType2 =.. [_|Args2],
986		maplist(equate_types,Args1,Args2)
987	;
988		unify_with_occurs_check(Type1,Type2)
989	).
990%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
991% Utility {{{
992
993lookup_eq([K - V | KVs],Key,Value) :-
994        ( K == Key ->
995                V = Value
996        ;
997                lookup_eq(KVs,Key,Value)
998        ).
999snd_of_pairs([],[]).
1000snd_of_pairs([_-Y|XYs],[Y|Ys]) :-
1001        snd_of_pairs(XYs,Ys).
1002
1003pairup([],[],[]).
1004pairup([X|Xs],[Y|Ys],[X-Y|Rest]) :- pairup(Xs,Ys,Rest).
1005% }}}
1006%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1007% Goal expansion {{{
1008user:goal_expansion(UnsafeCall :: Signature, SafeCall) :- !,
1009	( type_checking_runtime ->
1010		% Already at end_of_file when this code get executed.
1012		% prolog_load_context(term_position,'\$stream_position'(_, LineNumber, _, _, _)),
1013		% format('Expanding annotation in ~w at line ~w\n',[File,LineNumber]),
1014		functor(UnsafeCall,F,A),
1015		functor(Signature,F,A),
1016		UnsafeCall =.. [_|Args],
1017		Signature  =.. [_|Types],
1018		args_body(Args,Types,Guard,[],_),
1019		SafeCall = ( UnsafeCall, ( Guard -> true ; throw(runtime_type_error(UnsafeCall))  ) )
1020	;
1021		SafeCall = UnsafeCall
1022	).
1023
1024user:goal_expansion(UnsafeCall :< _Signature, Call) :- !,
1025	Call = UnsafeCall.
1026
1027user:goal_expansion(type_to_any(X,Y),(X = Y)).
1028user:goal_expansion(any_to_type(X,Y,Type),Goal) :- !,
1029	( type_checking_runtime ->
1030		Goal = (type_check:type_check_term(X,Type,[],_), X=Y)
1031	;
1032		Goal = (X = Y)
1033	).
1034% }}}
1035%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1036% Term expansion {{{
1037%	goes last
1038%	otherwise we end up type checking the type checker...
1039
1040% Strip modes {{{
1041strip_modes(FullSignature,Signature) :-
1042	FullSignature =.. [Functor|FullArgs],
1043	maplist(strip_mode,FullArgs,Args),
1044	Signature =.. [Functor|Args].
1045
1046strip_mode(FullArg,Arg) :-
1047	( var(FullArg) 		->	Arg = FullArg
1048	; FullArg = '+'(Arg)	-> 	true
1049	; FullArg = '-'(Arg)	->	true
1050	; FullArg = '?'(Arg) 	-> 	true
1051	; 				Arg = FullArg
1052	).
1053% }}}
1054
1055user:term_expansion((:- type_check_options(Options)),[]) :-
1056	handle_options(Options).
1057user:term_expansion((:- runtime_type_check(Flag)),[]) :-
1058	%writeln(type_checking_runtime(Flag)),
1059 	handle_option(runtime(Flag)).
1060user:term_expansion((:- type Name ---> Constructors),
1061		     Clauses
1062		    ) :-
1063	( \+ \+ ( numbervars(Name, 0, _), ground(Constructors) ) ->
1064		phrase(constructor_clauses(Constructors,Name), Clauses)
1065	;
1066		format("ERROR: invalid TYPE definition~w\n\tType definitions must be range-restricted!\n", [(:- type Name ---> Constructors)]),
1067		Clauses = []
1068	).
1069user:term_expansion((:- type Alias == Type),
1070		    [ Clause
1071		    ]) :-
1072	basic_normalize_clause(Alias,Type,Clause).
1073user:term_expansion((:- type _Name),[]).		% empty type
1074user:term_expansion((:- pred FullSignature),
1075		    [ Clause
1076		    ]) :-
1077	strip_modes(FullSignature,Signature),
1078	signature_clause(Signature,Clause).
1079user:term_expansion((:- trust_pred FullSignature),
1080		    [ SignatureClause
1081		    , TrustedPredicateClause
1082		    ]) :-
1083	strip_modes(FullSignature,Signature),
1084	signature_clause(Signature,SignatureClause),
1085	functor(Signature,P,N),
1086	TrustedPredicateClause = type_check:trusted_predicate(P/N).
1087user:term_expansion(end_of_file,Clauses) :-
1088	type_check_file(Clauses).
1089
1090user:term_expansion(Clause, NClause) :-
1091	only_check_participating_clauses(Clause),
1092	assert(clause_to_check(Clause)),
1093	NClause = [].
1094
1095% }}}
1096
1097% {{{
1098final_message(tc_stats(E,T)) :-
1099	( T > 0, type_checking_verbose ->
1101		write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'), nl,
1102		format('% Type checking for module `~w\' done:\n%\tfound type errors in ~w out of ~w clauses.\n',[Mod,E,T]),
1103		( E == 0 ->
1104			write('%\tWell-typed code can\'t go wrong!'), nl
1105		;
1106			true
1107		),
1108		write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'), nl
1109	;
1110		true
1111	).
1112
1113init_stats(tc_stats(0,0)).
1114
1115inc_error_stats(tc_stats(E,T),tc_stats(NE,NT)) :-
1116	NE is E + 1,
1117	NT is T + 1.
1118
1119inc_ok_stats(tc_stats(E,T),tc_stats(E,NT)) :-
1120	NT is T + 1.
1121% }}}
1122%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1123% Predefined types:	{{{
1124%
1125%  The types list(T), pair(A,B), boolean, integer and float are predefined by the type
1126%  checker.
1127
1128:- type list(T) 	---> [] ; [T|list(T)]. 1129
1130:- type pair(A,B) 	---> A - B. 1131
1132:- type boolean		---> true ; false. 1133
1134:- type cmp		---> (=) ; (>) ; (<). 1135
1136:- pred compare(cmp,T,T). 1137% }}}
1138
1139%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1140% Predefined signatures:	{{{
1141%
1142
1143% :- pred write(_).
1144% :- pred writeln(_).
1145
1146% }}}
1147%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1148% BUGS FOUND {{{
1149% ==========
1150%
1151% In rbtrees.pl (Vitor Santos Costa)
1152%
1153%	:- pred rb_lookupall(K,V,rbtree(K,V)).
1154%	:- pred lookupall(K,V,tree(K,V)).
1155%	:- pred lookupall(cmp,K,V,tree(K,V)).
1156%
1157%	rb_lookupall(Key, Val, t(_,Tree)) :-
1158%		lookupall(Key, Val, Tree).
1159%
1160%	lookupall(_, _, black(nil,_,_,nil)) :- !, fail.
1161%	lookupall(Key, Val, Tree) :-
1162%		getkey(Tree,KA),		% arg(2,Tree,KA),
1163%		compare(Cmp,KA,Key),
1164%		lookupall(Cmp,Key,Val,Tree).
1165%
1166%	lookupall(>, K, V, Tree) :-
1167%		getright(Tree,NTree),		% arg(4,Tree,NTree),
1168%		rb_lookupall(K, V, NTree).	% BUG !!!
1169%	lookupall(=, _, V, Tree) :-
1170%		getvalue(Tree,V),		% arg(3,Tree,V).
1171%	lookupall(=, K, V, Tree) :-
1172%		getleft(Tree,NTree),		% arg(1,Tree,NTree),
1173%		lookupall(K, V, NTree).
1174%	lookupall(<, K, V, Tree) :-
1175%		getleft(Tree,NTree),		% arg(1,Tree,NTree),
1176%		lookupall(K, V, NTree).
1177%
1178% }}}
1179%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1180%  NOTES {{{
1181%  =====
1182%
1183% In rbtrees.pl (Vitor Santos Costa)
1184%  * cannot share Nil in old and new tree:
1185%
1186%	:- pred rb_clone(rbtree(K,_V1),rbtree(K,V2),list(pair(K,V2))).
1187%	rb_clone(t(_Nil1,T),t(Nil2,NT),Ns) :-
1188%		new(Nil2),
1189%		clone(T,NT,Ns,[]).
1190%
1191% }}}
1192%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%