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