ok@edai.UUCP (Richard O'Keefe) (08/05/83)
This is the Prolog type checker I promised ages ago.
The rest of the file is an ed script for making the
files typech.pl and prolog.typ .
------------------------------------------------------------
a
% File : TYPECH.PL
% Author : Alan Mycroft & R.A.O'Keefe
% Updated: 23 June 1983
% 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 <type term> --> <constr>{| <constr>}.. .
% e.g. type tree(T) --> empty | tree(T,tree(T),tree(T)).
% and
% pred <pred decl>{, <pred decl>}.. .
% 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(['prolog.typ'|Files]).
load1(Var) :-
var(Var),
!,
display('! load: argument contains a variable'), ttynl,
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) :-
display('! load: argument not list or atom: '),
display(File), ttynl,
fail.
load2(File) :-
see(File),
repeat,
read(Term),
expand_term(Term, Expanded),
process_term(Expanded, File),
Expanded = end_of_file,
!,
seen,
display(File), display(' loaded.'), ttynl.
load2(File) :-
display('! load: can''t see '),
display(File), ttynl,
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)
; display('! ill-typed '), ttynl, fail
),
( call(Checked),
write(Checked), nl, display('more? '), ttyflush,
read(no)
; display('no (more) answers'), ttynl
).
process_command(Command, File) :-
( type_check(Command, Checked)
; display('! ill-typed '), write(Command),
display(' in '), display(File), ttynl, fail
),
( call(Checked), !
; display('! failed command '), write(Command),
display(' in '), display(File), ttynl, 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(<type head>, <type body>)
% checks that its arguments are well formed, and if they are,
% records the type information about the <type head> 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),
!,
display('! Type head is a variable.'), ttynl,
fail.
check_type_head(Head) :-
recorded(Head, (type), _),
!,
display('! Already a type: '), display(Head), ttynl,
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),
display('! Type head argument '), display(N),
display(' is bad.'), ttynl.
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) :-
display('! not a type: '),
display(Type), ttynl,
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,
!,
display('! Rhs of type def contains variables not in lhs.'), ttynl,
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}, _, _) :- !,
display('! Dud constructor : '),
display(Constructor), ttynl,
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),
!,
display('! variable in '), display(Sort),
display(' declaration.'), ttynl,
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), _),
!,
display('! already declared: '), display(Pred), ttynl,
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], !
; display('! ambiguous overloaded functor.'), ttynl, !, fail
).
type_check(_, _) :-
display('! no type can be assigned.'), ttynl, fail.
% 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).