moved classes / sorts to sorts.ML;
authorwenzelm
Wed Apr 16 18:25:46 1997 +0200 (1997-04-16)
changeset 2964557a11310988
parent 2963 f3b5af1c5a67
child 2965 afbda7e26f15
moved classes / sorts to sorts.ML;
moved (and reimplemented) type inference to type_infer.ML;
cleaned up type unification;
misc cleanup and tuning;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Wed Apr 16 18:23:25 1997 +0200
     1.2 +++ b/src/Pure/type.ML	Wed Apr 16 18:25:46 1997 +0200
     1.3 @@ -2,70 +2,78 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow & Lawrence C Paulson
     1.6  
     1.7 -Type classes and sorts. Type signatures. Type unification and inference.
     1.8 -
     1.9 -TODO:
    1.10 -  improve nonempty_sort!
    1.11 -  move type unification and inference to type_unify.ML (TypeUnify) (?)
    1.12 +Type signatures, unification of types, interface to type inference.
    1.13  *)
    1.14  
    1.15  signature TYPE =
    1.16 -  sig
    1.17 -  exception TUNIFY
    1.18 -  exception TYPE_MATCH
    1.19 +sig
    1.20 +  (*TFrees vs TVars*)
    1.21    val no_tvars: typ -> typ
    1.22    val varifyT: typ -> typ
    1.23    val unvarifyT: typ -> typ
    1.24    val varify: term * string list -> term
    1.25 -  val str_of_sort: sort -> string
    1.26 -  val str_of_arity: string * sort list * sort -> string
    1.27 +  val freeze_vars: typ -> typ
    1.28 +  val thaw_vars: typ -> typ
    1.29 +  val freeze: term -> term
    1.30 +
    1.31 +  (*type signatures*)
    1.32    type type_sig
    1.33    val rep_tsig: type_sig ->
    1.34      {classes: class list,
    1.35 -     subclass: (class * class list) list,
    1.36 +     classrel: (class * class list) list,
    1.37       default: sort,
    1.38       tycons: (string * int) list,
    1.39       abbrs: (string * (string list * typ)) list,
    1.40       arities: (string * (class * sort list) list) list}
    1.41    val defaultS: type_sig -> sort
    1.42 +  val logical_types: type_sig -> string list
    1.43 +
    1.44 +  val subsort: type_sig -> sort * sort -> bool
    1.45 +  val eq_sort: type_sig -> sort * sort -> bool
    1.46 +  val norm_sort: type_sig -> sort -> sort
    1.47 +  val nonempty_sort: type_sig -> sort list -> sort -> bool
    1.48 +  val rem_sorts: typ -> typ
    1.49 +
    1.50    val tsig0: type_sig
    1.51 -  val logical_types: type_sig -> string list
    1.52    val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
    1.53 -  val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
    1.54 +  val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
    1.55    val ext_tsig_defsort: type_sig -> sort -> type_sig
    1.56    val ext_tsig_types: type_sig -> (string * int) list -> type_sig
    1.57    val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
    1.58    val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
    1.59    val merge_tsigs: type_sig * type_sig -> type_sig
    1.60 -  val subsort: type_sig -> sort * sort -> bool
    1.61 -  val norm_sort: type_sig -> sort -> sort
    1.62 -  val eq_sort: type_sig -> sort * sort -> bool
    1.63 -  val rem_sorts: typ -> typ
    1.64 -  val nonempty_sort: type_sig -> sort list -> sort -> bool
    1.65 +
    1.66 +  val typ_errors: type_sig -> typ * string list -> string list
    1.67    val cert_typ: type_sig -> typ -> typ
    1.68    val norm_typ: type_sig -> typ -> typ
    1.69 -  val freeze: term -> term
    1.70 -  val freeze_vars: typ -> typ
    1.71 -  val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
    1.72 -    -> indexname -> sort
    1.73 -  val infer_types: type_sig * (string -> typ option) *
    1.74 -                   (indexname -> typ option) * (indexname -> sort option) *
    1.75 -                   string list * bool * typ list * term list
    1.76 -                   -> term list * (indexname * typ) list
    1.77 +
    1.78    val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    1.79 -  val thaw_vars: typ -> typ
    1.80 -  val typ_errors: type_sig -> typ * string list -> string list
    1.81 -  val typ_instance: type_sig * typ * typ -> bool
    1.82 +
    1.83 +  (*type matching*)
    1.84 +  exception TYPE_MATCH
    1.85    val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
    1.86      -> (indexname * typ) list
    1.87 +  val typ_instance: type_sig * typ * typ -> bool
    1.88 +
    1.89 +  (*type unification*)
    1.90 +  exception TUNIFY
    1.91    val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
    1.92      -> (indexname * typ) list * int
    1.93    val raw_unify: typ * typ -> bool
    1.94 -  end;
    1.95  
    1.96 -structure Type : TYPE =
    1.97 +  (*type inference*)
    1.98 +  val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
    1.99 +    -> indexname -> sort
   1.100 +  val constrain: term -> typ -> term
   1.101 +  val infer_types: type_sig * (string -> typ option) * (indexname -> typ option)
   1.102 +    * (indexname -> sort option) * string list * bool * typ list * term list
   1.103 +    -> term list * (indexname * typ) list
   1.104 +end;
   1.105 +
   1.106 +structure Type: TYPE =
   1.107  struct
   1.108  
   1.109 +
   1.110  (*** TFrees vs TVars ***)
   1.111  
   1.112  (*disallow TVars*)
   1.113 @@ -73,93 +81,146 @@
   1.114    if null (typ_tvars T) then T
   1.115    else raise_type "Illegal schematic type variable(s)" [T] [];
   1.116  
   1.117 -(*turn TFrees into TVars to allow types & axioms to be written without "?"*)
   1.118 -val varifyT = map_type_tfree (fn (a, S) => TVar((a, 0), S));
   1.119 +(* varify, unvarify *)
   1.120  
   1.121 -(*inverse of varifyT*)
   1.122 +val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
   1.123 +
   1.124  fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
   1.125    | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
   1.126    | unvarifyT T = T;
   1.127  
   1.128 -(*turn TFrees except those in fixed into new TVars*)
   1.129  fun varify (t, fixed) =
   1.130    let
   1.131      val fs = add_term_tfree_names (t, []) \\ fixed;
   1.132      val ixns = add_term_tvar_ixns (t, []);
   1.133      val fmap = fs ~~ variantlist (fs, map #1 ixns)
   1.134 -    fun thaw(f as (a,S)) = case assoc (fmap, a) of
   1.135 -                             None => TFree(f)
   1.136 -                           | Some b => TVar((b, 0), S)
   1.137 -  in  map_term_types (map_type_tfree thaw) t  end;
   1.138 +    fun thaw (f as (a, S)) =
   1.139 +      (case assoc (fmap, a) of
   1.140 +        None => TFree f
   1.141 +      | Some b => TVar ((b, 0), S));
   1.142 +  in
   1.143 +    map_term_types (map_type_tfree thaw) t
   1.144 +  end;
   1.145 +
   1.146 +
   1.147 +(* thaw, freeze *)
   1.148  
   1.149 +val thaw_vars =
   1.150 +  let
   1.151 +    fun thaw (f as (a, S)) =
   1.152 +      (case explode a of
   1.153 +        "?" :: "'" :: vn =>
   1.154 +          let val ((b, i), _) = Syntax.scan_varname vn in
   1.155 +            TVar (("'" ^ b, i), S)
   1.156 +          end
   1.157 +      | _ => TFree f)
   1.158 +  in map_type_tfree thaw end;
   1.159 +
   1.160 +val freeze_vars =
   1.161 +  map_type_tvar (fn (v, S) => TFree (Syntax.string_of_vname v, S));
   1.162  
   1.163  
   1.164 -(*** type classes and sorts ***)
   1.165 -
   1.166 -(*
   1.167 -  Classes denote (possibly empty) collections of types (e.g. sets of types)
   1.168 -  and are partially ordered by 'inclusion'. They are represented by strings.
   1.169 +local
   1.170 +  fun nextname (pref, c) =
   1.171 +    if c = "z" then (pref ^ "a", "a")
   1.172 +    else (pref, chr (ord c + 1));
   1.173  
   1.174 -  Sorts are intersections of finitely many classes. They are represented by
   1.175 -  lists of classes.
   1.176 -*)
   1.177 -
   1.178 -type domain = sort list;
   1.179 +  fun newtvars used =
   1.180 +    let
   1.181 +      fun new ([], _, vmap) = vmap
   1.182 +        | new (ixn :: ixns, p as (pref, c), vmap) =
   1.183 +            let val nm = pref ^ c in
   1.184 +              if nm mem_string used then new (ixn :: ixns, nextname p, vmap)
   1.185 +              else new (ixns, nextname p, (ixn, nm) :: vmap)
   1.186 +            end
   1.187 +    in new end;
   1.188  
   1.189 -
   1.190 -(* print sorts and arities *)
   1.191 -
   1.192 -fun str_of_sort [c] = c
   1.193 -  | str_of_sort cs = enclose "{" "}" (commas cs);
   1.194 +  (*Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
   1.195 +    Note that if t contains frozen TVars there is the possibility that a TVar is
   1.196 +    turned into one of those. This is sound but not complete.*)
   1.197  
   1.198 -fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
   1.199 -
   1.200 -fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
   1.201 -  | str_of_arity (t, SS, S) =
   1.202 -      t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
   1.203 +  fun convert used freeze p t =
   1.204 +    let
   1.205 +      val used =
   1.206 +        if freeze then add_term_tfree_names (t, used)
   1.207 +        else used union (map #1 (filter_out p (add_term_tvar_ixns (t, []))));
   1.208 +      val ixns = filter p (add_term_tvar_ixns (t, []));
   1.209 +      val vmap = newtvars used (ixns, ("'", "a"), []);
   1.210 +      fun conv (var as (ixn, S)) =
   1.211 +        (case assoc (vmap, ixn) of
   1.212 +          None => TVar(var)
   1.213 +        | Some a => if freeze then TFree (a, S) else TVar ((a, 0), S));
   1.214 +    in
   1.215 +      map_term_types (map_type_tvar conv) t
   1.216 +    end;
   1.217 +in
   1.218 +  fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
   1.219 +end;
   1.220  
   1.221  
   1.222  
   1.223  (*** type signatures ***)
   1.224  
   1.225 +(* type type_sig *)
   1.226 +
   1.227  (*
   1.228    classes:
   1.229 -    a list of all declared classes;
   1.230 +    list of all declared classes;
   1.231  
   1.232 -  subclass:
   1.233 -    an association list representing the subclass relation; (c, cs) is
   1.234 -    interpreted as "c is a proper subclass of all elemenst of cs"; note that
   1.235 -    c itself is not a member of cs;
   1.236 +  classrel:
   1.237 +    (see Pure/sorts.ML)
   1.238  
   1.239    default:
   1.240 -    the default sort attached to all unconstrained type vars;
   1.241 +    default sort attached to all unconstrained type vars;
   1.242  
   1.243    tycons:
   1.244 -    an association list of all declared types with the number of their
   1.245 +    association list of all declared types with the number of their
   1.246      arguments;
   1.247  
   1.248    abbrs:
   1.249 -    an association list of type abbreviations;
   1.250 +    association list of type abbreviations;
   1.251  
   1.252    arities:
   1.253 -    a two-fold association list of all type arities; (t, al) means that type
   1.254 -    constructor t has the arities in al; an element (c, ss) of al represents
   1.255 -    the arity (ss)c;
   1.256 +    (see Pure/sorts.ML)
   1.257  *)
   1.258  
   1.259  datatype type_sig =
   1.260    TySg of {
   1.261      classes: class list,
   1.262 -    subclass: (class * class list) list,
   1.263 +    classrel: (class * class list) list,
   1.264      default: sort,
   1.265      tycons: (string * int) list,
   1.266      abbrs: (string * (string list * typ)) list,
   1.267 -    arities: (string * (class * domain) list) list};
   1.268 +    arities: (string * (class * sort list) list) list};
   1.269  
   1.270  fun rep_tsig (TySg comps) = comps;
   1.271  
   1.272  fun defaultS (TySg {default, ...}) = default;
   1.273  
   1.274 +fun logical_types (TySg {classrel, arities, tycons, ...}) =
   1.275 +  let
   1.276 +    fun log_class c = Sorts.class_le classrel (c, logicC);
   1.277 +    fun log_type t = exists (log_class o #1) (assocs arities t);
   1.278 +  in
   1.279 +    filter log_type (map #1 tycons)
   1.280 +  end;
   1.281 +
   1.282 +
   1.283 +(* sorts *)
   1.284 +
   1.285 +(* FIXME declared!? *)
   1.286 +
   1.287 +fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
   1.288 +fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
   1.289 +fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
   1.290 +
   1.291 +fun nonempty_sort (tsig as TySg {classrel, arities, ...}) hyps S =
   1.292 +  Sorts.nonempty_sort classrel arities hyps S;
   1.293 +
   1.294 +fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
   1.295 +  | rem_sorts (TFree (x, _)) = TFree (x, [])
   1.296 +  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
   1.297 +
   1.298  
   1.299  (* error messages *)
   1.300  
   1.301 @@ -183,8 +244,9 @@
   1.302  fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
   1.303  
   1.304  
   1.305 +(* FIXME err_undcl_class! *)
   1.306  (* 'leq' checks the partial order on classes according to the
   1.307 -   statements in the association list 'a' (i.e. 'subclass')
   1.308 +   statements in the association list 'a' (i.e. 'classrel')
   1.309  *)
   1.310  
   1.311  fun less a (C, D) = case assoc (a, C) of
   1.312 @@ -194,102 +256,8 @@
   1.313  fun leq a (C, D)  =  C = D orelse less a (C, D);
   1.314  
   1.315  
   1.316 -(* logical_types *)
   1.317  
   1.318 -(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
   1.319 -  and c <= logic*)
   1.320 -
   1.321 -fun logical_types tsig =
   1.322 -  let
   1.323 -    val TySg {subclass, arities, tycons, ...} = tsig;
   1.324 -
   1.325 -    fun log_class c = leq subclass (c, logicC);
   1.326 -    fun log_type t = exists (log_class o #1) (assocs arities t);
   1.327 -  in
   1.328 -    filter log_type (map #1 tycons)
   1.329 -  end;
   1.330 -
   1.331 -
   1.332 -(* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
   1.333 -   S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
   1.334 -   with C1 <= C2 (according to an association list 'a')
   1.335 -*)
   1.336 -
   1.337 -fun sortorder a (S1, S2) =
   1.338 -  forall  (fn C2 => exists  (fn C1 => leq a (C1, C2))  S1)  S2;
   1.339 -
   1.340 -
   1.341 -(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
   1.342 -  there exists no class in S which is <= C;
   1.343 -  the resulting set is minimal if S was minimal
   1.344 -*)
   1.345 -
   1.346 -fun inj a (C, S) =
   1.347 -  let fun inj1 [] = [C]
   1.348 -        | inj1 (D::T) = if leq a (D, C) then D::T
   1.349 -                        else if leq a (C, D) then inj1 T
   1.350 -                             else D::(inj1 T)
   1.351 -  in inj1 S end;
   1.352 -
   1.353 -
   1.354 -(* 'union_sort' forms the minimal union set of two sorts S1 and S2
   1.355 -   under the assumption that S2 is minimal *)
   1.356 -(* FIXME rename to inter_sort (?) *)
   1.357 -
   1.358 -fun union_sort a = foldr (inj a);
   1.359 -
   1.360 -
   1.361 -(* 'elementwise_union' forms elementwise the minimal union set of two
   1.362 -   sort lists under the assumption that the two lists have the same length
   1.363 -*)
   1.364 -
   1.365 -fun elementwise_union a (Ss1, Ss2) = ListPair.map (union_sort a) (Ss1,Ss2);
   1.366 -
   1.367 -
   1.368 -(* 'lew' checks for two sort lists the ordering for all corresponding list
   1.369 -   elements (i.e. sorts) *)
   1.370 -
   1.371 -fun lew a (w1, w2) = ListPair.all (sortorder a)  (w1,w2);
   1.372 -
   1.373 -
   1.374 -(* 'is_min' checks if a class C is minimal in a given sort S under the
   1.375 -   assumption that S contains C *)
   1.376 -
   1.377 -fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
   1.378 -
   1.379 -
   1.380 -(* 'min_sort' reduces a sort to its minimal classes *)
   1.381 -
   1.382 -fun min_sort a S = distinct(filter (is_min a S) S);
   1.383 -
   1.384 -
   1.385 -(* 'min_domain' minimizes the domain sorts of type declarationsl;
   1.386 -   the function will be applied on the type declarations in extensions *)
   1.387 -
   1.388 -fun min_domain subclass =
   1.389 -  let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
   1.390 -  in map one_min end;
   1.391 -
   1.392 -
   1.393 -(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
   1.394 -   and gives back a list of those range classes whose domains meet the
   1.395 -   predicate 'pred' *)
   1.396 -
   1.397 -fun min_filter a pred ars =
   1.398 -  let fun filt ([], l) = l
   1.399 -        | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
   1.400 -                               else filt (xs, l)
   1.401 -  in filt (ars, []) end;
   1.402 -
   1.403 -
   1.404 -(* 'cod_above' filters all arities whose domains are elementwise >= than
   1.405 -   a given domain 'w' and gives back a list of the corresponding range
   1.406 -   classes *)
   1.407 -
   1.408 -fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
   1.409 -
   1.410 -
   1.411 -
   1.412 +(* FIXME *)
   1.413  (*Instantiation of type variables in types*)
   1.414  (*Pre: instantiations obey restrictions! *)
   1.415  fun inst_typ tye =
   1.416 @@ -298,25 +266,10 @@
   1.417                                  | None => TVar(var)
   1.418    in map_type_tvar inst end;
   1.419  
   1.420 -(* 'least_sort' returns for a given type its maximum sort:
   1.421 -   - type variables, free types: the sort brought with
   1.422 -   - type constructors: recursive determination of the maximum sort of the
   1.423 -                    arguments if the type is declared in 'arities' of the
   1.424 -                    given type signature  *)
   1.425  
   1.426 -fun least_sort (tsig as TySg{subclass, arities, ...}) =
   1.427 -  let fun ls(T as Type(a, Ts)) =
   1.428 -                 (case assoc (arities, a) of
   1.429 -                          Some(ars) => cod_above(subclass, map ls Ts, ars)
   1.430 -                        | None => raise TYPE(undcl_type a, [T], []))
   1.431 -        | ls(TFree(a, S)) = S
   1.432 -        | ls(TVar(a, S)) = S
   1.433 -  in ls end;
   1.434 -
   1.435 -
   1.436 -fun check_has_sort(tsig as TySg{subclass, arities, ...}, T, S) =
   1.437 -  if sortorder subclass ((least_sort tsig T), S) then ()
   1.438 -  else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
   1.439 +fun check_has_sort (TySg {classrel, arities, ...}, T, S) =
   1.440 +  if Sorts.sort_le classrel ((Sorts.least_sort classrel arities T), S) then ()
   1.441 +  else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
   1.442  
   1.443  
   1.444  (*Instantiation of type variables in types *)
   1.445 @@ -348,66 +301,18 @@
   1.446    end;
   1.447  
   1.448  
   1.449 -(** type matching **)
   1.450 -
   1.451 -exception TYPE_MATCH;
   1.452 -
   1.453 -(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
   1.454 -fun typ_match tsig =
   1.455 -  let
   1.456 -    fun match (subs, (TVar (v, S), T)) =
   1.457 -          (case assoc (subs, v) of
   1.458 -            None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
   1.459 -              handle TYPE _ => raise TYPE_MATCH)
   1.460 -          | Some U => if U = T then subs else raise TYPE_MATCH)
   1.461 -      | match (subs, (Type (a, Ts), Type (b, Us))) =
   1.462 -          if a <> b then raise TYPE_MATCH
   1.463 -          else foldl match (subs, Ts ~~ Us)
   1.464 -      | match (subs, (TFree x, TFree y)) =
   1.465 -          if x = y then subs else raise TYPE_MATCH
   1.466 -      | match _ = raise TYPE_MATCH;
   1.467 -  in match end;
   1.468 -
   1.469 -
   1.470 -fun typ_instance (tsig, T, U) =
   1.471 -  (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
   1.472  
   1.473  
   1.474  
   1.475  (** build type signatures **)
   1.476  
   1.477 -fun make_tsig (classes, subclass, default, tycons, abbrs, arities) =
   1.478 -  TySg {classes = classes, subclass = subclass, default = default,
   1.479 +fun make_tsig (classes, classrel, default, tycons, abbrs, arities) =
   1.480 +  TySg {classes = classes, classrel = classrel, default = default,
   1.481      tycons = tycons, abbrs = abbrs, arities = arities};
   1.482  
   1.483  val tsig0 = make_tsig ([], [], [], [], [], []);
   1.484  
   1.485  
   1.486 -(* sorts *)
   1.487 -
   1.488 -fun subsort (TySg {subclass, ...}) (S1, S2) =
   1.489 -  sortorder subclass (S1, S2);
   1.490 -
   1.491 -fun norm_sort (TySg {subclass, ...}) S =
   1.492 -  sort_strings (min_sort subclass S);
   1.493 -
   1.494 -(* FIXME tmp! (sorts.ML) *)
   1.495 -fun eq_sort tsig (S1, S2) =
   1.496 -  norm_sort tsig S1 = norm_sort tsig S2;
   1.497 -
   1.498 -fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
   1.499 -  | rem_sorts (TFree (x, _)) = TFree (x, [])
   1.500 -  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
   1.501 -
   1.502 -
   1.503 -(* nonempty_sort *)
   1.504 -
   1.505 -(* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
   1.506 -fun nonempty_sort _ _ [] = true
   1.507 -  | nonempty_sort (tsig as TySg {arities, ...}) hyps S =
   1.508 -      exists (exists (fn (c, ss) => [c] = S andalso null ss) o snd) arities
   1.509 -        orelse exists (fn S' => subsort tsig (S', S)) hyps;
   1.510 -
   1.511  
   1.512  
   1.513  (* typ_errors *)
   1.514 @@ -450,12 +355,11 @@
   1.515  
   1.516  (* cert_typ *)
   1.517  
   1.518 -(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
   1.519 -
   1.520 -fun cert_typ tsig ty =
   1.521 -  (case typ_errors tsig (ty, []) of
   1.522 -    [] => norm_typ tsig ty
   1.523 -  | errs => raise_type (cat_lines errs) [ty] []);
   1.524 +(*check and normalize typ wrt. tsig*)           (*exception TYPE*)
   1.525 +fun cert_typ tsig T =
   1.526 +  (case typ_errors tsig (T, []) of
   1.527 +    [] => norm_typ tsig T
   1.528 +  | errs => raise_type (cat_lines errs) [T] []);
   1.529  
   1.530  
   1.531  
   1.532 @@ -467,19 +371,19 @@
   1.533  fun assoc_union (as1, []) = as1
   1.534    | assoc_union (as1, (key, l2) :: as2) =
   1.535        (case assoc_string (as1, key) of
   1.536 -        Some l1 => assoc_union 
   1.537 -	              (overwrite (as1, (key, l1 union_string l2)), as2)
   1.538 +        Some l1 => assoc_union
   1.539 +                      (overwrite (as1, (key, l1 union_string l2)), as2)
   1.540        | None => assoc_union ((key, l2) :: as1, as2));
   1.541  
   1.542  
   1.543 -(* merge subclass *)
   1.544 +(* merge classrel *)
   1.545  
   1.546 -fun merge_subclass (subclass1, subclass2) =
   1.547 -  let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) 
   1.548 +fun merge_classrel (classrel1, classrel2) =
   1.549 +  let val classrel = transitive_closure (assoc_union (classrel1, classrel2))
   1.550    in
   1.551 -    if exists (op mem_string) subclass then
   1.552 +    if exists (op mem_string) classrel then
   1.553        error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
   1.554 -    else subclass
   1.555 +    else classrel
   1.556    end;
   1.557  
   1.558  
   1.559 @@ -490,8 +394,8 @@
   1.560  fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
   1.561        Some(w1) => if w = w1 then () else
   1.562          error("There are two declarations\n" ^
   1.563 -              str_of_arity(t, w, [C]) ^ " and\n" ^
   1.564 -              str_of_arity(t, w1, [C]) ^ "\n" ^
   1.565 +              Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
   1.566 +              Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
   1.567                "with the same result class.")
   1.568      | None => ();
   1.569  
   1.570 @@ -499,19 +403,21 @@
   1.571     such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
   1.572  
   1.573  fun coreg_err(t, (C1,w1), (C2,w2)) =
   1.574 -    error("Declarations " ^ str_of_arity(t, w1, [C1]) ^ " and "
   1.575 -                          ^ str_of_arity(t, w2, [C2]) ^ " are in conflict");
   1.576 +    error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
   1.577 +                          ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");
   1.578  
   1.579 -fun coreg subclass (t, Cw1) =
   1.580 -  let fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   1.581 -        if leq subclass (C1,C2)
   1.582 -        then if lew subclass (w1,w2) then () else coreg_err(t, Cw1, Cw2)
   1.583 -        else ()
   1.584 -      fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   1.585 +fun coreg classrel (t, Cw1) =
   1.586 +  let
   1.587 +    fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   1.588 +      if leq classrel (C1,C2) then
   1.589 +        if Sorts.sorts_le classrel (w1,w2) then ()
   1.590 +        else coreg_err(t, Cw1, Cw2)
   1.591 +      else ()
   1.592 +    fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   1.593    in seq check end;
   1.594  
   1.595 -fun add_arity subclass ars (tCw as (_,Cw)) =
   1.596 -      (is_unique_decl ars tCw; coreg subclass tCw ars; Cw ins ars);
   1.597 +fun add_arity classrel ars (tCw as (_,Cw)) =
   1.598 +      (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
   1.599  
   1.600  fun varying_decls t =
   1.601    error ("Type constructor " ^ quote t ^ " has varying number of arguments");
   1.602 @@ -521,8 +427,8 @@
   1.603     it only checks the two restriction conditions and inserts afterwards
   1.604     all elements of the second list into the first one *)
   1.605  
   1.606 -fun merge_arities subclass =
   1.607 -  let fun test_ar t (ars1, sw) = add_arity subclass ars1 (t,sw);
   1.608 +fun merge_arities classrel =
   1.609 +  let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
   1.610  
   1.611        fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
   1.612            Some(ars1) =>
   1.613 @@ -547,23 +453,23 @@
   1.614  (* 'merge_tsigs' takes the above declared functions to merge two type
   1.615    signatures *)
   1.616  
   1.617 -fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1,
   1.618 +fun merge_tsigs(TySg{classes=classes1, default=default1, classrel=classrel1,
   1.619                       tycons=tycons1, arities=arities1, abbrs=abbrs1},
   1.620 -                TySg{classes=classes2, default=default2, subclass=subclass2,
   1.621 +                TySg{classes=classes2, default=default2, classrel=classrel2,
   1.622                       tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
   1.623    let val classes' = classes1 union_string classes2;
   1.624 -      val subclass' = merge_subclass (subclass1, subclass2);
   1.625 +      val classrel' = merge_classrel (classrel1, classrel2);
   1.626        val tycons' = foldl add_tycons (tycons1, tycons2)
   1.627 -      val arities' = merge_arities subclass' (arities1, arities2);
   1.628 -      val default' = min_sort subclass' (default1 @ default2);
   1.629 +      val arities' = merge_arities classrel' (arities1, arities2);
   1.630 +      val default' = Sorts.norm_sort classrel' (default1 @ default2);
   1.631        val abbrs' = merge_abbrs(abbrs1, abbrs2);
   1.632 -  in make_tsig(classes', subclass', default', tycons', abbrs', arities') end;
   1.633 +  in make_tsig(classes', classrel', default', tycons', abbrs', arities') end;
   1.634  
   1.635  
   1.636  
   1.637  (*** extend type signatures ***)
   1.638  
   1.639 -(** add classes and subclass relations**)
   1.640 +(** add classes and classrel relations **)
   1.641  
   1.642  fun add_classes classes cs =
   1.643    (case cs inter_string classes of
   1.644 @@ -571,74 +477,74 @@
   1.645    | dups => err_dup_classes cs);
   1.646  
   1.647  
   1.648 -(*'add_subclass' adds a tuple consisting of a new class (the new class has
   1.649 +(*'add_classrel' adds a tuple consisting of a new class (the new class has
   1.650    already been inserted into the 'classes' list) and its superclasses (they
   1.651 -  must be declared in 'classes' too) to the 'subclass' list of the given type
   1.652 +  must be declared in 'classes' too) to the 'classrel' list of the given type
   1.653    signature; furthermore all inherited superclasses according to the
   1.654    superclasses brought with are inserted and there is a check that there are
   1.655    no cycles (i.e. C <= D <= C, with C <> D);*)
   1.656  
   1.657 -fun add_subclass classes (subclass, (s, ges)) =
   1.658 +fun add_classrel classes (classrel, (s, ges)) =
   1.659    let
   1.660 -    fun upd (subclass, s') =
   1.661 +    fun upd (classrel, s') =
   1.662        if s' mem_string classes then
   1.663 -        let val ges' = the (assoc (subclass, s))
   1.664 -        in case assoc (subclass, s') of
   1.665 +        let val ges' = the (assoc (classrel, s))
   1.666 +        in case assoc (classrel, s') of
   1.667               Some sups => if s mem_string sups
   1.668                             then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
   1.669 -                           else overwrite 
   1.670 -			          (subclass, (s, sups union_string ges'))
   1.671 -           | None => subclass
   1.672 +                           else overwrite
   1.673 +                                  (classrel, (s, sups union_string ges'))
   1.674 +           | None => classrel
   1.675          end
   1.676        else err_undcl_class s'
   1.677 -  in foldl upd (subclass @ [(s, ges)], ges) end;
   1.678 +  in foldl upd (classrel @ [(s, ges)], ges) end;
   1.679  
   1.680  
   1.681  (* 'extend_classes' inserts all new classes into the corresponding
   1.682 -   lists ('classes', 'subclass') if possible *)
   1.683 +   lists ('classes', 'classrel') if possible *)
   1.684  
   1.685 -fun extend_classes (classes, subclass, new_classes) =
   1.686 +fun extend_classes (classes, classrel, new_classes) =
   1.687    let
   1.688      val classes' = add_classes classes (map fst new_classes);
   1.689 -    val subclass' = foldl (add_subclass classes') (subclass, new_classes);
   1.690 -  in (classes', subclass') end;
   1.691 +    val classrel' = foldl (add_classrel classes') (classrel, new_classes);
   1.692 +  in (classes', classrel') end;
   1.693  
   1.694  
   1.695  (* ext_tsig_classes *)
   1.696  
   1.697  fun ext_tsig_classes tsig new_classes =
   1.698    let
   1.699 -    val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   1.700 -    val (classes',subclass') = extend_classes (classes,subclass,new_classes);
   1.701 +    val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
   1.702 +    val (classes',classrel') = extend_classes (classes,classrel,new_classes);
   1.703    in
   1.704 -    make_tsig (classes', subclass', default, tycons, abbrs, arities)
   1.705 +    make_tsig (classes', classrel', default, tycons, abbrs, arities)
   1.706    end;
   1.707  
   1.708  
   1.709 -(* ext_tsig_subclass *)
   1.710 +(* ext_tsig_classrel *)
   1.711  
   1.712 -fun ext_tsig_subclass tsig pairs =
   1.713 +fun ext_tsig_classrel tsig pairs =
   1.714    let
   1.715 -    val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   1.716 +    val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
   1.717  
   1.718      (* FIXME clean! *)
   1.719 -    val subclass' =
   1.720 -      merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
   1.721 +    val classrel' =
   1.722 +      merge_classrel (classrel, map (fn (c1, c2) => (c1, [c2])) pairs);
   1.723    in
   1.724 -    make_tsig (classes, subclass', default, tycons, abbrs, arities)
   1.725 +    make_tsig (classes, classrel', default, tycons, abbrs, arities)
   1.726    end;
   1.727  
   1.728  
   1.729  (* ext_tsig_defsort *)
   1.730  
   1.731 -fun ext_tsig_defsort(TySg{classes,subclass,tycons,abbrs,arities,...}) default =
   1.732 -  make_tsig (classes, subclass, default, tycons, abbrs, arities);
   1.733 +fun ext_tsig_defsort(TySg{classes,classrel,tycons,abbrs,arities,...}) default =
   1.734 +  make_tsig (classes, classrel, default, tycons, abbrs, arities);
   1.735  
   1.736  
   1.737  
   1.738  (** add types **)
   1.739  
   1.740 -fun ext_tsig_types (TySg {classes, subclass, default, tycons, abbrs, arities}) ts =
   1.741 +fun ext_tsig_types (TySg {classes, classrel, default, tycons, abbrs, arities}) ts =
   1.742    let
   1.743      fun check_type (c, n) =
   1.744        if n < 0 then err_neg_args c
   1.745 @@ -647,7 +553,7 @@
   1.746        else ();
   1.747    in
   1.748      seq check_type ts;
   1.749 -    make_tsig (classes, subclass, default, ts @ tycons, abbrs,
   1.750 +    make_tsig (classes, classrel, default, ts @ tycons, abbrs,
   1.751        map (rpair [] o #1) ts @ arities)
   1.752    end;
   1.753  
   1.754 @@ -696,10 +602,10 @@
   1.755      | msgs => err msgs)
   1.756    end;
   1.757  
   1.758 -fun add_abbr (tsig as TySg{classes,subclass,default,tycons,arities,abbrs},
   1.759 +fun add_abbr (tsig as TySg{classes,classrel,default,tycons,arities,abbrs},
   1.760                abbr) =
   1.761    make_tsig
   1.762 -    (classes,subclass,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
   1.763 +    (classes,classrel,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
   1.764  
   1.765  fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   1.766  
   1.767 @@ -715,14 +621,14 @@
   1.768     if one type declaration has passed all checks it is inserted into
   1.769     the 'arities' association list of the given type signatrure  *)
   1.770  
   1.771 -fun coregular (classes, subclass, tycons) =
   1.772 +fun coregular (classes, classrel, tycons) =
   1.773    let fun ex C = if C mem_string classes then () else err_undcl_class(C);
   1.774  
   1.775        fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
   1.776              Some(n) => if n <> length w then varying_decls(t) else
   1.777                       ((seq o seq) ex w; ex C;
   1.778                        let val ars = the (assoc(arities, t))
   1.779 -                          val ars' = add_arity subclass ars (t,(C,w))
   1.780 +                          val ars' = add_arity classrel ars (t,(C,w))
   1.781                        in overwrite(arities, (t,ars')) end)
   1.782            | None => error (undcl_type t);
   1.783  
   1.784 @@ -738,12 +644,12 @@
   1.785     no declaration t:(Ss')D with C <=D then the declaration holds
   1.786     for all range classes more general than C *)
   1.787  
   1.788 -fun close subclass arities =
   1.789 -  let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
   1.790 +fun close classrel arities =
   1.791 +  let fun check sl (l, (s, dom)) = case assoc (classrel, s) of
   1.792            Some sups =>
   1.793              let fun close_sup (l, sup) =
   1.794 -                  if exists (fn s'' => less subclass (s, s'') andalso
   1.795 -                                       leq subclass (s'', sup)) sl
   1.796 +                  if exists (fn s'' => less classrel (s, s'') andalso
   1.797 +                                       leq classrel (s'', sup)) sl
   1.798                    then l
   1.799                    else (sup, dom)::l
   1.800              in foldl close_sup (l, sups) end
   1.801 @@ -754,200 +660,149 @@
   1.802  
   1.803  (* ext_tsig_arities *)
   1.804  
   1.805 +fun norm_domain classrel =
   1.806 +  let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
   1.807 +  in map one_min end;
   1.808 +
   1.809  fun ext_tsig_arities tsig sarities =
   1.810    let
   1.811 -    val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
   1.812 +    val TySg {classes, classrel, default, tycons, arities, abbrs} = tsig;
   1.813      val arities1 =
   1.814 -      List.concat 
   1.815 +      List.concat
   1.816            (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   1.817 -    val arities2 = foldl (coregular (classes, subclass, tycons))
   1.818 -                         (arities, min_domain subclass arities1)
   1.819 -      |> close subclass;
   1.820 +    val arities2 = foldl (coregular (classes, classrel, tycons))
   1.821 +                         (arities, norm_domain classrel arities1)
   1.822 +      |> close classrel;
   1.823    in
   1.824 -    make_tsig (classes, subclass, default, tycons, abbrs, arities2)
   1.825 +    make_tsig (classes, classrel, default, tycons, abbrs, arities2)
   1.826    end;
   1.827  
   1.828  
   1.829  
   1.830 -(*** type unification and inference ***)
   1.831 +(*** type unification and friends ***)
   1.832  
   1.833 -(*
   1.834 -  Input:
   1.835 -    - a 'raw' term which contains only dummy types and some explicit type
   1.836 -      constraints encoded as terms.
   1.837 -    - the expected type of the term.
   1.838 +(** matching **)
   1.839  
   1.840 -  Output:
   1.841 -    - the correctly typed term
   1.842 -    - the substitution needed to unify the actual type of the term with its
   1.843 -      expected type; only the TVars in the expected type are included.
   1.844 +exception TYPE_MATCH;
   1.845  
   1.846 -  During type inference all TVars in the term have index > maxidx, where
   1.847 -  maxidx is the max. index in the expected type of the term (T). This keeps
   1.848 -  them apart, because at the end the type of the term is unified with T.
   1.849 +fun typ_match tsig =
   1.850 +  let
   1.851 +    fun match (subs, (TVar (v, S), T)) =
   1.852 +          (case assoc (subs, v) of
   1.853 +            None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
   1.854 +              handle TYPE _ => raise TYPE_MATCH)
   1.855 +          | Some U => if U = T then subs else raise TYPE_MATCH)
   1.856 +      | match (subs, (Type (a, Ts), Type (b, Us))) =
   1.857 +          if a <> b then raise TYPE_MATCH
   1.858 +          else foldl match (subs, Ts ~~ Us)
   1.859 +      | match (subs, (TFree x, TFree y)) =
   1.860 +          if x = y then subs else raise TYPE_MATCH
   1.861 +      | match _ = raise TYPE_MATCH;
   1.862 +  in match end;
   1.863  
   1.864 -  1. Add initial type information to the term (attach_types).
   1.865 -     This freezes (freeze_vars) TVars in explicitly provided types (eg
   1.866 -     constraints or defaults) by turning them into TFrees.
   1.867 -  2. Carry out type inference.
   1.868 -  3. Unify actual and expected type.
   1.869 -  4. Turn all local (i.e. > maxidx) TVars into unique new TFrees (freeze).
   1.870 -  5. Thaw all TVars frozen in step 1 (thaw_vars).
   1.871 -*)
   1.872 +fun typ_instance (tsig, T, U) =
   1.873 +  (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
   1.874 +
   1.875  
   1.876 -(*Raised if types are not unifiable*)
   1.877 +
   1.878 +(** unification **)
   1.879 +
   1.880  exception TUNIFY;
   1.881  
   1.882 -val tyvar_count = ref 0;
   1.883  
   1.884 -fun tyinit(i) = (tyvar_count := i);
   1.885 -
   1.886 -fun new_tvar_inx () = (tyvar_count := !tyvar_count + 1; !tyvar_count)
   1.887 +(* occurs check *)
   1.888  
   1.889 -(*
   1.890 -Generate new TVar.  Index is > maxidx+1 to distinguish it from TVars
   1.891 -generated from variable names (see id_type).
   1.892 -Name is arbitrary because index is new.
   1.893 -*)
   1.894 -
   1.895 -fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
   1.896 -
   1.897 -(*Occurs check: type variable occurs in type?*)
   1.898 -fun occ v tye =
   1.899 -  let fun occ(Type(_, Ts)) = exists occ Ts
   1.900 -        | occ(TFree _) = false
   1.901 -        | occ(TVar(w, _)) = eq_ix(v,w) orelse
   1.902 -                           (case assoc(tye, w) of
   1.903 -                              None   => false
   1.904 -                            | Some U => occ U);
   1.905 +fun occurs v tye =
   1.906 +  let
   1.907 +    fun occ (Type (_, Ts)) = exists occ Ts
   1.908 +      | occ (TFree _) = false
   1.909 +      | occ (TVar (w, _)) =
   1.910 +          eq_ix (v, w) orelse
   1.911 +            (case assoc (tye, w) of
   1.912 +              None => false
   1.913 +            | Some U => occ U);
   1.914    in occ end;
   1.915  
   1.916 -(*Chase variable assignments in tye.
   1.917 -  If devar (T, tye) returns a type var then it must be unassigned.*)
   1.918 -fun devar (T as TVar(v, _), tye) = (case  assoc(tye, v)  of
   1.919 -          Some U =>  devar (U, tye)
   1.920 -        | None   =>  T)
   1.921 +
   1.922 +(* chase variable assignments *)
   1.923 +
   1.924 +(*if devar returns a type var then it must be unassigned*)
   1.925 +fun devar (T as TVar (v, _), tye) =
   1.926 +      (case  assoc (tye, v) of
   1.927 +        Some U => devar (U, tye)
   1.928 +      | None => T)
   1.929    | devar (T, tye) = T;
   1.930  
   1.931 -(* use add_to_tye(t,tye) instead of t::tye
   1.932 -to avoid chains of the form 'a |-> 'b |-> 'c ... *)
   1.933  
   1.934 -fun add_to_tye(p,[]) = [p]
   1.935 -  | add_to_tye(vT as (v,T),(xU as (x,TVar(w,S)))::ps) =
   1.936 -      (if eq_ix(v,w) then (x,T) else xU) :: (add_to_tye(vT,ps))
   1.937 -  | add_to_tye(v,x::xs) = x::(add_to_tye(v,xs));
   1.938 -
   1.939 -(* 'dom' returns for a type constructor t the list of those domains
   1.940 -   which deliver a given range class C *)
   1.941 +(* add_env *)
   1.942  
   1.943 -fun dom arities t C = case assoc2 (arities, (t, C)) of
   1.944 -    Some(Ss) => Ss
   1.945 -  | None => raise TUNIFY;
   1.946 -
   1.947 -
   1.948 -(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
   1.949 -   (i.e. a set of range classes ); the union is carried out elementwise
   1.950 -   for the seperate sorts in the domains *)
   1.951 -
   1.952 -fun union_dom (subclass, arities) (t, S) =
   1.953 -    case map (dom arities t) S of
   1.954 -	[] => []
   1.955 -      | (d::ds) => foldl (elementwise_union subclass) (d,ds);
   1.956 +(*avoids chains 'a |-> 'b |-> 'c ...*)
   1.957 +fun add_env (p, []) = [p]
   1.958 +  | add_env (vT as (v, T), (xU as (x, TVar (w, S))) :: ps) =
   1.959 +      (if eq_ix (v, w) then (x, T) else xU) :: add_env (vT, ps)
   1.960 +  | add_env (v, x :: xs) = x :: add_env (v, xs);
   1.961  
   1.962  
   1.963 -fun W ((T, S), tsig as TySg{subclass, arities, ...}, tye) =
   1.964 -  let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
   1.965 -      fun Wk(T as TVar(v, S')) =
   1.966 -              if sortorder subclass (S', S) then tye
   1.967 -              else add_to_tye((v, gen_tyvar(union_sort subclass (S', S))),tye)
   1.968 -        | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
   1.969 -                                 else raise TUNIFY
   1.970 -        | Wk(T as Type(f, Ts)) =
   1.971 -           if null S then tye
   1.972 -           else foldr Wd (Ts~~(union_dom (subclass, arities) (f, S)) , tye)
   1.973 -  in Wk(T) end;
   1.974 +(* unify *)
   1.975 +
   1.976 +fun unify (tsig as TySg {classrel, arities, ...}) maxidx tyenv TU =
   1.977 +  let
   1.978 +    val tyvar_count = ref maxidx;
   1.979 +    fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   1.980 +
   1.981 +    fun mg_domain a S =
   1.982 +      Sorts.mg_domain classrel arities a S handle TYPE _ => raise TUNIFY;
   1.983 +
   1.984 +    fun meet ((_, []), tye) = tye
   1.985 +      | meet ((TVar (xi, S'), S), tye) =
   1.986 +          if Sorts.sort_le classrel (S', S) then tye
   1.987 +          else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
   1.988 +      | meet ((TFree (_, S'), S), tye) =
   1.989 +          if Sorts.sort_le classrel (S', S) then tye
   1.990 +          else raise TUNIFY
   1.991 +      | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
   1.992 +    and meets (([], []), tye) = tye
   1.993 +      | meets ((T :: Ts, S :: Ss), tye) =
   1.994 +          meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
   1.995 +      | meets _ = sys_error "meets";
   1.996 +
   1.997 +    fun unif ((ty1, ty2), tye) =
   1.998 +      (case (devar (ty1, tye), devar (ty2, tye)) of
   1.999 +        (T as TVar (v, S1), U as TVar (w, S2)) =>
  1.1000 +          if eq_ix (v, w) then tye
  1.1001 +          else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye)
  1.1002 +          else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye)
  1.1003 +          else
  1.1004 +            let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
  1.1005 +              add_env ((v, S), add_env ((w, S), tye))
  1.1006 +            end
  1.1007 +      | (TVar (v, S), T) =>
  1.1008 +          if occurs v tye T then raise TUNIFY
  1.1009 +          else meet ((T, S), add_env ((v, T), tye))
  1.1010 +      | (T, TVar (v, S)) =>
  1.1011 +          if occurs v tye T then raise TUNIFY
  1.1012 +          else meet ((T, S), add_env ((v, T), tye))
  1.1013 +      | (Type (a, Ts), Type (b, Us)) =>
  1.1014 +          if a <> b then raise TUNIFY
  1.1015 +          else foldr unif (Ts ~~ Us, tye)
  1.1016 +      | (T, U) => if T = U then tye else raise TUNIFY);
  1.1017 +  in
  1.1018 +    (unif (TU, tyenv), ! tyvar_count)
  1.1019 +  end;
  1.1020  
  1.1021  
  1.1022 -(* Order-sorted Unification of Types (U)  *)
  1.1023 +(* raw_unify *)
  1.1024  
  1.1025 -(* Precondition: both types are well-formed w.r.t. type constructor arities *)
  1.1026 -fun unify1 (tsig as TySg{subclass, arities, ...}) =
  1.1027 -  let fun unif ((T, U), tye) =
  1.1028 -        case (devar(T, tye), devar(U, tye)) of
  1.1029 -          (T as TVar(v, S1), U as TVar(w, S2)) =>
  1.1030 -             if eq_ix(v,w) then tye else
  1.1031 -             if sortorder subclass (S1, S2) then add_to_tye((w, T),tye) else
  1.1032 -             if sortorder subclass (S2, S1) then add_to_tye((v, U),tye)
  1.1033 -             else let val nu = gen_tyvar (union_sort subclass (S1, S2))
  1.1034 -                  in add_to_tye((v, nu),add_to_tye((w, nu),tye)) end
  1.1035 -        | (T as TVar(v, S), U) =>
  1.1036 -             if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((v, U),tye))
  1.1037 -        | (U, T as TVar (v, S)) =>
  1.1038 -             if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((v, U),tye))
  1.1039 -        | (Type(a, Ts), Type(b, Us)) =>
  1.1040 -             if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
  1.1041 -        | (T, U) => if T=U then tye else raise TUNIFY
  1.1042 -  in unif end;
  1.1043 -
  1.1044 -fun unify tsig maxidx tye TU =
  1.1045 -  (tyinit maxidx; (unify1 tsig (TU,tye), !tyvar_count) );
  1.1046 -
  1.1047 -(* raw_unify (ignores sorts) *)
  1.1048 -
  1.1049 +(*purely structural unification -- ignores sorts*)
  1.1050  fun raw_unify (ty1, ty2) =
  1.1051    (unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true)
  1.1052      handle TUNIFY => false;
  1.1053  
  1.1054  
  1.1055 -(*Type inference for polymorphic term*)
  1.1056 -fun infer tsig =
  1.1057 -  let fun inf(Ts, Const (_, T), tye) = (T, tye)
  1.1058 -        | inf(Ts, Free  (_, T), tye) = (T, tye)
  1.1059 -        | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
  1.1060 -          handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
  1.1061 -        | inf(Ts, Var (_, T), tye) = (T, tye)
  1.1062 -        | inf(Ts, Abs (_, T, body), tye) =
  1.1063 -            let val (U, tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
  1.1064 -        | inf(Ts, f$u, tye) =
  1.1065 -            let val (U, tyeU) = inf(Ts, u, tye);
  1.1066 -                val (T, tyeT) = inf(Ts, f, tyeU);
  1.1067 -                fun err s =
  1.1068 -                  raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
  1.1069 -		val msg = "function type is incompatible with argument type"
  1.1070 -            in case T of
  1.1071 -                 Type("fun", [T1, T2]) =>
  1.1072 -                   ( (T2, unify1 tsig ((T1, U), tyeT))
  1.1073 -                     handle TUNIFY => err msg)
  1.1074 -               | TVar _ =>
  1.1075 -                   let val T2 = gen_tyvar([])
  1.1076 -                   in (T2, unify1 tsig ((T, U-->T2), tyeT))
  1.1077 -                      handle TUNIFY => err msg
  1.1078 -                   end
  1.1079 -               | _ => err"function type is expected in application"
  1.1080 -           end
  1.1081 -  in inf end;
  1.1082  
  1.1083 -val freeze_vars =
  1.1084 -      map_type_tvar (fn (v, S) => TFree(Syntax.string_of_vname v, S));
  1.1085 -
  1.1086 -(* Attach a type to a constant *)
  1.1087 -fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
  1.1088 -
  1.1089 -(*Find type of ident.  If not in table then use ident's name for tyvar
  1.1090 -  to get consistent typing.*)
  1.1091 -fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
  1.1092 +(** type inference **)
  1.1093  
  1.1094 -fun type_of_ixn(types, ixn as (a, _),maxidx1) =
  1.1095 -  case types ixn of Some T => freeze_vars T
  1.1096 -                  | None   => TVar(("'"^a, maxidx1), []);
  1.1097 -
  1.1098 -fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
  1.1099 -
  1.1100 -fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
  1.1101 -  | constrainAbs _ = sys_error "constrainAbs";
  1.1102 -
  1.1103 -
  1.1104 -(* get_sort *)
  1.1105 +(* constraints *)
  1.1106  
  1.1107  fun get_sort tsig def_sort env xi =
  1.1108    (case (assoc (env, xi), def_sort xi) of
  1.1109 @@ -959,137 +814,74 @@
  1.1110        else error ("Sort constraint inconsistent with default for type variable " ^
  1.1111          quote (Syntax.string_of_vname' xi)));
  1.1112  
  1.1113 -
  1.1114 -(* attach_types *)
  1.1115 -
  1.1116 -(*
  1.1117 -  Attach types to a term. Input is a "parse tree" containing dummy types.
  1.1118 -  Type constraints are translated and checked for validity wrt tsig. TVars in
  1.1119 -  constraints are frozen.
  1.1120 -
  1.1121 -  The atoms in the resulting term satisfy the following spec:
  1.1122 -
  1.1123 -  Const (a, T):
  1.1124 -    T is a renamed copy of the generic type of a; renaming increases index of
  1.1125 -    all TVars by new_tvar_inx(), which is > maxidx+1.
  1.1126 -
  1.1127 -  Free (a, T), Var (ixn, T):
  1.1128 -    T is either the frozen default type of a or TVar (("'"^a, maxidx+1), [])
  1.1129 -
  1.1130 -  Abs (a, T, _):
  1.1131 -    T is either a type constraint or TVar (("'" ^ a, i), []), where i is
  1.1132 -    generated by new_tvar_inx(). Thus different abstractions can have the
  1.1133 -    bound variables of the same name but different types.
  1.1134 -*)
  1.1135 -
  1.1136 -fun attach_types (tsig, const_type, types, sorts, maxidx1) tm =
  1.1137 -  let
  1.1138 -    val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm;
  1.1139 -
  1.1140 -    fun prepareT t =
  1.1141 -      freeze_vars (cert_typ tsig (Syntax.typ_of_term (get_sort tsig sorts sort_env) t));
  1.1142 -
  1.1143 -    fun add (Const (a, _)) =
  1.1144 -          (case const_type a of
  1.1145 -            Some T => type_const (a, T)
  1.1146 -          | None => raise_type ("No such constant: " ^ quote a) [] [])
  1.1147 -      | add (Free (a, _)) =
  1.1148 -          (case const_type a of
  1.1149 -            Some T => type_const (a, T)
  1.1150 -          | None => Free (a, type_of_ixn (types,(a,~1),maxidx1)))
  1.1151 -      | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn, maxidx1))
  1.1152 -      | add (Bound i) = Bound i
  1.1153 -      | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
  1.1154 -      | add ((f as Const (a, _) $ t1) $ t2) =
  1.1155 -          if a = Syntax.constrainC then
  1.1156 -            constrain (add t1, prepareT t2)
  1.1157 -          else if a = Syntax.constrainAbsC then
  1.1158 -            constrainAbs (add t1, prepareT t2)
  1.1159 -          else add f $ add t2
  1.1160 -      | add (f $ t) = add f $ add t;
  1.1161 -  in add tm end;
  1.1162 +fun constrain t T =
  1.1163 +  if T = dummyT then t
  1.1164 +  else Const ("_type_constraint_", T) $ t;
  1.1165  
  1.1166  
  1.1167 -(* Post-Processing *)
  1.1168 +(* decode_types *)
  1.1169  
  1.1170 -(*Instantiation of type variables in terms*)
  1.1171 -fun inst_types tye = map_term_types (inst_typ tye);
  1.1172 +(*transform parse tree into raw term (idempotent)*)
  1.1173 +fun decode_types tsig is_const def_type def_sort tm =
  1.1174 +  let
  1.1175 +    fun get_type xi = if_none (def_type xi) dummyT;
  1.1176 +    val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm;
  1.1177 +
  1.1178 +    fun decodeT t =
  1.1179 +      cert_typ tsig (Syntax.typ_of_term (get_sort tsig def_sort sort_env) t);
  1.1180  
  1.1181 -(*Delete explicit constraints -- occurrences of "_constrain" *)
  1.1182 -fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
  1.1183 -  | unconstrain ((f as Const(a, _)) $ t) =
  1.1184 -      if a=Syntax.constrainC then unconstrain t
  1.1185 -      else unconstrain f $ unconstrain t
  1.1186 -  | unconstrain (f$t) = unconstrain f $ unconstrain t
  1.1187 -  | unconstrain (t) = t;
  1.1188 +    fun decode (Const ("_constrain", _) $ t $ typ) =
  1.1189 +          constrain (decode t) (decodeT typ)
  1.1190 +      | decode (Const ("_constrainAbs", _) $ (abs as Abs (x, T, t)) $ typ) =
  1.1191 +          if T = dummyT then Abs (x, decodeT typ, decode t)
  1.1192 +          else constrain abs (decodeT typ --> dummyT)
  1.1193 +      | decode (Abs (x, T, t)) = Abs (x, T, decode t)
  1.1194 +      | decode (t $ u) = decode t $ decode u
  1.1195 +      | decode (t as Free (x, T)) =
  1.1196 +          if is_const x then Const (x, T)
  1.1197 +          else if T = dummyT then Free (x, get_type (x, ~1))
  1.1198 +          else constrain t (get_type (x, ~1))
  1.1199 +      | decode (t as Var (xi, T)) =
  1.1200 +          if T = dummyT then Var (xi, get_type xi)
  1.1201 +          else constrain t (get_type xi)
  1.1202 +      | decode (t as Bound _) = t
  1.1203 +      | decode (t as Const _) = t;
  1.1204 +  in
  1.1205 +    decode tm
  1.1206 +  end;
  1.1207  
  1.1208 -fun nextname(pref,c) = if c="z" then (pref^"a", "a") else (pref,chr(ord(c)+1));
  1.1209  
  1.1210 -fun newtvars used =
  1.1211 -  let fun new([],_,vmap) = vmap
  1.1212 -        | new(ixn::ixns,p as (pref,c),vmap) =
  1.1213 -            let val nm = pref ^ c
  1.1214 -            in if nm mem_string used then new(ixn::ixns,nextname p, vmap)
  1.1215 -               else new(ixns, nextname p, (ixn,nm)::vmap)
  1.1216 -            end
  1.1217 -  in new end;
  1.1218 +(* infer_types *)
  1.1219  
  1.1220  (*
  1.1221 -Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
  1.1222 -Note that if t contains frozen TVars there is the possibility that a TVar is
  1.1223 -turned into one of those. This is sound but not complete.
  1.1224 +  Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
  1.1225 +  unifies with Ti (for i=1,...,n).
  1.1226 +
  1.1227 +  tsig: type signature
  1.1228 +  const_type: term signature
  1.1229 +  def_type: partial map from indexnames to types (constrains Frees, Vars)
  1.1230 +  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
  1.1231 +  used: list of already used type variables
  1.1232 +  freeze: if true then generated parameters are turned into TFrees, else TVars
  1.1233  *)
  1.1234 -fun convert used freeze p t =
  1.1235 -  let val used = if freeze then add_term_tfree_names(t, used)
  1.1236 -                 else used union
  1.1237 -                      (map #1 (filter_out p (add_term_tvar_ixns(t, []))))
  1.1238 -      val ixns = filter p (add_term_tvar_ixns(t, []));
  1.1239 -      val vmap = newtvars used (ixns,("'","a"),[]);
  1.1240 -      fun conv(var as (ixn,S)) = case assoc(vmap,ixn) of
  1.1241 -            None => TVar(var) |
  1.1242 -            Some(a) => if freeze then TFree(a,S) else TVar((a,0),S);
  1.1243 -  in map_term_types (map_type_tvar conv) t end;
  1.1244 -
  1.1245 -fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
  1.1246 -
  1.1247 -(* Thaw all TVars that were frozen in freeze_vars *)
  1.1248 -val thaw_vars =
  1.1249 -  let fun thaw(f as (a, S)) = (case explode a of
  1.1250 -          "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
  1.1251 -                          in TVar(("'"^b, i), S) end
  1.1252 -        | _ => TFree f)
  1.1253 -  in map_type_tfree thaw end;
  1.1254 -
  1.1255  
  1.1256 -fun restrict maxidx1 tye =
  1.1257 -  let fun clean(tye1, ((a, i), T)) =
  1.1258 -        if i >= maxidx1 then tye1 else ((a, i), inst_typ tye T) :: tye1
  1.1259 -  in foldl clean ([], tye) end
  1.1260 -
  1.1261 +(*user-supplied inference parameters*)
  1.1262 +fun q_is_param (x, _) =
  1.1263 +  (case explode x of
  1.1264 +    "?" :: _ => true
  1.1265 +  | _ => false);
  1.1266  
  1.1267 -(*Infer types for terms.  Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that
  1.1268 -	the type of ti unifies with Ti (i=1,...,n).
  1.1269 -  types is a partial map from indexnames to types (constrains Free, Var).
  1.1270 -  sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
  1.1271 -  used is the list of already used type variables.
  1.1272 -  If freeze then internal TVars are turned into TFrees, else TVars.*)
  1.1273 -fun infer_types (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
  1.1274 +fun infer_types (tsig, const_type, def_type, def_sort, used, freeze, pat_Ts, raw_ts) =
  1.1275    let
  1.1276 -    val maxidx1 = maxidx_of_typs Ts + 1;
  1.1277 -    val () = tyinit(maxidx1+1);
  1.1278 -    val us = map (attach_types (tsig, const_type, types, sorts, maxidx1)) ts;
  1.1279 -    val u = list_comb(Const("",Ts ---> propT),us)
  1.1280 -    val (_, tye) = infer tsig ([], u, []);
  1.1281 -    val uu = unconstrain u;
  1.1282 -    val Ttye = restrict maxidx1 tye (*restriction to TVars in Ts*)
  1.1283 -    val all = Const("", Type("", map snd Ttye)) $ (inst_types tye uu)
  1.1284 -      (*all is a dummy term which contains all exported TVars*)
  1.1285 -    val Const(_, Type(_, Us)) $ u'' =
  1.1286 -      map_term_types thaw_vars (convert used freeze (fn (_,i) => i >= maxidx1) all)
  1.1287 -      (*convert all internally generated TVars into TFrees or TVars
  1.1288 -        and thaw all initially frozen TVars*)
  1.1289 +    val TySg {classrel, arities, ...} = tsig;
  1.1290 +    val pat_Ts' = map (cert_typ tsig) pat_Ts;
  1.1291 +    val raw_ts' =
  1.1292 +      map (decode_types tsig (is_some o const_type) def_type def_sort) raw_ts;
  1.1293 +    val (ts, Ts, unifier) =
  1.1294 +      TypeInfer.infer_types const_type classrel arities used freeze
  1.1295 +        q_is_param raw_ts' pat_Ts';
  1.1296    in
  1.1297 -    (#2(strip_comb u''), ListPair.zip(map #1 Ttye, Us))
  1.1298 +    (ts, unifier)
  1.1299    end;
  1.1300  
  1.1301  end;