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
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
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 268 269 270 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 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
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
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 , ( 413 414 inc_error_stats(Stats0,Stats1)
415 )
416 ),
417 type_check_clauses(Clauses,Stats1,Stats).
418
419type_check_clause((:- _)) :- !,
420 true. 421type_check_clause((Head :- Body)) :- !,
422 functor(Head,P,N),
423 ( trusted_predicate(P/N) ->
424 true
425 ;
426 type_check_clause_main(Head,Body)
427 ).
428type_check_clause(Head) :-
429 type_check_clause((Head :- true)).
430
431type_check_clause_main(Head,Body) :-
432 Env0 = [],
433
434 catch(
435 signature(Head,ArgTypes,Env0,Env1),
436 error(type_error(Term,Exp,Inf)),
437 ( head_error(Term,Exp,Inf,Head,Body), fail )
438 ),
439 440 catch(
441 type_check_control(Body,top,Env1,_Env2),
442 error(type_error(Term,Exp,Inf),Context),
443 (control_error(Term,Exp,Inf,Head,Context),fail)
444 ),
445 functor(Head,Name,Arity),
446 InfSig =.. [Name|ArgTypes],
447 448 check_ambiguous_types(InfSig),
449 450 functor(Prototype,Name,Arity),
451 signature(Prototype,ProtoTypes,Env0,_ProtoEnv),
452 ( variant(ArgTypes, ProtoTypes) 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
471check_ambiguous_types(Head) :-
472 term_variables(Head,TyVars),
473 filter(TyVars,is_ambiguous_numeric_type,AmbTyVars),
474 ( AmbTyVars == [] ->
475 true
476 ;
477 copy_term_nat(Head-AmbTyVars,Head1-AmbTyVars1),
478 numbervars(Head1-AmbTyVars1,0,_),
479 write( '%------------------------------------------------------------------------------%'), nl,
480 format('TYPE ERROR: Ambiguous numeric types `~p\'.\n',[AmbTyVars1]),
481 format(' in predicate `~p\'\n',[Head1]),
482 format(' types should be one of `integer\' or `float\' \n',[]),
483 throw(type_error)
484 ).
485
486
497
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))).
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
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 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 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 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 724 Warning = unknown_predicate_call(Goal),
725 W = [Warning|RW],
726 Env1 = Env2.
728
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) :- !, 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), 747 type_check_expression(Exp,integer,Env1,Env2).
748type_check_expression(integer(Exp),Type,Env1,Env2) :- !,
749 equate_types(Type,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 802 type_check_term(Exp,Type,Env1,Env2).
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
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
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 ].
861
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).
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
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.
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,_,[],_).
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 ).
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).
1008user:goal_expansion(UnsafeCall :: Signature, SafeCall) :- !,
1009 ( type_checking_runtime ->
1010 1011 1012 1013 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 ).
1039
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 ).
1054
1055user:term_expansion((:- type_check_options(Options)),[]) :-
1056 handle_options(Options).
1057user:term_expansion((:- runtime_type_check(Flag)),[]) :-
1058 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),[]). 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
1096
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.
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). 1138
1142
1145