# HG changeset patch # User wenzelm # Date 861207946 -7200 # Node ID 557a113109884b3da36b9235e3a084f883cd9d59 # Parent f3b5af1c5a6788c4c35e6dd0cd170c53d1824f32 moved classes / sorts to sorts.ML; moved (and reimplemented) type inference to type_infer.ML; cleaned up type unification; misc cleanup and tuning; diff -r f3b5af1c5a67 -r 557a11310988 src/Pure/type.ML --- 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;