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