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
   10%       Spyros Hadjichristodoulou
   11%	YOUR NAME HERE
   12%
   13% ACKNOWLEDGEMENTS:
   14%	Ulrich Neumerkel for providing feedback	
   15%	Vitor Santos Costa
   16%	Jose Santos
   17%	YOUR NAME HERE
   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:
  147%	* added cmp/0 type
  148%	* added compare/3 built-in
  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
  157%	* added call/1 built-in
  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'
  162%	* added string/0 type
  163%	* added get_char/1 built-in
  164%	* added atom_concat/3 built-in
  165%	* added atom_length/2 built-in
  166%	* added atom_chars/2 built-in
  167%	* added concat_atom/2 built-in
  168%	* added any/0 type
  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)). % for maplist/*
  193
  194:- op(1150, fx, type).  195:- op(1130, xfx, ---> ).  196:- op(1150, fx, pred).  197:- op(500,yfx,::).  198:- op(500,yfx,:<).  199
  200:- multifile
  201	user:term_expansion/2,
  202	user:goal_expansion/2,
  203	prolog:message/3,
  204	constructor/4,
  205	constructor_info/4,
  206	signature/4,
  207	trusted_predicate/1,
  208	basic_normalize/2.  209
  210:- dynamic
  211	user:term_expansion/2,
  212	user:goal_expansion/2,
  213	signature/4,
  214	constructor_info/4,
  215	trusted_predicate/1,
  216	basic_normalize/2.  217
  218tc_version('$Id: type_check.pl,v 1.52 2010-06-16 03:51:31 toms Exp $').
  219
  220%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  221%% Type checker options {{{
  222
  223:- nb_setval(type_check_runtime,off).  224:- nb_setval(type_check,on).  225:- nb_setval(type_check_verbose,on).  226
  227handle_options(List) :- maplist(handle_option,List).
  228
  229handle_option(verbose(Flag)) :- !, nb_setval(type_check_verbose,Flag).
  230handle_option(runtime(Flag)) :- !, nb_setval(type_check_runtime,Flag).
  231handle_option(check(Flag))   :- !, nb_setval(type_check,Flag).
  232handle_option(Other)	     :- format('Unsupported type checker option `~w\'.\n',[Other]).
  233
  234
  235type_checking_runtime :- nb_getval(type_check_runtime,on).
  236type_checking_verbose :- nb_getval(type_check_verbose,on).
  237type_checking         :- nb_getval(type_check,on).
  238
  239% }}}
  240%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  241
  242
  243
  244
  245type_check_term(Term,ExpectedType,EnvIn,EnvOut) :-
  246	normalize_type(ExpectedType,NormalExpectedType),
  247	type_check_term_(Term,NormalExpectedType,EnvIn,EnvOut).
  248
  249type_check_term_(Term,ExpectedType,EnvIn,EnvOut) :-
  250	var(Term), !,
  251	( lookup_eq(EnvIn,Term,EnvType) ->
  252		( equate_types(ExpectedType,EnvType) ->
  253			true
  254		;
  255			term_type_error(Term,ExpectedType,EnvType)
  256		),
  257		EnvIn = EnvOut
  258	;	
  259		EnvOut = [Term-ExpectedType|EnvIn]
  260	).
  261type_check_term_(Term,Type,EnvIn,EnvOut) :-
  262	integer(Term), !,
  263	numeric_type(Type),
  264	EnvIn = EnvOut.	
  265	% ( equate_types(Type,integer) ->
  266	%	EnvIn = EnvOut
  267	% ;
  268	%	term_type_error(Term,integer,Type)
  269	% ).
  270type_check_term_(Term,Type,EnvIn,EnvOut) :-
  271	float(Term), !,
  272	( equate_types(Type,float) ->
  273		EnvIn = EnvOut
  274	;
  275		term_type_error(Term,float,Type)
  276	).
  277
  278type_check_term_(Term,Type,EnvIn,EnvOut) :-
  279	nonvar(Type),
  280	functor(Type,pred,Arity),
  281	!,
  282	Type =.. [_|ArgTypes], 
  283	Term =.. [Functor|Args],
  284	length(DummyArgs,Arity),
  285	append(Args,DummyArgs,FullArgs),
  286	Goal =.. [Functor|FullArgs],
  287	pairup(DummyArgs,ArgTypes,ExtraEnv),
  288	append(ExtraEnv,EnvIn,Env),
  289	type_check_control(Goal,top,Env,EnvOut).
  290
  291type_check_term_(Term,Type,EnvIn,EnvOut) :-
  292	Type == string, !,
  293	( atom(Term) -> EnvIn = EnvOut
  294	; term_type_error(Term,unknown_type,Type)
  295	).
  296
  297type_check_term_(_Term,Type,EnvIn,EnvOut) :-
  298	Type == any, !,
  299	EnvIn = EnvOut.
  300
  301type_check_term_(Term,Type,EnvIn,EnvOut) :-
  302	% constructor(Term,Type,EnvIn,EnvOut), !.
  303	functor_constraint(Term,Type,Args,Types), !,
  304	type_check_terms(Args,Types,EnvIn,EnvOut).
  305
  306type_check_term_(Term,Type,_EnvIn,_EnvOut) :-
  307	term_type_error(Term,unknown_type,Type).
  308
  309type_check_terms([],[],Env,Env).
  310type_check_terms([Term|Terms],[Type|Types],Env1,Env3) :-
  311	type_check_term(Term,Type,Env1,Env2),
  312	type_check_terms(Terms,Types,Env2,Env3).
  313
  314term_type_error(Term,ExpectedType,EnvType) :-
  315	throw(error(type_error(Term,ExpectedType,EnvType))).
  316
  317%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  318
  319constructor_clauses((A;B),Type) --> !,
  320	constructor_clauses(A,Type),
  321	constructor_clauses(B,Type).
  322constructor_clauses(Constructor,Type) -->
  323	{ functor(Constructor, Name, Arity),
  324	  functor(Term, Name, Arity),
  325	  Term        =.. [_|Args],
  326	  Constructor =.. [_|Types],
  327	  args_body(Args,Types,Body,EnvIn,EnvOut)
  328	},
  329	[ ( type_check:constructor(Term, ExpectedType, EnvIn, EnvOut) :-
  330		( type_check:equate_types(ExpectedType,Type) ->
  331			true
  332		;
  333			type_check:term_type_error(Term,ExpectedType,Type)
  334		),
  335		Body
  336	  )
  337	],
  338	constructor_info_clause(Constructor,Type).
  339
  340constructor_info_clause(Constructor,Type) -->
  341	{ functor(Constructor, Name, Arity),
  342	  functor(Term, Name, Arity),
  343	  Term        =.. [_|Args],
  344	  Constructor =.. [_|Types],
  345	  Clause = type_check:constructor_info(Term, Type, Args, Types)
  346	},
  347	[ Clause
  348	].
  349				
  350args_body([],[],true,Env,Env).
  351args_body([Term|Terms],[Type|Types],(type_check:type_check_term(Term,Type,EnvIn,Env),Body),EnvIn,EnvOut) :-
  352	args_body(Terms,Types,Body,Env,EnvOut).
  353
  354signature_clause(Signature, Clause) :-
  355	( check_signature(Signature) ->
  356		signature_clause_(Signature, Clause)
  357	;
  358		true
  359	).
  360
  361
  362signature_clause_(Signature,Clause) :-
  363	functor(Signature,Name,Arity),
  364	functor(Call,Name,Arity),
  365	Call      =.. [_|Args],
  366	Signature =.. [_|Types],	
  367	args_body(Args,Types,Body,EnvIn,EnvOut),
  368	Clause = 
  369	( type_check:signature(Call,Types,EnvIn,EnvOut) :-
  370		Body
  371	).
  372
  373check_signature(Signature) :-
  374	nonvar(Signature),
  375	functor(Signature,Name,Arity),
  376	functor(Prototype,Name,Arity),
  377	( signature(Prototype,_,[],_) ->
  378		duplicate_signature_error(Signature),
  379		fail
  380	;
  381		true
  382	).
  383
  384%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  385type_check_file(NClauses) :-
  386	findall(Clause,retract(clause_to_check(Clause)),Clauses),
  387	( type_checking ->
  388		type_check_clauses(Clauses,Stats),
  389		( type_checking_runtime ->
  390			transform_clauses(Clauses,NClauses)
  391		;
  392			NClauses = Clauses
  393		),
  394		final_message(Stats)
  395	;
  396		NClauses = Clauses	
  397	).
  398
  399type_check_clauses(Clauses,Stats) :-
  400	init_stats(Stats0),
  401	type_check_clauses(Clauses,Stats0,Stats).
  402
  403type_check_clauses([],Stats,Stats).
  404type_check_clauses([Clause|Clauses],Stats0,Stats) :-
  405	catch(
  406		( type_check_clause(Clause) , 
  407		  inc_ok_stats(Stats0,Stats1)
  408		)
  409	     ,  error(type_error(_Term,_ExpType,_InfType))
  410	     ,  ( %format('TYPE ERROR in clause: \n\n',[]),
  411	  	  %portray_clause(Clause),
  412		  inc_error_stats(Stats0,Stats1)
  413		)
  414	     ),
  415	type_check_clauses(Clauses,Stats1,Stats).
  416
  417type_check_clause((:- _)) :- !,
  418	true. % ignoring
  419type_check_clause((Head :- Body)) :- !,
  420	functor(Head,P,N),
  421	( trusted_predicate(P/N) ->
  422		true
  423	;
  424		type_check_clause_main(Head,Body)
  425	).
  426type_check_clause(Head) :- 
  427	type_check_clause((Head :- true)).
  428
  429type_check_clause_main(Head,Body) :-
  430	Env0 = [], 
  431        /* check the head */ 
  432        catch(
  433		signature(Head,ArgTypes,Env0,Env1),
  434		error(type_error(Term,Exp,Inf)),
  435		( head_error(Term,Exp,Inf,Head,Body), fail )
  436	),
  437	/* check the body */
  438	catch( 
  439	  	 type_check_control(Body,top,Env1,_Env2),
  440		error(type_error(Term,Exp,Inf),Context),
  441		(control_error(Term,Exp,Inf,Head,Context),fail)
  442	),
  443	functor(Head,Name,Arity),
  444	InfSig =.. [Name|ArgTypes],
  445	/* check for ambiguous types */
  446	check_ambiguous_types(InfSig),
  447	/* check whether Head is variant of signature */
  448	functor(Prototype,Name,Arity),
  449	signature(Prototype,ProtoTypes,Env0,_ProtoEnv),
  450	( variant(ArgTypes, ProtoTypes) % JCAS: equivalent to  ArgTypes =@= ProtoTypes but does not require SWI.pl
  451	 ->
  452	  true
  453	;
  454	  DecSig =.. [Name|ProtoTypes],
  455	  less_polymorphic_error((:- pred InfSig),
  456	  			 (:- pred DecSig)), 
  457	  throw(type_error)
  458	). 
  459
  460filter([],_Pred,[]).
  461filter([X|Xs],Pred,Result) :-
  462	( call(Pred,X) ->
  463		Result = [X|More],
  464		filter(Xs,Pred,More)
  465	;
  466		filter(Xs,Pred,Result)
  467	).
  468
  469check_ambiguous_types(Head) :-
  470	term_variables(Head,TyVars),
  471	filter(TyVars,is_ambiguous_numeric_type,AmbTyVars),			
  472	( AmbTyVars == [] ->
  473		true
  474	;
  475		copy_term_nat(Head-AmbTyVars,Head1-AmbTyVars1),
  476		numbervars(Head1-AmbTyVars1,0,_),
  477		write( '%------------------------------------------------------------------------------%'), nl,
  478		format('TYPE ERROR: Ambiguous numeric types `~p\'.\n',[AmbTyVars1]), 
  479		format('           in predicate `~p\'\n',[Head1]),
  480		format('            types should be one of `integer\' or `float\' \n',[]),
  481		throw(type_error)
  482	).
  483		
  484
  485% context ::=
  486%	  top
  487%	| lconj parent right
  488%	| rconj parent left
  489%	| ldisj parent right
  490%	| rdisj parent left
  491%	| cond  parent then
  492%	| then  parent cond
  493%	| once  parent
  494%	| findall parent pattern result
  495
  496% 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
  813head_error(Term,ExpType,InfType,Head,Body) :-
  814	write( '%------------------------------------------------------------------------------%'), nl,
  815	format('TYPE ERROR: expected type `~w\' for term `~w\'\n',[ExpType,Term]),
  816	format('           inferred type `~w\'\n',[InfType]),
  817	format('\tin head `~w\' of clause:\n',[Head]),
  818	portray_clause((Head :- Body)),
  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
  837% control_error(+term,+type,+type,+head,+context) {{{ 
  838control_error(Term,ExpType,InfType,Head,context(Source,Context)) :-
  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),
  843	portray_clause((Head :- 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%
  906% 6 ?- functor(Head,p,2), Clause = (Head :- signature(Head)), portray_clause(Clause).
  907% p(_, _) :-
  908%         signature(p(_, _)).
  909
  910wrapper_clause(F/A,Clause) :-
  911	functor(Head,F,A),
  912	tc_head(Head,Call),
  913	Clause = (Head :- type_check:signature(Head,_,[],_), Call ).
  914
  915tc_clause((Head :- Body),(TcHead :- TcBody)) :- !,
  916	tc_head(Head,TcHead),
  917	tc_body(Body,TcBody).
  918tc_clause(Head, TcHead) :-
  919	tc_head(Head,TcHead).
  920
  921tc_head(Head,TcHead) :-
  922	Head =.. [F|Args],
  923	atom_concat('$tc_',F,NF),
  924	TcHead =.. [NF|Args].
  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), !,
  941	tc_head(Body,TcBody).
  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.
  954only_check_participating_clauses((Head :- _),FA) :- !,
  955	participating_predicate(Head),
  956	FA = F / A,
  957	functor(Head,F,A).
  958only_check_participating_clauses(Head,FA) :-
  959	participating_predicate(Head),
  960	FA = F / A,
  961	functor(Head,F,A).
  962
  963participating_predicate(Head) :-
  964	functor(Head,Name,Arity),
  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.
 1011		% prolog_load_context(file,File),
 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 -> 
 1100		prolog_load_context(module,Mod),
 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%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%