src/Pure/type.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 162 58d54dc482d1
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	Types and Sorts
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:	Tobias Nipkow & Lawrence C Paulson
clasohm@0
     4
clasohm@0
     5
Maybe type classes should go in a separate module?
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
clasohm@0
     9
signature TYPE =
clasohm@0
    10
sig
clasohm@0
    11
  structure Symtab:SYMTAB
clasohm@0
    12
  type type_sig
clasohm@0
    13
  val defaultS: type_sig -> sort
clasohm@0
    14
  val extend: type_sig * (class * class list)list * sort *
clasohm@0
    15
	      (string list * int)list *
clasohm@0
    16
	      (string list * (sort list * class))list -> type_sig
clasohm@0
    17
  val freeze: (indexname -> bool) -> term -> term
clasohm@0
    18
  val freeze_vars: typ -> typ
clasohm@0
    19
  val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) *
clasohm@0
    20
		   (indexname -> sort option) * (typ -> string) * typ * term
clasohm@0
    21
		   -> term * (indexname*typ)list
clasohm@0
    22
  val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term
clasohm@0
    23
  val logical_type: type_sig -> string -> bool
clasohm@0
    24
  val merge: type_sig * type_sig -> type_sig
clasohm@0
    25
  val thaw_vars: typ -> typ
clasohm@0
    26
  val tsig0: type_sig
clasohm@0
    27
  val type_errors: type_sig * (typ->string) -> typ * string list -> string list
clasohm@0
    28
  val typ_instance: type_sig * typ * typ -> bool
clasohm@0
    29
  val typ_match: type_sig -> (indexname*typ)list * (typ*typ) ->
clasohm@0
    30
		 (indexname*typ)list
clasohm@0
    31
  val unify: type_sig -> (typ*typ) * (indexname*typ)list -> (indexname*typ)list
clasohm@0
    32
  val varifyT: typ -> typ
clasohm@0
    33
  val varify: term * string list -> term
clasohm@0
    34
  exception TUNIFY
clasohm@0
    35
  exception TYPE_MATCH;
clasohm@0
    36
end;
clasohm@0
    37
clasohm@0
    38
functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) : TYPE =
clasohm@0
    39
struct
clasohm@0
    40
structure Symtab = Symtab
clasohm@0
    41
clasohm@0
    42
(* Miscellany *)
clasohm@0
    43
clasohm@0
    44
val commas = space_implode ",";
clasohm@0
    45
fun str_of_sort S = "{" ^ commas S ^ "}";
clasohm@0
    46
fun str_of_dom dom = "(" ^ commas (map str_of_sort dom) ^ ")";
clasohm@0
    47
fun str_of_decl(t,w,C) = t ^ ": " ^ str_of_dom w ^ C;
clasohm@0
    48
clasohm@0
    49
clasohm@0
    50
(* Association list Manipulation  *)
clasohm@0
    51
clasohm@0
    52
clasohm@0
    53
(* two-fold Association list lookup *)
clasohm@0
    54
clasohm@0
    55
fun assoc2 (aal,(key1,key2)) = case assoc (aal,key1) of
clasohm@0
    56
    Some (al) => assoc (al,key2)
clasohm@0
    57
  | None => None;
clasohm@0
    58
clasohm@0
    59
clasohm@0
    60
clasohm@0
    61
(**** TYPE CLASSES ****)
clasohm@0
    62
clasohm@0
    63
type domain = sort list;
clasohm@0
    64
type arity = domain * class;
clasohm@0
    65
clasohm@0
    66
datatype type_sig =
clasohm@0
    67
   TySg of {classes: class list,
clasohm@0
    68
	    default: sort,
clasohm@0
    69
	    subclass: (class * class list) list,
clasohm@0
    70
	    args: (string * int) list,
clasohm@0
    71
	    coreg: (string * (class * domain) list) list };
clasohm@0
    72
clasohm@0
    73
(* classes: a list of all declared classes;
clasohm@0
    74
   default: the default sort attached to all unconstrained TVars
clasohm@0
    75
            occurring in a term to be type-inferred;
clasohm@0
    76
   subclass: association list representation of subclass relationship;
clasohm@0
    77
             (c,cs) is interpreted as "c is a proper subclass of all
clasohm@0
    78
             elemenst of cs". Note that c itself is not a memeber of cs.
clasohm@0
    79
   args: an association list of all declared types with the number of their
clasohm@0
    80
         arguments
clasohm@0
    81
   coreg: a two-fold association list of all type arities; (t,al) means that
clasohm@0
    82
          type constructor t has the arities in al; an element (c,ss) of al
clasohm@0
    83
          represents the arity (ss)c
clasohm@0
    84
*)
clasohm@0
    85
clasohm@0
    86
clasohm@0
    87
val tsig0 = TySg{classes = [],
clasohm@0
    88
		 default = [],
clasohm@0
    89
		 subclass = [],
clasohm@0
    90
		 args = [],
clasohm@0
    91
		 coreg = []};
clasohm@0
    92
clasohm@0
    93
fun undcl_class (s) = error("Class " ^ s ^ " has not been declared");
clasohm@0
    94
clasohm@0
    95
fun undcl_type(c) = "Undeclared type: " ^ c;
clasohm@0
    96
fun undcl_type_err(c) = error(undcl_type(c));
clasohm@0
    97
clasohm@0
    98
clasohm@0
    99
(* 'leq' checks the partial order on classes according to the
clasohm@0
   100
   statements in the association list 'a' (i.e.'subclass')
clasohm@0
   101
*)
clasohm@0
   102
clasohm@0
   103
fun less a (C,D) = case assoc (a,C) of
clasohm@0
   104
     Some(ss) => D mem ss
clasohm@0
   105
   | None => undcl_class (C) ;
clasohm@0
   106
clasohm@0
   107
fun leq a (C,D)  =  C = D orelse less a (C,D);
clasohm@0
   108
clasohm@0
   109
clasohm@0
   110
fun defaultS(TySg{default,...}) = default;
clasohm@0
   111
clasohm@0
   112
