% File : TYPECH.PL % Author : Alan Mycroft & R.A.O'Keefe % Updated: 8 June 1984 % Purpose: Prolog type-checker :- public load/1, % for users type_check/5. % for setof/3 %>> This module uses unify/2 from Util:MetUtl.Pl . %>> It also uses append/3 from the utilities. % This program defines a "type-checked consult" operation % load(Files) % where Files is an atom or a list of atoms. There is no % analogue of the reconsult operation. In the Files type % declarations may be given in addition to the usual sort % of commands, questions, clauses, and declarations. You % can put the type declarations in separate files, so that % load(['foo.typ','foo.pl']) can be used to type-check and % load the interpreted version, and compile('foo.pl') can % be used to compile the same code. Note that declarations % have to be processed before clauses using the things % declared. % There are two new declarations: % type --> {| }.. . % e.g. type tree(T) --> empty | tree(T,tree(T),tree(T)). % and % pred {, }.. . % e.g. pred append(list(T), list(T), list(T)). % You may use a semicolon instead of a vertical bar if you like. % As a convenience for defining grammar rules, % rule p(T1,...,Tk). % has the same effect as % pred p(T1,...,Tk,list(T_),list(T_)). % where T_ is not further specified. 'C'/3 is predefined as % pred 'C'(list(X), X, list(X)). :- op(1199, fx, [(type), (pred), (rule)]). :- op(1198, xfy, (-->)). :- op( 999, xfy, (:)). % load/1 is defined in the usual way. The juggling with (no)fileerrors % is to determine whether failure to find a file causes an error message % and abort, or just (as here) a failure. expandterm/2 is where grammar % rules are translated to ordinary Prolog. In Dec-10 Prolog, the style % of programming which uses failure-driven loops is nearly obsolete, % thanks to the introduction of TRO to the compiler, and it was never % considered to be anything other than a hack. However, this stuff has % to be useful in C Prolog and other Prologs which still lack TRO, so % the hack remains. load(Files) :- recorded(void, (type), _), !, % the definitions have been loaded load1(Files). load(Files) :- recordz(void, (type), _), recordz(any, (type), _), recordz((_:-_), type((void:-void), void), _), % for assert load1(['util:prolog.typ'|Files]). load1(Var) :- var(Var), !, write('! load: argument contains a variable'), nl, fail. load1([Head|Tail]) :- !, load1(Head), !, % discard this cut on non-TRO systems load1(Tail). load1(File) :- atom(File), !, nofileerrors, seeing(Old), load2(File), fileerrors, see(Old). load1(File) :- write('! load: argument not list or atom: '), write(File), nl, fail. load2(File) :- see(File), repeat, read(Term), expand_term(Term, Expanded), process_term(Expanded, File), Expanded = end_of_file, !, seen, write(File), write(' loaded.'), nl. load2(File) :- write('! load: can''t see '), write(File), nl, fail. % process_term(Expansion, File) % handles a command, question, clause, or declaration. % Questions are treated as if they were commands, which is just plain % wrong, but only in Prolog-X is a version of 'read' standardly % available which gives you a name->variable list so that you can % print the answers. Type checking wants to be built into a Prolog % system top level from the word go, not added on as an afterthought. process_term(end_of_file, File) :- !. process_term((:- Command), File) :- !, process_command(Command, File). process_term((?- Question), File) :- !, process_command(Question, File). process_term({Unchecked}, File) :- !, assertz(Unchecked). process_term((Head :- Body), File) :- !, type_check((Head:-Body), Clause), assertz(Clause). process_term(Head, File) :- type_check((Head:-true), Clause), assertz(Clause). % process_command(Command, File) % mainly handles declarations. process_command((type Type --> Constructors), File) :- !, process_type(Type, Constructors). process_command((pred Predicates), File) :- !, process_pred(Predicates, (pred)). process_command((rule GrammarRules), File) :- !, process_pred(GrammarRules, (rule)). process_command([Files], File) :- !, load1(Files). process_command((mode Modes), File) :- !, true. % could maybe note that we expect a type? process_command((public PublicDeclarations), File) :- !, true. % could maybe note that we expect a type? process_command(Question, user) :- !, ( type_check(Question, Checked) ; write('! ill-typed '), nl, fail ), ( call(Checked), write(Checked), nl, write('more? '), ttyflush, read(no) ; write('no (more) answers'), nl ). process_command(Command, File) :- ( type_check(Command, Checked) ; write('! ill-typed '), write(Command), write(' in '), write(File), nl, fail ), ( call(Checked), ! ; write('! failed command '), write(Command), write(' in '), write(File), nl, fail ). % The "typed premise" described in Mycroft & O'Keefe is stored two % ways. The types of variables are held in a dynamic data structure % used only within a single clause. The types of predicates and % functors are held in the data base. We use the Dec-10 "recorded" % data base here to reduce clashes with user clauses and make access % a little bit faster, but ordinary clauses could just as easily be % used. There are three cases: % % recorded(Key, (type), _) % - use type_def(Key) as clauses % means that the Key is a type constructor. E.g. after % processing the declaration :- type tree(T) --> ... . % recorded(tree(T), (type), _) % would be true. % % recorded(Key, type(Pat,void), _) % - use has_type(Key, Pat, void) as clauses % means that the Key is defined as a predicate. The Pat looks like % the Key, but has type terms for its arguments. E.g. after % processing the declaration :- pred elem(T, tree(T)). % recorded(elem(_,_), type(elem(T,tree(T)),void), _) % would be true. % % recorded(Key, type(Pat,Val), _) % - use has_type(Key, Pat, Val) as clauses % means that the Key is defined as a function. The Pat looks like % the Key, but has type terms for its arguments. E.g. after % processing the declaration % :- type tree(T) --> empty | t(T,tree(T),tree(T)). % recorded(empty, type(empty,tree(T)), _) and % recorded(t(_,_,_), type(t(T,tree(T),tree(T)),tree(T)), _) % would both be true. % % These declarations are the only way that data of the given forms % are recorded. % process_type(, ) % checks that its arguments are well formed, and if they are, % records the type information about the and the % constructors. process_type(Head, Body) :- check_type_head(Head), recordz(Head, (type), _), % recorded here for recursive types check_type_body(Head, Body, Constructors), process_type_body(Constructors, Head). process_type_body([Constructor|Constructors], Head) :- recordz(Constructor, type(Constructor,Head), _), !, process_type_body(Constructors, Head). process_type_body([], _). check_type_head(Head) :- var(Head), !, write('! Type head is a variable.'), nl, fail. check_type_head(Head) :- recorded(Head, (type), _), !, write('! Already a type: '), write(Head), nl, fail. check_type_head(Head) :- functor(Head, _, N), check_type_head(N, Head), !, fail. check_type_head(_). check_type_head(N, Head) :- arg(N, Head, Arg), nonvar(Arg), write('! Type head argument '), write(N), write(' is bad.'), nl. check_type_head(N, Head) :- arg(N, Head, N), M is N-1, check_type_head(M, Head). % is_type_expr(Term) % succeeds when Term is a type expression, that is, when all the % constructors it is made from are type constructors. If we had % type macros (:- type Lhs = Rhs) this is where we would expand % them. That will come later. is_type_expr(Type) :- var(Type), !. is_type_expr(Type) :- recorded(Type, (type), _), !, functor(Type, _, N), is_type_expr(N, Type). is_type_expr(Type) :- write('! not a type: '), write(Type), nl, fail. is_type_expr(0, Type) :- !. is_type_expr(N, Type) :- arg(N, Type, Arg), is_type_expr(Arg), M is N-1, !, is_type_expr(M, Type). check_type_body(Head, Body, _) :- numbervars(Head, 0, M), numbervars(Body, M, N), N > M, !, write('! Rhs of type def contains variables not in lhs.'), nl, fail. check_type_body(Head, Body, Constructors) :- check_type_body_(Body, Constructors, []). check_type_body_(( Constr1 ; Constr2 ), CL, CR) :- !, check_type_body_(Constr1, CL, CM), check_type_body_(Constr2, CM, CR). check_type_body_({Constructor}, [Constructor|CR], CR) :- nonvar(Constructor), functor(Constructor, _, N), is_type_expr(N, Constructor), !. check_type_body_({Constructor}, _, _) :- !, write('! Dud constructor : '), write(Constructor), nl, fail. check_type_body_(Constructor, CL, CR) :- check_type_body_({Constructor}, CL, CR). % process_pred(Preds, Sort) % processes pred (Sort=pred) and rule (Sort=rule) declarations. % Several predicates may be declared in one declaration, and they % may be separated by any mixture of commas and semicolons. To % declare comma or semicolon as a predicate, you have to put it % inside braces { }, e.g. :- pred {void,void}. The same escape % convention is used to let you define these symbols as constructors % in type declarations. process_pred(Var, Sort) :- var(Var), !, write('! variable in '), write(Sort), write(' declaration.'), nl, fail. process_pred((Preds1 , Preds2), Sort) :- !, process_pred(Preds1, Sort), process_pred(Preds2, Sort). process_pred((Preds1 ; Preds2), Sort) :- !, process_pred(Preds1, Sort), process_pred(Preds2, Sort). process_pred({Pred}, (pred)) :- recorded(Pred, type(_,void), _), !, write('! already declared: '), write(Pred), nl, fail. process_pred({Pred}, (pred)) :- !, functor(Pred, _, N), is_type_expr(N, Pred), recordz(Pred, type(Pred,void), _). process_pred({Rule}, (rule)) :- !, Rule =.. List, append(List, [list(T),list(T)], Full), Pred =.. Full, process_pred({Pred}, (pred)). process_pred(Other, Sort) :- process_pred({Other}, Sort). % To perform type checking we use the Milner algorithm with overloading. % The idea is that we consider (via backtracking) all the type resolutions % possible, and accept the typing if exactly one type assignment exists. % For this (second order) operation we use 'setof'. The typed premise % is in two parts. The predicate and functor assignments are held in the % data base, the variable assignments (which only have significance within % the current clause) in held in Tenv (type environment) variables. % type tenv --> var | var(variable,type,tenv). type_check(Given, Pruned) :- setof(P, To^type_check(Given, P, var, To, void), PP), ( PP = [Pruned], ! ; write('! ambiguous overloaded functor.'), nl, !, fail ). type_check(:-(Head,Body), _) :- write('% no type can be assigned to the rule'), nl, !, pp_explicit(:-(Head,Body), Head). type_check(Head, _) :- write('% no type can be assigned to the fact'), nl, !, pp_explicit(Head, Head). % type_check(Given, Pruned, TenvIn, TenvOut, Expected) % checks a Given term which is expected to have type Expected. % It may extend the type environment, as well as further specifying % existing variable assignments, and it returns the Given term % Pruned of ":Type" annotations. The point of the latter is to % help the type system when it comes across an overloaded term that % it is otherwise unable to resolve. type_check(X, X, Ti, Ti, Expected) :- Expected == any, !. % X had better not contain :annotations! type_check(Var, Var, Ti, To, Context) :- var(Var), !, type_check(Var, Ti, To, Context). type_check((Given:Type), Pruned, Ti, To, Expected) :- !, unify(Type, Expected), type_check(Given, Pruned, Ti, To, Expected). type_check((Head:-Body), (Lhs:-Rhs), Ti, To, void) :- !, recorded(Head, type(HeadT,void), _), numbervars(HeadT, 0, _), % crucial functor(Head, F, N), functor(Lhs, F, N), type_check(N, Head, Lhs, Ti, Tm, HeadT), type_check(Body, Rhs, Tm, To, void). type_check(Int, Int, Ti, Ti, integer) :- integer(Int), !. % special hack for numbers type_check(Given, Pruned, Ti, To, Expected) :- recorded(Given, type(GivenT, ResultT), _), unify(ResultT, Expected), functor(Given, F, N), functor(Pruned, F, N), type_check(N, Given, Pruned, Ti, To, GivenT). % Type check a variable type_check(Var, Ti, Ti, Expected) :- varassoc(Ti, Var, VarT), !, unify(VarT, Expected). type_check(Var, Ti, var(Var,Expected,Ti), Expected). varassoc(var(V,T,_), Var, T) :- V == Var, !. varassoc(var(_,_,R), Var, T) :- varassoc(R, Var, T). % Type check the arguments of a term. The Given, Pruned, and Expected % arguments all have the same principal functor, and N is the number % of arguments still to be checked. type_check(0, _, _, Ti, Ti, _) :- !. type_check(N, Given, Pruned, Ti, To, Expected) :- arg(N, Given, Agiven), arg(N, Expected, Aexpected), type_check(Agiven, Apruned, Ti, Tm, Aexpected), arg(N, Pruned, Apruned), M is N-1, % There *MUSTN'T* be a cut here, as we want type_check/5 % to be able to back-track and try another assignment. type_check(M, Given, Pruned, Tm, To, Expected).