# HG changeset patch # User paulson # Date 818415348 -3600 # Node ID 1b4ae50e0e0a336cd09f838c445c334e26995aab # Parent 893e8d93a54c9c4ff331731a5fccf3f9c73dd0d8 infer_types now takes a term list and a type list as argument. It is defined using the new function infer_terms. Error messages and comments also improved. diff -r 893e8d93a54c -r 1b4ae50e0e0a src/Pure/type.ML --- a/src/Pure/type.ML Fri Dec 08 10:25:26 1995 +0100 +++ b/src/Pure/type.ML Fri Dec 08 10:35:48 1995 +0100 @@ -46,8 +46,8 @@ val freeze_vars: typ -> typ val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) * (indexname -> sort option) * - string list * bool * typ * term - -> term * (indexname * typ) list + string list * bool * typ list * term list + -> term list * (indexname * typ) list val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term val thaw_vars: typ -> typ val typ_errors: type_sig -> typ * string list -> string list @@ -902,16 +902,17 @@ val (T, tyeT) = inf(Ts, f, tyeU); fun err s = raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u]) + val msg = "function type is incompatible with argument type" in case T of Type("fun", [T1, T2]) => ( (T2, unify tsig ((T1, U), tyeT)) - handle TUNIFY => err"type mismatch in application" ) + handle TUNIFY => err msg) | TVar _ => let val T2 = gen_tyvar([]) in (T2, unify tsig ((T, U-->T2), tyeT)) - handle TUNIFY => err"type mismatch in application" + handle TUNIFY => err msg end - | _ => err"rator must have function type" + | _ => err"function type is expected in application" end in inf end; @@ -1044,27 +1045,30 @@ in foldl clean ([], tye) end -(*Infer types for term t using tables. Check that t's type and T unify *) -(*freeze determines if internal TVars are turned into TFrees or TVars*) -fun infer_term (tsig, const_type, types, sorts, used, freeze, T, t) = +(*Infer types for terms. Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that + the type of ti unifies with Ti (i=1,...,n). + types is a partial map from indexnames to types (constrains Free, Var). + sorts is a partial map from indexnames to sorts (constrains TFree, TVar). + used is the list of already used type variables. + If freeze then internal TVars are turned into TFrees, else TVars.*) +fun infer_terms (tsig, const_type, types, sorts, used, freeze, Ts, ts) = let - val u = attach_types (tsig, const_type, types, sorts) t; - val (U, tye) = infer tsig ([], u, []); + val us = map (attach_types (tsig, const_type, types, sorts)) ts; + val u = list_comb(Const("",Ts ---> propT),us) + val (_, 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) + val Ttye = restrict tye (*restriction to TVars in Ts*) + 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'' = + val Const(_, Type(_, Us)) $ u'' = map_term_types thaw_vars (convert used freeze (fn (_, i) => i < 0) all) (*convert all internally generated TVars into TFrees or TVars and thaw all initially frozen TVars*) in - (u'', (map fst Ttye) ~~ Ts) + (snd(strip_comb u''), (map fst Ttye) ~~ Us) end; -fun infer_types args = (tyinit (); infer_term args); +fun infer_types args = (tyinit (); infer_terms args); end;