src/Pure/type.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2753 bcde71e5f371
child 2964 557a11310988
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     1 (*  Title:      Pure/type.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Lawrence C Paulson
     4 
     5 Type classes and sorts. Type signatures. Type unification and inference.
     6 
     7 TODO:
     8   improve nonempty_sort!
     9   move type unification and inference to type_unify.ML (TypeUnify) (?)
    10 *)
    11 
    12 signature TYPE =
    13   sig
    14   exception TUNIFY
    15   exception TYPE_MATCH
    16   val no_tvars: typ -> typ
    17   val varifyT: typ -> typ
    18   val unvarifyT: typ -> typ
    19   val varify: term * string list -> term
    20   val str_of_sort: sort -> string
    21   val str_of_arity: string * sort list * sort -> string
    22   type type_sig
    23   val rep_tsig: type_sig ->
    24     {classes: class list,
    25      subclass: (class * class list) list,
    26      default: sort,
    27      tycons: (string * int) list,
    28      abbrs: (string * (string list * typ)) list,
    29      arities: (string * (class * sort list) list) list}
    30   val defaultS: type_sig -> sort
    31   val tsig0: type_sig
    32   val logical_types: type_sig -> string list
    33   val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
    34   val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
    35   val ext_tsig_defsort: type_sig -> sort -> type_sig
    36   val ext_tsig_types: type_sig -> (string * int) list -> type_sig
    37   val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
    38   val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
    39   val merge_tsigs: type_sig * type_sig -> type_sig
    40   val subsort: type_sig -> sort * sort -> bool
    41   val norm_sort: type_sig -> sort -> sort
    42   val eq_sort: type_sig -> sort * sort -> bool
    43   val rem_sorts: typ -> typ
    44   val nonempty_sort: type_sig -> sort list -> sort -> bool
    45   val cert_typ: type_sig -> typ -> typ
    46   val norm_typ: type_sig -> typ -> typ
    47   val freeze: term -> term
    48   val freeze_vars: typ -> typ
    49   val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
    50     -> indexname -> sort
    51   val infer_types: type_sig * (string -> typ option) *
    52                    (indexname -> typ option) * (indexname -> sort option) *
    53                    string list * bool * typ list * term list
    54                    -> term list * (indexname * typ) list
    55   val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    56   val thaw_vars: typ -> typ
    57   val typ_errors: type_sig -> typ * string list -> string list
    58   val typ_instance: type_sig * typ * typ -> bool
    59   val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
    60     -> (indexname * typ) list
    61   val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
    62     -> (indexname * typ) list * int
    63   val raw_unify: typ * typ -> bool
    64   end;
    65 
    66 structure Type : TYPE =
    67 struct
    68 
    69 (*** TFrees vs TVars ***)
    70 
    71 (*disallow TVars*)
    72 fun no_tvars T =
    73   if null (typ_tvars T) then T
    74   else raise_type "Illegal schematic type variable(s)" [T] [];
    75 
    76 (*turn TFrees into TVars to allow types & axioms to be written without "?"*)
    77 val varifyT = map_type_tfree (fn (a, S) => TVar((a, 0), S));
    78 
    79 (*inverse of varifyT*)
    80 fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    81   | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    82   | unvarifyT T = T;
    83 
    84 (*turn TFrees except those in fixed into new TVars*)
    85 fun varify (t, fixed) =
    86   let
    87     val fs = add_term_tfree_names (t, []) \\ fixed;
    88     val ixns = add_term_tvar_ixns (t, []);
    89     val fmap = fs ~~ variantlist (fs, map #1 ixns)
    90     fun thaw(f as (a,S)) = case assoc (fmap, a) of
    91                              None => TFree(f)
    92                            | Some b => TVar((b, 0), S)
    93   in  map_term_types (map_type_tfree thaw) t  end;
    94 
    95 
    96 
    97 (*** type classes and sorts ***)
    98 
    99 (*
   100   Classes denote (possibly empty) collections of types (e.g. sets of types)
   101   and are partially ordered by 'inclusion'. They are represented by strings.
   102 
   103   Sorts are intersections of finitely many classes. They are represented by
   104   lists of classes.
   105 *)
   106 
   107 type domain = sort list;
   108 
   109 
   110 (* print sorts and arities *)
   111 
   112 fun str_of_sort [c] = c
   113   | str_of_sort cs = enclose "{" "}" (commas cs);
   114 
   115 fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
   116 
   117 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
   118   | str_of_arity (t, SS, S) =
   119       t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
   120 
   121 
   122 
   123 (*** type signatures ***)
   124 
   125 (*
   126   classes:
   127     a list of all declared classes;
   128 
   129   subclass:
   130     an association list representing the subclass relation; (c, cs) is
   131     interpreted as "c is a proper subclass of all elemenst of cs"; note that
   132     c itself is not a member of cs;
   133 
   134   default:
   135     the default sort attached to all unconstrained type vars;
   136 
   137   tycons:
   138     an association list of all declared types with the number of their
   139     arguments;
   140 
   141   abbrs:
   142     an association list of type abbreviations;
   143 
   144   arities:
   145     a two-fold association list of all type arities; (t, al) means that type
   146     constructor t has the arities in al; an element (c, ss) of al represents
   147     the arity (ss)c;
   148 *)
   149 
   150 datatype type_sig =
   151   TySg of {
   152     classes: class list,
   153     subclass: (class * class list) list,
   154     default: sort,
   155     tycons: (string * int) list,
   156     abbrs: (string * (string list * typ)) list,
   157     arities: (string * (class * domain) list) list};
   158 
   159 fun rep_tsig (TySg comps) = comps;
   160 
   161 fun defaultS (TySg {default, ...}) = default;
   162 
   163 
   164 (* error messages *)
   165 
   166 fun undcl_class c = "Undeclared class " ^ quote c;
   167 fun err_undcl_class s = error (undcl_class s);
   168 
   169 fun err_dup_classes cs =
   170   error ("Duplicate declaration of class(es) " ^ commas_quote cs);
   171 
   172 fun undcl_type c = "Undeclared type constructor " ^ quote c;
   173 
   174 fun err_neg_args c =
   175   error ("Negative number of arguments of type constructor " ^ quote c);
   176 
   177 fun err_dup_tycon c =
   178   error ("Duplicate declaration of type constructor " ^ quote c);
   179 
   180 fun dup_tyabbrs ts =
   181   "Duplicate declaration of type abbreviation(s) " ^ commas_quote ts;
   182 
   183 fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
   184 
   185 
   186 (* 'leq' checks the partial order on classes according to the
   187    statements in the association list 'a' (i.e. 'subclass')
   188 *)
   189 
   190 fun less a (C, D) = case assoc (a, C) of
   191      Some ss => D mem_string ss
   192    | None => err_undcl_class C;
   193 
   194 fun leq a (C, D)  =  C = D orelse less a (C, D);
   195 
   196 
   197 (* logical_types *)
   198 
   199 (*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
   200   and c <= logic*)
   201 
   202 fun logical_types tsig =
   203   let
   204     val TySg {subclass, arities, tycons, ...} = tsig;
   205 
   206     fun log_class c = leq subclass (c, logicC);
   207     fun log_type t = exists (log_class o #1) (assocs arities t);
   208   in
   209     filter log_type (map #1 tycons)
   210   end;
   211 
   212 
   213 (* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
   214    S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
   215    with C1 <= C2 (according to an association list 'a')
   216 *)
   217 
   218 fun sortorder a (S1, S2) =
   219   forall  (fn C2 => exists  (fn C1 => leq a (C1, C2))  S1)  S2;
   220 
   221 
   222 (* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
   223   there exists no class in S which is <= C;
   224   the resulting set is minimal if S was minimal
   225 *)
   226 
   227 fun inj a (C, S) =
   228   let fun inj1 [] = [C]
   229         | inj1 (D::T) = if leq a (D, C) then D::T
   230                         else if leq a (C, D) then inj1 T
   231                              else D::(inj1 T)
   232   in inj1 S end;
   233 
   234 
   235 (* 'union_sort' forms the minimal union set of two sorts S1 and S2
   236    under the assumption that S2 is minimal *)
   237 (* FIXME rename to inter_sort (?) *)
   238 
   239 fun union_sort a = foldr (inj a);
   240 
   241 
   242 (* 'elementwise_union' forms elementwise the minimal union set of two
   243    sort lists under the assumption that the two lists have the same length
   244 *)
   245 
   246 fun elementwise_union a (Ss1, Ss2) = ListPair.map (union_sort a) (Ss1,Ss2);
   247 
   248 
   249 (* 'lew' checks for two sort lists the ordering for all corresponding list
   250    elements (i.e. sorts) *)
   251 
   252 fun lew a (w1, w2) = ListPair.all (sortorder a)  (w1,w2);
   253 
   254 
   255 (* 'is_min' checks if a class C is minimal in a given sort S under the
   256    assumption that S contains C *)
   257 
   258 fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
   259 
   260 
   261 (* 'min_sort' reduces a sort to its minimal classes *)
   262 
   263 fun min_sort a S = distinct(filter (is_min a S) S);
   264 
   265 
   266 (* 'min_domain' minimizes the domain sorts of type declarationsl;
   267    the function will be applied on the type declarations in extensions *)
   268 
   269 fun min_domain subclass =
   270   let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
   271   in map one_min end;
   272 
   273 
   274 (* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
   275    and gives back a list of those range classes whose domains meet the
   276    predicate 'pred' *)
   277 
   278 fun min_filter a pred ars =
   279   let fun filt ([], l) = l
   280         | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
   281                                else filt (xs, l)
   282   in filt (ars, []) end;
   283 
   284 
   285 (* 'cod_above' filters all arities whose domains are elementwise >= than
   286    a given domain 'w' and gives back a list of the corresponding range
   287    classes *)
   288 
   289 fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
   290 
   291 
   292 
   293 (*Instantiation of type variables in types*)
   294 (*Pre: instantiations obey restrictions! *)
   295 fun inst_typ tye =
   296   let fun inst(var as (v, _)) = case assoc(tye, v) of
   297                                   Some U => inst_typ tye U
   298                                 | None => TVar(var)
   299   in map_type_tvar inst end;
   300 
   301 (* 'least_sort' returns for a given type its maximum sort:
   302    - type variables, free types: the sort brought with
   303    - type constructors: recursive determination of the maximum sort of the
   304                     arguments if the type is declared in 'arities' of the
   305                     given type signature  *)
   306 
   307 fun least_sort (tsig as TySg{subclass, arities, ...}) =
   308   let fun ls(T as Type(a, Ts)) =
   309                  (case assoc (arities, a) of
   310                           Some(ars) => cod_above(subclass, map ls Ts, ars)
   311                         | None => raise TYPE(undcl_type a, [T], []))
   312         | ls(TFree(a, S)) = S
   313         | ls(TVar(a, S)) = S
   314   in ls end;
   315 
   316 
   317 fun check_has_sort(tsig as TySg{subclass, arities, ...}, T, S) =
   318   if sortorder subclass ((least_sort tsig T), S) then ()
   319   else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
   320 
   321 
   322 (*Instantiation of type variables in types *)
   323 fun inst_typ_tvars(tsig, tye) =
   324   let fun inst(var as (v, S)) = case assoc(tye, v) of
   325               Some U => (check_has_sort(tsig, U, S); U)
   326             | None => TVar(var)
   327   in map_type_tvar inst end;
   328 
   329 (*Instantiation of type variables in terms *)
   330 fun inst_term_tvars (_,[]) t = t
   331   | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;
   332 
   333 
   334 (* norm_typ *)
   335 
   336 fun norm_typ (TySg {abbrs, ...}) ty =
   337   let
   338     val idx = maxidx_of_typ ty + 1;
   339 
   340     fun expand (Type (a, Ts)) =
   341           (case assoc (abbrs, a) of
   342             Some (vs, U) =>
   343               expand (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
   344           | None => Type (a, map expand Ts))
   345       | expand T = T
   346   in
   347     expand ty
   348   end;
   349 
   350 
   351 (** type matching **)
   352 
   353 exception TYPE_MATCH;
   354 
   355 (*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
   356 fun typ_match tsig =
   357   let
   358     fun match (subs, (TVar (v, S), T)) =
   359           (case assoc (subs, v) of
   360             None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
   361               handle TYPE _ => raise TYPE_MATCH)
   362           | Some U => if U = T then subs else raise TYPE_MATCH)
   363       | match (subs, (Type (a, Ts), Type (b, Us))) =
   364           if a <> b then raise TYPE_MATCH
   365           else foldl match (subs, Ts ~~ Us)
   366       | match (subs, (TFree x, TFree y)) =
   367           if x = y then subs else raise TYPE_MATCH
   368       | match _ = raise TYPE_MATCH;
   369   in match end;
   370 
   371 
   372 fun typ_instance (tsig, T, U) =
   373   (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
   374 
   375 
   376 
   377 (** build type signatures **)
   378 
   379 fun make_tsig (classes, subclass, default, tycons, abbrs, arities) =
   380   TySg {classes = classes, subclass = subclass, default = default,
   381     tycons = tycons, abbrs = abbrs, arities = arities};
   382 
   383 val tsig0 = make_tsig ([], [], [], [], [], []);
   384 
   385 
   386 (* sorts *)
   387 
   388 fun subsort (TySg {subclass, ...}) (S1, S2) =
   389   sortorder subclass (S1, S2);
   390 
   391 fun norm_sort (TySg {subclass, ...}) S =
   392   sort_strings (min_sort subclass S);
   393 
   394 (* FIXME tmp! (sorts.ML) *)
   395 fun eq_sort tsig (S1, S2) =
   396   norm_sort tsig S1 = norm_sort tsig S2;
   397 
   398 fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
   399   | rem_sorts (TFree (x, _)) = TFree (x, [])
   400   | rem_sorts (TVar (xi, _)) = TVar (xi, []);
   401 
   402 
   403 (* nonempty_sort *)
   404 
   405 (* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
   406 fun nonempty_sort _ _ [] = true
   407   | nonempty_sort (tsig as TySg {arities, ...}) hyps S =
   408       exists (exists (fn (c, ss) => [c] = S andalso null ss) o snd) arities
   409         orelse exists (fn S' => subsort tsig (S', S)) hyps;
   410 
   411 
   412 
   413 (* typ_errors *)
   414 
   415 (*check validity of (not necessarily normal) type; accumulate error messages*)
   416 
   417 fun typ_errors tsig (typ, errors) =
   418   let
   419     val TySg {classes, tycons, abbrs, ...} = tsig;
   420 
   421     fun class_err (errs, c) =
   422       if c mem_string classes then errs
   423       else undcl_class c ins_string errs;
   424 
   425     val sort_err = foldl class_err;
   426 
   427     fun typ_errs (Type (c, Us), errs) =
   428           let
   429             val errs' = foldr typ_errs (Us, errs);
   430             fun nargs n =
   431               if n = length Us then errs'
   432               else ("Wrong number of arguments: " ^ quote c) ins_string errs';
   433           in
   434             (case assoc (tycons, c) of
   435               Some n => nargs n
   436             | None =>
   437                 (case assoc (abbrs, c) of
   438                   Some (vs, _) => nargs (length vs)
   439                 | None => undcl_type c ins_string errs))
   440           end
   441     | typ_errs (TFree (_, S), errs) = sort_err (errs, S)
   442     | typ_errs (TVar ((x, i), S), errs) =
   443         if i < 0 then
   444           ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
   445         else sort_err (errs, S);
   446   in
   447     typ_errs (typ, errors)
   448   end;
   449 
   450 
   451 (* cert_typ *)
   452 
   453 (*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
   454 
   455 fun cert_typ tsig ty =
   456   (case typ_errors tsig (ty, []) of
   457     [] => norm_typ tsig ty
   458   | errs => raise_type (cat_lines errs) [ty] []);
   459 
   460 
   461 
   462 (** merge type signatures **)
   463 
   464 (*'assoc_union' merges two association lists if the contents associated
   465   the keys are lists*)
   466 
   467 fun assoc_union (as1, []) = as1
   468   | assoc_union (as1, (key, l2) :: as2) =
   469       (case assoc_string (as1, key) of
   470         Some l1 => assoc_union 
   471 	              (overwrite (as1, (key, l1 union_string l2)), as2)
   472       | None => assoc_union ((key, l2) :: as1, as2));
   473 
   474 
   475 (* merge subclass *)
   476 
   477 fun merge_subclass (subclass1, subclass2) =
   478   let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) 
   479   in
   480     if exists (op mem_string) subclass then
   481       error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
   482     else subclass
   483   end;
   484 
   485 
   486 (* coregularity *)
   487 
   488 (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
   489 
   490 fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
   491       Some(w1) => if w = w1 then () else
   492         error("There are two declarations\n" ^
   493               str_of_arity(t, w, [C]) ^ " and\n" ^
   494               str_of_arity(t, w1, [C]) ^ "\n" ^
   495               "with the same result class.")
   496     | None => ();
   497 
   498 (* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   499    such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
   500 
   501 fun coreg_err(t, (C1,w1), (C2,w2)) =
   502     error("Declarations " ^ str_of_arity(t, w1, [C1]) ^ " and "
   503                           ^ str_of_arity(t, w2, [C2]) ^ " are in conflict");
   504 
   505 fun coreg subclass (t, Cw1) =
   506   let fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   507         if leq subclass (C1,C2)
   508         then if lew subclass (w1,w2) then () else coreg_err(t, Cw1, Cw2)
   509         else ()
   510       fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   511   in seq check end;
   512 
   513 fun add_arity subclass ars (tCw as (_,Cw)) =
   514       (is_unique_decl ars tCw; coreg subclass tCw ars; Cw ins ars);
   515 
   516 fun varying_decls t =
   517   error ("Type constructor " ^ quote t ^ " has varying number of arguments");
   518 
   519 
   520 (* 'merge_arities' builds the union of two 'arities' lists;
   521    it only checks the two restriction conditions and inserts afterwards
   522    all elements of the second list into the first one *)
   523 
   524 fun merge_arities subclass =
   525   let fun test_ar t (ars1, sw) = add_arity subclass ars1 (t,sw);
   526 
   527       fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
   528           Some(ars1) =>
   529             let val ars = foldl (test_ar t) (ars1, ars2)
   530             in overwrite (arities1, (t,ars)) end
   531         | None => c::arities1
   532   in foldl merge_c end;
   533 
   534 fun add_tycons (tycons, tn as (t,n)) =
   535   (case assoc (tycons, t) of
   536     Some m => if m = n then tycons else varying_decls t
   537   | None => tn :: tycons);
   538 
   539 fun merge_abbrs (abbrs1, abbrs2) =
   540   let val abbrs = abbrs1 union abbrs2 in
   541     (case gen_duplicates eq_fst abbrs of
   542       [] => abbrs
   543     | dups => raise_term (dup_tyabbrs (map fst dups)) [])
   544   end;
   545 
   546 
   547 (* 'merge_tsigs' takes the above declared functions to merge two type
   548   signatures *)
   549 
   550 fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1,
   551                      tycons=tycons1, arities=arities1, abbrs=abbrs1},
   552                 TySg{classes=classes2, default=default2, subclass=subclass2,
   553                      tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
   554   let val classes' = classes1 union_string classes2;
   555       val subclass' = merge_subclass (subclass1, subclass2);
   556       val tycons' = foldl add_tycons (tycons1, tycons2)
   557       val arities' = merge_arities subclass' (arities1, arities2);
   558       val default' = min_sort subclass' (default1 @ default2);
   559       val abbrs' = merge_abbrs(abbrs1, abbrs2);
   560   in make_tsig(classes', subclass', default', tycons', abbrs', arities') end;
   561 
   562 
   563 
   564 (*** extend type signatures ***)
   565 
   566 (** add classes and subclass relations**)
   567 
   568 fun add_classes classes cs =
   569   (case cs inter_string classes of
   570     [] => cs @ classes
   571   | dups => err_dup_classes cs);
   572 
   573 
   574 (*'add_subclass' adds a tuple consisting of a new class (the new class has
   575   already been inserted into the 'classes' list) and its superclasses (they
   576   must be declared in 'classes' too) to the 'subclass' list of the given type
   577   signature; furthermore all inherited superclasses according to the
   578   superclasses brought with are inserted and there is a check that there are
   579   no cycles (i.e. C <= D <= C, with C <> D);*)
   580 
   581 fun add_subclass classes (subclass, (s, ges)) =
   582   let
   583     fun upd (subclass, s') =
   584       if s' mem_string classes then
   585         let val ges' = the (assoc (subclass, s))
   586         in case assoc (subclass, s') of
   587              Some sups => if s mem_string sups
   588                            then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
   589                            else overwrite 
   590 			          (subclass, (s, sups union_string ges'))
   591            | None => subclass
   592         end
   593       else err_undcl_class s'
   594   in foldl upd (subclass @ [(s, ges)], ges) end;
   595 
   596 
   597 (* 'extend_classes' inserts all new classes into the corresponding
   598    lists ('classes', 'subclass') if possible *)
   599 
   600 fun extend_classes (classes, subclass, new_classes) =
   601   let
   602     val classes' = add_classes classes (map fst new_classes);
   603     val subclass' = foldl (add_subclass classes') (subclass, new_classes);
   604   in (classes', subclass') end;
   605 
   606 
   607 (* ext_tsig_classes *)
   608 
   609 fun ext_tsig_classes tsig new_classes =
   610   let
   611     val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   612     val (classes',subclass') = extend_classes (classes,subclass,new_classes);
   613   in
   614     make_tsig (classes', subclass', default, tycons, abbrs, arities)
   615   end;
   616 
   617 
   618 (* ext_tsig_subclass *)
   619 
   620 fun ext_tsig_subclass tsig pairs =
   621   let
   622     val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   623 
   624     (* FIXME clean! *)
   625     val subclass' =
   626       merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
   627   in
   628     make_tsig (classes, subclass', default, tycons, abbrs, arities)
   629   end;
   630 
   631 
   632 (* ext_tsig_defsort *)
   633 
   634 fun ext_tsig_defsort(TySg{classes,subclass,tycons,abbrs,arities,...}) default =
   635   make_tsig (classes, subclass, default, tycons, abbrs, arities);
   636 
   637 
   638 
   639 (** add types **)
   640 
   641 fun ext_tsig_types (TySg {classes, subclass, default, tycons, abbrs, arities}) ts =
   642   let
   643     fun check_type (c, n) =
   644       if n < 0 then err_neg_args c
   645       else if is_some (assoc (tycons, c)) then err_dup_tycon c
   646       else if is_some (assoc (abbrs, c)) then error (ty_confl c)
   647       else ();
   648   in
   649     seq check_type ts;
   650     make_tsig (classes, subclass, default, ts @ tycons, abbrs,
   651       map (rpair [] o #1) ts @ arities)
   652   end;
   653 
   654 
   655 
   656 (** add type abbreviations **)
   657 
   658 fun abbr_errors tsig (a, (lhs_vs, rhs)) =
   659   let
   660     val TySg {tycons, abbrs, ...} = tsig;
   661     val rhs_vs = map (#1 o #1) (typ_tvars rhs);
   662 
   663     val dup_lhs_vars =
   664       (case duplicates lhs_vs of
   665         [] => []
   666       | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);
   667 
   668     val extra_rhs_vars =
   669       (case gen_rems (op =) (rhs_vs, lhs_vs) of
   670         [] => []
   671       | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
   672 
   673     val tycon_confl =
   674       if is_none (assoc (tycons, a)) then []
   675       else [ty_confl a];
   676 
   677     val dup_abbr =
   678       if is_none (assoc (abbrs, a)) then []
   679       else ["Duplicate declaration of abbreviation"];
   680   in
   681     dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
   682       typ_errors tsig (rhs, [])
   683   end;
   684 
   685 fun prep_abbr tsig (a, vs, raw_rhs) =
   686   let
   687     fun err msgs = (seq writeln msgs;
   688       error ("The error(s) above occurred in type abbreviation " ^ quote a));
   689 
   690     val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
   691       handle TYPE (msg, _, _) => err [msg];
   692     val abbr = (a, (vs, rhs));
   693   in
   694     (case abbr_errors tsig abbr of
   695       [] => abbr
   696     | msgs => err msgs)
   697   end;
   698 
   699 fun add_abbr (tsig as TySg{classes,subclass,default,tycons,arities,abbrs},
   700               abbr) =
   701   make_tsig
   702     (classes,subclass,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
   703 
   704 fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   705 
   706 
   707 
   708 (** add arities **)
   709 
   710 (* 'coregular' checks
   711    - the two restrictions 'is_unique_decl' and 'coreg'
   712    - if the classes in the new type declarations are known in the
   713      given type signature
   714    - if one type constructor has always the same number of arguments;
   715    if one type declaration has passed all checks it is inserted into
   716    the 'arities' association list of the given type signatrure  *)
   717 
   718 fun coregular (classes, subclass, tycons) =
   719   let fun ex C = if C mem_string classes then () else err_undcl_class(C);
   720 
   721       fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
   722             Some(n) => if n <> length w then varying_decls(t) else
   723                      ((seq o seq) ex w; ex C;
   724                       let val ars = the (assoc(arities, t))
   725                           val ars' = add_arity subclass ars (t,(C,w))
   726                       in overwrite(arities, (t,ars')) end)
   727           | None => error (undcl_type t);
   728 
   729   in addar end;
   730 
   731 
   732 (* 'close' extends the 'arities' association list after all new type
   733    declarations have been inserted successfully:
   734    for every declaration t:(Ss)C , for all classses D with C <= D:
   735       if there is no declaration t:(Ss')C' with C < C' and C' <= D
   736       then insert the declaration t:(Ss)D into 'arities'
   737    this means, if there exists a declaration t:(Ss)C and there is
   738    no declaration t:(Ss')D with C <=D then the declaration holds
   739    for all range classes more general than C *)
   740 
   741 fun close subclass arities =
   742   let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
   743           Some sups =>
   744             let fun close_sup (l, sup) =
   745                   if exists (fn s'' => less subclass (s, s'') andalso
   746                                        leq subclass (s'', sup)) sl
   747                   then l
   748                   else (sup, dom)::l
   749             in foldl close_sup (l, sups) end
   750         | None => l;
   751       fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
   752   in map ext arities end;
   753 
   754 
   755 (* ext_tsig_arities *)
   756 
   757 fun ext_tsig_arities tsig sarities =
   758   let
   759     val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
   760     val arities1 =
   761       List.concat 
   762           (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   763     val arities2 = foldl (coregular (classes, subclass, tycons))
   764                          (arities, min_domain subclass arities1)
   765       |> close subclass;
   766   in
   767     make_tsig (classes, subclass, default, tycons, abbrs, arities2)
   768   end;
   769 
   770 
   771 
   772 (*** type unification and inference ***)
   773 
   774 (*
   775   Input:
   776     - a 'raw' term which contains only dummy types and some explicit type
   777       constraints encoded as terms.
   778     - the expected type of the term.
   779 
   780   Output:
   781     - the correctly typed term
   782     - the substitution needed to unify the actual type of the term with its
   783       expected type; only the TVars in the expected type are included.
   784 
   785   During type inference all TVars in the term have index > maxidx, where
   786   maxidx is the max. index in the expected type of the term (T). This keeps
   787   them apart, because at the end the type of the term is unified with T.
   788 
   789   1. Add initial type information to the term (attach_types).
   790      This freezes (freeze_vars) TVars in explicitly provided types (eg
   791      constraints or defaults) by turning them into TFrees.
   792   2. Carry out type inference.
   793   3. Unify actual and expected type.
   794   4. Turn all local (i.e. > maxidx) TVars into unique new TFrees (freeze).
   795   5. Thaw all TVars frozen in step 1 (thaw_vars).
   796 *)
   797 
   798 (*Raised if types are not unifiable*)
   799 exception TUNIFY;
   800 
   801 val tyvar_count = ref 0;
   802 
   803 fun tyinit(i) = (tyvar_count := i);
   804 
   805 fun new_tvar_inx () = (tyvar_count := !tyvar_count + 1; !tyvar_count)
   806 
   807 (*
   808 Generate new TVar.  Index is > maxidx+1 to distinguish it from TVars
   809 generated from variable names (see id_type).
   810 Name is arbitrary because index is new.
   811 *)
   812 
   813 fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
   814 
   815 (*Occurs check: type variable occurs in type?*)
   816 fun occ v tye =
   817   let fun occ(Type(_, Ts)) = exists occ Ts
   818         | occ(TFree _) = false
   819         | occ(TVar(w, _)) = eq_ix(v,w) orelse
   820                            (case assoc(tye, w) of
   821                               None   => false
   822                             | Some U => occ U);
   823   in occ end;
   824 
   825 (*Chase variable assignments in tye.
   826   If devar (T, tye) returns a type var then it must be unassigned.*)
   827 fun devar (T as TVar(v, _), tye) = (case  assoc(tye, v)  of
   828           Some U =>  devar (U, tye)
   829         | None   =>  T)
   830   | devar (T, tye) = T;
   831 
   832 (* use add_to_tye(t,tye) instead of t::tye
   833 to avoid chains of the form 'a |-> 'b |-> 'c ... *)
   834 
   835 fun add_to_tye(p,[]) = [p]
   836   | add_to_tye(vT as (v,T),(xU as (x,TVar(w,S)))::ps) =
   837       (if eq_ix(v,w) then (x,T) else xU) :: (add_to_tye(vT,ps))
   838   | add_to_tye(v,x::xs) = x::(add_to_tye(v,xs));
   839 
   840 (* 'dom' returns for a type constructor t the list of those domains
   841    which deliver a given range class C *)
   842 
   843 fun dom arities t C = case assoc2 (arities, (t, C)) of
   844     Some(Ss) => Ss
   845   | None => raise TUNIFY;
   846 
   847 
   848 (* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
   849    (i.e. a set of range classes ); the union is carried out elementwise
   850    for the seperate sorts in the domains *)
   851 
   852 fun union_dom (subclass, arities) (t, S) =
   853     case map (dom arities t) S of
   854 	[] => []
   855       | (d::ds) => foldl (elementwise_union subclass) (d,ds);
   856 
   857 
   858 fun W ((T, S), tsig as TySg{subclass, arities, ...}, tye) =
   859   let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
   860       fun Wk(T as TVar(v, S')) =
   861               if sortorder subclass (S', S) then tye
   862               else add_to_tye((v, gen_tyvar(union_sort subclass (S', S))),tye)
   863         | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
   864                                  else raise TUNIFY
   865         | Wk(T as Type(f, Ts)) =
   866            if null S then tye
   867            else foldr Wd (Ts~~(union_dom (subclass, arities) (f, S)) , tye)
   868   in Wk(T) end;
   869 
   870 
   871 (* Order-sorted Unification of Types (U)  *)
   872 
   873 (* Precondition: both types are well-formed w.r.t. type constructor arities *)
   874 fun unify1 (tsig as TySg{subclass, arities, ...}) =
   875   let fun unif ((T, U), tye) =
   876         case (devar(T, tye), devar(U, tye)) of
   877           (T as TVar(v, S1), U as TVar(w, S2)) =>
   878              if eq_ix(v,w) then tye else
   879              if sortorder subclass (S1, S2) then add_to_tye((w, T),tye) else
   880              if sortorder subclass (S2, S1) then add_to_tye((v, U),tye)
   881              else let val nu = gen_tyvar (union_sort subclass (S1, S2))
   882                   in add_to_tye((v, nu),add_to_tye((w, nu),tye)) end
   883         | (T as TVar(v, S), U) =>
   884              if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((v, U),tye))
   885         | (U, T as TVar (v, S)) =>
   886              if occ v tye U then raise TUNIFY else W ((U,S), tsig, add_to_tye((v, U),tye))
   887         | (Type(a, Ts), Type(b, Us)) =>
   888              if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
   889         | (T, U) => if T=U then tye else raise TUNIFY
   890   in unif end;
   891 
   892 fun unify tsig maxidx tye TU =
   893   (tyinit maxidx; (unify1 tsig (TU,tye), !tyvar_count) );
   894 
   895 (* raw_unify (ignores sorts) *)
   896 
   897 fun raw_unify (ty1, ty2) =
   898   (unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true)
   899     handle TUNIFY => false;
   900 
   901 
   902 (*Type inference for polymorphic term*)
   903 fun infer tsig =
   904   let fun inf(Ts, Const (_, T), tye) = (T, tye)
   905         | inf(Ts, Free  (_, T), tye) = (T, tye)
   906         | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
   907           handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
   908         | inf(Ts, Var (_, T), tye) = (T, tye)
   909         | inf(Ts, Abs (_, T, body), tye) =
   910             let val (U, tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
   911         | inf(Ts, f$u, tye) =
   912             let val (U, tyeU) = inf(Ts, u, tye);
   913                 val (T, tyeT) = inf(Ts, f, tyeU);
   914                 fun err s =
   915                   raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
   916 		val msg = "function type is incompatible with argument type"
   917             in case T of
   918                  Type("fun", [T1, T2]) =>
   919                    ( (T2, unify1 tsig ((T1, U), tyeT))
   920                      handle TUNIFY => err msg)
   921                | TVar _ =>
   922                    let val T2 = gen_tyvar([])
   923                    in (T2, unify1 tsig ((T, U-->T2), tyeT))
   924                       handle TUNIFY => err msg
   925                    end
   926                | _ => err"function type is expected in application"
   927            end
   928   in inf end;
   929 
   930 val freeze_vars =
   931       map_type_tvar (fn (v, S) => TFree(Syntax.string_of_vname v, S));
   932 
   933 (* Attach a type to a constant *)
   934 fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
   935 
   936 (*Find type of ident.  If not in table then use ident's name for tyvar
   937   to get consistent typing.*)
   938 fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
   939 
   940 fun type_of_ixn(types, ixn as (a, _),maxidx1) =
   941   case types ixn of Some T => freeze_vars T
   942                   | None   => TVar(("'"^a, maxidx1), []);
   943 
   944 fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
   945 
   946 fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
   947   | constrainAbs _ = sys_error "constrainAbs";
   948 
   949 
   950 (* get_sort *)
   951 
   952 fun get_sort tsig def_sort env xi =
   953   (case (assoc (env, xi), def_sort xi) of
   954     (None, None) => defaultS tsig
   955   | (None, Some S) => S
   956   | (Some S, None) => S
   957   | (Some S, Some S') =>
   958       if eq_sort tsig (S, S') then S
   959       else error ("Sort constraint inconsistent with default for type variable " ^
   960         quote (Syntax.string_of_vname' xi)));
   961 
   962 
   963 (* attach_types *)
   964 
   965 (*
   966   Attach types to a term. Input is a "parse tree" containing dummy types.
   967   Type constraints are translated and checked for validity wrt tsig. TVars in
   968   constraints are frozen.
   969 
   970   The atoms in the resulting term satisfy the following spec:
   971 
   972   Const (a, T):
   973     T is a renamed copy of the generic type of a; renaming increases index of
   974     all TVars by new_tvar_inx(), which is > maxidx+1.
   975 
   976   Free (a, T), Var (ixn, T):
   977     T is either the frozen default type of a or TVar (("'"^a, maxidx+1), [])
   978 
   979   Abs (a, T, _):
   980     T is either a type constraint or TVar (("'" ^ a, i), []), where i is
   981     generated by new_tvar_inx(). Thus different abstractions can have the
   982     bound variables of the same name but different types.
   983 *)
   984 
   985 fun attach_types (tsig, const_type, types, sorts, maxidx1) tm =
   986   let
   987     val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm;
   988 
   989     fun prepareT t =
   990       freeze_vars (cert_typ tsig (Syntax.typ_of_term (get_sort tsig sorts sort_env) t));
   991 
   992     fun add (Const (a, _)) =
   993           (case const_type a of
   994             Some T => type_const (a, T)
   995           | None => raise_type ("No such constant: " ^ quote a) [] [])
   996       | add (Free (a, _)) =
   997           (case const_type a of
   998             Some T => type_const (a, T)
   999           | None => Free (a, type_of_ixn (types,(a,~1),maxidx1)))
  1000       | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn, maxidx1))
  1001       | add (Bound i) = Bound i
  1002       | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
  1003       | add ((f as Const (a, _) $ t1) $ t2) =
  1004           if a = Syntax.constrainC then
  1005             constrain (add t1, prepareT t2)
  1006           else if a = Syntax.constrainAbsC then
  1007             constrainAbs (add t1, prepareT t2)
  1008           else add f $ add t2
  1009       | add (f $ t) = add f $ add t;
  1010   in add tm end;
  1011 
  1012 
  1013 (* Post-Processing *)
  1014 
  1015 (*Instantiation of type variables in terms*)
  1016 fun inst_types tye = map_term_types (inst_typ tye);
  1017 
  1018 (*Delete explicit constraints -- occurrences of "_constrain" *)
  1019 fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
  1020   | unconstrain ((f as Const(a, _)) $ t) =
  1021       if a=Syntax.constrainC then unconstrain t
  1022       else unconstrain f $ unconstrain t
  1023   | unconstrain (f$t) = unconstrain f $ unconstrain t
  1024   | unconstrain (t) = t;
  1025 
  1026 fun nextname(pref,c) = if c="z" then (pref^"a", "a") else (pref,chr(ord(c)+1));
  1027 
  1028 fun newtvars used =
  1029   let fun new([],_,vmap) = vmap
  1030         | new(ixn::ixns,p as (pref,c),vmap) =
  1031             let val nm = pref ^ c
  1032             in if nm mem_string used then new(ixn::ixns,nextname p, vmap)
  1033                else new(ixns, nextname p, (ixn,nm)::vmap)
  1034             end
  1035   in new end;
  1036 
  1037 (*
  1038 Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
  1039 Note that if t contains frozen TVars there is the possibility that a TVar is
  1040 turned into one of those. This is sound but not complete.
  1041 *)
  1042 fun convert used freeze p t =
  1043   let val used = if freeze then add_term_tfree_names(t, used)
  1044                  else used union
  1045                       (map #1 (filter_out p (add_term_tvar_ixns(t, []))))
  1046       val ixns = filter p (add_term_tvar_ixns(t, []));
  1047       val vmap = newtvars used (ixns,("'","a"),[]);
  1048       fun conv(var as (ixn,S)) = case assoc(vmap,ixn) of
  1049             None => TVar(var) |
  1050             Some(a) => if freeze then TFree(a,S) else TVar((a,0),S);
  1051   in map_term_types (map_type_tvar conv) t end;
  1052 
  1053 fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
  1054 
  1055 (* Thaw all TVars that were frozen in freeze_vars *)
  1056 val thaw_vars =
  1057   let fun thaw(f as (a, S)) = (case explode a of
  1058           "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
  1059                           in TVar(("'"^b, i), S) end
  1060         | _ => TFree f)
  1061   in map_type_tfree thaw end;
  1062 
  1063 
  1064 fun restrict maxidx1 tye =
  1065   let fun clean(tye1, ((a, i), T)) =
  1066         if i >= maxidx1 then tye1 else ((a, i), inst_typ tye T) :: tye1
  1067   in foldl clean ([], tye) end
  1068 
  1069 
  1070 (*Infer types for terms.  Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that
  1071 	the type of ti unifies with Ti (i=1,...,n).
  1072   types is a partial map from indexnames to types (constrains Free, Var).
  1073   sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
  1074   used is the list of already used type variables.
  1075   If freeze then internal TVars are turned into TFrees, else TVars.*)
  1076 fun infer_types (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
  1077   let
  1078     val maxidx1 = maxidx_of_typs Ts + 1;
  1079     val () = tyinit(maxidx1+1);
  1080     val us = map (attach_types (tsig, const_type, types, sorts, maxidx1)) ts;
  1081     val u = list_comb(Const("",Ts ---> propT),us)
  1082     val (_, tye) = infer tsig ([], u, []);
  1083     val uu = unconstrain u;
  1084     val Ttye = restrict maxidx1 tye (*restriction to TVars in Ts*)
  1085     val all = Const("", Type("", map snd Ttye)) $ (inst_types tye uu)
  1086       (*all is a dummy term which contains all exported TVars*)
  1087     val Const(_, Type(_, Us)) $ u'' =
  1088       map_term_types thaw_vars (convert used freeze (fn (_,i) => i >= maxidx1) all)
  1089       (*convert all internally generated TVars into TFrees or TVars
  1090         and thaw all initially frozen TVars*)
  1091   in
  1092     (#2(strip_comb u''), ListPair.zip(map #1 Ttye, Us))
  1093   end;
  1094 
  1095 end;