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