(* 'logical_type' checks if some type declaration t has as range
clasohm@0
   113
   a class which is a subclass of "logic" *)
clasohm@0
   114
clasohm@0
   115
fun logical_type(tsig as TySg{subclass,coreg,...}) t =
clasohm@0
   116
  let fun is_log C = leq subclass (C,"logic")
clasohm@0
   117
  in case assoc (coreg,t) of
clasohm@0
   118
      Some(ars) => exists (is_log o #1) ars
clasohm@0
   119
    | None => undcl_type_err(t)
clasohm@0
   120
  end;
clasohm@0
   121
clasohm@0
   122
clasohm@0
   123
(* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
clasohm@0
   124
   S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1
clasohm@0
   125
   with C1 <= C2 (according to an association list 'a')
clasohm@0
   126
*)
clasohm@0
   127
clasohm@0
   128
fun sortorder a (S1,S2) =
clasohm@0
   129
  forall  (fn C2 => exists  (fn C1 => leq a (C1,C2))  S1)  S2;
clasohm@0
   130
clasohm@0
   131
clasohm@0
   132
(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
clasohm@0
   133
  there exists no class in S which is <= C;
clasohm@0
   134
  the resulting set is minimal if S was minimal
clasohm@0
   135
*)
clasohm@0
   136
clasohm@0
   137
fun inj a (C,S) =
clasohm@0
   138
  let fun inj1 [] = [C]
clasohm@0
   139
        | inj1 (D::T) = if leq a (D,C) then D::T
clasohm@0
   140
                        else if leq a (C,D) then inj1 T
clasohm@0
   141
                             else D::(inj1 T)
clasohm@0
   142
  in inj1 S end;
clasohm@0
   143
clasohm@0
   144
clasohm@0
   145
(* 'union_sort' forms the minimal union set of two sorts S1 and S2
clasohm@0
   146
   under the assumption that S2 is minimal *)
clasohm@0
   147
clasohm@0
   148
fun union_sort a = foldr (inj a);
clasohm@0
   149
clasohm@0
   150
clasohm@0
   151
(* 'elementwise_union' forms elementwise the minimal union set of two
clasohm@0
   152
   sort lists under the assumption that the two lists have the same length
clasohm@0
   153
*) 
clasohm@0
   154
clasohm@0
   155
fun elementwise_union a (Ss1,Ss2) = map (union_sort a) (Ss1~~Ss2);
clasohm@0
   156
   
clasohm@0
   157
clasohm@0
   158
(* 'lew' checks for two sort lists the ordering for all corresponding list
clasohm@0
   159
   elements (i.e. sorts) *)
clasohm@0
   160
clasohm@0
   161
fun lew a (w1,w2) = forall (sortorder a)  (w1~~w2);
clasohm@0
   162
clasohm@0
   163
 
clasohm@0
   164
(* 'is_min' checks if a class C is minimal in a given sort S under the 
clasohm@0
   165
   assumption that S contains C *) 
clasohm@0
   166
clasohm@0
   167
fun is_min a S C = not (exists (fn (D) => less a (D,C)) S);
clasohm@0
   168
clasohm@0
   169
clasohm@0
   170
(* 'min_sort' reduces a sort to its minimal classes *)
clasohm@0
   171
clasohm@0
   172
fun min_sort a S = distinct(filter (is_min a S) S);
clasohm@0
   173
clasohm@0
   174
clasohm@0
   175
(* 'min_domain' minimizes the domain sorts of type declarationsl;
clasohm@0
   176
   the function will be applied on the type declarations in extensions *) 
clasohm@0
   177
clasohm@0
   178
fun min_domain subclass =
clasohm@0
   179
  let fun one_min (f,(doms,ran)) = (f, (map (min_sort subclass) doms, ran))
clasohm@0
   180
  in map one_min end;
clasohm@0
   181
clasohm@0
   182
clasohm@0
   183
(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
clasohm@0
   184
   and gives back a list of those range classes whose domains meet the 
clasohm@0
   185
   predicate 'pred' *)
clasohm@0
   186
   
clasohm@0
   187
fun min_filter a pred ars =
clasohm@0
   188
  let fun filt ([],l) = l
clasohm@0
   189
        | filt ((c,x)::xs,l) = if pred(x) then filt (xs,inj a (c,l))
clasohm@0
   190
                               else filt (xs,l)
clasohm@0
   191
  in filt (ars,[]) end;
clasohm@0
   192
clasohm@0
   193
clasohm@0
   194
(* 'cod_above' filters all arities whose domains are elementwise >= than
clasohm@0
   195
   a given domain 'w' and gives back a list of the corresponding range 
clasohm@0
   196
   classes *)
clasohm@0
   197
clasohm@0
   198
fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars;
clasohm@0
   199
clasohm@0
   200
clasohm@0
   201
(* 'least_sort' returns for a given type its maximum sort:
clasohm@0
   202
   - type variables, free types: the sort brought with
clasohm@0
   203
   - type constructors: recursive determination of the maximum sort of the
clasohm@0
   204
                    arguments if the type is declared in 'coreg' of the 
clasohm@0
   205
                    given type signature  *) 
clasohm@0
   206
clasohm@0
   207
fun least_sort (tsig as TySg{subclass,coreg,...}) =
clasohm@0
   208
  let fun ls(T as Type(a,Ts)) =
clasohm@0
   209
	  let val ars = case assoc (coreg,a) of Some(ars) => ars
clasohm@0
   210
			      | None => raise TYPE(undcl_type a,[T],[]);
clasohm@0
   211
	  in cod_above(subclass,map ls Ts,ars) end
clasohm@0
   212
	| ls(TFree(a,S)) = S
clasohm@0
   213
	| ls(TVar(a,S)) = S
clasohm@0
   214
  in ls end;
clasohm@0
   215
clasohm@0
   216
clasohm@0
   217
fun check_has_sort(tsig as TySg{subclass,coreg,...},T,S) =
clasohm@0
   218
  if sortorder subclass ((least_sort tsig T),S) then ()
clasohm@0
   219
  else raise TYPE("Type not of sort " ^ (str_of_sort S),[T],[])
clasohm@0
   220
clasohm@0
   221
clasohm@0
   222
(*Instantiation of type variables in types *)
clasohm@0
   223
fun inst_typ_tvars(tsig,tye) =
clasohm@0
   224
  let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
clasohm@0
   225
	| inst(T as TFree _) = T
clasohm@0
   226
	| inst(T as TVar(v,S)) = (case assoc(tye,v) of
clasohm@0
   227
		None => T | Some(U) => (check_has_sort(tsig,U,S); U))
clasohm@0
   228
  in inst end;
clasohm@0
   229
clasohm@0
   230
(*Instantiation of type variables in terms *)
clasohm@0
   231
fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye));
clasohm@0
   232
