src/Pure/type.ML

now more than 256 generated bound variables possible

(*  Title:      Pure/type.ML
    ID:         $Id$
    Author:     Tobias Nipkow & Lawrence C Paulson

Type signatures, unification of types, interface to type inference.
*)

signature TYPE =
sig
  (*TFrees and TVars*)
  val no_tvars: typ -> typ
  val varifyT: typ -> typ
  val unvarifyT: typ -> typ
  val varify: term * string list -> term
  val freeze_thaw : term -> term * (term -> term)

  (*type signatures*)
  type type_sig
  val rep_tsig: type_sig ->
    {classes: class list,
     classrel: Sorts.classrel,
     default: sort,
     tycons: int Symtab.table,
     log_types: string list,
     univ_witness: (typ * sort) option,
     abbrs: (string list * typ) Symtab.table,
     arities: Sorts.arities}
  val classes: type_sig -> class list
  val defaultS: type_sig -> sort
  val logical_types: type_sig -> string list
  val univ_witness: type_sig -> (typ * sort) option
  val subsort: type_sig -> sort * sort -> bool
  val eq_sort: type_sig -> sort * sort -> bool
  val norm_sort: type_sig -> sort -> sort
  val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
  val rem_sorts: typ -> typ
  val tsig0: type_sig
  val ext_tsig_classes: type_sig -> (class * class list) 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 typ_errors: type_sig -> typ * string list -> string list
  val cert_typ: type_sig -> typ -> typ
  val norm_typ: type_sig -> typ -> typ
  val norm_term: type_sig -> term -> term
  val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term

  (*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
  val of_sort: type_sig -> typ * sort -> 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

  (*type inference*)
  val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
    -> (indexname * sort) list -> indexname -> sort
  val constrain: term -> typ -> term
  val param: string list -> string * sort -> typ
  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    -> type_sig -> (string -> typ option) -> (indexname -> typ option)
    -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
    -> (sort -> sort) -> string list -> bool -> typ list -> term list
    -> term list * (indexname * typ) list
end;

structure Type: TYPE =
struct


(*** TFrees and TVars ***)

fun no_tvars T =
  if null (typ_tvars T) then T
  else raise TYPE ("Illegal schematic type variable(s)", [T], []);


(* varify, unvarify *)

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;

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;


(* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)

local

fun new_name (ix, (pairs,used)) =
      let val v = variant used (string_of_indexname ix)
      in  ((ix,v)::pairs, v::used)  end;

fun freeze_one alist (ix,sort) =
  TFree (the (assoc (alist, ix)), sort)
    handle OPTION =>
      raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);

fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
      handle OPTION => TFree(a,sort);

(*this sort of code could replace unvarifyT (?) -- currently unused*)
fun freeze_thaw_type T =
  let
    val used = add_typ_tfree_names (T, [])
    and tvars = map #1 (add_typ_tvars (T, []));
    val (alist, _) = foldr new_name (tvars, ([], used));
  in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;

in

fun freeze_thaw t =
  let
    val used = it_term_types add_typ_tfree_names (t, [])
    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
    val (alist, _) = foldr new_name (tvars, ([], used));
  in
    (case alist of
      [] => (t, fn x => x) (*nothing to do!*)
    | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
      map_term_types (map_type_tfree (thaw_one (map swap alist)))))
  end;

end;



(*** type signatures ***)

(* type type_sig *)

(*
  classes: list of all declared classes;
  classrel: (see Pure/sorts.ML)
  default: default sort attached to all unconstrained type vars;
  tycons: table of all declared types with the number of their arguments;
  log_types: list of logical type constructors sorted by number of arguments;
  univ_witness: type witnessing non-emptiness of least sort
  abbrs: table of type abbreviations;
  arities: (see Pure/sorts.ML)
*)

