src/Pure/type.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12314 160013745a92
child 12501 36b2ac65e18d
permissions -rw-r--r--
changed Thm.varifyT';
     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
   536     make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   537     |> rebuild_tsig
   538   end;
   539 
   540 
   541 (* ext_tsig_classrel *)
   542 
   543 fun ext_tsig_classrel tsig pairs =
   544   let
   545     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   546     val cert = cert_class tsig;
   547 
   548     (* FIXME clean! *)
   549     val classrel' =
   550       merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
   551   in
   552     make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   553     |> rebuild_tsig
   554   end;
   555 
   556 
   557 (* ext_tsig_defsort *)
   558 
   559 fun ext_tsig_defsort
   560     (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
   561   make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);
   562 
   563 
   564 
   565 (** add types **)
   566 
   567 fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
   568   let
   569     fun check_type (c, n) =
   570       if n < 0 then err_neg_args c
   571       else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
   572       else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
   573       else ();
   574     val _ = seq check_type ts;
   575     val tycons' = Symtab.extend (tycons, ts);
   576     val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
   577   in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;
   578 
   579 
   580 
   581 (** add type abbreviations **)
   582 
   583 fun abbr_errors tsig (a, (lhs_vs, rhs)) =
   584   let
   585     val TySg {tycons, abbrs, ...} = tsig;
   586     val rhs_vs = map (#1 o #1) (typ_tvars rhs);
   587 
   588     val dup_lhs_vars =
   589       (case duplicates lhs_vs of
   590         [] => []
   591       | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);
   592 
   593     val extra_rhs_vars =
   594       (case gen_rems (op =) (rhs_vs, lhs_vs) of
   595         [] => []
   596       | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
   597 
   598     val tycon_confl =
   599       if is_none (Symtab.lookup (tycons, a)) then []
   600       else [ty_confl a];
   601 
   602     val dup_abbr =
   603       if is_none (Symtab.lookup (abbrs, a)) then []
   604       else ["Duplicate declaration of abbreviation"];
   605   in
   606     dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
   607       typ_errors tsig (rhs, [])
   608   end;
   609 
   610 fun prep_abbr tsig (a, vs, raw_rhs) =
   611   let
   612     fun err msgs = (seq error_msg msgs;
   613       error ("The error(s) above occurred in type abbreviation " ^ quote a));
   614 
   615     val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
   616       handle TYPE (msg, _, _) => err [msg];
   617     val abbr = (a, (vs, rhs));
   618   in
   619     (case abbr_errors tsig abbr of
   620       [] => abbr
   621     | msgs => err msgs)
   622   end;
   623 
   624 fun add_abbr
   625     (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
   626   make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
   627     Symtab.update (prep_abbr tsig abbr, abbrs), arities);
   628 
   629 fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   630 
   631 
   632 
   633 (** add arities **)
   634 
   635 (* 'coregular' checks
   636    - the two restrictions 'is_unique_decl' and 'coreg'
   637    - if the classes in the new type declarations are known in the
   638      given type signature
   639    - if one type constructor has always the same number of arguments;
   640    if one type declaration has passed all checks it is inserted into
   641    the 'arities' association list of the given type signatrure  *)
   642 
   643 fun coregular (classes, classrel, tycons) =
   644   let fun ex C = if C mem_string classes then () else err_undeclared_class(C);
   645 
   646       fun addar(arities, (t, (w, C))) = case Symtab.lookup (tycons, t) of
   647             Some(n) => if n <> length w then varying_decls(t) else
   648                      ((seq o seq) ex w; ex C;
   649                       let val ars = the (Symtab.lookup (arities, t))
   650                           val ars' = add_arity classrel ars (t,(C,w))
   651                       in Symtab.update ((t,ars'), arities) end)
   652           | None => error (undeclared_type t);
   653 
   654   in addar end;
   655 
   656 
   657 (* 'close' extends the 'arities' association list after all new type
   658    declarations have been inserted successfully:
   659    for every declaration t:(Ss)C , for all classses D with C <= D:
   660       if there is no declaration t:(Ss')C' with C < C' and C' <= D
   661       then insert the declaration t:(Ss)D into 'arities'
   662    this means, if there exists a declaration t:(Ss)C and there is
   663    no declaration t:(Ss')D with C <=D then the declaration holds
   664    for all range classes more general than C *)
   665 
   666 fun close classrel arities =
   667   let fun check sl (l, (s, dom)) = case Symtab.lookup (classrel, s) of
   668           Some sups =>
   669             let fun close_sup (l, sup) =
   670                   if exists (fn s'' => less classrel (s, s'') andalso
   671                                        leq classrel (s'', sup)) sl
   672                   then l
   673                   else (sup, dom)::l
   674             in foldl close_sup (l, sups) end
   675         | None => l;
   676       fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
   677   in map ext arities end;
   678 
   679 
   680 (* ext_tsig_arities *)
   681 
   682 fun norm_domain classrel =
   683   let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
   684   in map one_min end;
   685 
   686 fun ext_tsig_arities tsig sarities =
   687   let
   688     val TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
   689     val arities1 =
   690       flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   691     val arities2 =
   692       foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
   693       |> Symtab.dest |> close classrel |> Symtab.make;
   694   in
   695     make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
   696     |> rebuild_tsig
   697   end;
   698 
   699 
   700 
   701 (*** type unification and friends ***)
   702 
   703 (** matching **)
   704 
   705 exception TYPE_MATCH;
   706 
   707 fun typ_match tsig =
   708   let
   709     fun match (subs, (TVar (v, S), T)) =
   710           (case Vartab.lookup (subs, v) of
   711             None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs)
   712               handle TYPE _ => raise TYPE_MATCH)
   713           | Some U => if U = T then subs else raise TYPE_MATCH)
   714       | match (subs, (Type (a, Ts), Type (b, Us))) =
   715           if a <> b then raise TYPE_MATCH
   716           else foldl match (subs, Ts ~~ Us)
   717       | match (subs, (TFree x, TFree y)) =
   718           if x = y then subs else raise TYPE_MATCH
   719       | match _ = raise TYPE_MATCH;
   720   in match end;
   721 
   722 fun typ_instance (tsig, T, U) =
   723   (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
   724 
   725 
   726 
   727 (** unification **)
   728 
   729 exception TUNIFY;
   730 
   731 
   732 (* occurs check *)
   733 
   734 fun occurs v tye =
   735   let
   736     fun occ (Type (_, Ts)) = exists occ Ts
   737       | occ (TFree _) = false
   738       | occ (TVar (w, _)) =
   739           eq_ix (v, w) orelse
   740             (case Vartab.lookup (tye, w) of
   741               None => false
   742             | Some U => occ U);
   743   in occ end;
   744 
   745 
   746 (* chase variable assignments *)
   747 
   748 (*if devar returns a type var then it must be unassigned*)
   749 fun devar (T as TVar (v, _), tye) =
   750       (case  Vartab.lookup (tye, v) of
   751         Some U => devar (U, tye)
   752       | None => T)
   753   | devar (T, tye) = T;
   754 
   755 
   756 (* add_env *)
   757 
   758 (*avoids chains 'a |-> 'b |-> 'c ...*)
   759 fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map
   760   (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab);
   761 
   762 (* unify *)
   763 
   764 fun unify (tsig as TySg {classrel, arities, ...}) maxidx tyenv TU =
   765   let
   766     val tyvar_count = ref maxidx;
   767     fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   768 
   769     fun mg_domain a S =
   770       Sorts.mg_domain (classrel, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
   771 
   772     fun meet ((_, []), tye) = tye
   773       | meet ((TVar (xi, S'), S), tye) =
   774           if Sorts.sort_le classrel (S', S) then tye
   775           else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
   776       | meet ((TFree (_, S'), S), tye) =
   777           if Sorts.sort_le classrel (S', S) then tye
   778           else raise TUNIFY
   779       | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
   780     and meets (([], []), tye) = tye
   781       | meets ((T :: Ts, S :: Ss), tye) =
   782           meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
   783       | meets _ = sys_error "meets";
   784 
   785     fun unif ((ty1, ty2), tye) =
   786       (case (devar (ty1, tye), devar (ty2, tye)) of
   787         (T as TVar (v, S1), U as TVar (w, S2)) =>
   788           if eq_ix (v, w) then tye
   789           else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye)
   790           else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye)
   791           else
   792             let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
   793               add_env ((v, S), add_env ((w, S), tye))
   794             end
   795       | (TVar (v, S), T) =>
   796           if occurs v tye T then raise TUNIFY
   797           else meet ((T, S), add_env ((v, T), tye))
   798       | (T, TVar (v, S)) =>
   799           if occurs v tye T then raise TUNIFY
   800           else meet ((T, S), add_env ((v, T), tye))
   801       | (Type (a, Ts), Type (b, Us)) =>
   802           if a <> b then raise TUNIFY
   803           else foldr unif (Ts ~~ Us, tye)
   804       | (T, U) => if T = U then tye else raise TUNIFY);
   805   in
   806     (unif (TU, tyenv), ! tyvar_count)
   807   end;
   808 
   809 
   810 (* raw_unify *)
   811 
   812 (*purely structural unification -- ignores sorts*)
   813 fun raw_unify (ty1, ty2) =
   814   (unify tsig0 0 Vartab.empty (rem_sorts ty1, rem_sorts ty2); true)
   815     handle TUNIFY => false;
   816 
   817 
   818 
   819 (** type inference **)
   820 
   821 (* sort constraints *)
   822 
   823 fun get_sort tsig def_sort map_sort raw_env =
   824   let
   825     fun eq ((xi, S), (xi', S')) =
   826       xi = xi' andalso eq_sort tsig (S, S');
   827 
   828     val env = gen_distinct eq (map (apsnd map_sort) raw_env);
   829     val _ =
   830       (case gen_duplicates eq_fst env of
   831         [] => ()
   832       | dups => error ("Inconsistent sort constraints for type variable(s) " ^
   833           commas (map (quote o Syntax.string_of_vname' o fst) dups)));
   834 
   835     fun get xi =
   836       (case (assoc (env, xi), def_sort xi) of
   837         (None, None) => defaultS tsig
   838       | (None, Some S) => S
   839       | (Some S, None) => S
   840       | (Some S, Some S') =>
   841           if eq_sort tsig (S, S') then S'
   842           else error ("Sort constraint inconsistent with default for type variable " ^
   843             quote (Syntax.string_of_vname' xi)));
   844   in get end;
   845 
   846 
   847 (* type constraints *)
   848 
   849 fun constrain t T =
   850   if T = dummyT then t
   851   else Const ("_type_constraint_", T) $ t;
   852 
   853 
   854 (* user parameters *)
   855 
   856 fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
   857 fun param used (x, S) = TVar ((variant used ("?" ^ x), 0), S);
   858 
   859 
   860 (* decode_types *)
   861 
   862 (*transform parse tree into raw term*)
   863 fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   864   let
   865     fun get_type xi = if_none (def_type xi) dummyT;
   866     fun is_free x = is_some (def_type (x, ~1));
   867     val raw_env = Syntax.raw_term_sorts tm;
   868     val sort_of = get_sort tsig def_sort map_sort raw_env;
   869 
   870     val certT = cert_typ tsig o map_type;
   871     fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
   872 
   873     fun decode (Const ("_constrain", _) $ t $ typ) =
   874           constrain (decode t) (decodeT typ)
   875       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   876           if T = dummyT then Abs (x, decodeT typ, decode t)
   877           else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
   878       | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
   879       | decode (t $ u) = decode t $ decode u
   880       | decode (Free (x, T)) =
   881           let val c = map_const x in
   882             if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
   883               Const (c, certT T)
   884             else if T = dummyT then Free (x, get_type (x, ~1))
   885             else constrain (Free (x, certT T)) (get_type (x, ~1))
   886           end
   887       | decode (Var (xi, T)) =
   888           if T = dummyT then Var (xi, get_type xi)
   889           else constrain (Var (xi, certT T)) (get_type xi)
   890       | decode (t as Bound _) = t
   891       | decode (Const (c, T)) = Const (map_const c, certT T);
   892   in decode tm end;
   893 
   894 
   895 (* infer_types *)
   896 
   897 (*
   898   Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
   899   unifies with Ti (for i=1,...,n).
   900 
   901   tsig: type signature
   902   const_type: name mapping and signature lookup
   903   def_type: partial map from indexnames to types (constrains Frees, Vars)
   904   def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   905   used: list of already used type variables
   906   freeze: if true then generated parameters are turned into TFrees, else TVars
   907 *)
   908 
   909 fun infer_types prt prT tsig const_type def_type def_sort
   910     map_const map_type map_sort used freeze pat_Ts raw_ts =
   911   let
   912     val TySg {classrel, arities, ...} = tsig;
   913     val pat_Ts' = map (cert_typ tsig) pat_Ts;
   914     val is_const = is_some o const_type;
   915     val raw_ts' =
   916       map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
   917     val (ts, Ts, unifier) =
   918       TypeInfer.infer_types prt prT const_type classrel arities used freeze
   919         is_param raw_ts' pat_Ts';
   920   in (ts, unifier) end;
   921 
   922 
   923 end;