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