datatype type_sig =
  TySg of {
    classes: class list,
    classrel: Sorts.classrel,
    default: sort,
    tycons: int Symtab.table,
    log_types: string list,
    univ_witness: (typ * sort) option,
    abbrs: (string list * typ) Symtab.table,
    arities: Sorts.arities};

fun rep_tsig (TySg comps) = comps;

fun classes (TySg {classes = cs, ...}) = cs;
fun defaultS (TySg {default, ...}) = default;
fun logical_types (TySg {log_types, ...}) = log_types;
fun univ_witness (TySg {univ_witness, ...}) = univ_witness;


(* sorts *)

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 witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
  Sorts.witness_sorts (classrel, arities, log_types);

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 *)

fun undcl_class c = "Undeclared class " ^ quote c;
fun err_undcl_class s = error (undcl_class s);

fun err_dup_classes cs =
  error ("Duplicate declaration of class(es) " ^ commas_quote cs);

fun undcl_type c = "Undeclared type constructor " ^ quote c;

fun err_neg_args c =
  error ("Negative number of arguments of type constructor " ^ quote c);

fun err_dup_tycon c =
  error ("Duplicate declaration of type constructor " ^ quote c);

fun dup_tyabbrs ts =
  "Duplicate declaration of type abbreviation(s) " ^ commas_quote ts;

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 classrel 'a'
*)

fun less a (C, D) = case Symtab.lookup (a, C) of
     Some ss => D mem_string ss
   | None => err_undcl_class C;

fun leq a (C, D)  =  C = D orelse less a (C, D);



(* FIXME *)
(*Instantiation of type variables in types*)
(*Pre: instantiations obey restrictions! *)
fun inst_typ tye =
  let fun inst(var as (v, _)) = case assoc(tye, v) of
                                  Some U => inst_typ tye U
                                | None => TVar(var)
  in map_type_tvar inst end;



fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort (classrel, arities);

fun check_has_sort (tsig, T, S) =
  if of_sort tsig (T, S) then ()
  else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);


(*Instantiation of type variables in types *)
fun inst_typ_tvars(tsig, tye) =
  let fun inst(var as (v, S)) = case assoc(tye, v) of
              Some U => (check_has_sort(tsig, U, S); U)
            | None => TVar(var)
  in map_type_tvar inst end;

(*Instantiation of type variables in terms *)
fun inst_term_tvars (_,[]) t = t
  | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;


(* norm_typ, norm_term *)

(*expand abbreviations and normalize sorts*)
fun norm_typ (tsig as TySg {abbrs, ...}) ty =
  let
    val idx = maxidx_of_typ ty + 1;

    fun norm (Type (a, Ts)) =
          (case Symtab.lookup (abbrs, a) of
            Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
          | None => Type (a, map norm Ts))
      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);

    val ty' = norm ty;
  in if ty = ty' then ty else ty' end;  (*dumb tuning to avoid copying*)

fun norm_term tsig t =
  let val t' = map_term_types (norm_typ tsig) t
  in if t = t' then t else t' end;  (*dumb tuning to avoid copying*)



(** build type signatures **)

fun make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) =
  TySg {classes = classes, classrel = classrel, default = default, tycons = tycons,
    log_types = log_types, univ_witness = univ_witness, abbrs = abbrs, arities = arities};

fun rebuild_tsig (TySg {classes, classrel, default, tycons, log_types = _, univ_witness = _, abbrs, arities}) =
  let
    fun log_class c = Sorts.class_le classrel (c, logicC);
    fun log_type (t, _) = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
    val ts = filter log_type (Symtab.dest tycons);

    val log_types = map #1 (Library.sort (Library.int_ord o pairself #2) ts);
    val univ_witness =
      (case Sorts.witness_sorts (classrel, arities, log_types) [] [classes] of
        [w] => Some w | _ => None);
  in make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) end;

val tsig0 =
  make_tsig ([], Symtab.empty, [], Symtab.empty, [], None, Symtab.empty, Symtab.empty)
  |> rebuild_tsig;


(* typ_errors *)

