wenzelm@256: (*  Title:      Pure/type.ML
clasohm@0:     ID:         $Id$
wenzelm@416:     Author:     Tobias Nipkow & Lawrence C Paulson
clasohm@0: 
wenzelm@416: Type classes and sorts. Type signatures. Type unification and inference.
wenzelm@256: 
wenzelm@256: TODO:
wenzelm@416:   move type unification and inference to type_unify.ML (TypeUnify) (?)
wenzelm@416:   rename args -> tycons, coreg -> arities (?)
wenzelm@416:   clean err msgs
clasohm@0: *)
clasohm@0: 
clasohm@0: signature TYPE =
clasohm@0: sig
wenzelm@256:   structure Symtab: SYMTAB
wenzelm@416:   val str_of_sort: sort -> string
wenzelm@416:   val str_of_arity: string * sort list * sort -> string
clasohm@0:   type type_sig
nipkow@200:   val rep_tsig: type_sig ->
wenzelm@256:     {classes: class list,
wenzelm@256:      subclass: (class * class list) list,
wenzelm@256:      default: sort,
wenzelm@256:      args: (string * int) list,
wenzelm@256:      abbrs: (string * (indexname list * typ)) list,
wenzelm@256:      coreg: (string * (class * sort list) list) list}
clasohm@0:   val defaultS: type_sig -> sort
wenzelm@416:   val tsig0: type_sig
wenzelm@256:   val logical_types: type_sig -> string list
wenzelm@256:   val extend_tsig: type_sig ->
wenzelm@256:     (class * class list) list * sort * (string list * int) list *
wenzelm@256:     (string list * (sort list * class)) list -> type_sig
wenzelm@422:   val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
wenzelm@422:   val ext_tsig_defsort: type_sig -> sort -> type_sig
wenzelm@256:   val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list
wenzelm@256:     -> type_sig
wenzelm@256:   val merge_tsigs: type_sig * type_sig -> type_sig
wenzelm@416:   val subsort: type_sig -> sort * sort -> bool
wenzelm@416:   val norm_sort: type_sig -> sort -> sort
wenzelm@416:   val rem_sorts: typ -> typ
wenzelm@256:   val cert_typ: type_sig -> typ -> typ
wenzelm@256:   val norm_typ: type_sig -> typ -> typ
clasohm@0:   val freeze: (indexname -> bool) -> term -> term
clasohm@0:   val freeze_vars: typ -> typ
wenzelm@565:   val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) *
wenzelm@256:     (indexname -> sort option) * typ * term -> term * (indexname * typ) list
wenzelm@256:   val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
clasohm@0:   val thaw_vars: typ -> typ
wenzelm@256:   val typ_errors: type_sig -> typ * string list -> string list
clasohm@0:   val typ_instance: type_sig * typ * typ -> bool
wenzelm@256:   val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
wenzelm@256:     -> (indexname * typ) list
wenzelm@256:   val unify: type_sig -> (typ * typ) * (indexname * typ) list
wenzelm@256:     -> (indexname * typ) list
wenzelm@450:   val raw_unify: typ * typ -> bool
clasohm@0:   val varifyT: typ -> typ
clasohm@0:   val varify: term * string list -> term
clasohm@0:   exception TUNIFY
wenzelm@256:   exception TYPE_MATCH
clasohm@0: end;
clasohm@0: 
wenzelm@416: functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE =
clasohm@0: struct
clasohm@0: 
wenzelm@256: structure Symtab = Symtab;
clasohm@0: 
clasohm@0: 
wenzelm@416: (*** type classes and sorts ***)
wenzelm@416: 
wenzelm@416: (*
wenzelm@416:   Classes denote (possibly empty) collections of types (e.g. sets of types)
wenzelm@416:   and are partially ordered by 'inclusion'. They are represented by strings.
wenzelm@416: 
wenzelm@416:   Sorts are intersections of finitely many classes. They are represented by
wenzelm@416:   lists of classes.
wenzelm@416: *)
clasohm@0: 
clasohm@0: type domain = sort list;
wenzelm@416: 
wenzelm@416: 
wenzelm@416: (* print sorts and arities *)
clasohm@0: 
wenzelm@416: fun str_of_sort [c] = c
wenzelm@565:   | str_of_sort cs = enclose "{" "}" (commas cs);
wenzelm@416: 
wenzelm@565: fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
wenzelm@416: 
wenzelm@416: fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
wenzelm@416:   | str_of_arity (t, SS, S) =
wenzelm@416:       t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
wenzelm@256: 
wenzelm@256: 
wenzelm@256: 
wenzelm@416: (*** type signatures ***)
wenzelm@256: 
wenzelm@256: (*
wenzelm@256:   classes:
wenzelm@256:     a list of all declared classes;
clasohm@0: 
wenzelm@256:   subclass:
wenzelm@416:     an association list representing the subclass relation; (c, cs) is
wenzelm@256:     interpreted as "c is a proper subclass of all elemenst of cs"; note that
wenzelm@256:     c itself is not a memeber of cs;
wenzelm@256: 
wenzelm@256:   default:
wenzelm@256:     the default sort attached to all unconstrained type vars;
wenzelm@256: 
wenzelm@256:   args:
wenzelm@256:     an association list of all declared types with the number of their
wenzelm@256:     arguments;
wenzelm@256: 
wenzelm@256:   abbrs:
wenzelm@256:     an association list of type abbreviations;
wenzelm@256: 
wenzelm@256:   coreg:
wenzelm@256:     a two-fold association list of all type arities; (t, al) means that type
wenzelm@256:     constructor t has the arities in al; an element (c, ss) of al represents
wenzelm@256:     the arity (ss)c;
clasohm@0: *)
clasohm@0: 
wenzelm@256: datatype type_sig =
wenzelm@256:   TySg of {
wenzelm@256:     classes: class list,
wenzelm@256:     subclass: (class * class list) list,
wenzelm@256:     default: sort,
wenzelm@256:     args: (string * int) list,
wenzelm@256:     abbrs: (string * (indexname list * typ)) list,
wenzelm@256:     coreg: (string * (class * domain) list) list};
wenzelm@256: 
nipkow@189: fun rep_tsig (TySg comps) = comps;
clasohm@0: 
wenzelm@256: fun defaultS (TySg {default, ...}) = default;
wenzelm@256: 
wenzelm@256: 
wenzelm@416: (* error messages *)    (* FIXME move? *)
wenzelm@256: 
wenzelm@416: fun undcl_class c = "Undeclared class " ^ quote c;
wenzelm@256: val err_undcl_class = error o undcl_class;
clasohm@0: 
wenzelm@422: fun err_dup_classes cs =
wenzelm@422:   error ("Duplicate declaration of class(es) " ^ commas_quote cs);
wenzelm@416: 
wenzelm@416: fun undcl_type c = "Undeclared type constructor " ^ quote c;
wenzelm@256: val err_undcl_type = error o undcl_type;
wenzelm@256: 
wenzelm@416: fun err_dup_tycon c =
wenzelm@416:   error ("Duplicate declaration of type constructor " ^ quote c);
wenzelm@416: 
wenzelm@416: fun err_neg_args c =
wenzelm@416:   error ("Negative number of arguments of type constructor " ^ quote c);
wenzelm@416: 
wenzelm@416: fun err_dup_tyabbr c =
wenzelm@416:   error ("Duplicate declaration of type abbreviation " ^ quote c);
wenzelm@416: 
wenzelm@416: fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
wenzelm@416: val err_ty_confl = error o ty_confl;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'leq' checks the partial order on classes according to the
clasohm@0:    statements in the association list 'a' (i.e.'subclass')
clasohm@0: *)
clasohm@0: 
wenzelm@256: fun less a (C, D) = case assoc (a, C) of
clasohm@0:      Some(ss) => D mem ss
wenzelm@256:    | None => err_undcl_class (C) ;
clasohm@0: 
wenzelm@256: fun leq a (C, D)  =  C = D orelse less a (C, D);
clasohm@0: 
clasohm@0: 
wenzelm@416: (* logical_types *)
clasohm@0: 
wenzelm@416: (*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
wenzelm@416:   and c <= logic*)
clasohm@0: 
wenzelm@416: fun logical_types tsig =
wenzelm@416:   let
wenzelm@416:     val TySg {subclass, coreg, args, ...} = tsig;
wenzelm@416: 
wenzelm@416:     fun log_class c = leq subclass (c, logicC);
wenzelm@416:     fun log_type t = exists (log_class o #1) (assocs coreg t);
wenzelm@416:   in
wenzelm@416:     filter log_type (map #1 args)
clasohm@0:   end;
clasohm@0: 
nipkow@162: 
wenzelm@256: (* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
wenzelm@256:    S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
clasohm@0:    with C1 <= C2 (according to an association list 'a')
clasohm@0: *)
clasohm@0: 
wenzelm@256: fun sortorder a (S1, S2) =
wenzelm@256:   forall  (fn C2 => exists  (fn C1 => leq a (C1, C2))  S1)  S2;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
clasohm@0:   there exists no class in S which is <= C;
clasohm@0:   the resulting set is minimal if S was minimal
clasohm@0: *)
clasohm@0: 
wenzelm@256: fun inj a (C, S) =
clasohm@0:   let fun inj1 [] = [C]
wenzelm@256:         | inj1 (D::T) = if leq a (D, C) then D::T
wenzelm@256:                         else if leq a (C, D) then inj1 T
clasohm@0:                              else D::(inj1 T)
clasohm@0:   in inj1 S end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'union_sort' forms the minimal union set of two sorts S1 and S2
clasohm@0:    under the assumption that S2 is minimal *)
wenzelm@256: (* FIXME rename to inter_sort (?) *)
clasohm@0: 
clasohm@0: fun union_sort a = foldr (inj a);
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'elementwise_union' forms elementwise the minimal union set of two
clasohm@0:    sort lists under the assumption that the two lists have the same length
wenzelm@256: *)
clasohm@0: 
wenzelm@256: fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2);
wenzelm@256: 
clasohm@0: 
clasohm@0: (* 'lew' checks for two sort lists the ordering for all corresponding list
clasohm@0:    elements (i.e. sorts) *)
clasohm@0: 
wenzelm@256: fun lew a (w1, w2) = forall (sortorder a)  (w1~~w2);
wenzelm@256: 
clasohm@0: 
wenzelm@256: (* 'is_min' checks if a class C is minimal in a given sort S under the
wenzelm@256:    assumption that S contains C *)
clasohm@0: 
wenzelm@256: fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'min_sort' reduces a sort to its minimal classes *)
clasohm@0: 
clasohm@0: fun min_sort a S = distinct(filter (is_min a S) S);
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'min_domain' minimizes the domain sorts of type declarationsl;
wenzelm@256:    the function will be applied on the type declarations in extensions *)
clasohm@0: 
clasohm@0: fun min_domain subclass =
wenzelm@256:   let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
clasohm@0:   in map one_min end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
wenzelm@256:    and gives back a list of those range classes whose domains meet the
clasohm@0:    predicate 'pred' *)
wenzelm@256: 
clasohm@0: fun min_filter a pred ars =
wenzelm@256:   let fun filt ([], l) = l
wenzelm@256:         | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
wenzelm@256:                                else filt (xs, l)
wenzelm@256:   in filt (ars, []) end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'cod_above' filters all arities whose domains are elementwise >= than
wenzelm@256:    a given domain 'w' and gives back a list of the corresponding range
clasohm@0:    classes *)
clasohm@0: 
wenzelm@256: fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
wenzelm@256: 
wenzelm@256: 
clasohm@0: 
nipkow@200: (*Instantiation of type variables in types*)
nipkow@200: (*Pre: instantiations obey restrictions! *)
nipkow@200: fun inst_typ tye =
wenzelm@256:   let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
nipkow@200:         | inst(T as TFree _) = T
wenzelm@256:         | inst(T as TVar(v, _)) =
wenzelm@256:             (case assoc(tye, v) of Some U => inst U | None => T)
nipkow@200:   in inst end;
clasohm@0: 
clasohm@0: (* 'least_sort' returns for a given type its maximum sort:
clasohm@0:    - type variables, free types: the sort brought with
clasohm@0:    - type constructors: recursive determination of the maximum sort of the
wenzelm@256:                     arguments if the type is declared in 'coreg' of the
wenzelm@256:                     given type signature  *)
clasohm@0: 
wenzelm@256: fun least_sort (tsig as TySg{subclass, coreg, ...}) =
wenzelm@256:   let fun ls(T as Type(a, Ts)) =
wenzelm@256:                  (case assoc (coreg, a) of
wenzelm@256:                           Some(ars) => cod_above(subclass, map ls Ts, ars)
wenzelm@256:                         | None => raise TYPE(undcl_type a, [T], []))
wenzelm@256:         | ls(TFree(a, S)) = S
wenzelm@256:         | ls(TVar(a, S)) = S
clasohm@0:   in ls end;
clasohm@0: 
clasohm@0: 
wenzelm@256: fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =
wenzelm@256:   if sortorder subclass ((least_sort tsig T), S) then ()
wenzelm@256:   else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
clasohm@0: 
clasohm@0: 
clasohm@0: (*Instantiation of type variables in types *)
wenzelm@256: fun inst_typ_tvars(tsig, tye) =
wenzelm@256:   let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
wenzelm@256:         | inst(T as TFree _) = T
wenzelm@256:         | inst(T as TVar(v, S)) = (case assoc(tye, v) of
wenzelm@256:                 None => T | Some(U) => (check_has_sort(tsig, U, S); U))
clasohm@0:   in inst end;
clasohm@0: 
clasohm@0: (*Instantiation of type variables in terms *)
wenzelm@256: fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
nipkow@200: 
nipkow@200: 
nipkow@200: (* expand_typ *)
nipkow@200: 
wenzelm@256: fun expand_typ (TySg {abbrs, ...}) ty =
wenzelm@256:   let
wenzelm@256:     fun exptyp (Type (a, Ts)) =
wenzelm@256:           (case assoc (abbrs, a) of
wenzelm@256:             Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U)
wenzelm@256:           | None => Type (a, map exptyp Ts))
wenzelm@256:       | exptyp T = T
wenzelm@256:   in
wenzelm@256:     exptyp ty
wenzelm@256:   end;
wenzelm@256: 
wenzelm@256: 
wenzelm@256: (* norm_typ *)      (* FIXME norm sorts *)
wenzelm@256: 
wenzelm@256: val norm_typ = expand_typ;
wenzelm@256: 
wenzelm@256: 
wenzelm@256: 
wenzelm@256: (** type matching **)
nipkow@200: 
clasohm@0: exception TYPE_MATCH;
clasohm@0: 
wenzelm@256: (*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
wenzelm@256: fun typ_match tsig =
wenzelm@256:   let
wenzelm@256:     fun match (subs, (TVar (v, S), T)) =
wenzelm@256:           (case assoc (subs, v) of
wenzelm@256:             None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
wenzelm@256:               handle TYPE _ => raise TYPE_MATCH)
wenzelm@422:           | Some U => if U = T then subs else raise TYPE_MATCH)
wenzelm@256:       | match (subs, (Type (a, Ts), Type (b, Us))) =
wenzelm@256:           if a <> b then raise TYPE_MATCH
wenzelm@256:           else foldl match (subs, Ts ~~ Us)
wenzelm@422:       | match (subs, (TFree x, TFree y)) =
wenzelm@256:           if x = y then subs else raise TYPE_MATCH
wenzelm@256:       | match _ = raise TYPE_MATCH;
wenzelm@256:   in match end;
clasohm@0: 
clasohm@0: 
wenzelm@256: fun typ_instance (tsig, T, U) =
wenzelm@256:   (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
wenzelm@256: 
wenzelm@256: 
wenzelm@256: 
wenzelm@256: (** build type signatures **)
wenzelm@256: 
wenzelm@416: fun make_tsig (classes, subclass, default, args, abbrs, coreg) =
wenzelm@416:   TySg {classes = classes, subclass = subclass, default = default,
wenzelm@416:     args = args, abbrs = abbrs, coreg = coreg};
wenzelm@416: 
wenzelm@416: val tsig0 = make_tsig ([], [], [], [], [], []);
wenzelm@256: 
clasohm@0: 
wenzelm@401: (* sorts *)
wenzelm@401: 
wenzelm@416: fun subsort (TySg {subclass, ...}) (S1, S2) =
wenzelm@416:   sortorder subclass (S1, S2);
wenzelm@416: 
wenzelm@401: fun norm_sort (TySg {subclass, ...}) S =
wenzelm@401:   sort_strings (min_sort subclass S);
wenzelm@401: 
wenzelm@416: fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
wenzelm@416:   | rem_sorts (TFree (x, _)) = TFree (x, [])
wenzelm@416:   | rem_sorts (TVar (xi, _)) = TVar (xi, []);
wenzelm@401: 
wenzelm@401: 
clasohm@0: 
clasohm@0: fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
clasohm@0: 
wenzelm@256: fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
clasohm@0: 
clasohm@0: 
wenzelm@416: (* typ_errors *)
wenzelm@256: 
wenzelm@416: (*check validity of (not necessarily normal) type; accumulate error messages*)
wenzelm@256: 
wenzelm@416: fun typ_errors tsig (typ, errors) =
wenzelm@256:   let
wenzelm@416:     val TySg {classes, args, abbrs, ...} = tsig;
wenzelm@416: 
wenzelm@416:     fun class_err (errs, c) =
wenzelm@416:       if c mem classes then errs
wenzelm@416:       else undcl_class c ins errs;
wenzelm@256: 
wenzelm@256:     val sort_err = foldl class_err;
clasohm@0: 
wenzelm@256:     fun typ_errs (Type (c, Us), errs) =
wenzelm@256:           let
wenzelm@256:             val errs' = foldr typ_errs (Us, errs);
wenzelm@256:             fun nargs n =
wenzelm@256:               if n = length Us then errs'
wenzelm@416:               else ("Wrong number of arguments: " ^ quote c) ins errs';
wenzelm@256:           in
wenzelm@256:             (case assoc (args, c) of
wenzelm@256:               Some n => nargs n
wenzelm@256:             | None =>
wenzelm@256:                 (case assoc (abbrs, c) of
wenzelm@256:                   Some (vs, _) => nargs (length vs)
wenzelm@416:                 | None => undcl_type c ins errs))
wenzelm@256:           end
wenzelm@256:     | typ_errs (TFree (_, S), errs) = sort_err (errs, S)
wenzelm@416:     | typ_errs (TVar ((x, i), S), errs) =
wenzelm@416:         if i < 0 then
wenzelm@416:           ("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
wenzelm@416:         else sort_err (errs, S);
wenzelm@256:   in
wenzelm@416:     typ_errs (typ, errors)
wenzelm@256:   end;
wenzelm@256: 
wenzelm@256: 
wenzelm@256: (* cert_typ *)
wenzelm@256: 
wenzelm@256: (*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
wenzelm@256: 
wenzelm@256: fun cert_typ tsig ty =
wenzelm@256:   (case typ_errors tsig (ty, []) of
wenzelm@256:     [] => norm_typ tsig ty
wenzelm@256:   | errs => raise_type (cat_lines errs) [ty] []);
wenzelm@256: 
wenzelm@256: 
wenzelm@256: 
wenzelm@422: (** merge type signatures **)
wenzelm@256: 
wenzelm@422: (*'assoc_union' merges two association lists if the contents associated
wenzelm@422:   the keys are lists*)
clasohm@0: 
wenzelm@422: fun assoc_union (as1, []) = as1
wenzelm@422:   | assoc_union (as1, (key, l2) :: as2) =
wenzelm@422:       (case assoc (as1, key) of
wenzelm@422:         Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2)
wenzelm@422:       | None => assoc_union ((key, l2) :: as1, as2));
clasohm@0: 
clasohm@0: 
wenzelm@422: (* merge subclass *)
clasohm@0: 
wenzelm@422: fun merge_subclass (subclass1, subclass2) =
wenzelm@422:   let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in
wenzelm@422:     if exists (op mem) subclass then
wenzelm@422:       error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
wenzelm@422:     else subclass
wenzelm@416:   end;
wenzelm@416: 
wenzelm@416: 
wenzelm@422: (* coregularity *)
clasohm@0: 
clasohm@0: (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
clasohm@0: 
wenzelm@256: fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of
clasohm@0:       Some(w1) => if w = w1 then () else
wenzelm@256:         error("There are two declarations\n" ^
wenzelm@416:               str_of_arity(t, w, [s]) ^ " and\n" ^
wenzelm@416:               str_of_arity(t, w1, [s]) ^ "\n" ^
clasohm@0:               "with the same result class.")
clasohm@0:     | None => ();
clasohm@0: 
clasohm@0: (* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
clasohm@0:    such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
clasohm@0: 
wenzelm@256: fun subs (classes, subclass) C =
wenzelm@256:   let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl
wenzelm@256:   in foldl sub ([], classes) end;
clasohm@0: 
wenzelm@256: fun coreg_err(t, (w1, C), (w2, D)) =
wenzelm@416:     error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and "
wenzelm@416:                           ^ str_of_arity(t, w2, [D]) ^ " are in conflict");
clasohm@0: 
wenzelm@256: fun restr2 classes (subclass, coreg) (t, (s, w)) =
wenzelm@256:   let fun restr ([], test) = ()
wenzelm@416:         | restr (s1::Ss, test) =
wenzelm@416:             (case assoc2 (coreg, (t, s1)) of
wenzelm@416:               Some dom =>
wenzelm@416:                 if lew subclass (test (w, dom))
wenzelm@416:                 then restr (Ss, test)
wenzelm@416:                 else coreg_err (t, (w, s), (dom, s1))
wenzelm@256:             | None => restr (Ss, test))
wenzelm@256:       fun forward (t, (s, w)) =
wenzelm@256:         let val s_sups = case assoc (subclass, s) of
wenzelm@256:                    Some(s_sups) => s_sups | None => err_undcl_class(s);
wenzelm@256:         in restr (s_sups, I) end
wenzelm@256:       fun backward (t, (s, w)) =
wenzelm@256:         let val s_subs = subs (classes, subclass) s
wenzelm@256:         in restr (s_subs, fn (x, y) => (y, x)) end
wenzelm@256:   in (backward (t, (s, w)); forward (t, (s, w))) end;
clasohm@0: 
clasohm@0: 
wenzelm@256: fun varying_decls t =
wenzelm@256:   error ("Type constructor " ^ quote t ^ " has varying number of arguments");
clasohm@0: 
clasohm@0: 
wenzelm@422: (* 'merge_coreg' builds the union of two 'coreg' lists;
wenzelm@422:    it only checks the two restriction conditions and inserts afterwards
wenzelm@422:    all elements of the second list into the first one *)
wenzelm@422: 
wenzelm@422: fun merge_coreg classes subclass1 =
wenzelm@422:   let fun test_ar classes (t, ars1) (coreg1, (s, w)) =
wenzelm@422:         (is_unique_decl coreg1 (t, (s, w));
wenzelm@422:          restr2 classes (subclass1, coreg1) (t, (s, w));
wenzelm@422:          overwrite (coreg1, (t, (s, w) ins ars1)));
wenzelm@422: 
wenzelm@422:       fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of
wenzelm@422:           Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)
wenzelm@422:         | None => c::coreg1
wenzelm@422:   in foldl merge_c end;
wenzelm@422: 
wenzelm@422: fun merge_args (args, (t, n)) =
wenzelm@422:   (case assoc (args, t) of
wenzelm@422:     Some m => if m = n then args else varying_decls t
wenzelm@422:   | None => (t, n) :: args);
wenzelm@422: 
wenzelm@422: (* FIXME raise TERM *)
wenzelm@422: fun merge_abbrs (abbrs1, abbrs2) =
wenzelm@422:   let
wenzelm@422:     val abbrs = abbrs1 union abbrs2;
wenzelm@422:     val names = map fst abbrs;
wenzelm@422:   in
wenzelm@422:     (case duplicates names of
wenzelm@422:       [] => abbrs
wenzelm@422:     | dups => error ("Duplicate declaration of type abbreviations: " ^
wenzelm@422:         commas_quote dups))
wenzelm@422:   end;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (* 'merge_tsigs' takes the above declared functions to merge two type
wenzelm@422:   signatures *)
wenzelm@422: 
wenzelm@422: fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,
wenzelm@422:            coreg=coreg1, abbrs=abbrs1},
wenzelm@422:           TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,
wenzelm@422:            coreg=coreg2, abbrs=abbrs2}) =
wenzelm@422:   let val classes' = classes1 union classes2;
wenzelm@422:       val subclass' = merge_subclass (subclass1, subclass2);
wenzelm@422:       val args' = foldl merge_args (args1, args2)
wenzelm@422:       val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);
wenzelm@422:       val default' = min_sort subclass' (default1 @ default2);
wenzelm@422:       val abbrs' = merge_abbrs(abbrs1, abbrs2);
wenzelm@422:   in TySg{classes=classes' , default=default', subclass=subclass', args=args',
wenzelm@422:           coreg=coreg' , abbrs = abbrs' }
wenzelm@422:   end;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (*** extend type signatures ***)
wenzelm@422: 
wenzelm@422: (** add classes **)
wenzelm@422: 
wenzelm@422: (* FIXME use? *)
wenzelm@422: fun add_classes classes cs =
wenzelm@422:   (case cs inter classes of
wenzelm@422:     [] => cs @ classes
wenzelm@422:   | dups => err_dup_classes cs);
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (* 'add_class' adds a new class to the list of all existing classes *)
wenzelm@422: 
wenzelm@422: fun add_class (classes, (s, _)) =
wenzelm@422:   if s mem classes then error("Class " ^ s ^ " declared twice.")
wenzelm@422:   else s :: classes;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (*'add_subclass' adds a tuple consisting of a new class (the new class has
wenzelm@422:   already been inserted into the 'classes' list) and its superclasses (they
wenzelm@422:   must be declared in 'classes' too) to the 'subclass' list of the given type
wenzelm@422:   signature; furthermore all inherited superclasses according to the
wenzelm@422:   superclasses brought with are inserted and there is a check that there are
wenzelm@422:   no cycles (i.e. C <= D <= C, with C <> D);*)
wenzelm@422: 
wenzelm@422: fun add_subclass classes (subclass, (s, ges)) =
wenzelm@422: let fun upd (subclass, s') = if s' mem classes then
wenzelm@422:         let val ges' = the (assoc (subclass, s))
wenzelm@422:         in case assoc (subclass, s') of
wenzelm@422:              Some sups => if s mem sups
wenzelm@422:                            then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
wenzelm@422:                            else overwrite (subclass, (s, sups union ges'))
wenzelm@422:            | None => subclass
wenzelm@422:          end
wenzelm@422:          else err_undcl_class(s')
wenzelm@422: in foldl upd (subclass@[(s, ges)], ges) end;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (* 'extend_classes' inserts all new classes into the corresponding
wenzelm@422:    lists ('classes', 'subclass') if possible *)
wenzelm@422: 
wenzelm@422: fun extend_classes (classes, subclass, newclasses) =
wenzelm@422:   if newclasses = [] then (classes, subclass) else
wenzelm@422:   let val classes' = foldl add_class (classes, newclasses);
wenzelm@422:       val subclass' = foldl (add_subclass classes') (subclass, newclasses);
wenzelm@422:   in (classes', subclass') end;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (* ext_tsig_subclass *)
wenzelm@422: 
wenzelm@422: fun ext_tsig_subclass tsig pairs =
wenzelm@422:   let
wenzelm@422:     val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
wenzelm@422: 
wenzelm@422:     (* FIXME clean! *)
wenzelm@422:     val subclass' =
wenzelm@422:       merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
wenzelm@422:   in
wenzelm@422:     make_tsig (classes, subclass', default, args, abbrs, coreg)
wenzelm@422:   end;
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (* ext_tsig_defsort *)
wenzelm@422: 
wenzelm@422: fun ext_tsig_defsort (TySg {classes, subclass, args, abbrs, coreg, ...}) default =
wenzelm@422:   make_tsig (classes, subclass, default, args, abbrs, coreg);
wenzelm@422: 
wenzelm@422: 
wenzelm@422: 
wenzelm@422: (** add arities **)
wenzelm@422: 
clasohm@0: (* 'coregular' checks
clasohm@0:    - the two restriction conditions 'is_unique_decl' and 'restr2'
wenzelm@256:    - if the classes in the new type declarations are known in the
clasohm@0:      given type signature
clasohm@0:    - if one type constructor has always the same number of arguments;
wenzelm@256:    if one type declaration has passed all checks it is inserted into
clasohm@0:    the 'coreg' association list of the given type signatrure  *)
clasohm@0: 
wenzelm@256: fun coregular (classes, subclass, args) =
wenzelm@256:   let fun ex C = if C mem classes then () else err_undcl_class(C);
clasohm@0: 
wenzelm@256:       fun addar(w, C) (coreg, t) = case assoc(args, t) of
clasohm@0:             Some(n) => if n <> length w then varying_decls(t) else
wenzelm@256:                      (is_unique_decl coreg (t, (C, w));
wenzelm@256:                       (seq o seq) ex w;
wenzelm@256:                       restr2 classes (subclass, coreg) (t, (C, w));
wenzelm@416:                       let val ars = the (assoc(coreg, t))
wenzelm@256:                       in overwrite(coreg, (t, (C, w) ins ars)) end)
wenzelm@256:           | None => err_undcl_type(t);
clasohm@0: 
wenzelm@256:       fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)
clasohm@0: 
clasohm@0:   in addts end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'close' extends the 'coreg' association list after all new type
clasohm@0:    declarations have been inserted successfully:
clasohm@0:    for every declaration t:(Ss)C , for all classses D with C <= D:
clasohm@0:       if there is no declaration t:(Ss')C' with C < C' and C' <= D
clasohm@0:       then insert the declaration t:(Ss)D into 'coreg'
clasohm@0:    this means, if there exists a declaration t:(Ss)C and there is
clasohm@0:    no declaration t:(Ss')D with C <=D then the declaration holds
wenzelm@256:    for all range classes more general than C *)
wenzelm@256: 
wenzelm@256: fun close (coreg, subclass) =
wenzelm@256:   let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
clasohm@0:           Some(sups) =>
wenzelm@256:             let fun close_sup (l, sup) =
wenzelm@256:                   if exists (fn s'' => less subclass (s, s'') andalso
wenzelm@256:                                        leq subclass (s'', sup)) sl
clasohm@0:                   then l
wenzelm@256:                   else (sup, dom)::l
wenzelm@256:             in foldl close_sup (l, sups) end
clasohm@0:         | None => l;
wenzelm@256:       fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
clasohm@0:   in map ext coreg end;
clasohm@0: 
wenzelm@422: 
wenzelm@422: (** add types **)
wenzelm@422: 
wenzelm@416: fun add_types (aca, (ts, n)) =
wenzelm@416:   let
wenzelm@416:     fun add_type ((args, coreg, abbrs), t) =
wenzelm@416:       case assoc(args, t) of              (* FIXME from new *)
wenzelm@416:         Some _ => twice(t)
wenzelm@416:       | None =>
wenzelm@416:           (case assoc(abbrs, t) of
wenzelm@416:             Some _ => tyab_conflict(t)
wenzelm@416:           | None => ((t, n)::args, (t, [])::coreg, abbrs))
wenzelm@416:   in
wenzelm@416:     if n < 0 then     (* FIXME err_neg_args *)
wenzelm@416:       error ("Type constructor cannot have negative number of arguments")
wenzelm@416:     else foldl add_type (aca, ts)
clasohm@0:   end;
clasohm@0: 
wenzelm@256: 
wenzelm@422: 
wenzelm@422: (** add type abbreviations **)
wenzelm@256: 
wenzelm@416: fun abbr_errors tsig (a, (lhs_vs, rhs)) =
wenzelm@416:   let
wenzelm@416:     val TySg {args, abbrs, ...} = tsig;
wenzelm@416:     val rhs_vs = map #1 (typ_tvars rhs);
wenzelm@416:     val show_idxs = commas_quote o map fst;
wenzelm@416: 
wenzelm@416:     val dup_lhs_vars =
wenzelm@416:       (case duplicates lhs_vs of
wenzelm@416:         [] => []
wenzelm@416:       | vs => ["Duplicate variables on lhs: " ^ show_idxs vs]);
wenzelm@416: 
wenzelm@416:     val extra_rhs_vars =
wenzelm@416:       (case gen_rems (op =) (rhs_vs, lhs_vs) of
wenzelm@416:         [] => []
wenzelm@416:       | vs => ["Extra variables on rhs: " ^ show_idxs vs]);
wenzelm@416: 
wenzelm@416:     val tycon_confl =
wenzelm@416:       if is_none (assoc (args, a)) then []
wenzelm@416:       else [ty_confl a];
wenzelm@416: 
wenzelm@416:     val dup_abbr =
wenzelm@416:       if is_none (assoc (abbrs, a)) then []
wenzelm@416:       else ["Duplicate declaration of abbreviation"];
wenzelm@416:   in
wenzelm@416:     dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
wenzelm@416:       typ_errors tsig (rhs, [])
wenzelm@416:   end;
wenzelm@416: 
wenzelm@416: fun add_abbr (tsig, abbr as (a, _)) =
wenzelm@422:   let val TySg {classes, subclass, default, args, coreg, abbrs} = tsig in
wenzelm@416:     (case abbr_errors tsig abbr of
wenzelm@416:       [] => make_tsig (classes, subclass, default, args, abbr :: abbrs, coreg)
wenzelm@416:     | errs => (seq writeln errs;
wenzelm@416:         error ("The error(s) above occurred in type abbreviation " ^ quote a)))
wenzelm@416:   end;
wenzelm@416: 
wenzelm@416: fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);
wenzelm@416: 
wenzelm@416: 
nipkow@200: 
wenzelm@256: (* 'extend_tsig' takes the above described check- and extend-functions to
clasohm@0:    extend a given type signature with new classes and new type declarations *)
clasohm@0: 
wenzelm@256: fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs})
wenzelm@256:             (newclasses, newdefault, types, arities) =
wenzelm@416:   let
wenzelm@416:     val (classes', subclass') = extend_classes(classes, subclass, newclasses);
wenzelm@256:     val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types);
wenzelm@422: 
clasohm@0:     val old_coreg = map #1 coreg;
wenzelm@416:     val coreg'' =
wenzelm@416:       foldl (coregular (classes', subclass', args'))
wenzelm@416:         (coreg', min_domain subclass' arities);
wenzelm@256:     val coreg''' = close (coreg'', subclass');
wenzelm@422: 
clasohm@0:     val default' = if null newdefault then default else newdefault;
wenzelm@416:   in
wenzelm@416:     TySg {classes = classes', subclass = subclass', default = default',
wenzelm@416:       args = args', coreg = coreg''', abbrs = abbrs}
wenzelm@416:   end;
clasohm@0: 
clasohm@0: 
wenzelm@416: 
wenzelm@416: 
wenzelm@416: (*** type unification and inference ***)
clasohm@0: 
clasohm@0: (*
clasohm@0: 
clasohm@0: Input:
clasohm@0: - a 'raw' term which contains only dummy types and some explicit type
clasohm@0:   constraints encoded as terms.
clasohm@0: - the expected type of the term.
clasohm@0: 
clasohm@0: Output:
clasohm@0: - the correctly typed term
clasohm@0: - the substitution needed to unify the actual type of the term with its
clasohm@0:   expected type; only the TVars in the expected type are included.
clasohm@0: 
clasohm@0: During type inference all TVars in the term have negative index. This keeps
clasohm@0: them apart from normal TVars, which is essential, because at the end the type
clasohm@0: of the term is unified with the expected type, which contains normal TVars.
clasohm@0: 
wenzelm@565: 1. Add initial type information to the term (attach_types).
clasohm@0:    This freezes (freeze_vars) TVars in explicitly provided types (eg
clasohm@0:    constraints or defaults) by turning them into TFrees.
clasohm@0: 2. Carry out type inference, possibly introducing new negative TVars.
clasohm@0: 3. Unify actual and expected type.
clasohm@0: 4. Turn all (negative) TVars into unique new TFrees (freeze).
clasohm@0: 5. Thaw all TVars frozen in step 1 (thaw_vars).
clasohm@0: 
clasohm@0: *)
clasohm@0: 
clasohm@0: (*Raised if types are not unifiable*)
clasohm@0: exception TUNIFY;
clasohm@0: 
clasohm@0: val tyvar_count = ref(~1);
clasohm@0: 
clasohm@0: fun tyinit() = (tyvar_count := ~1);
clasohm@0: 
clasohm@0: fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
clasohm@0: 
clasohm@0: (*
clasohm@0: Generate new TVar.  Index is < ~1 to distinguish it from TVars generated from
clasohm@0: variable names (see id_type).  Name is arbitrary because index is new.
clasohm@0: *)
clasohm@0: 
wenzelm@256: fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
clasohm@0: 
clasohm@0: (*Occurs check: type variable occurs in type?*)
clasohm@0: fun occ v tye =
wenzelm@256:   let fun occ(Type(_, Ts)) = exists occ Ts
clasohm@0:         | occ(TFree _) = false
wenzelm@256:         | occ(TVar(w, _)) = v=w orelse
wenzelm@256:                            (case assoc(tye, w) of
clasohm@0:                               None   => false
clasohm@0:                             | Some U => occ U);
clasohm@0:   in occ end;
clasohm@0: 
wenzelm@256: (*Chase variable assignments in tye.
wenzelm@256:   If devar (T, tye) returns a type var then it must be unassigned.*)
wenzelm@256: fun devar (T as TVar(v, _), tye) = (case  assoc(tye, v)  of
wenzelm@256:           Some U =>  devar (U, tye)
clasohm@0:         | None   =>  T)
wenzelm@256:   | devar (T, tye) = T;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'dom' returns for a type constructor t the list of those domains
clasohm@0:    which deliver a given range class C *)
clasohm@0: 
wenzelm@256: fun dom coreg t C = case assoc2 (coreg, (t, C)) of
clasohm@0:     Some(Ss) => Ss
clasohm@0:   | None => raise TUNIFY;
clasohm@0: 
clasohm@0: 
clasohm@0: (* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
clasohm@0:    (i.e. a set of range classes ); the union is carried out elementwise
clasohm@0:    for the seperate sorts in the domains *)
clasohm@0: 
wenzelm@256: fun Dom (subclass, coreg) (t, S) =
clasohm@0:   let val domlist = map (dom coreg t) S;
clasohm@0:   in if null domlist then []
wenzelm@256:      else foldl (elementwise_union subclass) (hd domlist, tl domlist)
clasohm@0:   end;
clasohm@0: 
clasohm@0: 
wenzelm@256: fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =
wenzelm@256:   let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
wenzelm@256:       fun Wk(T as TVar(v, S')) =
wenzelm@256:               if sortorder subclass (S', S) then tye
wenzelm@256:               else (v, gen_tyvar(union_sort subclass (S', S)))::tye
wenzelm@256:         | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
wenzelm@256:                                  else raise TUNIFY
wenzelm@256:         | Wk(T as Type(f, Ts)) =
wenzelm@256:            if null S then tye
wenzelm@256:            else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)
clasohm@0:   in Wk(T) end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* Order-sorted Unification of Types (U)  *)
clasohm@0: 
clasohm@0: (* Precondition: both types are well-formed w.r.t. type constructor arities *)
wenzelm@256: fun unify (tsig as TySg{subclass, coreg, ...}) =
wenzelm@256:   let fun unif ((T, U), tye) =
wenzelm@256:         case (devar(T, tye), devar(U, tye)) of
wenzelm@256:           (T as TVar(v, S1), U as TVar(w, S2)) =>
clasohm@0:              if v=w then tye else
wenzelm@256:              if sortorder subclass (S1, S2) then (w, T)::tye else
wenzelm@256:              if sortorder subclass (S2, S1) then (v, U)::tye
wenzelm@256:              else let val nu = gen_tyvar (union_sort subclass (S1, S2))
wenzelm@256:                   in (v, nu)::(w, nu)::tye end
wenzelm@256:         | (T as TVar(v, S), U) =>
wenzelm@256:              if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
wenzelm@256:         | (U, T as TVar (v, S)) =>
wenzelm@256:              if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
wenzelm@256:         | (Type(a, Ts), Type(b, Us)) =>
wenzelm@256:              if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
wenzelm@256:         | (T, U) => if T=U then tye else raise TUNIFY
clasohm@0:   in unif end;
clasohm@0: 
clasohm@0: 
wenzelm@450: (* raw_unify (ignores sorts) *)
wenzelm@450: 
wenzelm@450: fun raw_unify (ty1, ty2) =
wenzelm@450:   (unify tsig0 ((rem_sorts ty1, rem_sorts ty2), []); true)
wenzelm@450:     handle TUNIFY => false;
wenzelm@450: 
wenzelm@450: 
clasohm@0: (*Type inference for polymorphic term*)
clasohm@0: fun infer tsig =
wenzelm@256:   let fun inf(Ts, Const (_, T), tye) = (T, tye)
wenzelm@256:         | inf(Ts, Free  (_, T), tye) = (T, tye)
wenzelm@256:         | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
clasohm@0:           handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
wenzelm@256:         | inf(Ts, Var (_, T), tye) = (T, tye)
wenzelm@256:         | inf(Ts, Abs (_, T, body), tye) =
wenzelm@256:             let val (U, tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
clasohm@0:         | inf(Ts, f$u, tye) =
wenzelm@256:             let val (U, tyeU) = inf(Ts, u, tye);
wenzelm@256:                 val (T, tyeT) = inf(Ts, f, tyeU);
clasohm@0:                 fun err s =
clasohm@0:                   raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
wenzelm@256:             in case T of
wenzelm@256:                  Type("fun", [T1, T2]) =>
wenzelm@256:                    ( (T2, unify tsig ((T1, U), tyeT))
clasohm@0:                      handle TUNIFY => err"type mismatch in application" )
wenzelm@256:                | TVar _ =>
clasohm@0:                    let val T2 = gen_tyvar([])
clasohm@0:                    in (T2, unify tsig ((T, U-->T2), tyeT))
clasohm@0:                       handle TUNIFY => err"type mismatch in application"
clasohm@0:                    end
clasohm@0:                | _ => err"rator must have function type"
clasohm@0:            end
clasohm@0:   in inf end;
clasohm@0: 
wenzelm@256: fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)
clasohm@0:   | freeze_vars(T as TFree _) = T
wenzelm@256:   | freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);
clasohm@0: 
clasohm@0: (* Attach a type to a constant *)
wenzelm@256: fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
clasohm@0: 
clasohm@0: (*Find type of ident.  If not in table then use ident's name for tyvar
clasohm@0:   to get consistent typing.*)
wenzelm@256: fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
wenzelm@256: fun type_of_ixn(types, ixn as (a, _)) =
wenzelm@565:   case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
wenzelm@565: 
wenzelm@565: fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
clasohm@0: 
wenzelm@565: fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
wenzelm@565:   | constrainAbs _ = sys_error "constrainAbs";
wenzelm@256: 
clasohm@0: 
wenzelm@565: (* attach_types *)
wenzelm@565: 
clasohm@0: (*
wenzelm@256:   Attach types to a term. Input is a "parse tree" containing dummy types.
wenzelm@256:   Type constraints are translated and checked for validity wrt tsig. TVars in
wenzelm@256:   constraints are frozen.
clasohm@0: 
wenzelm@256:   The atoms in the resulting term satisfy the following spec:
clasohm@0: 
wenzelm@256:   Const (a, T):
wenzelm@256:     T is a renamed copy of the generic type of a; renaming decreases index of
wenzelm@256:     all TVars by new_tvar_inx(), which is less than ~1. The index of all
wenzelm@256:     TVars in the generic type must be 0 for this to work!
clasohm@0: 
wenzelm@256:   Free (a, T), Var (ixn, T):
wenzelm@256:     T is either the frozen default type of a or TVar (("'"^a, ~1), [])
clasohm@0: 
wenzelm@256:   Abs (a, T, _):
wenzelm@256:     T is either a type constraint or TVar (("'" ^ a, i), []), where i is
wenzelm@256:     generated by new_tvar_inx(). Thus different abstractions can have the
wenzelm@256:     bound variables of the same name but different types.
clasohm@0: *)
clasohm@0: 
wenzelm@565: (* FIXME consitency of sort_env / sorts (!?) *)
wenzelm@256: 
wenzelm@565: (* FIXME check *)
wenzelm@565: 
wenzelm@565: fun attach_types (tsig, const_type, types, sorts) tm =
wenzelm@256:   let
wenzelm@565:     val sort_env = Syntax.raw_term_sorts tm;
wenzelm@565:     fun def_sort xi = if_none (sorts xi) (defaultS tsig);
wenzelm@256: 
wenzelm@565:     fun prepareT t =
wenzelm@565:       freeze_vars (cert_typ tsig (Syntax.typ_of_term sort_env def_sort t));
wenzelm@256: 
wenzelm@256:     fun add (Const (a, _)) =
wenzelm@565:           (case const_type a of
wenzelm@256:             Some T => type_const (a, T)
wenzelm@256:           | None => raise_type ("No such constant: " ^ quote a) [] [])
wenzelm@256:       | add (Free (a, _)) =
wenzelm@565:           (case const_type a of
wenzelm@256:             Some T => type_const (a, T)
wenzelm@256:           | None => Free (a, type_of_ixn (types, (a, ~1))))
wenzelm@256:       | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
wenzelm@565:       | add (Bound i) = Bound i
wenzelm@256:       | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
wenzelm@256:       | add ((f as Const (a, _) $ t1) $ t2) =
wenzelm@256:           if a = Syntax.constrainC then
wenzelm@256:             constrain (add t1, prepareT t2)
wenzelm@256:           else if a = Syntax.constrainAbsC then
wenzelm@256:             constrainAbs (add t1, prepareT t2)
wenzelm@256:           else add f $ add t2
wenzelm@256:       | add (f $ t) = add f $ add t;
wenzelm@565:   in add tm end;
clasohm@0: 
clasohm@0: 
clasohm@0: (* Post-Processing *)
clasohm@0: 
clasohm@0: (*Instantiation of type variables in terms*)
clasohm@0: fun inst_types tye = map_term_types (inst_typ tye);
clasohm@0: 
clasohm@0: (*Delete explicit constraints -- occurrences of "_constrain" *)
wenzelm@256: fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
wenzelm@256:   | unconstrain ((f as Const(a, _)) $ t) =
clasohm@0:       if a=Syntax.constrainC then unconstrain t
clasohm@0:       else unconstrain f $ unconstrain t
clasohm@0:   | unconstrain (f$t) = unconstrain f $ unconstrain t
clasohm@0:   | unconstrain (t) = t;
clasohm@0: 
clasohm@0: 
clasohm@0: (* Turn all TVars which satisfy p into new TFrees *)
clasohm@0: fun freeze p t =
wenzelm@256:   let val fs = add_term_tfree_names(t, []);
wenzelm@256:       val inxs = filter p (add_term_tvar_ixns(t, []));
clasohm@0:       val vmap = inxs ~~ variantlist(map #1 inxs, fs);
wenzelm@256:       fun free(Type(a, Ts)) = Type(a, map free Ts)
wenzelm@256:         | free(T as TVar(v, S)) =
wenzelm@256:             (case assoc(vmap, v) of None => T | Some(a) => TFree(a, S))
clasohm@0:         | free(T as TFree _) = T
clasohm@0:   in map_term_types free t end;
clasohm@0: 
clasohm@0: (* Thaw all TVars that were frozen in freeze_vars *)
wenzelm@256: fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)
wenzelm@256:   | thaw_vars(T as TFree(a, S)) = (case explode a of
wenzelm@256:           "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
wenzelm@256:                           in TVar(("'"^b, i), S) end
wenzelm@256:         | _ => T)
clasohm@0:   | thaw_vars(T) = T;
clasohm@0: 
clasohm@0: 
clasohm@0: fun restrict tye =
wenzelm@256:   let fun clean(tye1, ((a, i), T)) =
wenzelm@256:         if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1
wenzelm@256:   in foldl clean ([], tye) end
clasohm@0: 
clasohm@0: 
clasohm@0: (*Infer types for term t using tables. Check that t's type and T unify *)
clasohm@0: 
wenzelm@565: fun infer_term (tsig, const_type, types, sorts, T, t) =
wenzelm@565:   let
wenzelm@565:     val u = attach_types (tsig, const_type, types, sorts) t;
wenzelm@565:     val (U, tye) = infer tsig ([], u, []);
wenzelm@565:     val uu = unconstrain u;
wenzelm@565:     val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
wenzelm@565:       ("Term does not have expected type", [T, U], [inst_types tye uu])
wenzelm@565:     val Ttye = restrict tye' (*restriction to TVars in T*)
wenzelm@565:     val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
wenzelm@565:       (*all is a dummy term which contains all exported TVars*)
wenzelm@565:     val Const(_, Type(_, Ts)) $ u'' =
wenzelm@565:       map_term_types thaw_vars (freeze (fn (_, i) => i < 0) all)
wenzelm@565:       (*turn all internally generated TVars into TFrees
wenzelm@565:         and thaw all initially frozen TVars*)
wenzelm@565:   in
wenzelm@565:     (u'', (map fst Ttye) ~~ Ts)
wenzelm@565:   end;
clasohm@0: 
clasohm@0: fun infer_types args = (tyinit(); infer_term args);
clasohm@0: 
clasohm@0: 
clasohm@0: (* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
wenzelm@256: fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)
wenzelm@256:   | varifyT (TFree (a, S)) = TVar ((a, 0), S)
wenzelm@256:   | varifyT T = T;
clasohm@0: 
clasohm@0: (* Turn TFrees except those in fixed into new TVars *)
wenzelm@256: fun varify (t, fixed) =
wenzelm@256:   let val fs = add_term_tfree_names(t, []) \\ fixed;
wenzelm@256:       val ixns = add_term_tvar_ixns(t, []);
clasohm@0:       val fmap = fs ~~ variantlist(fs, map #1 ixns)
wenzelm@256:       fun thaw(Type(a, Ts)) = Type(a, map thaw Ts)
clasohm@0:         | thaw(T as TVar _) = T
wenzelm@256:         | thaw(T as TFree(a, S)) =
wenzelm@256:             (case assoc(fmap, a) of None => T | Some b => TVar((b, 0), S))
clasohm@0:   in map_term_types thaw t end;
clasohm@0: 
clasohm@0: 
clasohm@0: end;
wenzelm@256: