--- a/src/Pure/type.ML Wed Apr 16 18:23:25 1997 +0200
+++ b/src/Pure/type.ML Wed Apr 16 18:25:46 1997 +0200
@@ -2,70 +2,78 @@
ID: $Id$
Author: Tobias Nipkow & Lawrence C Paulson
-Type classes and sorts. Type signatures. Type unification and inference.
-
-TODO:
- improve nonempty_sort!
- move type unification and inference to type_unify.ML (TypeUnify) (?)
+Type signatures, unification of types, interface to type inference.
*)
signature TYPE =
- sig
- exception TUNIFY
- exception TYPE_MATCH
+sig
+ (*TFrees vs TVars*)
val no_tvars: typ -> typ
val varifyT: typ -> typ
val unvarifyT: typ -> typ
val varify: term * string list -> term
- val str_of_sort: sort -> string
- val str_of_arity: string * sort list * sort -> string
+ val freeze_vars: typ -> typ
+ val thaw_vars: typ -> typ
+ val freeze: term -> term
+
+ (*type signatures*)
type type_sig
val rep_tsig: type_sig ->
{classes: class list,
- subclass: (class * class list) list,
+ classrel: (class * class list) list,
default: sort,
tycons: (string * int) list,
abbrs: (string * (string list * typ)) list,
arities: (string * (class * sort list) list) list}
val defaultS: type_sig -> sort
+ val logical_types: type_sig -> string list
+
+ val subsort: type_sig -> sort * sort -> bool
+ val eq_sort: type_sig -> sort * sort -> bool
+ val norm_sort: type_sig -> sort -> sort
+ val nonempty_sort: type_sig -> sort list -> sort -> bool
+ val rem_sorts: typ -> typ
+
val tsig0: type_sig
- val logical_types: type_sig -> string list
val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
- val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
+ val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
val ext_tsig_defsort: type_sig -> sort -> type_sig
val ext_tsig_types: type_sig -> (string * int) list -> type_sig
val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
val merge_tsigs: type_sig * type_sig -> type_sig
- val subsort: type_sig -> sort * sort -> bool
- val norm_sort: type_sig -> sort -> sort
- val eq_sort: type_sig -> sort * sort -> bool
- val rem_sorts: typ -> typ
- val nonempty_sort: type_sig -> sort list -> sort -> bool
+
+ val typ_errors: type_sig -> typ * string list -> string list
val cert_typ: type_sig -> typ -> typ
val norm_typ: type_sig -> typ -> typ
- val freeze: term -> term
- val freeze_vars: typ -> typ
- val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
- -> indexname -> sort
- val infer_types: type_sig * (string -> typ option) *
- (indexname -> typ option) * (indexname -> sort option) *
- 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
- val typ_instance: type_sig * typ * typ -> bool
+
+ (*type matching*)
+ exception TYPE_MATCH
val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
-> (indexname * typ) list
+ val typ_instance: type_sig * typ * typ -> bool
+
+ (*type unification*)
+ exception TUNIFY
val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
-> (indexname * typ) list * int
val raw_unify: typ * typ -> bool
- end;
-structure Type : TYPE =
+ (*type inference*)
+ val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
+ -> indexname -> sort
+ val constrain: term -> typ -> term
+ val infer_types: type_sig * (string -> typ option) * (indexname -> typ option)
+ * (indexname -> sort option) * string list * bool * typ list * term list
+ -> term list * (indexname * typ) list
+end;
+
+structure Type: TYPE =
struct
+
(*** TFrees vs TVars ***)
(*disallow TVars*)
@@ -73,93 +81,146 @@
if null (typ_tvars T) then T
else raise_type "Illegal schematic type variable(s)" [T] [];
-(*turn TFrees into TVars to allow types & axioms to be written without "?"*)
-val varifyT = map_type_tfree (fn (a, S) => TVar((a, 0), S));
+(* varify, unvarify *)
-(*inverse of varifyT*)
+val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
+
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
| unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
| unvarifyT 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(f as (a,S)) = case assoc (fmap, a) of
- None => TFree(f)
- | Some b => TVar((b, 0), S)
- in map_term_types (map_type_tfree thaw) t end;
+ fun thaw (f as (a, S)) =
+ (case assoc (fmap, a) of
+ None => TFree f
+ | Some b => TVar ((b, 0), S));
+ in
+ map_term_types (map_type_tfree thaw) t
+ end;
+
+
+(* thaw, freeze *)
+val thaw_vars =
+ let
+ fun thaw (f as (a, S)) =
+ (case explode a of
+ "?" :: "'" :: vn =>
+ let val ((b, i), _) = Syntax.scan_varname vn in
+ TVar (("'" ^ b, i), S)
+ end
+ | _ => TFree f)
+ in map_type_tfree thaw end;
+
+val freeze_vars =
+ map_type_tvar (fn (v, S) => TFree (Syntax.string_of_vname v, S));
-(*** type classes and sorts ***)
-
-(*
- Classes denote (possibly empty) collections of types (e.g. sets of types)
- and are partially ordered by 'inclusion'. They are represented by strings.
+local
+ fun nextname (pref, c) =
+ if c = "z" then (pref ^ "a", "a")
+ else (pref, chr (ord c + 1));
- Sorts are intersections of finitely many classes. They are represented by
- lists of classes.
-*)
-
-type domain = sort list;
+ fun newtvars used =
+ let
+ fun new ([], _, vmap) = vmap
+ | new (ixn :: ixns, p as (pref, c), vmap) =
+ let val nm = pref ^ c in
+ if nm mem_string used then new (ixn :: ixns, nextname p, vmap)
+ else new (ixns, nextname p, (ixn, nm) :: vmap)
+ end
+ in new end;
-
-(* print sorts and arities *)
-
-fun str_of_sort [c] = c
- | str_of_sort cs = enclose "{" "}" (commas cs);
+ (*Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
+ Note that if t contains frozen TVars there is the possibility that a TVar is
+ turned into one of those. This is sound but not complete.*)
-fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
-
-fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
- | str_of_arity (t, SS, S) =
- t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
+ fun convert used freeze p t =
+ let
+ val used =
+ if freeze then add_term_tfree_names (t, used)
+ else used union (map #1 (filter_out p (add_term_tvar_ixns (t, []))));
+ val ixns = filter p (add_term_tvar_ixns (t, []));
+ val vmap = newtvars used (ixns, ("'", "a"), []);
+ fun conv (var as (ixn, S)) =
+ (case assoc (vmap, ixn) of
+ None => TVar(var)
+ | Some a => if freeze then TFree (a, S) else TVar ((a, 0), S));
+ in
+ map_term_types (map_type_tvar conv) t
+ end;
+in
+ fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
+end;
(*** type signatures ***)
+(* type type_sig *)
+
(*
classes:
- a list of all declared classes;
+ list of all declared classes;
- subclass:
- an association list representing the subclass relation; (c, cs) is
- interpreted as "c is a proper subclass of all elemenst of cs"; note that
- c itself is not a member of cs;
+ classrel:
+ (see Pure/sorts.ML)
default:
- the default sort attached to all unconstrained type vars;
+ default sort attached to all unconstrained type vars;
tycons:
- an association list of all declared types with the number of their
+ association list of all declared types with the number of their
arguments;
abbrs:
- an association list of type abbreviations;
+ association list of type abbreviations;
arities:
- 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;
+ (see Pure/sorts.ML)
*)
datatype type_sig =
TySg of {
classes: class list,
- subclass: (class * class list) list,
+ classrel: (class * class list) list,
default: sort,
tycons: (string * int) list,
abbrs: (string * (string list * typ)) list,
- arities: (string * (class * domain) list) list};
+ arities: (string * (class * sort list) list) list};
fun rep_tsig (TySg comps) = comps;
fun defaultS (TySg {default, ...}) = default;
+fun logical_types (TySg {classrel, arities, tycons, ...}) =
+ let
+ fun log_class c = Sorts.class_le classrel (c, logicC);
+ fun log_type t = exists (log_class o #1) (assocs arities t);
+ in
+ filter log_type (map #1 tycons)
+ end;
+
+
+(* sorts *)
+
+(* FIXME declared!? *)
+
+fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
+fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
+fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
+
+fun nonempty_sort (tsig as TySg {classrel, arities, ...}) hyps S =
+ Sorts.nonempty_sort classrel arities hyps S;
+
+fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
+ | rem_sorts (TFree (x, _)) = TFree (x, [])
+ | rem_sorts (TVar (xi, _)) = TVar (xi, []);
+
(* error messages *)
@@ -183,8 +244,9 @@
fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
+(* FIXME err_undcl_class! *)
(* 'leq' checks the partial order on classes according to the
- statements in the association list 'a' (i.e. 'subclass')
+ statements in the association list 'a' (i.e. 'classrel')
*)
fun less a (C, D) = case assoc (a, C) of
@@ -194,102 +256,8 @@
fun leq a (C, D) = C = D orelse less a (C, D);
-(* logical_types *)
-(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
- and c <= logic*)
-
-fun logical_types tsig =
- let
- val TySg {subclass, arities, tycons, ...} = tsig;
-
- fun log_class c = leq subclass (c, logicC);
- fun log_type t = exists (log_class o #1) (assocs arities t);
- in
- filter log_type (map #1 tycons)
- 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 *)
-(* FIXME rename to inter_sort (?) *)
-
-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) = ListPair.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) = ListPair.all (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;
-
-
-
+(* FIXME *)
(*Instantiation of type variables in types*)
(*Pre: instantiations obey restrictions! *)
fun inst_typ tye =
@@ -298,25 +266,10 @@
| None => TVar(var)
in map_type_tvar inst end;
-(* '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 'arities' of the
- given type signature *)
-fun least_sort (tsig as TySg{subclass, arities, ...}) =
- let fun ls(T as Type(a, Ts)) =
- (case assoc (arities, a) of
- Some(ars) => cod_above(subclass, map ls Ts, ars)
- | None => raise TYPE(undcl_type a, [T], []))
- | ls(TFree(a, S)) = S
- | ls(TVar(a, S)) = S
- in ls end;
-
-
-fun check_has_sort(tsig as TySg{subclass, arities, ...}, T, S) =
- if sortorder subclass ((least_sort tsig T), S) then ()
- else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
+fun check_has_sort (TySg {classrel, arities, ...}, T, S) =
+ if Sorts.sort_le classrel ((Sorts.least_sort classrel arities T), S) then ()
+ else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
(*Instantiation of type variables in types *)
@@ -348,66 +301,18 @@
end;
-(** type matching **)
-
-exception TYPE_MATCH;
-
-(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
-fun typ_match tsig =
- let
- fun match (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)
- | match (subs, (Type (a, Ts), Type (b, Us))) =
- if a <> b then raise TYPE_MATCH
- else foldl match (subs, Ts ~~ Us)
- | match (subs, (TFree x, TFree y)) =
- if x = y then subs else raise TYPE_MATCH
- | match _ = raise TYPE_MATCH;
- in match end;
-
-
-fun typ_instance (tsig, T, U) =
- (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
(** build type signatures **)
-fun make_tsig (classes, subclass, default, tycons, abbrs, arities) =
- TySg {classes = classes, subclass = subclass, default = default,
+fun make_tsig (classes, classrel, default, tycons, abbrs, arities) =
+ TySg {classes = classes, classrel = classrel, default = default,
tycons = tycons, abbrs = abbrs, arities = arities};
val tsig0 = make_tsig ([], [], [], [], [], []);
-(* sorts *)
-
-fun subsort (TySg {subclass, ...}) (S1, S2) =
- sortorder subclass (S1, S2);
-
-fun norm_sort (TySg {subclass, ...}) S =
- sort_strings (min_sort subclass S);
-
-(* FIXME tmp! (sorts.ML) *)
-fun eq_sort tsig (S1, S2) =
- norm_sort tsig S1 = norm_sort tsig S2;
-
-fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
- | rem_sorts (TFree (x, _)) = TFree (x, [])
- | rem_sorts (TVar (xi, _)) = TVar (xi, []);
-
-
-(* nonempty_sort *)
-
-(* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
-fun nonempty_sort _ _ [] = true
- | nonempty_sort (tsig as TySg {arities, ...}) hyps S =
- exists (exists (fn (c, ss) => [c] = S andalso null ss) o snd) arities
- orelse exists (fn S' => subsort tsig (S', S)) hyps;
-
(* typ_errors *)
@@ -450,12 +355,11 @@
(* cert_typ *)
-(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
-
-fun cert_typ tsig ty =
- (case typ_errors tsig (ty, []) of
- [] => norm_typ tsig ty
- | errs => raise_type (cat_lines errs) [ty] []);
+(*check and normalize typ wrt. tsig*) (*exception TYPE*)
+fun cert_typ tsig T =
+ (case typ_errors tsig (T, []) of
+ [] => norm_typ tsig T
+ | errs => raise_type (cat_lines errs) [T] []);
@@ -467,19 +371,19 @@
fun assoc_union (as1, []) = as1
| assoc_union (as1, (key, l2) :: as2) =
(case assoc_string (as1, key) of
- Some l1 => assoc_union
- (overwrite (as1, (key, l1 union_string l2)), as2)
+ Some l1 => assoc_union
+ (overwrite (as1, (key, l1 union_string l2)), as2)
| None => assoc_union ((key, l2) :: as1, as2));
-(* merge subclass *)
+(* merge classrel *)
-fun merge_subclass (subclass1, subclass2) =
- let val subclass = transitive_closure (assoc_union (subclass1, subclass2))
+fun merge_classrel (classrel1, classrel2) =
+ let val classrel = transitive_closure (assoc_union (classrel1, classrel2))
in
- if exists (op mem_string) subclass then
+ if exists (op mem_string) classrel then
error ("Cyclic class structure!") (* FIXME improve msg, raise TERM *)
- else subclass
+ else classrel
end;
@@ -490,8 +394,8 @@
fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
Some(w1) => if w = w1 then () else
error("There are two declarations\n" ^
- str_of_arity(t, w, [C]) ^ " and\n" ^
- str_of_arity(t, w1, [C]) ^ "\n" ^
+ Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
+ Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
"with the same result class.")
| None => ();
@@ -499,19 +403,21 @@
such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
fun coreg_err(t, (C1,w1), (C2,w2)) =
- error("Declarations " ^ str_of_arity(t, w1, [C1]) ^ " and "
- ^ str_of_arity(t, w2, [C2]) ^ " are in conflict");
+ error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
+ ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");
-fun coreg subclass (t, Cw1) =
- let fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
- if leq subclass (C1,C2)
- then if lew subclass (w1,w2) then () else coreg_err(t, Cw1, Cw2)
- else ()
- fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
+fun coreg classrel (t, Cw1) =
+ let
+ fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
+ if leq classrel (C1,C2) then
+ if Sorts.sorts_le classrel (w1,w2) then ()
+ else coreg_err(t, Cw1, Cw2)
+ else ()
+ fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
in seq check end;
-fun add_arity subclass ars (tCw as (_,Cw)) =
- (is_unique_decl ars tCw; coreg subclass tCw ars; Cw ins ars);
+fun add_arity classrel ars (tCw as (_,Cw)) =
+ (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
fun varying_decls t =
error ("Type constructor " ^ quote t ^ " has varying number of arguments");
@@ -521,8 +427,8 @@
it only checks the two restriction conditions and inserts afterwards
all elements of the second list into the first one *)
-fun merge_arities subclass =
- let fun test_ar t (ars1, sw) = add_arity subclass ars1 (t,sw);
+fun merge_arities classrel =
+ let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
Some(ars1) =>
@@ -547,23 +453,23 @@
(* 'merge_tsigs' takes the above declared functions to merge two type
signatures *)
-fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1,
+fun merge_tsigs(TySg{classes=classes1, default=default1, classrel=classrel1,
tycons=tycons1, arities=arities1, abbrs=abbrs1},
- TySg{classes=classes2, default=default2, subclass=subclass2,
+ TySg{classes=classes2, default=default2, classrel=classrel2,
tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
let val classes' = classes1 union_string classes2;
- val subclass' = merge_subclass (subclass1, subclass2);
+ val classrel' = merge_classrel (classrel1, classrel2);
val tycons' = foldl add_tycons (tycons1, tycons2)
- val arities' = merge_arities subclass' (arities1, arities2);
- val default' = min_sort subclass' (default1 @ default2);
+ val arities' = merge_arities classrel' (arities1, arities2);
+ val default' = Sorts.norm_sort classrel' (default1 @ default2);
val abbrs' = merge_abbrs(abbrs1, abbrs2);
- in make_tsig(classes', subclass', default', tycons', abbrs', arities') end;
+ in make_tsig(classes', classrel', default', tycons', abbrs', arities') end;
(*** extend type signatures ***)
-(** add classes and subclass relations**)
+(** add classes and classrel relations **)
fun add_classes classes cs =
(case cs inter_string classes of
@@ -571,74 +477,74 @@
| dups => err_dup_classes cs);
-(*'add_subclass' adds a tuple consisting of a new class (the new class has
+(*'add_classrel' adds a tuple consisting 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
+ must be declared in 'classes' too) to the 'classrel' 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)) =
+fun add_classrel classes (classrel, (s, ges)) =
let
- fun upd (subclass, s') =
+ fun upd (classrel, s') =
if s' mem_string classes then
- let val ges' = the (assoc (subclass, s))
- in case assoc (subclass, s') of
+ let val ges' = the (assoc (classrel, s))
+ in case assoc (classrel, s') of
Some sups => if s mem_string sups
then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
- else overwrite
- (subclass, (s, sups union_string ges'))
- | None => subclass
+ else overwrite
+ (classrel, (s, sups union_string ges'))
+ | None => classrel
end
else err_undcl_class s'
- in foldl upd (subclass @ [(s, ges)], ges) end;
+ in foldl upd (classrel @ [(s, ges)], ges) end;
(* 'extend_classes' inserts all new classes into the corresponding
- lists ('classes', 'subclass') if possible *)
+ lists ('classes', 'classrel') if possible *)
-fun extend_classes (classes, subclass, new_classes) =
+fun extend_classes (classes, classrel, new_classes) =
let
val classes' = add_classes classes (map fst new_classes);
- val subclass' = foldl (add_subclass classes') (subclass, new_classes);
- in (classes', subclass') end;
+ val classrel' = foldl (add_classrel classes') (classrel, new_classes);
+ in (classes', classrel') end;
(* ext_tsig_classes *)
fun ext_tsig_classes tsig new_classes =
let
- val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
- val (classes',subclass') = extend_classes (classes,subclass,new_classes);
+ val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
+ val (classes',classrel') = extend_classes (classes,classrel,new_classes);
in
- make_tsig (classes', subclass', default, tycons, abbrs, arities)
+ make_tsig (classes', classrel', default, tycons, abbrs, arities)
end;
-(* ext_tsig_subclass *)
+(* ext_tsig_classrel *)
-fun ext_tsig_subclass tsig pairs =
+fun ext_tsig_classrel tsig pairs =
let
- val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
+ val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
(* FIXME clean! *)
- val subclass' =
- merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
+ val classrel' =
+ merge_classrel (classrel, map (fn (c1, c2) => (c1, [c2])) pairs);
in
- make_tsig (classes, subclass', default, tycons, abbrs, arities)
+ make_tsig (classes, classrel', default, tycons, abbrs, arities)
end;
(* ext_tsig_defsort *)
-fun ext_tsig_defsort(TySg{classes,subclass,tycons,abbrs,arities,...}) default =
- make_tsig (classes, subclass, default, tycons, abbrs, arities);
+fun ext_tsig_defsort(TySg{classes,classrel,tycons,abbrs,arities,...}) default =
+ make_tsig (classes, classrel, default, tycons, abbrs, arities);
(** add types **)
-fun ext_tsig_types (TySg {classes, subclass, default, tycons, abbrs, arities}) ts =
+fun ext_tsig_types (TySg {classes, classrel, default, tycons, abbrs, arities}) ts =
let
fun check_type (c, n) =
if n < 0 then err_neg_args c
@@ -647,7 +553,7 @@
else ();
in
seq check_type ts;
- make_tsig (classes, subclass, default, ts @ tycons, abbrs,
+ make_tsig (classes, classrel, default, ts @ tycons, abbrs,
map (rpair [] o #1) ts @ arities)
end;
@@ -696,10 +602,10 @@
| msgs => err msgs)
end;
-fun add_abbr (tsig as TySg{classes,subclass,default,tycons,arities,abbrs},
+fun add_abbr (tsig as TySg{classes,classrel,default,tycons,arities,abbrs},
abbr) =
make_tsig
- (classes,subclass,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
+ (classes,classrel,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
@@ -715,14 +621,14 @@
if one type declaration has passed all checks it is inserted into
the 'arities' association list of the given type signatrure *)
-fun coregular (classes, subclass, tycons) =
+fun coregular (classes, classrel, tycons) =
let fun ex C = if C mem_string classes then () else err_undcl_class(C);
fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
Some(n) => if n <> length w then varying_decls(t) else
((seq o seq) ex w; ex C;
let val ars = the (assoc(arities, t))
- val ars' = add_arity subclass ars (t,(C,w))
+ val ars' = add_arity classrel ars (t,(C,w))
in overwrite(arities, (t,ars')) end)
| None => error (undcl_type t);
@@ -738,12 +644,12 @@
no declaration t:(Ss')D with C <=D then the declaration holds
for all range classes more general than C *)
-fun close subclass arities =
- let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
+fun close classrel arities =
+ let fun check sl (l, (s, dom)) = case assoc (classrel, s) of
Some sups =>
let fun close_sup (l, sup) =
- if exists (fn s'' => less subclass (s, s'') andalso
- leq subclass (s'', sup)) sl
+ if exists (fn s'' => less classrel (s, s'') andalso
+ leq classrel (s'', sup)) sl
then l
else (sup, dom)::l
in foldl close_sup (l, sups) end
@@ -754,200 +660,149 @@
(* ext_tsig_arities *)
+fun norm_domain classrel =
+ let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
+ in map one_min end;
+
fun ext_tsig_arities tsig sarities =
let
- val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
+ val TySg {classes, classrel, default, tycons, arities, abbrs} = tsig;
val arities1 =
- List.concat
+ List.concat
(map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
- val arities2 = foldl (coregular (classes, subclass, tycons))
- (arities, min_domain subclass arities1)
- |> close subclass;
+ val arities2 = foldl (coregular (classes, classrel, tycons))
+ (arities, norm_domain classrel arities1)
+ |> close classrel;
in
- make_tsig (classes, subclass, default, tycons, abbrs, arities2)
+ make_tsig (classes, classrel, default, tycons, abbrs, arities2)
end;
-(*** type unification and inference ***)
+(*** type unification and friends ***)
-(*
- Input:
- - a 'raw' term which contains only dummy types and some explicit type
- constraints encoded as terms.
- - the expected type of the term.
+(** matching **)
- 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.
+exception TYPE_MATCH;
- During type inference all TVars in the term have index > maxidx, where
- maxidx is the max. index in the expected type of the term (T). This keeps
- them apart, because at the end the type of the term is unified with T.
+fun typ_match tsig =
+ let
+ fun match (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)
+ | match (subs, (Type (a, Ts), Type (b, Us))) =
+ if a <> b then raise TYPE_MATCH
+ else foldl match (subs, Ts ~~ Us)
+ | match (subs, (TFree x, TFree y)) =
+ if x = y then subs else raise TYPE_MATCH
+ | match _ = raise TYPE_MATCH;
+ in match end;
- 1. Add initial type information to the term (attach_types).
- This freezes (freeze_vars) TVars in explicitly provided types (eg
- constraints or defaults) by turning them into TFrees.
- 2. Carry out type inference.
- 3. Unify actual and expected type.
- 4. Turn all local (i.e. > maxidx) TVars into unique new TFrees (freeze).
- 5. Thaw all TVars frozen in step 1 (thaw_vars).
-*)
+fun typ_instance (tsig, T, U) =
+ (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
+
-(*Raised if types are not unifiable*)
+
+(** unification **)
+
exception TUNIFY;
-val tyvar_count = ref 0;
-fun tyinit(i) = (tyvar_count := i);
-
-fun new_tvar_inx () = (tyvar_count := !tyvar_count + 1; !tyvar_count)
+(* occurs check *)
-(*
-Generate new TVar. Index is > maxidx+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);
-
-(*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, _)) = eq_ix(v,w) orelse
- (case assoc(tye, w) of
- None => false
- | Some U => occ U);
+fun occurs v tye =
+ let
+ fun occ (Type (_, Ts)) = exists occ Ts
+ | occ (TFree _) = false
+ | occ (TVar (w, _)) =
+ eq_ix (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)
+
+(* chase variable assignments *)
+
+(*if devar 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;
-(* use add_to_tye(t,tye) instead of t::tye
-to avoid chains of the form 'a |-> 'b |-> 'c ... *)
-fun add_to_tye(p,[]) = [p]
- | add_to_tye(vT as (v,T),(xU as (x,TVar(w,S)))::ps) =
- (if eq_ix(v,w) then (x,T) else xU) :: (add_to_tye(vT,ps))
- | add_to_tye(v,x::xs) = x::(add_to_tye(v,xs));
-
-(* 'dom' returns for a type constructor t the list of those domains
- which deliver a given range class C *)
+(* add_env *)
-fun dom arities t C = case assoc2 (arities, (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 union_dom (subclass, arities) (t, S) =
- case map (dom arities t) S of
- [] => []
- | (d::ds) => foldl (elementwise_union subclass) (d,ds);
+(*avoids chains 'a |-> 'b |-> 'c ...*)
+fun add_env (p, []) = [p]
+ | add_env (vT as (v, T), (xU as (x, TVar (w, S))) :: ps) =
+ (if eq_ix (v, w) then (x, T) else xU) :: add_env (vT, ps)
+ | add_env (v, x :: xs) = x :: add_env (v, xs);
-fun W ((T, S), tsig as TySg{subclass, arities, ...}, 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 add_to_tye((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~~(union_dom (subclass, arities) (f, S)) , tye)
- in Wk(T) end;
+(* unify *)
+
+fun unify (tsig as TySg {classrel, arities, ...}) maxidx tyenv TU =
+ let
+ val tyvar_count = ref maxidx;
+ fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
+
+ fun mg_domain a S =
+ Sorts.mg_domain classrel arities a S handle TYPE _ => raise TUNIFY;
+
+ fun meet ((_, []), tye) = tye
+ | meet ((TVar (xi, S'), S), tye) =
+ if Sorts.sort_le classrel (S', S) then tye
+ else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
+ | meet ((TFree (_, S'), S), tye) =
+ if Sorts.sort_le classrel (S', S) then tye
+ else raise TUNIFY
+ | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
+ and meets (([], []), tye) = tye
+ | meets ((T :: Ts, S :: Ss), tye) =
+ meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
+ | meets _ = sys_error "meets";
+
+ fun unif ((ty1, ty2), tye) =
+ (case (devar (ty1, tye), devar (ty2, tye)) of
+ (T as TVar (v, S1), U as TVar (w, S2)) =>
+ if eq_ix (v, w) then tye
+ else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye)
+ else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye)
+ else
+ let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
+ add_env ((v, S), add_env ((w, S), tye))
+ end
+ | (TVar (v, S), T) =>
+ if occurs v tye T then raise TUNIFY
+ else meet ((T, S), add_env ((v, T), tye))
+ | (T, TVar (v, S)) =>
+ if occurs v tye T then raise TUNIFY
+ else meet ((T, S), add_env ((v, T), 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 (TU, tyenv), ! tyvar_count)
+ end;
-(* Order-sorted Unification of Types (U) *)
+(* raw_unify *)
-(* Precondition: both types are well-formed w.r.t. type constructor arities *)
-fun unify1 (tsig as TySg{subclass, arities, ...}) =
- 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 eq_ix(v,w) then tye else
- if sortorder subclass (S1, S2) then add_to_tye((w, T),tye) else
- if sortorder subclass (S2, S1) then add_to_tye((v, U),tye)
- else let val nu = gen_tyvar (union_sort subclass (S1, S2))
- in add_to_tye((v, nu),add_to_tye((w, nu),tye)) end
- | (T as TVar(v, S), U) =>
- if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((v, U),tye))
- | (U, T as TVar (v, S)) =>
- if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((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;
-
-fun unify tsig maxidx tye TU =
- (tyinit maxidx; (unify1 tsig (TU,tye), !tyvar_count) );
-
-(* raw_unify (ignores sorts) *)
-
+(*purely structural unification -- ignores sorts*)
fun raw_unify (ty1, ty2) =
(unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true)
handle TUNIFY => false;
-(*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])
- val msg = "function type is incompatible with argument type"
- in case T of
- Type("fun", [T1, T2]) =>
- ( (T2, unify1 tsig ((T1, U), tyeT))
- handle TUNIFY => err msg)
- | TVar _ =>
- let val T2 = gen_tyvar([])
- in (T2, unify1 tsig ((T, U-->T2), tyeT))
- handle TUNIFY => err msg
- end
- | _ => err"function type is expected in application"
- end
- in inf end;
-val freeze_vars =
- map_type_tvar (fn (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 new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
+(** type inference **)
-fun type_of_ixn(types, ixn as (a, _),maxidx1) =
- case types ixn of Some T => freeze_vars T
- | None => TVar(("'"^a, maxidx1), []);
-
-fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
-
-fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
- | constrainAbs _ = sys_error "constrainAbs";
-
-
-(* get_sort *)
+(* constraints *)
fun get_sort tsig def_sort env xi =
(case (assoc (env, xi), def_sort xi) of
@@ -959,137 +814,74 @@
else error ("Sort constraint inconsistent with default for type variable " ^
quote (Syntax.string_of_vname' xi)));
-
-(* attach_types *)
-
-(*
- 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 increases index of
- all TVars by new_tvar_inx(), which is > maxidx+1.
-
- Free (a, T), Var (ixn, T):
- T is either the frozen default type of a or TVar (("'"^a, maxidx+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 attach_types (tsig, const_type, types, sorts, maxidx1) tm =
- let
- val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm;
-
- fun prepareT t =
- freeze_vars (cert_typ tsig (Syntax.typ_of_term (get_sort tsig sorts sort_env) t));
-
- fun add (Const (a, _)) =
- (case const_type a of
- Some T => type_const (a, T)
- | None => raise_type ("No such constant: " ^ quote a) [] [])
- | add (Free (a, _)) =
- (case const_type a of
- Some T => type_const (a, T)
- | None => Free (a, type_of_ixn (types,(a,~1),maxidx1)))
- | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn, maxidx1))
- | add (Bound i) = Bound i
- | 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 tm end;
+fun constrain t T =
+ if T = dummyT then t
+ else Const ("_type_constraint_", T) $ t;
-(* Post-Processing *)
+(* decode_types *)
-(*Instantiation of type variables in terms*)
-fun inst_types tye = map_term_types (inst_typ tye);
+(*transform parse tree into raw term (idempotent)*)
+fun decode_types tsig is_const def_type def_sort tm =
+ let
+ fun get_type xi = if_none (def_type xi) dummyT;
+ val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm;
+
+ fun decodeT t =
+ cert_typ tsig (Syntax.typ_of_term (get_sort tsig def_sort sort_env) t);
-(*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;
+ fun decode (Const ("_constrain", _) $ t $ typ) =
+ constrain (decode t) (decodeT typ)
+ | decode (Const ("_constrainAbs", _) $ (abs as Abs (x, T, t)) $ typ) =
+ if T = dummyT then Abs (x, decodeT typ, decode t)
+ else constrain abs (decodeT typ --> dummyT)
+ | decode (Abs (x, T, t)) = Abs (x, T, decode t)
+ | decode (t $ u) = decode t $ decode u
+ | decode (t as Free (x, T)) =
+ if is_const x then Const (x, T)
+ else if T = dummyT then Free (x, get_type (x, ~1))
+ else constrain t (get_type (x, ~1))
+ | decode (t as Var (xi, T)) =
+ if T = dummyT then Var (xi, get_type xi)
+ else constrain t (get_type xi)
+ | decode (t as Bound _) = t
+ | decode (t as Const _) = t;
+ in
+ decode tm
+ end;
-fun nextname(pref,c) = if c="z" then (pref^"a", "a") else (pref,chr(ord(c)+1));
-fun newtvars used =
- let fun new([],_,vmap) = vmap
- | new(ixn::ixns,p as (pref,c),vmap) =
- let val nm = pref ^ c
- in if nm mem_string used then new(ixn::ixns,nextname p, vmap)
- else new(ixns, nextname p, (ixn,nm)::vmap)
- end
- in new end;
+(* infer_types *)
(*
-Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
-Note that if t contains frozen TVars there is the possibility that a TVar is
-turned into one of those. This is sound but not complete.
+ Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
+ unifies with Ti (for i=1,...,n).
+
+ tsig: type signature
+ const_type: term signature
+ def_type: partial map from indexnames to types (constrains Frees, Vars)
+ def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
+ used: list of already used type variables
+ freeze: if true then generated parameters are turned into TFrees, else TVars
*)
-fun convert used freeze p t =
- let val used = if freeze then add_term_tfree_names(t, used)
- else used union
- (map #1 (filter_out p (add_term_tvar_ixns(t, []))))
- val ixns = filter p (add_term_tvar_ixns(t, []));
- val vmap = newtvars used (ixns,("'","a"),[]);
- fun conv(var as (ixn,S)) = case assoc(vmap,ixn) of
- None => TVar(var) |
- Some(a) => if freeze then TFree(a,S) else TVar((a,0),S);
- in map_term_types (map_type_tvar conv) t end;
-
-fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
-
-(* Thaw all TVars that were frozen in freeze_vars *)
-val thaw_vars =
- let fun thaw(f as (a, S)) = (case explode a of
- "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
- in TVar(("'"^b, i), S) end
- | _ => TFree f)
- in map_type_tfree thaw end;
-
-fun restrict maxidx1 tye =
- let fun clean(tye1, ((a, i), T)) =
- if i >= maxidx1 then tye1 else ((a, i), inst_typ tye T) :: tye1
- in foldl clean ([], tye) end
-
+(*user-supplied inference parameters*)
+fun q_is_param (x, _) =
+ (case explode x of
+ "?" :: _ => true
+ | _ => false);
-(*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_types (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
+fun infer_types (tsig, const_type, def_type, def_sort, used, freeze, pat_Ts, raw_ts) =
let
- val maxidx1 = maxidx_of_typs Ts + 1;
- val () = tyinit(maxidx1+1);
- val us = map (attach_types (tsig, const_type, types, sorts, maxidx1)) ts;
- val u = list_comb(Const("",Ts ---> propT),us)
- val (_, tye) = infer tsig ([], u, []);
- val uu = unconstrain u;
- val Ttye = restrict maxidx1 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(_, Us)) $ u'' =
- map_term_types thaw_vars (convert used freeze (fn (_,i) => i >= maxidx1) all)
- (*convert all internally generated TVars into TFrees or TVars
- and thaw all initially frozen TVars*)
+ val TySg {classrel, arities, ...} = tsig;
+ val pat_Ts' = map (cert_typ tsig) pat_Ts;
+ val raw_ts' =
+ map (decode_types tsig (is_some o const_type) def_type def_sort) raw_ts;
+ val (ts, Ts, unifier) =
+ TypeInfer.infer_types const_type classrel arities used freeze
+ q_is_param raw_ts' pat_Ts';
in
- (#2(strip_comb u''), ListPair.zip(map #1 Ttye, Us))
+ (ts, unifier)
end;
end;