(*check validity of (not necessarily normal) type; accumulate error messages*)

fun typ_errors tsig (typ, errors) =
  let
    val {classes, tycons, abbrs, ...} = rep_tsig tsig;

    fun class_err (errs, c) =
      if c mem_string classes then errs
      else undcl_class c ins_string errs;

    val sort_err = foldl class_err;

    fun typ_errs (errs, Type (c, Us)) =
          let
            val errs' = foldl typ_errs (errs, Us);
            fun nargs n =
              if n = length Us then errs'
              else ("Wrong number of arguments: " ^ quote c) ins_string errs';
          in
            (case Symtab.lookup (tycons, c) of
              Some n => nargs n
            | None =>
                (case Symtab.lookup (abbrs, c) of
                  Some (vs, _) => nargs (length vs)
                | None => undcl_type c ins_string errs))
          end
    | typ_errs (errs, TFree (_, S)) = sort_err (errs, S)
    | typ_errs (errs, TVar ((x, i), S)) =
        if i < 0 then
          ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
        else sort_err (errs, S);
  in typ_errs (errors, typ) end;


(* cert_typ *)

(*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], []));



(** merge type signatures **)

(* merge classrel *)

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)
      | None => assoc_union ((key, l2) :: as1, as2));

fun merge_classrel (classrel1, classrel2) =
  let
    val classrel = transitive_closure (assoc_union (Symtab.dest classrel1, Symtab.dest classrel2))
  in
    if exists (op mem_string) classrel then
      error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
    else Symtab.make classrel
  end;


(* coregularity *)

local

(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)

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" ^
              Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
              Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
              "with the same result class.")
    | None => ();

(* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)

fun coreg_err(t, (C1,w1), (C2,w2)) =
    error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
                          ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");

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;

in

fun add_arity classrel ars (tCw as (_,Cw)) =
      (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);

end;


(* 'merge_arities' builds the union of two 'arities' lists;
   it only checks the two restriction conditions and inserts afterwards
   all elements of the second list into the first one *)

local

fun merge_arities_aux 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) =>
            let val ars = foldl (test_ar t) (ars1, ars2)
            in overwrite (arities1, (t,ars)) end
        | None => c::arities1
  in foldl merge_c end;

in

fun merge_arities classrel (a1, a2) =
  Symtab.make (merge_arities_aux classrel (Symtab.dest a1, Symtab.dest a2));

end;


(* tycons *)

fun varying_decls t =
  error ("Type constructor " ^ quote t ^ " has varying number of arguments");

fun add_tycons (tycons, tn as (t,n)) =
  (case Symtab.lookup (tycons, t) of
    Some m => if m = n then tycons else varying_decls t
  | None => Symtab.update (tn, tycons));


(* merge_abbrs *)

fun merge_abbrs abbrs =
  Symtab.merge (op =) abbrs handle Symtab.DUPS dups => raise TERM (dup_tyabbrs dups, []);


(* merge_tsigs *)

fun merge_tsigs
 (TySg {classes = classes1, default = default1, classrel = classrel1, tycons = tycons1,
    log_types = _, univ_witness = _, arities = arities1, abbrs = abbrs1},
  TySg {classes = classes2, default = default2, classrel = classrel2, tycons = tycons2,
    log_types = _, univ_witness = _, arities = arities2, abbrs = abbrs2}) =
  let
    val classes' = classes1 union_string classes2;
    val classrel' = merge_classrel (classrel1, classrel2);
    val arities' = merge_arities classrel' (arities1, arities2);
    val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2);
    val default' = Sorts.norm_sort classrel' (default1 @ default2);
    val abbrs' = merge_abbrs (abbrs1, abbrs2);
  in
    make_tsig (classes', classrel', default', tycons', [], None, abbrs', arities')
    |> rebuild_tsig
  end;



(*** extend type signatures ***)

(** add classes and classrel relations **)

fun add_classes classes cs =
  (case cs inter_string classes of
    [] => cs @ classes
  | dups => err_dup_classes cs);


