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