src/Pure/type.ML
author wenzelm
Tue Dec 18 02:18:38 2001 +0100 (2001-12-18 ago)
changeset 12528 b8bc541a4544
parent 12501 36b2ac65e18d
child 12726 5ae4034883d5
permissions -rw-r--r--
tuned interface of unify, param;
added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;
     1 (*  Title:      Pure/type.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Lawrence C Paulson
     4 
     5 Type signatures, unification of types, interface to type inference.
     6 *)
     7 
     8 signature TYPE =
     9 sig
    10   (*TFrees and TVars*)
    11   val no_tvars: typ -> typ
    12   val varifyT: typ -> typ
    13   val unvarifyT: typ -> typ
    14   val varify: term * string list -> term * (string * indexname) list
    15   val freeze_thaw_type : typ -> typ * (typ -> typ)
    16   val freeze_thaw : term -> term * (term -> term)
    17 
    18   (*type signatures*)
    19   type type_sig
    20   val rep_tsig: type_sig ->
    21     {classes: class list,
    22      classrel: Sorts.classrel,
    23      default: sort,
    24      tycons: int Symtab.table,
    25      log_types: string list,
    26      univ_witness: (typ * sort) option,
    27      abbrs: (string list * typ) Symtab.table,
    28      arities: Sorts.arities}
    29   val classes: type_sig -> class list
    30   val defaultS: type_sig -> sort
    31   val logical_types: type_sig -> string list
    32   val univ_witness: type_sig -> (typ * sort) option
    33   val subsort: type_sig -> sort * sort -> bool
    34   val eq_sort: type_sig -> sort * sort -> bool
    35   val norm_sort: type_sig -> sort -> sort
    36   val cert_class: type_sig -> class -> class
    37   val cert_sort: type_sig -> sort -> sort
    38   val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
    39   val rem_sorts: typ -> typ
    40   val tsig0: type_sig
    41   val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
    42   val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
    43   val ext_tsig_defsort: type_sig -> sort -> type_sig
    44   val ext_tsig_types: type_sig -> (string * int) list -> type_sig
    45   val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
    46   val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
    47   val merge_tsigs: type_sig * type_sig -> type_sig
    48   val typ_errors: type_sig -> typ * string list -> string list
    49   val cert_typ: type_sig -> typ -> typ
    50   val cert_typ_no_norm: type_sig -> typ -> typ
    51   val norm_typ: type_sig -> typ -> typ
    52   val norm_term: type_sig -> term -> term
    53   val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    54   val inst_typ_tvars: type_sig * (indexname * typ) list -> typ -> typ
    55 
    56   (*type matching*)
    57   exception TYPE_MATCH
    58   val typ_match: type_sig -> typ Vartab.table * (typ * typ)
    59     -> typ Vartab.table
    60   val typ_instance: type_sig * typ * typ -> bool
    61   val of_sort: type_sig -> typ * sort -> bool
    62 
    63   (*type unification*)
    64   exception TUNIFY
    65   val unify: type_sig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
    66   val raw_unify: typ * typ -> bool
    67 
    68   (*type inference*)
    69   val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
    70     -> (indexname * sort) list -> indexname -> sort
    71   val constrain: term -> typ -> term
    72   val param: int -> string * sort -> typ
    73   val paramify_dummies: int * typ -> int * typ
    74   val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    75     -> type_sig -> (string -> typ option) -> (indexname -> typ option)
    76     -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
    77     -> (sort -> sort) -> string list -> bool -> typ list -> term list
    78     -> term list * (indexname * typ) list
    79 end;
    80 
    81 structure Type: TYPE =
    82 struct
    83 
    84 
    85 (*** TFrees and TVars ***)
    86 
    87 fun no_tvars T =
    88   (case typ_tvars T of [] => T
    89   | vs => raise TYPE ("Illegal schematic type variable(s): " ^
    90       commas (map (Syntax.string_of_vname o #1) vs), [T], []));
    91 
    92 
    93 (* varify, unvarify *)
    94 
    95 val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
    96 
    97 fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    98   | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    99   | unvarifyT T = T;
   100 
   101 fun varify (t, fixed) =
   102   let
   103     val fs = add_term_tfree_names (t, []) \\ fixed;
   104     val ixns = add_term_tvar_ixns (t, []);
   105     val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
   106     fun thaw (f as (a, S)) =
   107       (case assoc (fmap, a) of
   108         None => TFree f
   109       | Some b => TVar (b, S));
   110   in (map_term_types (map_type_tfree thaw) t, fmap) end;
   111 
   112 
   113 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
   114 
   115 local
   116 
   117 fun new_name (ix, (pairs,used)) =
   118       let val v = variant used (string_of_indexname ix)
   119       in  ((ix,v)::pairs, v::used)  end;
   120 
   121 fun freeze_one alist (ix,sort) =
   122   TFree (the (assoc (alist, ix)), sort)
   123     handle OPTION =>
   124       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   125 
   126 fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
   127       handle OPTION => TFree(a,sort);
   128 
   129 in
   130 
   131 (*this sort of code could replace unvarifyT*)
   132 fun freeze_thaw_type T =
   133   let
   134     val used = add_typ_tfree_names (T, [])
   135     and tvars = map #1 (add_typ_tvars (T, []));
   136     val (alist, _) = foldr new_name (tvars, ([], used));
   137   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   138 
   139 fun freeze_thaw t =
   140   let
   141     val used = it_term_types add_typ_tfree_names (t, [])
   142     and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   143     val (alist, _) = foldr new_name (tvars, ([], used));
   144   in
   145     (case alist of
   146       [] => (t, fn x => x) (*nothing to do!*)
   147     | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
   148       map_term_types (map_type_tfree (thaw_one (map swap alist)))))
   149   end;
   150 
   151 end;
   152 
   153 
   154 
   155 (*** type signatures ***)
   156 
   157 (* type type_sig *)
   158 
   159 (*
   160   classes: list of all declared classes;
   161   classrel: (see Pure/sorts.ML)
   162   default: default sort attached to all unconstrained type vars;
   163   tycons: table of all declared types with the number of their arguments;
   164   log_types: list of logical type constructors sorted by number of arguments;
   165   univ_witness: type witnessing non-emptiness of least sort
   166   abbrs: table of type abbreviations;
   167   arities: (see Pure/sorts.ML)
   168 *)
   169 
   170 datatype type_sig =
   171   TySg of {
   172     classes: class list,
   173     classrel: Sorts.classrel,
   174     default: sort,
   175     tycons: int Symtab.table,
   176     log_types: string list,
   177     univ_witness: (typ * sort) option,
   178     abbrs: (string list * typ) Symtab.table,
   179     arities: Sorts.arities};
   180 
   181 fun rep_tsig (TySg comps) = comps;
   182 
   183 fun classes (TySg {classes = cs, ...}) = cs;
   184 fun defaultS (TySg {default, ...}) = default;
   185 fun logical_types (TySg {log_types, ...}) = log_types;
   186 fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
   187 
   188 
   189 (* error messages *)
   190 
   191 fun undeclared_class c = "Undeclared class: " ^ quote c;
   192 fun undeclared_classes cs = "Undeclared class(es): " ^ commas_quote cs;
   193 
   194 fun err_undeclared_class s = error (undeclared_class s);
   195 
   196 fun err_dup_classes cs =
   197   error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   198 
   199 fun undeclared_type c = "Undeclared type constructor: " ^ quote c;
   200 
   201 fun err_neg_args c =
   202   error ("Negative number of arguments of type constructor: " ^ quote c);
   203 
   204 fun err_dup_tycon c =
   205   error ("Duplicate declaration of type constructor: " ^ quote c);
   206 
   207 fun dup_tyabbrs ts =
   208   "Duplicate declaration of type abbreviation(s): " ^ commas_quote ts;
   209 
   210 fun ty_confl c = "Conflicting type constructor and abbreviation: " ^ quote c;
   211 
   212 
   213 (* sorts *)
   214 
   215 fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
   216 fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
   217 fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
   218 
   219 fun cert_class (TySg {classes, ...}) c =
   220   if c mem_string classes then c else raise TYPE (undeclared_class c, [], []);
   221 
   222 fun cert_sort tsig S = norm_sort tsig (map (cert_class tsig) S);
   223 
   224 fun witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
   225   Sorts.witness_sorts (classrel, arities, log_types);
   226 
   227 fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
   228   | rem_sorts (TFree (x, _)) = TFree (x, [])
   229   | rem_sorts (TVar (xi, _)) = TVar (xi, []);
   230 
   231 
   232 (* FIXME err_undeclared_class! *)
   233 (* 'leq' checks the partial order on classes according to the
   234    statements in classrel 'a'
   235 *)
   236 
   237 fun less a (C, D) = case Symtab.lookup (a, C) of
   238      Some ss => D mem_string ss
   239    | None => err_undeclared_class C;
   240 
   241 fun leq a (C, D)  =  C = D orelse less a (C, D);
   242 
   243 
   244 
   245 (* FIXME *)
   246 (*Instantiation of type variables in types*)
   247 (*Pre: instantiations obey restrictions! *)
   248 fun inst_typ tye =
   249   let fun inst(var as (v, _)) = case assoc(tye, v) of
   250                                   Some U => inst_typ tye U
   251                                 | None => TVar(var)
   252   in map_type_tvar inst end;
   253 
   254 
   255 
   256 fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort (classrel, arities);
   257 
   258 fun check_has_sort (tsig, T, S) =
   259   if of_sort tsig (T, S) then ()
   260   else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
   261 
   262 
   263 (*Instantiation of type variables in types *)
   264 fun inst_typ_tvars(tsig, tye) =
   265   let fun inst(var as (v, S)) = case assoc(tye, v) of
   266               Some U => (check_has_sort(tsig, U, S); U)
   267             | None => TVar(var)
   268   in map_type_tvar inst end;
   269 
   270 (*Instantiation of type variables in terms *)
   271 fun inst_term_tvars (_,[]) t = t
   272   | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;
   273 
   274 
   275 (* norm_typ, norm_term *)
   276 
   277 (*expand abbreviations and normalize sorts*)
   278 fun norm_typ (tsig as TySg {abbrs, ...}) ty =
   279   let
   280     val idx = maxidx_of_typ ty + 1;
   281 
   282     fun norm (Type (a, Ts)) =
   283           (case Symtab.lookup (abbrs, a) of
   284             Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
   285           | None => Type (a, map norm Ts))
   286       | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
   287       | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
   288 
   289     val ty' = norm ty;
   290   in if ty = ty' then ty else ty' end;  (*dumb tuning to avoid copying*)
   291 
   292 fun norm_term tsig t =
   293   let val t' = map_term_types (norm_typ tsig) t
   294   in if t = t' then t else t' end;  (*dumb tuning to avoid copying*)
   295 
   296 
   297 
   298 (** build type signatures **)
   299 
   300 fun make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) =
   301   TySg {classes = classes, classrel = classrel, default = default, tycons = tycons,
   302     log_types = log_types, univ_witness = univ_witness, abbrs = abbrs, arities = arities};
   303 
   304 fun rebuild_tsig (TySg {classes, classrel, default, tycons, log_types = _, univ_witness = _, abbrs, arities}) =
   305   let
   306     fun log_class c = Sorts.class_le classrel (c, logicC);
   307     fun log_type (t, _) = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
   308     val ts = filter log_type (Symtab.dest tycons);
   309 
   310     val log_types = map #1 (Library.sort (Library.int_ord o pairself #2) ts);
   311     val univ_witness =
   312       (case Sorts.witness_sorts (classrel, arities, log_types) [] [classes] of
   313         [w] => Some w | _ => None);
   314   in make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) end;
   315 
   316 val tsig0 =
   317   make_tsig ([], Symtab.empty, [], Symtab.empty, [], None, Symtab.empty, Symtab.empty)
   318   |> rebuild_tsig;
   319 
   320 
   321 (* typ_errors *)
   322 
   323 (*check validity of (not necessarily normal) type; accumulate error messages*)
   324 
   325 fun typ_errors tsig (typ, errors) =
   326   let
   327     val {classes, tycons, abbrs, ...} = rep_tsig tsig;
   328 
   329     fun class_err (errs, c) =
   330       if c mem_string classes then errs
   331       else undeclared_class c ins_string errs;
   332 
   333     val sort_err = foldl class_err;
   334 
   335     fun typ_errs (errs, Type (c, Us)) =
   336           let
   337             val errs' = foldl typ_errs (errs, Us);
   338             fun nargs n =
   339               if n = length Us then errs'
   340               else ("Wrong number of arguments: " ^ quote c) ins_string errs';
   341           in
   342             (case Symtab.lookup (tycons, c) of
   343               Some n => nargs n
   344             | None =>
   345                 (case Symtab.lookup (abbrs, c) of
   346                   Some (vs, _) => nargs (length vs)
   347                 | None => undeclared_type c ins_string errs))
   348           end
   349     | typ_errs (errs, TFree (_, S)) = sort_err (errs, S)
   350     | typ_errs (errs, TVar ((x, i), S)) =
   351         if i < 0 then
   352           ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
   353         else sort_err (errs, S);
   354   in typ_errs (errors, typ) end;
   355 
   356 
   357 (* cert_typ *)           (*exception TYPE*)
   358 
   359 fun cert_typ_no_norm tsig T =
   360   (case typ_errors tsig (T, []) of
   361     [] => T
   362   | errs => raise TYPE (cat_lines errs, [T], []));
   363 
   364 fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
   365 
   366 
   367 
   368 (** merge type signatures **)
   369 
   370 (* merge classrel *)
   371 
   372 fun assoc_union (as1, []) = as1
   373   | assoc_union (as1, (key, l2) :: as2) =
   374       (case assoc_string (as1, key) of
   375         Some l1 => assoc_union (overwrite (as1, (key, l1 union_string l2)), as2)
   376       | None => assoc_union ((key, l2) :: as1, as2));
   377 
   378 fun merge_classrel (classrel1, classrel2) =
   379   let
   380     val classrel = transitive_closure (assoc_union (Symtab.dest classrel1, Symtab.dest classrel2))
   381   in
   382     if exists (op mem_string) classrel then
   383       error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
   384     else Symtab.make classrel
   385   end;
   386 
   387 
   388 (* coregularity *)
   389 
   390 local
   391 
   392 (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
   393 
   394 fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
   395       Some(w1) => if w = w1 then () else
   396         error("There are two declarations\n" ^
   397               Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
   398               Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
   399               "with the same result class.")
   400     | None => ();
   401 
   402 (* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   403    such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
   404 
   405 fun coreg_err(t, (C1,w1), (C2,w2)) =
   406     error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
   407                           ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");
   408 
   409 fun coreg classrel (t, Cw1) =
   410   let
   411     fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   412       if leq classrel (C1,C2) then
   413         if Sorts.sorts_le classrel (w1,w2) then ()
   414         else coreg_err(t, Cw1, Cw2)
   415       else ()
   416     fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   417   in seq check end;
   418 
   419 in
   420 
   421 fun add_arity classrel ars (tCw as (_,Cw)) =
   422       (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
   423 
   424 end;
   425 
   426 
   427 (* 'merge_arities' builds the union of two 'arities' lists;
   428    it only checks the two restriction conditions and inserts afterwards
   429    all elements of the second list into the first one *)
   430 
   431 local
   432 
   433 fun merge_arities_aux classrel =
   434   let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
   435 
   436       fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
   437           Some(ars1) =>
   438             let val ars = foldl (test_ar t) (ars1, ars2)
   439             in overwrite (arities1, (t,ars)) end
   440         | None => c::arities1
   441   in foldl merge_c end;
   442 
   443 in
   444 
   445 fun merge_arities classrel (a1, a2) =
   446   Symtab.make (merge_arities_aux classrel (Symtab.dest a1, Symtab.dest a2));
   447 
   448 end;
   449 
   450 
   451 (* tycons *)
   452 
   453 fun varying_decls t =
   454   error ("Type constructor " ^ quote t ^ " has varying number of arguments");
   455 
   456 fun add_tycons (tycons, tn as (t,n)) =
   457   (case Symtab.lookup (tycons, t) of
   458     Some m => if m = n then tycons else varying_decls t
   459   | None => Symtab.update (tn, tycons));
   460 
   461 
   462 (* merge_abbrs *)
   463 
   464 fun merge_abbrs abbrs =
   465   Symtab.merge (op =) abbrs handle Symtab.DUPS dups => raise TERM (dup_tyabbrs dups, []);
   466 
   467 
   468 (* merge_tsigs *)
   469 
   470 fun merge_tsigs
   471  (TySg {classes = classes1, default = default1, classrel = classrel1, tycons = tycons1,
   472     log_types = _, univ_witness = _, arities = arities1, abbrs = abbrs1},
   473   TySg {classes = classes2, default = default2, classrel = classrel2, tycons = tycons2,
   474     log_types = _, univ_witness = _, arities = arities2, abbrs = abbrs2}) =
   475   let
   476     val classes' = classes1 union_string classes2;
   477     val classrel' = merge_classrel (classrel1, classrel2);
   478     val arities' = merge_arities classrel' (arities1, arities2);
   479     val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2);
   480     val default' = Sorts.norm_sort classrel' (default1 @ default2);
   481     val abbrs' = merge_abbrs (abbrs1, abbrs2);
   482   in
   483     make_tsig (classes', classrel', default', tycons', [], None, abbrs', arities')
   484     |> rebuild_tsig
   485   end;
   486 
   487 
   488 
   489 (*** extend type signatures ***)
   490 
   491 (** add classes and classrel relations **)
   492 
   493 fun add_classes classes cs =
   494   (case cs inter_string classes of
   495     [] => cs @ classes
   496   | dups => err_dup_classes cs);
   497 
   498 
   499 (*'add_classrel' adds a tuple consisting of a new class (the new class has
   500   already been inserted into the 'classes' list) and its superclasses (they
   501   must be declared in 'classes' too) to the 'classrel' list of the given type
   502   signature; furthermore all inherited superclasses according to the
   503   superclasses brought with are inserted and there is a check that there are
   504   no cycles (i.e. C <= D <= C, with C <> D);*)
   505 
   506 fun add_classrel classes (classrel, (s, ges)) =
   507   let
   508     fun upd (classrel, s') =
   509       if s' mem_string classes then
   510         let val ges' = the (Symtab.lookup (classrel, s))
   511         in case Symtab.lookup (classrel, s') of
   512              Some sups => if s mem_string sups
   513                            then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
   514                            else Symtab.update ((s, sups union_string ges'), classrel)
   515            | None => classrel
   516         end
   517       else err_undeclared_class s'
   518   in foldl upd (Symtab.update ((s, ges), classrel), ges) end;
   519 
   520 
   521 (* 'extend_classes' inserts all new classes into the corresponding
   522    lists ('classes', 'classrel') if possible *)
   523 
   524 fun extend_classes (classes, classrel, new_classes) =
   525   let
   526     val classes' = add_classes classes (map fst new_classes);
   527     val classrel' = foldl (add_classrel classes') (classrel, new_classes);
   528   in (classes', classrel') end;
   529 
   530 
   531 (* ext_tsig_classes *)
   532 
   533 fun ext_tsig_classes tsig new_classes =
   534   let
   535     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   536     val (classes', classrel') = extend_classes (classes,classrel, new_classes);
   537   in
   538     make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   539     |> rebuild_tsig
   540   end;
   541 
   542 
   543 (* ext_tsig_classrel *)
   544 
   545 fun ext_tsig_classrel tsig pairs =
   546   let
   547     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   548     val cert = cert_class tsig;
   549 
   550     (* FIXME clean! *)
   551     val classrel' =
   552       merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
   553   in
   554     make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   555     |> rebuild_tsig
   556   end;
   557 
   558 
   559 (* ext_tsig_defsort *)
   560 
   561 fun ext_tsig_defsort
   562     (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
   563   make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);
   564 
   565 
   566 
   567 (** add types **)
   568 
   569 fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
   570   let
   571     fun check_type (c, n) =
   572       if n < 0 then err_neg_args c
   573       else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
   574       else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
   575       else ();
   576     val _ = seq check_type ts;
   577     val tycons' = Symtab.extend (tycons, ts);
   578     val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
   579   in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;
   580 
   581 
   582 
   583 (** add type abbreviations **)
   584 
   585 fun abbr_errors tsig (a, (lhs_vs, rhs)) =
   586   let
   587     val TySg {tycons, abbrs, ...} = tsig;
   588     val rhs_vs = map (#1 o #1) (typ_tvars rhs);
   589 
   590     val dup_lhs_vars =
   591       (case duplicates lhs_vs of
   592         [] => []
   593       | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);
   594 
   595     val extra_rhs_vars =
   596       (case gen_rems (op =) (rhs_vs, lhs_vs) of
   597         [] => []
   598       | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
   599 
   600     val tycon_confl =
   601       if is_none (Symtab.lookup (tycons, a)) then []
   602       else [ty_confl a];
   603 
   604     val dup_abbr =
   605       if is_none (Symtab.lookup (abbrs, a)) then []
   606       else ["Duplicate declaration of abbreviation"];
   607   in
   608     dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
   609       typ_errors tsig (rhs, [])
   610   end;
   611 
   612 fun prep_abbr tsig (a, vs, raw_rhs) =
   613   let
   614     fun err msgs = (seq error_msg msgs;
   615       error ("The error(s) above occurred in type abbreviation " ^ quote a));
   616 
   617     val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
   618       handle TYPE (msg, _, _) => err [msg];
   619     val abbr = (a, (vs, rhs));
   620   in
   621     (case abbr_errors tsig abbr of
   622       [] => abbr
   623     | msgs => err msgs)
   624   end;
   625 
   626 fun add_abbr
   627     (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
   628   make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
   629     Symtab.update (prep_abbr tsig abbr, abbrs), arities);
   630 
   631 fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   632 
   633 
   634 
   635 (** add arities **)
   636 
   637 (* 'coregular' checks
   638    - the two restrictions 'is_unique_decl' and 'coreg'
   639    - if the classes in the new type declarations are known in the
   640      given type signature
   641    - if one type constructor has always the same number of arguments;
   642    if one type declaration has passed all checks it is inserted into
   643    the 'arities' association list of the given type signatrure  *)
   644 
   645 fun coregular (classes, classrel, tycons) =
   646   let fun ex C = if C mem_string classes then () else err_undeclared_class(C);
   647 
   648       fun addar(arities, (t, (w, C))) = case Symtab.lookup (tycons, t) of
   649             Some(n) => if n <> length w then varying_decls(t) else
   650                      ((seq o seq) ex w; ex C;
   651                       let val ars = the (Symtab.lookup (arities, t))
   652                           val ars' = add_arity classrel ars (t,(C,w))
   653                       in Symtab.update ((t,ars'), arities) end)
   654           | None => error (undeclared_type t);
   655 
   656   in addar end;
   657 
   658 
   659 (* 'close' extends the 'arities' association list after all new type
   660    declarations have been inserted successfully:
   661    for every declaration t:(Ss)C , for all classses D with C <= D:
   662       if there is no declaration t:(Ss')C' with C < C' and C' <= D
   663       then insert the declaration t:(Ss)D into 'arities'
   664    this means, if there exists a declaration t:(Ss)C and there is
   665    no declaration t:(Ss')D with C <=D then the declaration holds
   666    for all range classes more general than C *)
   667 
   668 fun close classrel arities =
   669   let fun check sl (l, (s, dom)) = case Symtab.lookup (classrel, s) of
   670           Some sups =>
   671             let fun close_sup (l, sup) =
   672                   if exists (fn s'' => less classrel (s, s'') andalso
   673                                        leq classrel (s'', sup)) sl
   674                   then l
   675                   else (sup, dom)::l
   676             in foldl close_sup (l, sups) end
   677         | None => l;
   678       fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
   679   in map ext arities end;
   680 
   681 
   682 (* ext_tsig_arities *)
   683 
   684 fun norm_domain classrel =
   685   let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
   686   in map one_min end;
   687 
   688 fun ext_tsig_arities tsig sarities =
   689   let
   690     val TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
   691     val arities1 =
   692       flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   693     val arities2 =
   694       foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
   695       |> Symtab.dest |> close classrel |> Symtab.make;
   696   in
   697     make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
   698     |> rebuild_tsig
   699   end;
   700 
   701 
   702 
   703 (*** type unification and friends ***)
   704 
   705 (** matching **)
   706 
   707 exception TYPE_MATCH;
   708 
   709 fun typ_match tsig =
   710   let
   711     fun match (subs, (TVar (v, S), T)) =
   712           (case Vartab.lookup (subs, v) of
   713             None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs)
   714               handle TYPE _ => raise TYPE_MATCH)
   715           | Some U => if U = T then subs else raise TYPE_MATCH)
   716       | match (subs, (Type (a, Ts), Type (b, Us))) =
   717           if a <> b then raise TYPE_MATCH
   718           else foldl match (subs, Ts ~~ Us)
   719       | match (subs, (TFree x, TFree y)) =
   720           if x = y then subs else raise TYPE_MATCH
   721       | match _ = raise TYPE_MATCH;
   722   in match end;
   723 
   724 fun typ_instance (tsig, T, U) =
   725   (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
   726 
   727 
   728 
   729 (** unification **)
   730 
   731 exception TUNIFY;
   732 
   733 
   734 (* occurs check *)
   735 
   736 fun occurs v tye =
   737   let
   738     fun occ (Type (_, Ts)) = exists occ Ts
   739       | occ (TFree _) = false
   740       | occ (TVar (w, _)) =
   741           eq_ix (v, w) orelse
   742             (case Vartab.lookup (tye, w) of
   743               None => false
   744             | Some U => occ U);
   745   in occ end;
   746 
   747 
   748 (* chase variable assignments *)
   749 
   750 (*if devar returns a type var then it must be unassigned*)
   751 fun devar (T as TVar (v, _), tye) =
   752       (case  Vartab.lookup (tye, v) of
   753         Some U => devar (U, tye)
   754       | None => T)
   755   | devar (T, tye) = T;
   756 
   757 
   758 (* add_env *)
   759 
   760 (*avoids chains 'a |-> 'b |-> 'c ...*)
   761 fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map
   762   (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab);
   763 
   764 
   765 (* unify *)
   766 
   767 fun unify (tsig as TySg {classrel, arities, ...}) (tyenv, maxidx) TU =
   768   let
   769     val tyvar_count = ref maxidx;
   770     fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   771 
   772     fun mg_domain a S =
   773       Sorts.mg_domain (classrel, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
   774 
   775     fun meet ((_, []), tye) = tye
   776       | meet ((TVar (xi, S'), S), tye) =
   777           if Sorts.sort_le classrel (S', S) then tye
   778           else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
   779       | meet ((TFree (_, S'), S), tye) =
   780           if Sorts.sort_le classrel (S', S) then tye
   781           else raise TUNIFY
   782       | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
   783     and meets (([], []), tye) = tye
   784       | meets ((T :: Ts, S :: Ss), tye) =
   785           meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
   786       | meets _ = sys_error "meets";
   787 
   788     fun unif ((ty1, ty2), tye) =
   789       (case (devar (ty1, tye), devar (ty2, tye)) of
   790         (T as TVar (v, S1), U as TVar (w, S2)) =>
   791           if eq_ix (v, w) then tye
   792           else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye)
   793           else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye)
   794           else
   795             let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
   796               add_env ((v, S), add_env ((w, S), tye))
   797             end
   798       | (TVar (v, S), T) =>
   799           if occurs v tye T then raise TUNIFY
   800           else meet ((T, S), add_env ((v, T), tye))
   801       | (T, TVar (v, S)) =>
   802           if occurs v tye T then raise TUNIFY
   803           else meet ((T, S), add_env ((v, T), tye))
   804       | (Type (a, Ts), Type (b, Us)) =>
   805           if a <> b then raise TUNIFY
   806           else foldr unif (Ts ~~ Us, tye)
   807       | (T, U) => if T = U then tye else raise TUNIFY);
   808   in (unif (TU, tyenv), ! tyvar_count) end;
   809 
   810 
   811 (* raw_unify *)
   812 
   813 (*purely structural unification -- ignores sorts*)
   814 fun raw_unify (ty1, ty2) =
   815   (unify tsig0 (Vartab.empty, 0) (rem_sorts ty1, rem_sorts ty2); true)
   816     handle TUNIFY => false;
   817 
   818 
   819 
   820 (** type inference **)
   821 
   822 (* sort constraints *)
   823 
   824 fun get_sort tsig def_sort map_sort raw_env =
   825   let
   826     fun eq ((xi, S), (xi', S')) =
   827       xi = xi' andalso eq_sort tsig (S, S');
   828 
   829     val env = gen_distinct eq (map (apsnd map_sort) raw_env);
   830     val _ =
   831       (case gen_duplicates eq_fst env of
   832         [] => ()
   833       | dups => error ("Inconsistent sort constraints for type variable(s) " ^
   834           commas (map (quote o Syntax.string_of_vname' o fst) dups)));
   835 
   836     fun get xi =
   837       (case (assoc (env, xi), def_sort xi) of
   838         (None, None) => defaultS tsig
   839       | (None, Some S) => S
   840       | (Some S, None) => S
   841       | (Some S, Some S') =>
   842           if eq_sort tsig (S, S') then S'
   843           else error ("Sort constraint inconsistent with default for type variable " ^
   844             quote (Syntax.string_of_vname' xi)));
   845   in get end;
   846 
   847 
   848 (* type constraints *)
   849 
   850 fun constrain t T =
   851   if T = dummyT then t
   852   else Const ("_type_constraint_", T) $ t;
   853 
   854 
   855 (* user parameters *)
   856 
   857 fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
   858 fun param i (x, S) = TVar (("?" ^ x, i), S);
   859 
   860 fun paramify_dummies (i, TFree ("'_dummy_", S)) = (i + 1, param i ("'dummy", S))
   861   | paramify_dummies (i, Type (a, Ts)) =
   862       let val (i', Ts') = foldl_map paramify_dummies (i, Ts)
   863       in (i', Type (a, Ts')) end
   864   | paramify_dummies arg = arg;
   865 
   866 
   867 (* decode_types *)
   868 
   869 (*transform parse tree into raw term*)
   870 fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   871   let
   872     fun get_type xi = if_none (def_type xi) dummyT;
   873     fun is_free x = is_some (def_type (x, ~1));
   874     val raw_env = Syntax.raw_term_sorts tm;
   875     val sort_of = get_sort tsig def_sort map_sort raw_env;
   876 
   877     val certT = cert_typ tsig o map_type;
   878     fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
   879 
   880     fun decode (Const ("_constrain", _) $ t $ typ) =
   881           constrain (decode t) (decodeT typ)
   882       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   883           if T = dummyT then Abs (x, decodeT typ, decode t)
   884           else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
   885       | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
   886       | decode (t $ u) = decode t $ decode u
   887       | decode (Free (x, T)) =
   888           let val c = map_const x in
   889             if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
   890               Const (c, certT T)
   891             else if T = dummyT then Free (x, get_type (x, ~1))
   892             else constrain (Free (x, certT T)) (get_type (x, ~1))
   893           end
   894       | decode (Var (xi, T)) =
   895           if T = dummyT then Var (xi, get_type xi)
   896           else constrain (Var (xi, certT T)) (get_type xi)
   897       | decode (t as Bound _) = t
   898       | decode (Const (c, T)) = Const (map_const c, certT T);
   899   in decode tm end;
   900 
   901 
   902 (* infer_types *)
   903 
   904 (*
   905   Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
   906   unifies with Ti (for i=1,...,n).
   907 
   908   tsig: type signature
   909   const_type: name mapping and signature lookup
   910   def_type: partial map from indexnames to types (constrains Frees, Vars)
   911   def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   912   used: list of already used type variables
   913   freeze: if true then generated parameters are turned into TFrees, else TVars
   914 *)
   915 
   916 fun infer_types prt prT tsig const_type def_type def_sort
   917     map_const map_type map_sort used freeze pat_Ts raw_ts =
   918   let
   919     val TySg {classrel, arities, ...} = tsig;
   920     val pat_Ts' = map (cert_typ tsig) pat_Ts;
   921     val is_const = is_some o const_type;
   922     val raw_ts' =
   923       map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
   924     val (ts, Ts, unifier) =
   925       TypeInfer.infer_types prt prT const_type classrel arities used freeze
   926         is_param raw_ts' pat_Ts';
   927   in (ts, unifier) end;
   928 
   929 
   930 end;