clasohm@0
   233
exception TYPE_MATCH;
clasohm@0
   234
clasohm@0
   235
(* Typ matching
clasohm@0
   236
   typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *)
clasohm@0
   237
fun typ_match tsig =
clasohm@0
   238
let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of
clasohm@0
   239
		None => ( (v, (check_has_sort(tsig,T,S); T))::subs
clasohm@0
   240
			handle TYPE _ => raise TYPE_MATCH )
clasohm@0
   241
	      | Some(U) => if U=T then subs else raise TYPE_MATCH)
clasohm@0
   242
      | tm(subs, (Type(a,Ts), Type(b,Us))) =
clasohm@0
   243
	if a<>b then raise TYPE_MATCH
clasohm@0
   244
	else foldl tm (subs, Ts~~Us)
clasohm@0
   245
      | tm(subs, (TFree(x), TFree(y))) =
clasohm@0
   246
	if x=y then subs else raise TYPE_MATCH
clasohm@0
   247
      | tm _ = raise TYPE_MATCH
clasohm@0
   248
in tm end;
clasohm@0
   249
clasohm@0
   250
fun typ_instance(tsig,T,U) = let val x = typ_match tsig ([],(U,T)) in true end
clasohm@0
   251
			     handle TYPE_MATCH => false;
clasohm@0
   252
clasohm@0
   253
clasohm@0
   254
(* EXTENDING AND MERGIN TYPE SIGNATURES *)
clasohm@0
   255
clasohm@0
   256
fun not_ident(s) = error("Must be an identifier: " ^ s);
clasohm@0
   257
clasohm@0
   258
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
clasohm@0
   259
clasohm@0
   260
(*Is the type valid? Accumulates error messages in "errs".*)
clasohm@0
   261
fun type_errors (tsig as TySg{classes,subclass,args,...},
clasohm@0
   262
                 string_of_typ) (T,errs) =
clasohm@0
   263
let fun class_err([],errs) = errs
clasohm@0
   264
     |  class_err(S::Ss,errs) = 
clasohm@0
   265
          if S mem classes then class_err (Ss,errs)
clasohm@0
   266
	  else class_err (Ss,("Class " ^ S ^ " has not been declared") :: errs)
clasohm@0
   267
    fun errors(Type(c,Us), errs) =
clasohm@0
   268
	let val errs' = foldr errors (Us,errs)
clasohm@0
   269
	in case assoc(args,c) of
clasohm@0
   270
	     None => (undcl_type c) :: errs
clasohm@0
   271
	   | Some(n) => if n=length(Us) then errs'
clasohm@0
   272
		        else ("Wrong number of arguments: " ^ c) :: errs
clasohm@0
   273
	end
clasohm@0
   274
      | errors(TFree(_,S), errs) = class_err(S,errs)
clasohm@0
   275
      | errors(TVar(_,S), errs) = class_err(S,errs);
clasohm@0
   276
in case errors(T,[]) of
clasohm@0
   277
     [] => ((least_sort tsig T; errs)
clasohm@0
   278
	    handle TYPE(_,[U],_) => ("Ill-formed type: " ^ string_of_typ U)
clasohm@0
   279
				    :: errs)
clasohm@0
   280
   | errs' => errs'@errs
clasohm@0
   281
end;
clasohm@0
   282
clasohm@0
   283
clasohm@0
   284
(* 'add_class' adds a new class to the list of all existing classes *) 
clasohm@0
   285
clasohm@0
   286
fun add_class (classes,(s,_)) =
clasohm@0
   287
  if s mem classes then error("Class " ^ s ^ " declared twice.")
clasohm@0
   288
  else s::classes;
clasohm@0
   289
clasohm@0
   290
(* 'add_subclass' adds a tuple consisiting of a new class (the new class
clasohm@0
   291
   has already been inserted into the 'classes' list) and its
clasohm@0
   292
   superclasses (they must be declared in 'classes' too) to the 'subclass' 
clasohm@0
   293
   list of the given type signature; 
clasohm@0
   294
   furthermore all inherited superclasses according to the superclasses 
clasohm@0
   295
   brought with are inserted and there is a check that there are no
clasohm@0
   296
   cycles (i.e. C <= D <= C, with C <> D); *)
clasohm@0
   297
clasohm@0
   298
fun add_subclass classes (subclass,(s,ges)) =
clasohm@0
   299
