--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/type.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,783 @@
+(* Title: Types and Sorts
+ ID: $Id$
+ Author: Tobias Nipkow & Lawrence C Paulson
+
+Maybe type classes should go in a separate module?
+*)
+
+
+signature TYPE =
+sig
+ structure Symtab:SYMTAB
+ type type_sig
+ val defaultS: type_sig -> sort
+ val extend: type_sig * (class * class list)list * sort *
+ (string list * int)list *
+ (string list * (sort list * class))list -> type_sig
+ val freeze: (indexname -> bool) -> term -> term
+ val freeze_vars: typ -> typ
+ val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) *
+ (indexname -> sort option) * (typ -> string) * typ * term
+ -> term * (indexname*typ)list
+ val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term
+ val logical_type: type_sig -> string -> bool
+ val merge: type_sig * type_sig -> type_sig
+ val thaw_vars: typ -> typ
+ val tsig0: type_sig
+ val type_errors: type_sig * (typ->string) -> typ * string list -> string list
+ val typ_instance: type_sig * typ * typ -> bool
+ val typ_match: type_sig -> (indexname*typ)list * (typ*typ) ->
+ (indexname*typ)list
+ val unify: type_sig -> (typ*typ) * (indexname*typ)list -> (indexname*typ)list
+ val varifyT: typ -> typ
+ val varify: term * string list -> term
+ exception TUNIFY
+ exception TYPE_MATCH;
+end;
+
+functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) : TYPE =
+struct
+structure Symtab = Symtab
+
+(* Miscellany *)
+
+val commas = space_implode ",";
+fun str_of_sort S = "{" ^ commas S ^ "}";
+fun str_of_dom dom = "(" ^ commas (map str_of_sort dom) ^ ")";
+fun str_of_decl(t,w,C) = t ^ ": " ^ str_of_dom w ^ C;
+
+
+(* Association list Manipulation *)
+
+
+(* two-fold Association list lookup *)
+
+fun assoc2 (aal,(key1,key2)) = case assoc (aal,key1) of
+ Some (al) => assoc (al,key2)
+ | None => None;
+
+
+
+(**** TYPE CLASSES ****)
+
+type domain = sort list;
+type arity = domain * class;
+
+datatype type_sig =
+ TySg of {classes: class list,
+ default: sort,
+ subclass: (class * class list) list,
+ args: (string * int) list,
+ coreg: (string * (class * domain) list) list };
+
+(* classes: a list of all declared classes;
+ default: the default sort attached to all unconstrained TVars
+ occurring in a term to be type-inferred;
+ subclass: association list representation of subclass relationship;
+ (c,cs) is interpreted as "c is a proper subclass of all
+ elemenst of cs". Note that c itself is not a memeber of cs.
+ args: an association list of all declared types with the number of their
+ arguments
+ coreg: a two-fold association list of all type arities; (t,al) means that
+ type constructor t has the arities in al; an element (c,ss) of al
+ represents the arity (ss)c
+*)
+
+
+val tsig0 = TySg{classes = [],
+ default = [],
+ subclass = [],
+ args = [],
+ coreg = []};
+
+fun undcl_class (s) = error("Class " ^ s ^ " has not been declared");
+
+fun undcl_type(c) = "Undeclared type: " ^ c;
+fun undcl_type_err(c) = error(undcl_type(c));
+
+
+(* 'leq' checks the partial order on classes according to the
+ statements in the association list 'a' (i.e.'subclass')
+*)
+
+fun less a (C,D) = case assoc (a,C) of
+ Some(ss) => D mem ss
+ | None => undcl_class (C) ;
+
+fun leq a (C,D) = C = D orelse less a (C,D);
+
+
+fun defaultS(TySg{default,...}) = default;
+
+(* 'logical_type' checks if some type declaration t has as range
+ a class which is a subclass of "logic" *)
+
+fun logical_type(tsig as TySg{subclass,coreg,...}) t =
+ let fun is_log C = leq subclass (C,"logic")
+ in case assoc (coreg,t) of
+ Some(ars) => exists (is_log o #1) ars
+ | None => undcl_type_err(t)
+ end;
+
+
+(* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
+ S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1
+ with C1 <= C2 (according to an association list 'a')
+*)
+
+fun sortorder a (S1,S2) =
+ forall (fn C2 => exists (fn C1 => leq a (C1,C2)) S1) S2;
+
+
+(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
+ there exists no class in S which is <= C;
+ the resulting set is minimal if S was minimal
+*)
+
+fun inj a (C,S) =
+ let fun inj1 [] = [C]
+ | inj1 (D::T) = if leq a (D,C) then D::T
+ else if leq a (C,D) then inj1 T
+ else D::(inj1 T)
+ in inj1 S end;
+
+
+(* 'union_sort' forms the minimal union set of two sorts S1 and S2
+ under the assumption that S2 is minimal *)
+
+fun union_sort a = foldr (inj a);
+
+
+(* 'elementwise_union' forms elementwise the minimal union set of two
+ sort lists under the assumption that the two lists have the same length
+*)
+
+fun elementwise_union a (Ss1,Ss2) = map (union_sort a) (Ss1~~Ss2);
+
+
+(* 'lew' checks for two sort lists the ordering for all corresponding list
+ elements (i.e. sorts) *)
+
+fun lew a (w1,w2) = forall (sortorder a) (w1~~w2);
+
+
+(* 'is_min' checks if a class C is minimal in a given sort S under the
+ assumption that S contains C *)
+
+fun is_min a S C = not (exists (fn (D) => less a (D,C)) S);
+
+
+(* 'min_sort' reduces a sort to its minimal classes *)
+
+fun min_sort a S = distinct(filter (is_min a S) S);
+
+
+(* 'min_domain' minimizes the domain sorts of type declarationsl;
+ the function will be applied on the type declarations in extensions *)
+
+fun min_domain subclass =
+ let fun one_min (f,(doms,ran)) = (f, (map (min_sort subclass) doms, ran))
+ in map one_min end;
+
+
+(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
+ and gives back a list of those range classes whose domains meet the
+ predicate 'pred' *)
+
+fun min_filter a pred ars =
+ let fun filt ([],l) = l
+ | filt ((c,x)::xs,l) = if pred(x) then filt (xs,inj a (c,l))
+ else filt (xs,l)
+ in filt (ars,[]) end;
+
+
+(* 'cod_above' filters all arities whose domains are elementwise >= than
+ a given domain 'w' and gives back a list of the corresponding range
+ classes *)
+
+fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars;
+
+
+(* 'least_sort' returns for a given type its maximum sort:
+ - type variables, free types: the sort brought with
+ - type constructors: recursive determination of the maximum sort of the
+ arguments if the type is declared in 'coreg' of the
+ given type signature *)
+
+fun least_sort (tsig as TySg{subclass,coreg,...}) =
+ let fun ls(T as Type(a,Ts)) =
+ let val ars = case assoc (coreg,a) of Some(ars) => ars
+ | None => raise TYPE(undcl_type a,[T],[]);
+ in cod_above(subclass,map ls Ts,ars) end
+ | ls(TFree(a,S)) = S
+ | ls(TVar(a,S)) = S
+ in ls end;
+
+
+fun check_has_sort(tsig as TySg{subclass,coreg,...},T,S) =
+ if sortorder subclass ((least_sort tsig T),S) then ()
+ else raise TYPE("Type not of sort " ^ (str_of_sort S),[T],[])
+
+
+(*Instantiation of type variables in types *)
+fun inst_typ_tvars(tsig,tye) =
+ let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
+ | inst(T as TFree _) = T
+ | inst(T as TVar(v,S)) = (case assoc(tye,v) of
+ None => T | Some(U) => (check_has_sort(tsig,U,S); U))
+ in inst end;
+
+(*Instantiation of type variables in terms *)
+fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye));
+
+exception TYPE_MATCH;
+
+(* Typ matching
+ typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *)
+fun typ_match tsig =
+let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of
+ None => ( (v, (check_has_sort(tsig,T,S); T))::subs
+ handle TYPE _ => raise TYPE_MATCH )
+ | Some(U) => if U=T then subs else raise TYPE_MATCH)
+ | tm(subs, (Type(a,Ts), Type(b,Us))) =
+ if a<>b then raise TYPE_MATCH
+ else foldl tm (subs, Ts~~Us)
+ | tm(subs, (TFree(x), TFree(y))) =
+ if x=y then subs else raise TYPE_MATCH
+ | tm _ = raise TYPE_MATCH
+in tm end;
+
+fun typ_instance(tsig,T,U) = let val x = typ_match tsig ([],(U,T)) in true end
+ handle TYPE_MATCH => false;
+
+
+(* EXTENDING AND MERGIN TYPE SIGNATURES *)
+
+fun not_ident(s) = error("Must be an identifier: " ^ s);
+
+fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
+
+(*Is the type valid? Accumulates error messages in "errs".*)
+fun type_errors (tsig as TySg{classes,subclass,args,...},
+ string_of_typ) (T,errs) =
+let fun class_err([],errs) = errs
+ | class_err(S::Ss,errs) =
+ if S mem classes then class_err (Ss,errs)
+ else class_err (Ss,("Class " ^ S ^ " has not been declared") :: errs)
+ fun errors(Type(c,Us), errs) =
+ let val errs' = foldr errors (Us,errs)
+ in case assoc(args,c) of
+ None => (undcl_type c) :: errs
+ | Some(n) => if n=length(Us) then errs'
+ else ("Wrong number of arguments: " ^ c) :: errs
+ end
+ | errors(TFree(_,S), errs) = class_err(S,errs)
+ | errors(TVar(_,S), errs) = class_err(S,errs);
+in case errors(T,[]) of
+ [] => ((least_sort tsig T; errs)
+ handle TYPE(_,[U],_) => ("Ill-formed type: " ^ string_of_typ U)
+ :: errs)
+ | errs' => errs'@errs
+end;
+
+
+(* 'add_class' adds a new class to the list of all existing classes *)
+
+fun add_class (classes,(s,_)) =
+ if s mem classes then error("Class " ^ s ^ " declared twice.")
+ else s::classes;
+
+(* 'add_subclass' adds a tuple consisiting of a new class (the new class
+ has already been inserted into the 'classes' list) and its
+ superclasses (they must be declared in 'classes' too) to the 'subclass'
+ list of the given type signature;
+ furthermore all inherited superclasses according to the superclasses
+ brought with are inserted and there is a check that there are no
+ cycles (i.e. C <= D <= C, with C <> D); *)
+
+fun add_subclass classes (subclass,(s,ges)) =
+let fun upd (subclass,s') = if s' mem classes then
+ let val Some(ges') = assoc (subclass,s)
+ in case assoc (subclass,s') of
+ Some(sups) => if s mem sups
+ then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
+ else overwrite (subclass,(s,sups union ges'))
+ | None => subclass
+ end
+ else undcl_class(s')
+in foldl upd (subclass@[(s,ges)],ges) end;
+
+
+(* 'extend_classes' inserts all new classes into the corresponding
+ lists ('classes','subclass') if possible *)
+
+fun extend_classes (classes,subclass,newclasses) =
+ if newclasses = [] then (classes,subclass) else
+ let val classes' = foldl add_class (classes,newclasses);
+ val subclass' = foldl (add_subclass classes') (subclass,newclasses);
+ in (classes',subclass') end;
+
+(* Corregularity *)
+
+(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
+
+fun is_unique_decl coreg (t,(s,w)) = case assoc2 (coreg,(t,s)) of
+ Some(w1) => if w = w1 then () else
+ error("There are two declarations\n" ^
+ str_of_decl(t,w,s) ^ " and\n" ^
+ str_of_decl(t,w1,s) ^ "\n" ^
+ "with the same result class.")
+ | None => ();
+
+(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
+ such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
+
+fun subs (classes,subclass) C =
+ let fun sub (rl,l) = if leq subclass (l,C) then l::rl else rl
+ in foldl sub ([],classes) end;
+
+fun coreg_err(t,(w1,C),(w2,D)) =
+ error("Declarations " ^ str_of_decl(t,w1,C) ^ " and "
+ ^ str_of_decl(t,w2,D) ^ " are in conflict");
+
+fun restr2 classes (subclass,coreg) (t,(s,w)) =
+ let fun restr ([],test) = ()
+ | restr (s1::Ss,test) = (case assoc2 (coreg,(t,s1)) of
+ Some (dom) => if lew subclass (test (w,dom)) then restr (Ss,test)
+ else coreg_err (t,(w,s),(dom,s1))
+ | None => restr (Ss,test))
+ fun forward (t,(s,w)) =
+ let val s_sups = case assoc (subclass,s) of
+ Some(s_sups) => s_sups | None => undcl_class(s);
+ in restr (s_sups,I) end
+ fun backward (t,(s,w)) =
+ let val s_subs = subs (classes,subclass) s
+ in restr (s_subs,fn (x,y) => (y,x)) end
+ in (backward (t,(s,w)); forward (t,(s,w))) end;
+
+
+fun varying_decls(t) =
+ error("Type constructor "^t^" has varying number of arguments.");
+
+
+
+(* 'coregular' checks
+ - the two restriction conditions 'is_unique_decl' and 'restr2'
+ - if the classes in the new type declarations are known in the
+ given type signature
+ - if one type constructor has always the same number of arguments;
+ if one type declaration has passed all checks it is inserted into
+ the 'coreg' association list of the given type signatrure *)
+
+fun coregular (classes,subclass,args) =
+ let fun ex C = if C mem classes then () else undcl_class(C);
+
+ fun addar(w,C) (coreg,t) = case assoc(args,t) of
+ Some(n) => if n <> length w then varying_decls(t) else
+ (is_unique_decl coreg (t,(C,w));
+ (seq o seq) ex w;
+ restr2 classes (subclass,coreg) (t,(C,w));
+ let val Some(ars) = assoc(coreg,t)
+ in overwrite(coreg,(t,(C,w) ins ars)) end)
+ | None => undcl_type_err(t);
+
+ fun addts(coreg,(ts,ar)) = foldl (addar ar) (coreg,ts)
+
+ in addts end;
+
+
+(* 'close' extends the 'coreg' association list after all new type
+ declarations have been inserted successfully:
+ for every declaration t:(Ss)C , for all classses D with C <= D:
+ if there is no declaration t:(Ss')C' with C < C' and C' <= D
+ then insert the declaration t:(Ss)D into 'coreg'
+ this means, if there exists a declaration t:(Ss)C and there is
+ no declaration t:(Ss')D with C <=D then the declaration holds
+ for all range classes more general than C *)
+
+fun close (coreg,subclass) =
+ let fun check sl (l,(s,dom)) = case assoc (subclass,s) of
+ Some(sups) =>
+ let fun close_sup (l,sup) =
+ if exists (fn s'' => less subclass (s,s'') andalso
+ leq subclass (s'',sup)) sl
+ then l
+ else (sup,dom)::l
+ in foldl close_sup (l,sups) end
+ | None => l;
+ fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l));
+ in map ext coreg end;
+
+fun add_types(ac,(ts,n)) =
+ let fun add_type((args,coreg),t) = case assoc(args,t) of
+ Some _ => twice(t) | None => ((t,n)::args,(t,[])::coreg)
+ in if n<0
+ then error("Type constructor cannot have negative number of arguments")
+ else foldl add_type (ac,ts)
+ end;
+
+(* 'extend' takes the above described check- and extend-functions to
+ extend a given type signature with new classes and new type declarations *)
+
+fun extend (TySg{classes,default,subclass,args,coreg},
+ newclasses,newdefault,types,arities) =
+let val (classes',subclass') = extend_classes(classes,subclass,newclasses);
+ val (args',coreg') = foldl add_types ((args,coreg),types);
+ val old_coreg = map #1 coreg;
+ fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c);
+ fun is_new(c) = if c mem old_coreg then twice(c) else ();
+ val coreg'' = foldl (coregular (classes',subclass',args'))
+ (coreg',min_domain subclass' arities);
+ val coreg''' = close (coreg'',subclass');
+ val default' = if null newdefault then default else newdefault;
+in TySg{classes=classes', default=default',subclass=subclass', args=args',
+ coreg=coreg'''} end;
+
+
+(* 'assoc_union' merges two association lists if the contents associated
+ the keys are lists *)
+
+fun assoc_union (as1,[]) = as1
+ | assoc_union (as1,(key,l2)::as2) = case assoc (as1,key) of
+ Some(l1) => assoc_union (overwrite(as1,(key,l1 union l2)),as2)
+ | None => assoc_union ((key,l2)::as1,as2);
+
+
+fun trcl r =
+ let val r' = transitive_closure r
+ in if exists (op mem) r' then error("Cyclic class structure!") else r' end;
+
+
+(* 'merge_coreg' builds the union of two 'coreg' lists;
+ it only checks the two restriction conditions and inserts afterwards
+ all elements of the second list into the first one *)
+
+fun merge_coreg classes subclass1 =
+ let fun test_ar classes (t,ars1) (coreg1,(s,w)) =
+ (is_unique_decl coreg1 (t,(s,w));
+ restr2 classes (subclass1,coreg1) (t,(s,w));
+ overwrite (coreg1,(t,(s,w) ins ars1)));
+
+ fun merge_c (coreg1,(c as (t,ars2))) = case assoc (coreg1,t) of
+ Some(ars1) => foldl (test_ar classes (t,ars1)) (coreg1,ars2)
+ | None => c::coreg1
+ in foldl merge_c end;
+
+fun merge_args(args,(t,n)) = case assoc(args,t) of
+ Some(m) => if m=n then args else varying_decls(t)
+ | None => (t,n)::args;
+
+(* 'merge' takes the above declared functions to merge two type signatures *)
+
+fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1,
+ coreg=coreg1},
+ TySg{classes=classes2,default=default2,subclass=subclass2,args=args2,
+ coreg=coreg2}) =
+ let val classes' = classes1 union classes2;
+ val subclass' = trcl (assoc_union (subclass1,subclass2));
+ val args' = foldl merge_args (args1,args2)
+ val coreg' = merge_coreg classes' subclass' (coreg1,coreg2);
+ val default' = min_sort subclass' (default1 @ default2)
+ in TySg{classes=classes' , default=default',subclass=subclass', args=args',
+ coreg=coreg'}
+ end;
+
+(**** TYPE INFERENCE ****)
+
+(*
+
+Input:
+- a 'raw' term which contains only dummy types and some explicit type
+ constraints encoded as terms.
+- the expected type of the term.
+
+Output:
+- the correctly typed term
+- the substitution needed to unify the actual type of the term with its
+ expected type; only the TVars in the expected type are included.
+
+During type inference all TVars in the term have negative index. This keeps
+them apart from normal TVars, which is essential, because at the end the type
+of the term is unified with the expected type, which contains normal TVars.
+
+1. Add initial type information to the term (add_types).
+ This freezes (freeze_vars) TVars in explicitly provided types (eg
+ constraints or defaults) by turning them into TFrees.
+2. Carry out type inference, possibly introducing new negative TVars.
+3. Unify actual and expected type.
+4. Turn all (negative) TVars into unique new TFrees (freeze).
+5. Thaw all TVars frozen in step 1 (thaw_vars).
+
+*)
+
+(*Raised if types are not unifiable*)
+exception TUNIFY;
+
+val tyvar_count = ref(~1);
+
+fun tyinit() = (tyvar_count := ~1);
+
+fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
+
+(*
+Generate new TVar. Index is < ~1 to distinguish it from TVars generated from
+variable names (see id_type). Name is arbitrary because index is new.
+*)
+
+fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S);
+fun new_id_type(a) = TVar(("'"^a, new_tvar_inx()),[]);
+
+(*Occurs check: type variable occurs in type?*)
+fun occ v tye =
+ let fun occ(Type(_,Ts)) = exists occ Ts
+ | occ(TFree _) = false
+ | occ(TVar(w,_)) = v=w orelse
+ (case assoc(tye,w) of
+ None => false
+ | Some U => occ U);
+ in occ end;
+
+(*Chase variable assignments in tye.
+ If devar (T,tye) returns a type var then it must be unassigned.*)
+fun devar (T as TVar(v,_), tye) = (case assoc(tye,v) of
+ Some U => devar (U,tye)
+ | None => T)
+ | devar (T,tye) = T;
+
+
+(* 'dom' returns for a type constructor t the list of those domains
+ which deliver a given range class C *)
+
+fun dom coreg t C = case assoc2 (coreg, (t,C)) of
+ Some(Ss) => Ss
+ | None => raise TUNIFY;
+
+
+(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
+ (i.e. a set of range classes ); the union is carried out elementwise
+ for the seperate sorts in the domains *)
+
+fun Dom (subclass,coreg) (t,S) =
+ let val domlist = map (dom coreg t) S;
+ in if null domlist then []
+ else foldl (elementwise_union subclass) (hd domlist,tl domlist)
+ end;
+
+
+fun W ((T,S),tsig as TySg{subclass,coreg,...},tye) =
+ let fun Wd ((T,S),tye) = W ((devar (T,tye),S),tsig,tye)
+ fun Wk(T as TVar(v,S')) =
+ if sortorder subclass (S',S) then tye
+ else (v,gen_tyvar(union_sort subclass (S',S)))::tye
+ | Wk(T as TFree(v,S')) = if sortorder subclass (S',S) then tye
+ else raise TUNIFY
+ | Wk(T as Type(f,Ts)) =
+ if null S then tye
+ else foldr Wd (Ts~~(Dom (subclass,coreg) (f,S)) ,tye)
+ in Wk(T) end;
+
+
+(* Order-sorted Unification of Types (U) *)
+
+
+(* Precondition: both types are well-formed w.r.t. type constructor arities *)
+fun unify (tsig as TySg{subclass,coreg,...}) =
+ let fun unif ((T,U),tye) =
+ case (devar(T,tye), devar(U,tye)) of
+ (T as TVar(v,S1), U as TVar(w,S2)) =>
+ if v=w then tye else
+ if sortorder subclass (S1,S2) then (w,T)::tye else
+ if sortorder subclass (S2,S1) then (v,U)::tye
+ else let val nu = gen_tyvar (union_sort subclass (S1,S2))
+ in (v,nu)::(w,nu)::tye end
+ | (T as TVar(v,S), U) =>
+ if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
+ | (U, T as TVar (v,S)) =>
+ if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
+ | (Type(a,Ts),Type(b,Us)) =>
+ if a<>b then raise TUNIFY else foldr unif (Ts~~Us,tye)
+ | (T,U) => if T=U then tye else raise TUNIFY
+ in unif end;
+
+(*Instantiation of type variables in types*)
+(*Pre: instantiations obey restrictions! *)
+fun inst_typ tye =
+ let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
+ | inst(T as TFree _) = T
+ | inst(T as TVar(v,_)) =
+ (case assoc(tye,v) of Some U => inst U | None => T)
+ in inst end;
+
+(*Type inference for polymorphic term*)
+fun infer tsig =
+ let fun inf(Ts, Const (_,T), tye) = (T,tye)
+ | inf(Ts, Free (_,T), tye) = (T,tye)
+ | inf(Ts, Bound i, tye) = ((nth_elem(i,Ts) , tye)
+ handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
+ | inf(Ts, Var (_,T), tye) = (T,tye)
+ | inf(Ts, Abs (_,T,body), tye) =
+ let val (U,tye') = inf(T::Ts, body, tye) in (T-->U, tye') end
+ | inf(Ts, f$u, tye) =
+ let val (U,tyeU) = inf(Ts, u, tye);
+ val (T,tyeT) = inf(Ts, f, tyeU);
+ fun err s =
+ raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
+ in case T of
+ Type("fun",[T1,T2]) =>
+ ( (T2, unify tsig ((T1,U), tyeT))
+ handle TUNIFY => err"type mismatch in application" )
+ | TVar _ =>
+ let val T2 = gen_tyvar([])
+ in (T2, unify tsig ((T, U-->T2), tyeT))
+ handle TUNIFY => err"type mismatch in application"
+ end
+ | _ => err"rator must have function type"
+ end
+ in inf end;
+
+fun freeze_vars(Type(a,Ts)) = Type(a,map freeze_vars Ts)
+ | freeze_vars(T as TFree _) = T
+ | freeze_vars(TVar(v,S)) = TFree(Syntax.string_of_vname v, S);
+
+(* Attach a type to a constant *)
+fun type_const (a,T) = Const(a, incr_tvar (new_tvar_inx()) T);
+
+(*Find type of ident. If not in table then use ident's name for tyvar
+ to get consistent typing.*)
+fun type_of_ixn(types,ixn as (a,_)) =
+ case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
+
+fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term;
+fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body);
+
+(*
+
+Attach types to a term. Input is a "parse tree" containing dummy types.
+Type constraints are translated and checked for validity wrt tsig.
+TVars in constraints are frozen.
+
+The atoms in the resulting term satisfy the following spec:
+
+Const(a,T):
+ T is a renamed copy of the generic type of a; renaming decreases index of
+ all TVars by new_tvar_inx(), which is less than ~1. The index of all TVars
+ in the generic type must be 0 for this to work!
+
+Free(a,T), Var(ixn,T):
+ T is either the frozen default type of a or TVar(("'"^a,~1),[])
+
+Abs(a,T,_):
+ T is either a type constraint or TVar(("'"^a,i),[]), where i is generated
+ by new_tvar_inx(). Thus different abstractions can have the bound variables
+ of the same name but different types.
+
+*)
+
+fun add_types (tsig, const_tab, types, sorts, string_of_typ) =
+ let val S0 = defaultS tsig;
+ fun defS0 ixn = case sorts ixn of Some S => S | None => S0;
+ fun prepareT(typ) =
+ let val T = Syntax.typ_of_term defS0 typ;
+ val T' = freeze_vars T
+ in case type_errors (tsig,string_of_typ) (T,[]) of
+ [] => T'
+ | errs => raise TYPE(cat_lines errs,[T],[])
+ end
+ fun add (Const(a,_)) =
+ (case Symtab.lookup(const_tab, a) of
+ Some T => type_const(a,T)
+ | None => raise TYPE ("No such constant: "^a, [], []))
+ | add (Bound i) = Bound i
+ | add (Free(a,_)) =
+ (case Symtab.lookup(const_tab, a) of
+ Some T => type_const(a,T)
+ | None => Free(a, type_of_ixn(types,(a,~1))))
+ | add (Var(ixn,_)) = Var(ixn, type_of_ixn(types,ixn))
+ | add (Abs(a,_,body)) = Abs(a, new_id_type a, add body)
+ | add ((f as Const(a,_)$t1)$t2) =
+ if a=Syntax.constrainC then constrain(add t1,prepareT t2) else
+ if a=Syntax.constrainAbsC then constrainAbs(add t1,prepareT t2)
+ else add f $ add t2
+ | add (f$t) = add f $ add t
+ in add end;
+
+
+(* Post-Processing *)
+
+
+(*Instantiation of type variables in terms*)
+fun inst_types tye = map_term_types (inst_typ tye);
+
+(*Delete explicit constraints -- occurrences of "_constrain" *)
+fun unconstrain (Abs(a,T,t)) = Abs(a, T, unconstrain t)
+ | unconstrain ((f as Const(a,_)) $ t) =
+ if a=Syntax.constrainC then unconstrain t
+ else unconstrain f $ unconstrain t
+ | unconstrain (f$t) = unconstrain f $ unconstrain t
+ | unconstrain (t) = t;
+
+
+(* Turn all TVars which satisfy p into new TFrees *)
+fun freeze p t =
+ let val fs = add_term_tfree_names(t,[]);
+ val inxs = filter p (add_term_tvar_ixns(t,[]));
+ val vmap = inxs ~~ variantlist(map #1 inxs, fs);
+ fun free(Type(a,Ts)) = Type(a, map free Ts)
+ | free(T as TVar(v,S)) =
+ (case assoc(vmap,v) of None => T | Some(a) => TFree(a,S))
+ | free(T as TFree _) = T
+ in map_term_types free t end;
+
+(* Thaw all TVars that were frozen in freeze_vars *)
+fun thaw_vars(Type(a,Ts)) = Type(a, map thaw_vars Ts)
+ | thaw_vars(T as TFree(a,S)) = (case explode a of
+ "?"::"'"::vn => let val ((b,i),_) = Syntax.scan_varname vn
+ in TVar(("'"^b,i),S) end
+ | _ => T)
+ | thaw_vars(T) = T;
+
+
+fun restrict tye =
+ let fun clean(tye1, ((a,i),T)) =
+ if i < 0 then tye1 else ((a,i),inst_typ tye T) :: tye1
+ in foldl clean ([],tye) end
+
+
+(*Infer types for term t using tables. Check that t's type and T unify *)
+
+fun infer_term (tsig, const_tab, types, sorts, string_of_typ, T, t) =
+ let val u = add_types (tsig, const_tab, types, sorts, string_of_typ) t;
+ val (U,tye) = infer tsig ([], u, []);
+ val uu = unconstrain u;
+ val tye' = unify tsig ((T,U),tye) handle TUNIFY => raise TYPE
+ ("Term does not have expected type", [T, U], [inst_types tye uu])
+ val Ttye = restrict tye' (* restriction to TVars in T *)
+ val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
+ (* all is a dummy term which contains all exported TVars *)
+ val Const(_,Type(_,Ts)) $ u'' =
+ map_term_types thaw_vars (freeze (fn (_,i) => i<0) all)
+ (* turn all internally generated TVars into TFrees
+ and thaw all initially frozen TVars *)
+ in (u'', (map fst Ttye) ~~ Ts) end;
+
+fun infer_types args = (tyinit(); infer_term args);
+
+
+(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
+fun varifyT(Type(a,Ts)) = Type(a,map varifyT Ts)
+ | varifyT(TFree(a,S)) = TVar((a,0),S)
+ | varifyT(T) = T;
+
+(* Turn TFrees except those in fixed into new TVars *)
+fun varify(t,fixed) =
+ let val fs = add_term_tfree_names(t,[]) \\ fixed;
+ val ixns = add_term_tvar_ixns(t,[]);
+ val fmap = fs ~~ variantlist(fs, map #1 ixns)
+ fun thaw(Type(a,Ts)) = Type(a, map thaw Ts)
+ | thaw(T as TVar _) = T
+ | thaw(T as TFree(a,S)) =
+ (case assoc(fmap,a) of None => T | Some b => TVar((b,0),S))
+ in map_term_types thaw t end;
+
+
+end;