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