let fun upd (subclass,s') = if s' mem classes then
clasohm@0
   300
        let val Some(ges') = assoc (subclass,s)
clasohm@0
   301
        in case assoc (subclass,s') of
clasohm@0
   302
             Some(sups) => if s mem sups
clasohm@0
   303
                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
clasohm@0
   304
                           else overwrite (subclass,(s,sups union ges'))
clasohm@0
   305
           | None => subclass
clasohm@0
   306
         end
clasohm@0
   307
         else undcl_class(s')
clasohm@0
   308
in foldl upd (subclass@[(s,ges)],ges) end;
clasohm@0
   309
clasohm@0
   310
clasohm@0
   311
(* 'extend_classes' inserts all new classes into the corresponding
clasohm@0
   312
   lists ('classes','subclass') if possible *)
clasohm@0
   313
clasohm@0
   314
fun extend_classes (classes,subclass,newclasses) =
clasohm@0
   315
  if newclasses = [] then (classes,subclass) else
clasohm@0
   316
  let val classes' = foldl add_class (classes,newclasses);
clasohm@0
   317
      val subclass' = foldl (add_subclass classes') (subclass,newclasses);
clasohm@0
   318
  in (classes',subclass') end;
clasohm@0
   319
clasohm@0
   320
(* Corregularity *)
clasohm@0
   321
clasohm@0
   322
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
clasohm@0
   323
clasohm@0
   324
fun is_unique_decl coreg (t,(s,w)) = case assoc2 (coreg,(t,s)) of
clasohm@0
   325
      Some(w1) => if w = w1 then () else
clasohm@0
   326
	error("There are two declarations\n" ^
clasohm@0
   327
              str_of_decl(t,w,s) ^ " and\n" ^
clasohm@0
   328
	      str_of_decl(t,w1,s) ^ "\n" ^
clasohm@0
   329
              "with the same result class.")
clasohm@0
   330
    | None => ();
clasohm@0
   331
clasohm@0
   332
(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
clasohm@0
   333
   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
clasohm@0
   334
clasohm@0
   335
fun subs (classes,subclass) C = 
clasohm@0
   336
  let fun sub (rl,l) = if leq subclass (l,C) then l::rl else rl
clasohm@0
   337
  in foldl sub ([],classes) end;
clasohm@0
   338
clasohm@0
   339
fun coreg_err(t,(w1,C),(w2,D)) =
clasohm@0
   340
    error("Declarations " ^ str_of_decl(t,w1,C) ^ " and "
clasohm@0
   341
                          ^ str_of_decl(t,w2,D) ^ " are in conflict");
clasohm@0
   342
clasohm@0
   343
fun restr2 classes (subclass,coreg) (t,(s,w)) =
clasohm@0
   344
  let fun restr ([],test) = ()
clasohm@0
   345
        | restr (s1::Ss,test) = (case assoc2 (coreg,(t,s1)) of
clasohm@0
   346
              Some (dom) => if lew subclass (test (w,dom)) then restr (Ss,test)
clasohm@0
   347
                            else coreg_err (t,(w,s),(dom,s1))
clasohm@0
   348
            | None => restr (Ss,test))
clasohm@0
   349
      fun forward (t,(s,w)) =
clasohm@0
   350
        let val s_sups = case assoc (subclass,s) of
clasohm@0
   351
                   Some(s_sups) => s_sups | None => undcl_class(s);
clasohm@0
   352
        in restr (s_sups,I) end
clasohm@0
   353
      fun backward (t,(s,w)) =
clasohm@0
   354
        let val s_subs = subs (classes,subclass) s
clasohm@0
   355
        in restr (s_subs,fn (x,y) => (y,x)) end
clasohm@0
   356
  in (backward (t,(s,w)); forward (t,(s,w))) end;
clasohm@0
   357
clasohm@0
   358
clasohm@0
   359
fun varying_decls(t) =
clasohm@0
   360
    error("Type constructor "^t^" has varying number of arguments.");
clasohm@0
   361
clasohm@0
   362
clasohm@0
   363
clasohm@0
   364
(* 'coregular' checks
clasohm@0
   365
   - the two restriction conditions 'is_unique_decl' and 'restr2'
clasohm@0
   366
   - if the classes in the new type declarations are known in the 
clasohm@0
   367
     given type signature
clasohm@0
   368
   - if one type constructor has always the same number of arguments;
clasohm@0
   369
   if one type declaration has passed all checks it is inserted into 
clasohm@0
   370
   the 'coreg' association list of the given type signatrure  *)
clasohm@0
   371
clasohm@0
   372
fun coregular (classes,subclass,args) =
clasohm@0
   373
  let fun ex C = if C mem classes then () else undcl_class(C);
clasohm@0
   374
clasohm@0
   375
      fun addar(w,C) (coreg,t) = case assoc(args,t) of
clasohm@0
   376
            Some(n) => if n <> length w then varying_decls(t) else
clasohm@0
   377
                     (is_unique_decl coreg (t,(C,w));
clasohm@0
   378
	              (seq o seq) ex w;
clasohm@0
   379
	              restr2 classes (subclass,coreg) (t,(C,w));
clasohm@0
   380
                      let val Some(ars) = assoc(coreg,t)
clasohm@0
   381
                      in overwrite(coreg,(t,(C,w) ins ars)) end)
clasohm@0
   382
          | None => undcl_type_err(t);
clasohm@0
   383
clasohm@0
   384
      fun addts(coreg,(ts,ar)) = foldl (addar ar) (coreg,ts)
clasohm@0
   385
clasohm@0
   386
  in addts end;
clasohm@0
   387
clasohm@0
   388
clasohm@0
   389
(* 'close' extends the 'coreg' association list after all new type
clasohm@0
   390
   declarations have been inserted successfully:
clasohm@0
   391
   for every declaration t:(Ss)C , for all classses D with C <= D:
clasohm@0
   392
      if there is no declaration t:(Ss')C' with C < C' and C' <= D
clasohm@0
   393
      then insert the declaration t:(Ss)D into 'coreg'
clasohm@0
   394
   this means, if there exists a declaration t:(Ss)C and there is
clasohm@0
   395
   no declaration t:(Ss')D with C <=D then the declaration holds
clasohm@0
   396
   for all range classes more general than C *)   
clasohm@0
   397
   
clasohm@0
   398
fun close (coreg,subclass) =
clasohm@0
   399
  let fun check sl (l,(s,dom)) = case assoc (subclass,s) of
clasohm@0
   400
          Some(sups) =>
clasohm@0
   401
            let fun close_sup (l,sup) =
clasohm@0
   402
                  if exists (fn s'' => less subclass (s,s'') andalso
clasohm@0
   403
                                       leq subclass (s'',sup)) sl
clasohm@0
   404
                  then l
clasohm@0
   405
                  else (sup,dom)::l
clasohm@0
   406
            in foldl close_sup (l,sups) end
clasohm@0
   407
        | None => l;
clasohm@0
   408
      fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l));
clasohm@0
   409
  in map ext coreg end;
clasohm@0
   410
clasohm@0
   411
fun add_types(ac,(ts,n)) =
clasohm@0
   412
  let fun add_type((args,coreg),t) = case assoc(args,t) of
clasohm@0
   413
          Some _ => twice(t) | None => ((t,n)::args,(t,[])::coreg)
clasohm@0
   414
  in if n<0
clasohm@0
   415
     then error("Type constructor cannot have negative number of arguments")
clasohm@0
   416
     else foldl add_type (ac,ts)
clasohm@0
   417
  end;
clasohm@0
   418
clasohm@0
   419
(* 'extend' takes the above described check- and extend-functions to
clasohm@0
   420
   extend a given type signature with new classes and new type declarations *)
clasohm@0
   421
clasohm@0
   422
fun extend (TySg{classes,default,subclass,args,coreg},
clasohm@0
   423
            newclasses,newdefault,types,arities) =
clasohm@0
   424
let val (classes',subclass') = extend_classes(classes,subclass,newclasses);
clasohm@0
   425
    val (args',coreg') = foldl add_types ((args,coreg),types);
clasohm@0
   426
    val old_coreg = map #1 coreg;
clasohm@0
   427
    fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c);
clasohm@0
   428
    fun is_new(c) = if c mem old_coreg then twice(c) else ();
clasohm@0
   429
    val coreg'' = foldl (coregular (classes',subclass',args'))
clasohm@0
   430
                        (coreg',min_domain subclass' arities);
clasohm@0
   431
    val coreg''' = close (coreg'',subclass');
clasohm@0
   432
    val default' = if null newdefault then default else newdefault;
clasohm@0
   433
in TySg{classes=classes', default=default',subclass=subclass', args=args',
clasohm@0
   434
	coreg=coreg'''} end;
clasohm@0
   435
clasohm@0
   436
clasohm@0
   437
(* 'assoc_union' merges two association lists if the contents associated
clasohm@0
   438
   the keys are lists *)
clasohm@0
   439
clasohm@0
   440
fun assoc_union (as1,[]) = as1
clasohm@0
   441
  | assoc_union (as1,(key,l2)::as2) = case assoc (as1,key) of
clasohm@0
   442
        Some(l1) => assoc_union (overwrite(as1,(key,l1 union l2)),as2)
clasohm@0
   443
      | None => assoc_union ((key,l2)::as1,as2);
clasohm@0
   444
clasohm@0
   445
clasohm@0
   446
fun trcl r =
clasohm@0
   447
  let val r' = transitive_closure r
clasohm@0
   448
  in if exists (op mem) r' then error("Cyclic class structure!") else r' end;
clasohm@0
   449
clasohm@0
   450
clasohm@0
   451
(* 'merge_coreg' builds the union of two 'coreg' lists;
clasohm@0
   452
   it only checks the two restriction conditions and inserts afterwards
clasohm@0
   453
   all elements of the second list into the first one *) 
clasohm@0
   454
clasohm@0
   455
fun merge_coreg classes subclass1 =
clasohm@0
   456
  let fun test_ar classes (t,ars1) (coreg1,(s,w)) =
clasohm@0
   457
        (is_unique_decl coreg1 (t,(s,w));
clasohm@0
   458
	 restr2 classes (subclass1,coreg1) (t,(s,w));
clasohm@0
   459
	 overwrite (coreg1,(t,(s,w) ins ars1)));
clasohm@0
   460
clasohm@0
   461
      fun merge_c (coreg1,(c as (t,ars2))) = case assoc (coreg1,t) of
clasohm@0
   462
          Some(ars1) => foldl (test_ar classes (t,ars1)) (coreg1,ars2)
clasohm@0
   463
        | None => c::coreg1
clasohm@0
   464
  in foldl merge_c end;
clasohm@0
   465
clasohm@0
   466
fun merge_args(args,(t,n)) = case assoc(args,t) of
clasohm@0
   467
      Some(m) => if m=n then args else varying_decls(t)
clasohm@0
   468
    | None => (t,n)::args;
clasohm@0
   469
clasohm@0
   470
(* 'merge' takes the above declared functions to merge two type signatures *)
clasohm@0
   471
clasohm@0
   472
fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1,
clasohm@0
   473
           coreg=coreg1},
clasohm@0
   474
	  TySg{classes=classes2,default=default2,subclass=subclass2,args=args2,
clasohm@0
   475
           coreg=coreg2}) =
clasohm@0
   476
  let val classes' = classes1 union classes2;
clasohm@0
   477
      val subclass' = trcl (assoc_union (subclass1,subclass2));
clasohm@0
   478
      val args' = foldl merge_args (args1,args2)
clasohm@0
   479
      val coreg' = merge_coreg classes' subclass' (coreg1,coreg2);
clasohm@0
   480
      val default' = min_sort subclass' (default1 @ default2)
clasohm@0
   481
  in TySg{classes=classes' , default=default',subclass=subclass', args=args',
clasohm@0
   482
	  coreg=coreg'} 
clasohm@0
   483
  end;
clasohm@0
   484
clasohm@0
   485
(**** TYPE INFERENCE ****)
clasohm@0
   486
clasohm@0
   487
(*
clasohm@0
   488
clasohm@0
   489
Input:
clasohm@0
   490
- a 'raw' term which contains only dummy types and some explicit type
clasohm@0
   491
  constraints encoded as terms.
clasohm@0
   492
- the expected type of the term.
clasohm@0
   493
clasohm@0
   494
Output:
clasohm@0
   495
- the correctly typed term
clasohm@0
   496
- the substitution needed to unify the actual type of the term with its
clasohm@0
   497
  expected type; only the TVars in the expected type are included.
clasohm@0
   498
clasohm@0
   499
During type inference all TVars in the term have negative index. This keeps
clasohm@0
   500
them apart from normal TVars, which is essential, because at the end the type
clasohm@0
   501
of the term is unified with the expected type, which contains normal TVars.
clasohm@0
   502
clasohm@0
   503
1. Add initial type information to the term (add_types).
clasohm@0
   504
   This freezes (freeze_vars) TVars in explicitly provided types (eg
clasohm@0
   505
   constraints or defaults) by turning them into TFrees.
clasohm@0
   506
2. Carry out type inference, possibly introducing new negative TVars.
clasohm@0
   507
3. Unify actual and expected type.
clasohm@0
   508
4. Turn all (negative) TVars into unique new TFrees (freeze).
clasohm@0
   509
5. Thaw all TVars frozen in step 1 (thaw_vars).
clasohm@0
   510
clasohm@0
   511
*)
clasohm@0
   512
clasohm@0
   513
(*Raised if types are not unifiable*)
clasohm@0
   514
exception TUNIFY;
clasohm@0
   515
clasohm@0
   516
val tyvar_count = ref(~1);
clasohm@0
   517
clasohm@0
   518
fun tyinit() = (tyvar_count := ~1);
clasohm@0
   519
clasohm@0
   520
fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
clasohm@0
   521
clasohm@0
   522
(*
clasohm@0
   523
Generate new TVar.  Index is < ~1 to distinguish it from TVars generated from
clasohm@0
   524
variable names (see id_type).  Name is arbitrary because index is new.
clasohm@0
   525
*)
clasohm@0
   526
clasohm@0
   527
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S);
clasohm@0
   528
fun new_id_type(a) = TVar(("'"^a, new_tvar_inx()),[]);
clasohm@0
   529
clasohm@0
   530
(*Occurs check: type variable occurs in type?*)
clasohm@0
   531
fun occ v tye =
clasohm@0
   532
  let fun occ(Type(_,Ts)) = exists occ Ts
clasohm@0
   533
        | occ(TFree _) = false
clasohm@0
   534
        | occ(TVar(w,_)) = v=w orelse
clasohm@0
   535
                           (case assoc(tye,w) of
clasohm@0
   536
                              None   => false
clasohm@0
   537
                            | Some U => occ U);
clasohm@0
   538
  in occ end;
clasohm@0
   539
clasohm@0
   540
(*Chase variable assignments in tye.  
clasohm@0
   541
  If devar (T,tye) returns a type var then it must be unassigned.*) 
clasohm@0
   542
fun devar (T as TVar(v,_), tye) = (case  assoc(tye,v)  of
clasohm@0
   543
          Some U =>  devar (U,tye)
clasohm@0
   544
        | None   =>  T)
clasohm@0
   545
  | devar (T,tye) = T;
clasohm@0
   546
clasohm@0
   547
clasohm@0
   548
(* 'dom' returns for a type constructor t the list of those domains
clasohm@0
   549
   which deliver a given range class C *)
clasohm@0
   550
clasohm@0
   551
fun dom coreg t C = case assoc2 (coreg, (t,C)) of
clasohm@0
   552
    Some(Ss) => Ss
clasohm@0
   553
  | None => raise TUNIFY;
clasohm@0
   554
clasohm@0
   555
clasohm@0
   556
(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
clasohm@0
   557
   (i.e. a set of range classes ); the union is carried out elementwise
clasohm@0
   558
   for the seperate sorts in the domains *)
clasohm@0
   559
clasohm@0
   560
fun Dom (subclass,coreg) (t,S) =
clasohm@0
   561
  let val domlist = map (dom coreg t) S;
clasohm@0
   562
  in if null domlist then []
clasohm@0
   563
     else foldl (elementwise_union subclass) (hd domlist,tl domlist)
clasohm@0
   564
  end;
clasohm@0
   565
clasohm@0
   566
clasohm@0
   567
fun W ((T,S),tsig as TySg{subclass,coreg,...},tye) =
clasohm@0
   568
  let fun Wd ((T,S),tye) = W ((devar (T,tye),S),tsig,tye)
clasohm@0
   569
      fun Wk(T as TVar(v,S')) = 
clasohm@0
   570
	      if sortorder subclass (S',S) then tye
clasohm@0
   571
	      else (v,gen_tyvar(union_sort subclass (S',S)))::tye
clasohm@0
   572
	| Wk(T as TFree(v,S')) = if sortorder subclass (S',S) then tye
clasohm@0
   573
				 else raise TUNIFY
clasohm@0
   574
	| Wk(T as Type(f,Ts)) = 
clasohm@0
   575
	   if null S then tye 
clasohm@0
   576
	   else foldr Wd (Ts~~(Dom (subclass,coreg) (f,S)) ,tye)
clasohm@0
   577
  in Wk(T) end;
clasohm@0
   578
clasohm@0
   579
clasohm@0
   580
(* Order-sorted Unification of Types (U)  *)
clasohm@0
   581
clasohm@0
   582
clasohm@0
   583
(* Precondition: both types are well-formed w.r.t. type constructor arities *)
clasohm@0
   584
fun unify (tsig as TySg{subclass,coreg,...}) = 
clasohm@0
   585
  let fun unif ((T,U),tye) =
clasohm@0
   586
        case (devar(T,tye), devar(U,tye)) of
clasohm@0
   587
	  (T as TVar(v,S1), U as TVar(w,S2)) =>
clasohm@0
   588
             if v=w then tye else
clasohm@0
   589
             if sortorder subclass (S1,S2) then (w,T)::tye else
clasohm@0
   590
             if sortorder subclass (S2,S1) then (v,U)::tye
clasohm@0
   591
             else let val nu = gen_tyvar (union_sort subclass (S1,S2))
clasohm@0
   592
                  in (v,nu)::(w,nu)::tye end
clasohm@0
   593
        | (T as TVar(v,S), U) =>
clasohm@0
   594
             if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
clasohm@0
   595
        | (U, T as TVar (v,S)) =>
clasohm@0
   596
             if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
clasohm@0
   597
        | (Type(a,Ts),Type(b,Us)) =>
clasohm@0
   598
	     if a<>b then raise TUNIFY else foldr unif (Ts~~Us,tye)
clasohm@0
   599
        | (T,U) => if T=U then tye else raise TUNIFY
clasohm@0
   600
  in unif end;
clasohm@0
   601
clasohm@0
   602
(*Instantiation of type variables in types*)
clasohm@0
   603
(*Pre: instantiations obey restrictions! *)
clasohm@0
   604
fun inst_typ tye =
clasohm@0
   605
  let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
clasohm@0
   606
        | inst(T as TFree _) = T
clasohm@0
   607
        | inst(T as TVar(v,_)) =
clasohm@0
   608
            (case assoc(tye,v) of Some U => inst U | None => T)
clasohm@0
   609
  in inst end;
clasohm@0
   610
clasohm@0
   611
(*Type inference for polymorphic term*)
clasohm@0
   612
fun infer tsig =
clasohm@0
   613
  let fun inf(Ts, Const (_,T), tye) = (T,tye)
clasohm@0
   614
        | inf(Ts, Free  (_,T), tye) = (T,tye)
clasohm@0
   615
        | inf(Ts, Bound i, tye) = ((nth_elem(i,Ts) , tye)
clasohm@0
   616
          handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
clasohm@0
   617
        | inf(Ts, Var (_,T), tye) = (T,tye)
clasohm@0
   618
        | inf(Ts, Abs (_,T,body), tye) = 
clasohm@0
   619
	    let val (U,tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
clasohm@0
   620
        | inf(Ts, f$u, tye) =
clasohm@0
   621
	    let val (U,tyeU) = inf(Ts, u, tye);
clasohm@0
   622
	        val (T,tyeT) = inf(Ts, f, tyeU);
clasohm@0
   623
                fun err s =
clasohm@0
   624
                  raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
clasohm@0
   625
	    in case T of
clasohm@0
   626
	         Type("fun",[T1,T2]) =>
clasohm@0
   627
		   ( (T2, unify tsig ((T1,U), tyeT))
clasohm@0
   628
                     handle TUNIFY => err"type mismatch in application" )
clasohm@0
   629
	       | TVar _ => 
clasohm@0
   630
                   let val T2 = gen_tyvar([])
clasohm@0
   631
                   in (T2, unify tsig ((T, U-->T2), tyeT))
clasohm@0
   632
                      handle TUNIFY => err"type mismatch in application"
clasohm@0
   633
                   end
clasohm@0
   634
               | _ => err"rator must have function type"
clasohm@0
   635
           end
clasohm@0
   636
  in inf end;
clasohm@0
   637
clasohm@0
   638
fun freeze_vars(Type(a,Ts)) = Type(a,map freeze_vars Ts)
clasohm@0
   639
  | freeze_vars(T as TFree _) = T
clasohm@0
   640
  | freeze_vars(TVar(v,S)) = TFree(Syntax.string_of_vname v, S);
clasohm@0
   641
clasohm@0
   642
(* Attach a type to a constant *)
clasohm@0
   643
fun type_const (a,T) = Const(a, incr_tvar (new_tvar_inx()) T);
clasohm@0
   644
clasohm@0
   645
(*Find type of ident.  If not in table then use ident's name for tyvar
clasohm@0
   646
  to get consistent typing.*)
clasohm@0
   647
fun type_of_ixn(types,ixn as (a,_)) =
clasohm@0
   648
      case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
clasohm@0
   649
clasohm@0
   650
fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term;
clasohm@0
   651
fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body);
clasohm@0
   652
clasohm@0
   653
(*
clasohm@0
   654
clasohm@0
   655
Attach types to a term.  Input is a "parse tree" containing dummy types.
clasohm@0
   656
Type constraints are translated and checked for validity wrt tsig.
clasohm@0
   657
TVars in constraints are frozen.
clasohm@0
   658
clasohm@0
   659
The atoms in the resulting term satisfy the following spec:
clasohm@0
   660
clasohm@0
   661
Const(a,T):
clasohm@0
   662
  T is a renamed copy of the generic type of a; renaming decreases index of
clasohm@0
   663
  all TVars by new_tvar_inx(), which is less than ~1. The index of all TVars
clasohm@0
   664
  in the generic type must be 0 for this to work!
clasohm@0
   665
clasohm@0
   666
Free(a,T), Var(ixn,T):
clasohm@0
   667
  T is either the frozen default type of a or TVar(("'"^a,~1),[])
clasohm@0
   668
clasohm@0
   669
Abs(a,T,_):
clasohm@0
   670
  T is either a type constraint or TVar(("'"^a,i),[]), where i is generated
clasohm@0
   671
  by new_tvar_inx(). Thus different abstractions can have the bound variables
clasohm@0
   672
  of the same name but different types.
clasohm@0
   673
clasohm@0
   674
*)
clasohm@0
   675
clasohm@0
   676
fun add_types (tsig, const_tab, types, sorts, string_of_typ) =
clasohm@0
   677
  let val S0 = defaultS tsig;
clasohm@0
   678
      fun defS0 ixn = case sorts ixn of Some S => S | None => S0;
clasohm@0
   679
      fun prepareT(typ) =
clasohm@0
   680
	let val T = Syntax.typ_of_term defS0 typ;
clasohm@0
   681
	    val T' = freeze_vars T
clasohm@0
   682
	in case type_errors (tsig,string_of_typ) (T,[]) of
clasohm@0
   683
	     [] => T'
clasohm@0
   684
	   | errs => raise TYPE(cat_lines errs,[T],[])
clasohm@0
   685
	end
clasohm@0
   686
      fun add (Const(a,_)) =
clasohm@0
   687
            (case Symtab.lookup(const_tab, a) of
clasohm@0
   688
               Some T => type_const(a,T)
clasohm@0
   689
             | None => raise TYPE ("No such constant: "^a, [], []))
clasohm@0
   690
        | add (Bound i) = Bound i
clasohm@0
   691
        | add (Free(a,_)) =
clasohm@0
   692
            (case Symtab.lookup(const_tab, a) of
clasohm@0
   693
               Some T => type_const(a,T)
clasohm@0
   694
             | None => Free(a, type_of_ixn(types,(a,~1))))
clasohm@0
   695
        | add (Var(ixn,_)) = Var(ixn, type_of_ixn(types,ixn))
clasohm@0
   696
        | add (Abs(a,_,body)) = Abs(a, new_id_type a, add body)
clasohm@0
   697
        | add ((f as Const(a,_)$t1)$t2) =
clasohm@0
   698
	    if a=Syntax.constrainC then constrain(add t1,prepareT t2) else
clasohm@0
   699
	    if a=Syntax.constrainAbsC then constrainAbs(add t1,prepareT t2)
clasohm@0
   700
	    else add f $ add t2
clasohm@0
   701
        | add (f$t) = add f $ add t
clasohm@0
   702
  in  add  end;
clasohm@0
   703
clasohm@0
   704
clasohm@0
   705
(* Post-Processing *)
clasohm@0
   706
clasohm@0
   707
clasohm@0
   708
(*Instantiation of type variables in terms*)
clasohm@0
   709
fun inst_types tye = map_term_types (inst_typ tye);
clasohm@0
   710
clasohm@0
   711
(*Delete explicit constraints -- occurrences of "_constrain" *)
clasohm@0
   712
fun unconstrain (Abs(a,T,t)) = Abs(a, T, unconstrain t)
clasohm@0
   713
  | unconstrain ((f as Const(a,_)) $ t) =
clasohm@0
   714
      if a=Syntax.constrainC then unconstrain t
clasohm@0
   715
      else unconstrain f $ unconstrain t
clasohm@0
   716
  | unconstrain (f$t) = unconstrain f $ unconstrain t
clasohm@0
   717
  | unconstrain (t) = t;
clasohm@0
   718
clasohm@0
   719
clasohm@0
   720
(* Turn all TVars which satisfy p into new TFrees *)
clasohm@0
   721
fun freeze p t =
clasohm@0
   722
  let val fs = add_term_tfree_names(t,[]);
clasohm@0
   723
      val inxs = filter p (add_term_tvar_ixns(t,[]));
clasohm@0
   724
      val vmap = inxs ~~ variantlist(map #1 inxs, fs);
clasohm@0
   725
      fun free(Type(a,Ts)) = Type(a, map free Ts)
clasohm@0
   726
        | free(T as TVar(v,S)) =
clasohm@0
   727
            (case assoc(vmap,v) of None => T | Some(a) => TFree(a,S))
clasohm@0
   728
        | free(T as TFree _) = T
clasohm@0
   729
  in map_term_types free t end;
clasohm@0
   730
clasohm@0
   731
(* Thaw all TVars that were frozen in freeze_vars *)
clasohm@0
   732
fun thaw_vars(Type(a,Ts)) = Type(a, map thaw_vars Ts)
clasohm@0
   733
  | thaw_vars(T as TFree(a,S)) = (case explode a of
clasohm@0
   734
	  "?"::"'"::vn => let val ((b,i),_) = Syntax.scan_varname vn
clasohm@0
   735
			  in TVar(("'"^b,i),S) end
clasohm@0
   736
	| _ => T)
clasohm@0
   737
  | thaw_vars(T) = T;
clasohm@0
   738
clasohm@0
   739
clasohm@0
   740
fun restrict tye =
clasohm@0
   741
  let fun clean(tye1, ((a,i),T)) =
clasohm@0
   742
	if i < 0 then tye1 else ((a,i),inst_typ tye T) :: tye1
clasohm@0
   743
  in foldl clean ([],tye) end
clasohm@0
   744
clasohm@0
   745
clasohm@0
   746
(*Infer types for term t using tables. Check that t's type and T unify *)
clasohm@0
   747
clasohm@0
   748
fun infer_term (tsig, const_tab, types, sorts, string_of_typ, T, t) =
clasohm@0
   749
  let val u = add_types (tsig, const_tab, types, sorts, string_of_typ) t;
clasohm@0
   750
      val (U,tye) = infer tsig ([], u, []);
clasohm@0
   751
      val uu = unconstrain u;
clasohm@0
   752
      val tye' = unify tsig ((T,U),tye) handle TUNIFY => raise TYPE
clasohm@0
   753
	("Term does not have expected type", [T, U], [inst_types tye uu])
clasohm@0
   754
      val Ttye = restrict tye' (* restriction to TVars in T *)
clasohm@0
   755
      val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
clasohm@0
   756
        (* all is a dummy term which contains all exported TVars *)
clasohm@0
   757
      val Const(_,Type(_,Ts)) $ u'' =
clasohm@0
   758
            map_term_types thaw_vars (freeze (fn (_,i) => i<0) all)
clasohm@0
   759
        (* turn all internally generated TVars into TFrees
clasohm@0
   760
           and thaw all initially frozen TVars *)
clasohm@0
   761
  in (u'', (map fst Ttye) ~~ Ts) end;
clasohm@0
   762
clasohm@0
   763
fun infer_types args = (tyinit(); infer_term args);
clasohm@0
   764
clasohm@0
   765
clasohm@0
   766
(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
clasohm@0
   767
fun varifyT(Type(a,Ts)) = Type(a,map varifyT Ts)
clasohm@0
   768
  | varifyT(TFree(a,S)) = TVar((a,0),S)
clasohm@0
   769
  | varifyT(T) = T;
clasohm@0
   770
clasohm@0
   771
(* Turn TFrees except those in fixed into new TVars *)
clasohm@0
   772
fun varify(t,fixed) =
clasohm@0
   773
  let val fs = add_term_tfree_names(t,[]) \\ fixed;
clasohm@0
   774
      val ixns = add_term_tvar_ixns(t,[]);
clasohm@0
   775
      val fmap = fs ~~ variantlist(fs, map #1 ixns)
clasohm@0
   776
      fun thaw(Type(a,Ts)) = Type(a, map thaw Ts)
clasohm@0
   777
        | thaw(T as TVar _) = T
clasohm@0
   778
        | thaw(T as TFree(a,S)) =
clasohm@0
   779
            (case assoc(fmap,a) of None => T | Some b => TVar((b,0),S))
clasohm@0
   780
  in map_term_types thaw t end;
clasohm@0
   781
clasohm@0
   782
clasohm@0
   783
end;