(*'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 '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_classrel classes (classrel, (s, ges)) =
  let
    fun upd (classrel, s') =
      if s' mem_string classes then
        let val ges' = the (Symtab.lookup (classrel, s))
        in case Symtab.lookup (classrel, s') of
             Some sups => if s mem_string sups
                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
                           else Symtab.update ((s, sups union_string ges'), classrel)
           | None => classrel
        end
      else err_undcl_class s'
  in foldl upd (Symtab.update ((s, ges), classrel), ges) end;


(* 'extend_classes' inserts all new classes into the corresponding
   lists ('classes', 'classrel') if possible *)

fun extend_classes (classes, classrel, new_classes) =
  let
    val classes' = add_classes classes (map fst new_classes);
    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, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
    val (classes',classrel') = extend_classes (classes,classrel,new_classes);
  in make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities) end;


(* ext_tsig_classrel *)

fun ext_tsig_classrel tsig pairs =
  let
    val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;

    (* FIXME clean! *)
    val classrel' =
      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (c1, [c2])) pairs));
  in
    make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
    |> rebuild_tsig
  end;


(* ext_tsig_defsort *)

fun ext_tsig_defsort
    (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
  make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);



(** add types **)

fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
  let
    fun check_type (c, n) =
      if n < 0 then err_neg_args c
      else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
      else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
      else ();
    val _ = seq check_type ts;
    val tycons' = Symtab.extend (tycons, ts);
    val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
  in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;



(** add type abbreviations **)

fun abbr_errors tsig (a, (lhs_vs, rhs)) =
  let
    val TySg {tycons, abbrs, ...} = tsig;
    val rhs_vs = map (#1 o #1) (typ_tvars rhs);

    val dup_lhs_vars =
      (case duplicates lhs_vs of
        [] => []
      | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);

    val extra_rhs_vars =
      (case gen_rems (op =) (rhs_vs, lhs_vs) of
        [] => []
      | vs => ["Extra variables on rhs: " ^ commas_quote vs]);

    val tycon_confl =
      if is_none (Symtab.lookup (tycons, a)) then []
      else [ty_confl a];

    val dup_abbr =
      if is_none (Symtab.lookup (abbrs, a)) then []
      else ["Duplicate declaration of abbreviation"];
  in
    dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
      typ_errors tsig (rhs, [])
  end;

fun prep_abbr tsig (a, vs, raw_rhs) =
  let
    fun err msgs = (seq error_msg msgs;
      error ("The error(s) above occurred in type abbreviation " ^ quote a));

    val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
      handle TYPE (msg, _, _) => err [msg];
    val abbr = (a, (vs, rhs));
  in
    (case abbr_errors tsig abbr of
      [] => abbr
    | msgs => err msgs)
  end;

fun add_abbr
    (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
  make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
    Symtab.update (prep_abbr tsig abbr, abbrs), arities);

fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);



(** add arities **)

(* 'coregular' checks
   - the two restrictions 'is_unique_decl' and 'coreg'
   - if the classes in the new type declarations are known in the
     given type signature
   - if one type constructor has always the same number of arguments;
   if one type declaration has passed all checks it is inserted into
   the 'arities' association list of the given type signatrure  *)

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 Symtab.lookup (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 (Symtab.lookup (arities, t))
                          val ars' = add_arity classrel ars (t,(C,w))
                      in Symtab.update ((t,ars'), arities) end)
          | None => error (undcl_type t);

  in addar end;


(* 'close' extends the 'arities' association list after all new type
   declarations have been inserted successfully:
   for every declaration t:(Ss)C , for all classses D with C <= D:
      if there is no declaration t:(Ss')C' with C < C' and C' <= D
      then insert the declaration t:(Ss)D into 'arities'
   this means, if there exists a declaration t:(Ss)C and there is
   no declaration t:(Ss')D with C <=D then the declaration holds
   for all range classes more general than C *)

fun close classrel arities =
  let fun check sl (l, (s, dom)) = case Symtab.lookup (classrel, s) of
          Some sups =>
            let fun close_sup (l, sup) =
                  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
        | None => l;
      fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
  in map ext arities end;


(* 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, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
    val arities1 =
      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
    val arities2 =
      foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
      |> Symtab.dest |> close classrel |> Symtab.make;
  in
    make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
    |> rebuild_tsig
  end;



(*** type unification and friends ***)

(** matching **)

exception TYPE_MATCH;

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;



(** unification **)

exception TUNIFY;


(* occurs check *)

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 *)

(*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;


(* add_env *)

(*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);


(* 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 Sorts.DOMAIN _ => 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;


(* raw_unify *)

(*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 **)

(* sort constraints *)

fun get_sort tsig def_sort map_sort raw_env =
  let
    fun eq ((xi, S), (xi', S')) =
      xi = xi' andalso eq_sort tsig (S, S');

    val env = gen_distinct eq (map (apsnd map_sort) raw_env);
    val _ =
      (case gen_duplicates eq_fst env of
        [] => ()
      | dups => error ("Inconsistent sort constraints for type variable(s) " ^
          commas (map (quote o Syntax.string_of_vname' o fst) dups)));

    fun get xi =
      (case (assoc (env, xi), def_sort xi) of
        (None, None) => defaultS tsig
      | (None, Some S) => S
      | (Some S, None) => S
      | (Some S, Some S') =>
          if eq_sort tsig (S, S') then S'
          else error ("Sort constraint inconsistent with default for type variable " ^
            quote (Syntax.string_of_vname' xi)));
  in get end;


(* type constraints *)

fun constrain t T =
  if T = dummyT then t
  else Const ("_type_constraint_", T) $ t;


(* user parameters *)

fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
fun param used (x, S) = TVar ((variant used ("?" ^ x), 0), S);


(* decode_types *)

(*transform parse tree into raw term*)
fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
  let
    fun get_type xi = if_none (def_type xi) dummyT;
    fun is_free x = is_some (def_type (x, ~1));
    val raw_env = Syntax.raw_term_sorts tm;
    val sort_of = get_sort tsig def_sort map_sort raw_env;

    val certT = cert_typ tsig o map_type;
    fun decodeT t = certT (Syntax.typ_of_term sort_of t);

    fun decode (Const ("_constrain", _) $ t $ typ) =
          constrain (decode t) (decodeT typ)
      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
          if T = dummyT then Abs (x, decodeT typ, decode t)
          else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
      | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
      | decode (t $ u) = decode t $ decode u
      | decode (Free (x, T)) =
          let val c = map_const x in
            if not (is_free x) andalso (is_const c orelse NameSpace.qualified c) then
              Const (c, certT T)
            else if T = dummyT then Free (x, get_type (x, ~1))
            else constrain (Free (x, certT T)) (get_type (x, ~1))
          end
      | decode (Var (xi, T)) =
          if T = dummyT then Var (xi, get_type xi)
          else constrain (Var (xi, certT T)) (get_type xi)
      | decode (t as Bound _) = t
      | decode (Const (c, T)) = Const (map_const c, certT T);
  in
    decode tm
  end;


(* infer_types *)

(*
  Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
  unifies with Ti (for i=1,...,n).

  tsig: type signature
  const_type: name mapping and signature lookup
  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 infer_types prt prT tsig const_type def_type def_sort
    map_const map_type map_sort used freeze pat_Ts raw_ts =
  let
    val TySg {classrel, arities, ...} = tsig;
    val pat_Ts' = map (cert_typ tsig) pat_Ts;
    val is_const = is_some o const_type;
    val raw_ts' =
      map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
    val (ts, Ts, unifier) =
      TypeInfer.infer_types prt prT const_type classrel arities used freeze
        is_param raw_ts' pat_Ts';
  in (ts, unifier) end;


end;