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