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