src/Pure/term.ML
author wenzelm
Sat May 29 15:05:02 2004 +0200 (2004-05-29)
changeset 14829 cfa5fe01a7b7
parent 14786 24a7bc97a27a
child 14854 61bdf2ae4dc5
permissions -rw-r--r--
moved read_int etc. to library.ML; added type 'arity';
     1 (*  Title:      Pure/term.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Simply typed lambda-calculus: types, terms, and basic operations.
     7 *)
     8 
     9 infix 9  $;
    10 infixr 5 -->;
    11 infixr --->;
    12 infix aconv;
    13 
    14 signature BASIC_TERM =
    15 sig
    16   type indexname
    17   type class
    18   type sort
    19   type arity
    20   datatype typ =
    21     Type  of string * typ list |
    22     TFree of string * sort |
    23     TVar  of indexname * sort
    24   val --> : typ * typ -> typ
    25   val ---> : typ list * typ -> typ
    26   val is_TVar: typ -> bool
    27   val domain_type: typ -> typ
    28   val range_type: typ -> typ
    29   val binder_types: typ -> typ list
    30   val body_type: typ -> typ
    31   val strip_type: typ -> typ list * typ
    32   datatype term =
    33     Const of string * typ |
    34     Free of string * typ |
    35     Var of indexname * typ |
    36     Bound of int |
    37     Abs of string * typ * term |
    38     $ of term * term
    39   structure Vartab : TABLE
    40   structure Typtab : TABLE
    41   structure Termtab : TABLE
    42   exception TYPE of string * typ list * term list
    43   exception TERM of string * term list
    44   val is_Bound: term -> bool
    45   val is_Const: term -> bool
    46   val is_Free: term -> bool
    47   val is_Var: term -> bool
    48   val dest_Type: typ -> string * typ list
    49   val dest_Const: term -> string * typ
    50   val dest_Free: term -> string * typ
    51   val dest_Var: term -> indexname * typ
    52   val type_of: term -> typ
    53   val type_of1: typ list * term -> typ
    54   val fastype_of: term -> typ
    55   val fastype_of1: typ list * term -> typ
    56   val list_abs: (string * typ) list * term -> term
    57   val strip_abs_body: term -> term
    58   val strip_abs_vars: term -> (string * typ) list
    59   val strip_qnt_body: string -> term -> term
    60   val strip_qnt_vars: string -> term -> (string * typ) list
    61   val list_comb: term * term list -> term
    62   val strip_comb: term -> term * term list
    63   val head_of: term -> term
    64   val size_of_term: term -> int
    65   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    66   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    67   val map_term_types: (typ -> typ) -> term -> term
    68   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    69   val map_typ: (class -> class) -> (string -> string) -> typ -> typ
    70   val map_term:
    71      (class -> class) ->
    72      (string -> string) -> (string -> string) -> term -> term
    73   val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    74   val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    75   val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    76   val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
    77   val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
    78   val dummyT: typ
    79   val logicC: class
    80   val logicS: sort
    81   val itselfT: typ -> typ
    82   val a_itselfT: typ
    83   val propT: typ
    84   val implies: term
    85   val all: typ -> term
    86   val equals: typ -> term
    87   val strip_all_body: term -> term
    88   val strip_all_vars: term -> (string * typ) list
    89   val incr_bv: int * int * term -> term
    90   val incr_boundvars: int -> term -> term
    91   val add_loose_bnos: term * int * int list -> int list
    92   val loose_bnos: term -> int list
    93   val loose_bvar: term * int -> bool
    94   val loose_bvar1: term * int -> bool
    95   val subst_bounds: term list * term -> term
    96   val subst_bound: term * term -> term
    97   val subst_TVars: (indexname * typ) list -> term -> term
    98   val subst_TVars_Vartab: typ Vartab.table -> term -> term
    99   val betapply: term * term -> term
   100   val eq_ix: indexname * indexname -> bool
   101   val ins_ix: indexname * indexname list -> indexname list
   102   val mem_ix: indexname * indexname list -> bool
   103   val aconv: term * term -> bool
   104   val aconvs: term list * term list -> bool
   105   val mem_term: term * term list -> bool
   106   val subset_term: term list * term list -> bool
   107   val eq_set_term: term list * term list -> bool
   108   val ins_term: term * term list -> term list
   109   val union_term: term list * term list -> term list
   110   val inter_term: term list * term list -> term list
   111   val could_unify: term * term -> bool
   112   val subst_free: (term * term) list -> term -> term
   113   val subst_atomic: (term * term) list -> term -> term
   114   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   115   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   116   val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
   117   val subst_Vars: (indexname * term) list -> term -> term
   118   val incr_tvar: int -> typ -> typ
   119   val xless: (string * int) * indexname -> bool
   120   val atless: term * term -> bool
   121   val insert_aterm: term * term list -> term list
   122   val abstract_over: term * term -> term
   123   val lambda: term -> term -> term
   124   val absfree: string * typ * term -> term
   125   val list_abs_free: (string * typ) list * term -> term
   126   val list_all_free: (string * typ) list * term -> term
   127   val list_all: (string * typ) list * term -> term
   128   val maxidx_of_typ: typ -> int
   129   val maxidx_of_typs: typ list -> int
   130   val maxidx_of_term: term -> int
   131   val maxidx_of_terms: term list -> int
   132   val variant: string list -> string -> string
   133   val variantlist: string list * string list -> string list
   134   val variant_abs: string * typ * term -> string * term
   135   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   136   val add_new_id: string list * string -> string list
   137   val add_typ_classes: typ * class list -> class list
   138   val add_typ_ixns: indexname list * typ -> indexname list
   139   val add_typ_tfree_names: typ * string list -> string list
   140   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   141   val typ_tfrees: typ -> (string * sort) list
   142   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   143   val typ_tvars: typ -> (indexname * sort) list
   144   val add_typ_tycons: typ * string list -> string list
   145   val add_typ_varnames: typ * string list -> string list
   146   val add_term_classes: term * class list -> class list
   147   val add_term_consts: term * string list -> string list
   148   val term_consts: term -> string list
   149   val add_term_frees: term * term list -> term list
   150   val term_frees: term -> term list
   151   val add_term_free_names: term * string list -> string list
   152   val add_term_names: term * string list -> string list
   153   val add_term_tfree_names: term * string list -> string list
   154   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   155   val term_tfrees: term -> (string * sort) list
   156   val add_term_tvar_ixns: term * indexname list -> indexname list
   157   val add_term_tvarnames: term * string list -> string list
   158   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   159   val term_tvars: term -> (indexname * sort) list
   160   val add_term_tycons: term * string list -> string list
   161   val add_term_vars: term * term list -> term list
   162   val term_vars: term -> term list
   163   val exists_Const: (string * typ -> bool) -> term -> bool
   164   val exists_subterm: (term -> bool) -> term -> bool
   165   val compress_type: typ -> typ
   166   val compress_term: term -> term
   167 end;
   168 
   169 signature TERM =
   170 sig
   171   include BASIC_TERM
   172   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   173   val rename_abs: term -> term -> term -> term option
   174   val invent_names: string list -> string -> int -> string list
   175   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   176   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   177   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   178   val add_frees: (string * typ) list * term -> (string * typ) list
   179   val indexname_ord: indexname * indexname -> order
   180   val typ_ord: typ * typ -> order
   181   val typs_ord: typ list * typ list -> order
   182   val term_ord: term * term -> order
   183   val terms_ord: term list * term list -> order
   184   val hd_ord: term * term -> order
   185   val termless: term * term -> bool
   186   val no_dummyT: typ -> typ
   187   val dummy_patternN: string
   188   val no_dummy_patterns: term -> term
   189   val replace_dummy_patterns: int * term -> int * term
   190   val is_replaced_dummy_pattern: indexname -> bool
   191   val adhoc_freeze_vars: term -> term * string list
   192   val string_of_vname: indexname -> string
   193   val string_of_vname': indexname -> string
   194 end;
   195 
   196 structure Term: TERM =
   197 struct
   198 
   199 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   200   for resolution.*)
   201 type indexname = string*int;
   202 
   203 (* Types are classified by sorts. *)
   204 type class = string;
   205 type sort  = class list;
   206 type arity = string * sort list * sort;
   207 
   208 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   209 datatype typ = Type  of string * typ list
   210              | TFree of string * sort
   211              | TVar  of indexname * sort;
   212 
   213 (*Terms.  Bound variables are indicated by depth number.
   214   Free variables, (scheme) variables and constants have names.
   215   An term is "closed" if every bound variable of level "lev"
   216   is enclosed by at least "lev" abstractions.
   217 
   218   It is possible to create meaningless terms containing loose bound vars
   219   or type mismatches.  But such terms are not allowed in rules. *)
   220 
   221 
   222 
   223 datatype term =
   224     Const of string * typ
   225   | Free  of string * typ
   226   | Var   of indexname * typ
   227   | Bound of int
   228   | Abs   of string*typ*term
   229   | op $  of term*term;
   230 
   231 
   232 (*For errors involving type mismatches*)
   233 exception TYPE of string * typ list * term list;
   234 
   235 (*For system errors involving terms*)
   236 exception TERM of string * term list;
   237 
   238 
   239 (*Note variable naming conventions!
   240     a,b,c: string
   241     f,g,h: functions (including terms of function type)
   242     i,j,m,n: int
   243     t,u: term
   244     v,w: indexnames
   245     x,y: any
   246     A,B,C: term (denoting formulae)
   247     T,U: typ
   248 *)
   249 
   250 
   251 (** Types **)
   252 
   253 fun S --> T = Type("fun",[S,T]);
   254 
   255 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   256 val op ---> = foldr (op -->);
   257 
   258 fun dest_Type (Type x) = x
   259   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   260 
   261 
   262 (** Discriminators **)
   263 
   264 fun is_Bound (Bound _) = true
   265   | is_Bound _         = false;
   266 
   267 fun is_Const (Const _) = true
   268   | is_Const _ = false;
   269 
   270 fun is_Free (Free _) = true
   271   | is_Free _ = false;
   272 
   273 fun is_Var (Var _) = true
   274   | is_Var _ = false;
   275 
   276 fun is_TVar (TVar _) = true
   277   | is_TVar _ = false;
   278 
   279 (** Destructors **)
   280 
   281 fun dest_Const (Const x) =  x
   282   | dest_Const t = raise TERM("dest_Const", [t]);
   283 
   284 fun dest_Free (Free x) =  x
   285   | dest_Free t = raise TERM("dest_Free", [t]);
   286 
   287 fun dest_Var (Var x) =  x
   288   | dest_Var t = raise TERM("dest_Var", [t]);
   289 
   290 
   291 fun domain_type (Type("fun", [T,_])) = T
   292 and range_type  (Type("fun", [_,T])) = T;
   293 
   294 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   295 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   296   | binder_types _   =  [];
   297 
   298 (* maps  [T1,...,Tn]--->T  to T*)
   299 fun body_type (Type("fun",[S,T])) = body_type T
   300   | body_type T   =  T;
   301 
   302 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   303 fun strip_type T : typ list * typ =
   304   (binder_types T, body_type T);
   305 
   306 
   307 (*Compute the type of the term, checking that combinations are well-typed
   308   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   309 fun type_of1 (Ts, Const (_,T)) = T
   310   | type_of1 (Ts, Free  (_,T)) = T
   311   | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)
   312         handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   313   | type_of1 (Ts, Var (_,T)) = T
   314   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   315   | type_of1 (Ts, f$u) =
   316       let val U = type_of1(Ts,u)
   317           and T = type_of1(Ts,f)
   318       in case T of
   319             Type("fun",[T1,T2]) =>
   320               if T1=U then T2  else raise TYPE
   321                     ("type_of: type mismatch in application", [T1,U], [f$u])
   322           | _ => raise TYPE
   323                     ("type_of: function type is expected in application",
   324                      [T,U], [f$u])
   325       end;
   326 
   327 fun type_of t : typ = type_of1 ([],t);
   328 
   329 (*Determines the type of a term, with minimal checking*)
   330 fun fastype_of1 (Ts, f$u) =
   331     (case fastype_of1 (Ts,f) of
   332         Type("fun",[_,T]) => T
   333         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   334   | fastype_of1 (_, Const (_,T)) = T
   335   | fastype_of1 (_, Free (_,T)) = T
   336   | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
   337          handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   338   | fastype_of1 (_, Var (_,T)) = T
   339   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   340 
   341 fun fastype_of t : typ = fastype_of1 ([],t);
   342 
   343 
   344 val list_abs = foldr (fn ((x, T), t) => Abs (x, T, t));
   345 
   346 (* maps  (x1,...,xn)t   to   t  *)
   347 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   348   | strip_abs_body u  =  u;
   349 
   350 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   351 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   352   | strip_abs_vars u  =  [] : (string*typ) list;
   353 
   354 
   355 fun strip_qnt_body qnt =
   356 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   357       | strip t = t
   358 in strip end;
   359 
   360 fun strip_qnt_vars qnt =
   361 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   362       | strip t  =  [] : (string*typ) list
   363 in strip end;
   364 
   365 
   366 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   367 val list_comb : term * term list -> term = foldl (op $);
   368 
   369 
   370 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   371 fun strip_comb u : term * term list =
   372     let fun stripc (f$t, ts) = stripc (f, t::ts)
   373         |   stripc  x =  x
   374     in  stripc(u,[])  end;
   375 
   376 
   377 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   378 fun head_of (f$t) = head_of f
   379   | head_of u = u;
   380 
   381 
   382 (*Number of atoms and abstractions in a term*)
   383 fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
   384   | size_of_term (f$t) = size_of_term f  +  size_of_term t
   385   | size_of_term _ = 1;
   386 
   387 fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
   388   | map_type_tvar f (T as TFree _) = T
   389   | map_type_tvar f (TVar x) = f x;
   390 
   391 fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
   392   | map_type_tfree f (TFree x) = f x
   393   | map_type_tfree f (T as TVar _) = T;
   394 
   395 (* apply a function to all types in a term *)
   396 fun map_term_types f =
   397 let fun map(Const(a,T)) = Const(a, f T)
   398       | map(Free(a,T)) = Free(a, f T)
   399       | map(Var(v,T)) = Var(v, f T)
   400       | map(t as Bound _)  = t
   401       | map(Abs(a,T,t)) = Abs(a, f T, map t)
   402       | map(f$t) = map f $ map t;
   403 in map end;
   404 
   405 (* iterate a function over all types in a term *)
   406 fun it_term_types f =
   407 let fun iter(Const(_,T), a) = f(T,a)
   408       | iter(Free(_,T), a) = f(T,a)
   409       | iter(Var(_,T), a) = f(T,a)
   410       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   411       | iter(f$u, a) = iter(f, iter(u, a))
   412       | iter(Bound _, a) = a
   413 in iter end
   414 
   415 
   416 (** Connectives of higher order logic **)
   417 
   418 val logicC: class = "logic";
   419 val logicS: sort = [logicC];
   420 
   421 fun itselfT ty = Type ("itself", [ty]);
   422 val a_itselfT = itselfT (TFree ("'a", logicS));
   423 
   424 val propT : typ = Type("prop",[]);
   425 
   426 val implies = Const("==>", propT-->propT-->propT);
   427 
   428 fun all T = Const("all", (T-->propT)-->propT);
   429 
   430 fun equals T = Const("==", T-->T-->propT);
   431 
   432 (* maps  !!x1...xn. t   to   t  *)
   433 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   434   | strip_all_body t  =  t;
   435 
   436 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   437 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   438                 (a,T) :: strip_all_vars t
   439   | strip_all_vars t  =  [] : (string*typ) list;
   440 
   441 (*increments a term's non-local bound variables
   442   required when moving a term within abstractions
   443      inc is  increment for bound variables
   444      lev is  level at which a bound variable is considered 'loose'*)
   445 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   446   | incr_bv (inc, lev, Abs(a,T,body)) =
   447         Abs(a, T, incr_bv(inc,lev+1,body))
   448   | incr_bv (inc, lev, f$t) =
   449       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   450   | incr_bv (inc, lev, u) = u;
   451 
   452 fun incr_boundvars  0  t = t
   453   | incr_boundvars inc t = incr_bv(inc,0,t);
   454 
   455 (*Scan a pair of terms; while they are similar,
   456   accumulate corresponding bound vars in "al"*)
   457 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   458       match_bvs(s, t, if x="" orelse y="" then al
   459                                           else (x,y)::al)
   460   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   461   | match_bvs(_,_,al) = al;
   462 
   463 (* strip abstractions created by parameters *)
   464 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   465 
   466 fun rename_abs pat obj t =
   467   let
   468     val ren = match_bvs (pat, obj, []);
   469     fun ren_abs (Abs (x, T, b)) =
   470           Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b)
   471       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   472       | ren_abs t = t
   473   in if null ren then None else Some (ren_abs t) end;
   474 
   475 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   476    (Bound 0) is loose at level 0 *)
   477 fun add_loose_bnos (Bound i, lev, js) =
   478         if i<lev then js  else  (i-lev) ins_int js
   479   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   480   | add_loose_bnos (f$t, lev, js) =
   481         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   482   | add_loose_bnos (_, _, js) = js;
   483 
   484 fun loose_bnos t = add_loose_bnos (t, 0, []);
   485 
   486 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   487    level k or beyond. *)
   488 fun loose_bvar(Bound i,k) = i >= k
   489   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   490   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   491   | loose_bvar _ = false;
   492 
   493 fun loose_bvar1(Bound i,k) = i = k
   494   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   495   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   496   | loose_bvar1 _ = false;
   497 
   498 (*Substitute arguments for loose bound variables.
   499   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   500   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   501         and the appropriate call is  subst_bounds([b,a], c) .
   502   Loose bound variables >=n are reduced by "n" to
   503      compensate for the disappearance of lambdas.
   504 *)
   505 fun subst_bounds (args: term list, t) : term =
   506   let val n = length args;
   507       fun subst (t as Bound i, lev) =
   508            (if i<lev then  t    (*var is locally bound*)
   509             else  incr_boundvars lev (List.nth(args, i-lev))
   510                     handle Subscript => Bound(i-n)  (*loose: change it*))
   511         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   512         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   513         | subst (t,lev) = t
   514   in   case args of [] => t  | _ => subst (t,0)  end;
   515 
   516 (*Special case: one argument*)
   517 fun subst_bound (arg, t) : term =
   518   let fun subst (t as Bound i, lev) =
   519             if i<lev then  t    (*var is locally bound*)
   520             else  if i=lev then incr_boundvars lev arg
   521                            else Bound(i-1)  (*loose: change it*)
   522         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   523         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   524         | subst (t,lev) = t
   525   in  subst (t,0)  end;
   526 
   527 (*beta-reduce if possible, else form application*)
   528 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   529   | betapply (f,u) = f$u;
   530 
   531 
   532 (** Equality, membership and insertion of indexnames (string*ints) **)
   533 
   534 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
   535 fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
   536 
   537 (*membership in a list, optimized version for indexnames*)
   538 fun mem_ix (_, []) = false
   539   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
   540 
   541 (*insertion into list, optimized version for indexnames*)
   542 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   543 
   544 (*Tests whether 2 terms are alpha-convertible and have same type.
   545   Note that constants may have more than one type.*)
   546 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   547   | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
   548   | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
   549   | (Bound i)    aconv (Bound j)    = i=j
   550   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   551   | (f$t)        aconv (g$u)        = (f aconv g) andalso (t aconv u)
   552   | _ aconv _  =  false;
   553 
   554 (** Membership, insertion, union for terms **)
   555 
   556 fun mem_term (_, []) = false
   557   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   558 
   559 fun subset_term ([], ys) = true
   560   | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
   561 
   562 fun eq_set_term (xs, ys) =
   563     xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
   564 
   565 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   566 
   567 fun union_term (xs, []) = xs
   568   | union_term ([], ys) = ys
   569   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   570 
   571 fun inter_term ([], ys) = []
   572   | inter_term (x::xs, ys) =
   573       if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
   574 
   575 (*are two term lists alpha-convertible in corresponding elements?*)
   576 fun aconvs ([],[]) = true
   577   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   578   | aconvs _ = false;
   579 
   580 (*A fast unification filter: true unless the two terms cannot be unified.
   581   Terms must be NORMAL.  Treats all Vars as distinct. *)
   582 fun could_unify (t,u) =
   583   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   584         | matchrands _ = true
   585   in case (head_of t , head_of u) of
   586         (_, Var _) => true
   587       | (Var _, _) => true
   588       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   589       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   590       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   591       | (Abs _, _) =>  true   (*because of possible eta equality*)
   592       | (_, Abs _) =>  true
   593       | _ => false
   594   end;
   595 
   596 (*Substitute new for free occurrences of old in a term*)
   597 fun subst_free [] = (fn t=>t)
   598   | subst_free pairs =
   599       let fun substf u =
   600             case gen_assoc (op aconv) (pairs, u) of
   601                 Some u' => u'
   602               | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   603                                  | t$u' => substf t $ substf u'
   604                                  | _ => u)
   605       in  substf  end;
   606 
   607 (*a total, irreflexive ordering on index names*)
   608 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   609 
   610 
   611 (*Abstraction of the term "body" over its occurrences of v,
   612     which must contain no loose bound variables.
   613   The resulting term is ready to become the body of an Abs.*)
   614 fun abstract_over (v,body) =
   615   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   616       (case u of
   617           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   618         | f$rand => abst(lev,f) $ abst(lev,rand)
   619         | _ => u)
   620   in  abst(0,body)  end;
   621 
   622 fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   623   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   624   | lambda v t = raise TERM ("lambda", [v, t]);
   625 
   626 (*Form an abstraction over a free variable.*)
   627 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   628 
   629 (*Abstraction over a list of free variables*)
   630 fun list_abs_free ([ ] ,     t) = t
   631   | list_abs_free ((a,T)::vars, t) =
   632       absfree(a, T, list_abs_free(vars,t));
   633 
   634 (*Quantification over a list of free variables*)
   635 fun list_all_free ([], t: term) = t
   636   | list_all_free ((a,T)::vars, t) =
   637         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   638 
   639 (*Quantification over a list of variables (already bound in body) *)
   640 fun list_all ([], t) = t
   641   | list_all ((a,T)::vars, t) =
   642         (all T) $ (Abs(a, T, list_all(vars,t)));
   643 
   644 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)].
   645   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   646 fun subst_atomic [] t = t : term
   647   | subst_atomic (instl: (term*term) list) t =
   648       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   649             | subst (f$t') = subst f $ subst t'
   650             | subst t = if_none (assoc(instl,t)) t
   651       in  subst t  end;
   652 
   653 (*Substitute for type Vars in a type*)
   654 fun typ_subst_TVars iTs T = if null iTs then T else
   655   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   656         | subst(T as TFree _) = T
   657         | subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T
   658   in subst T end;
   659 
   660 (*Substitute for type Vars in a term*)
   661 val subst_TVars = map_term_types o typ_subst_TVars;
   662 
   663 (*Substitute for Vars in a term; see also envir/norm_term*)
   664 fun subst_Vars itms t = if null itms then t else
   665   let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v
   666         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   667         | subst(f$t) = subst f $ subst t
   668         | subst(t) = t
   669   in subst t end;
   670 
   671 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
   672 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   673   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   674         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   675         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   676             None   => Var(ixn,typ_subst_TVars iTs T)
   677           | Some t => t)
   678         | subst(b as Bound _) = b
   679         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   680         | subst(f$t) = subst f $ subst t
   681   in subst end;
   682 
   683 
   684 (*Computing the maximum index of a typ*)
   685 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   686   | maxidx_of_typ(TFree _) = ~1
   687   | maxidx_of_typ(TVar((_,i),_)) = i
   688 and maxidx_of_typs [] = ~1
   689   | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   690 
   691 
   692 (*Computing the maximum index of a term*)
   693 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   694   | maxidx_of_term (Bound _) = ~1
   695   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   696   | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   697   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   698   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   699 
   700 fun maxidx_of_terms ts = foldl Int.max (~1, map maxidx_of_term ts);
   701 
   702 
   703 (* Increment the index of all Poly's in T by k *)
   704 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
   705 
   706 
   707 (**** Syntax-related declarations ****)
   708 
   709 
   710 (*Dummy type for parsing and printing.  Will be replaced during type inference. *)
   711 val dummyT = Type("dummy",[]);
   712 
   713 fun no_dummyT typ =
   714   let
   715     fun check (T as Type ("dummy", _)) =
   716           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   717       | check (Type (_, Ts)) = seq check Ts
   718       | check _ = ();
   719   in check typ; typ end;
   720 
   721 
   722 (*** Printing ***)
   723 
   724 (*Makes a variant of a name distinct from the names in bs.
   725   First attaches the suffix and then increments this;
   726   preserves a suffix of underscores "_". *)
   727 fun variant bs name =
   728   let
   729     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
   730     fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
   731     fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
   732   in vary1 (if c = "" then "u" else c) ^ u end;
   733 
   734 (*Create variants of the list of names, with priority to the first ones*)
   735 fun variantlist ([], used) = []
   736   | variantlist(b::bs, used) =
   737       let val b' = variant used b
   738       in  b' :: variantlist (bs, b'::used)  end;
   739 
   740 (*Invent fresh names*)
   741 fun invent_names _ _ 0 = []
   742   | invent_names used a n =
   743       let val b = Symbol.bump_string a in
   744         if a mem_string used then invent_names used b n
   745         else a :: invent_names used b (n - 1)
   746       end;
   747 
   748 
   749 
   750 (** Consts etc. **)
   751 
   752 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs)
   753   | add_typ_classes (TFree (_, S), cs) = S union cs
   754   | add_typ_classes (TVar (_, S), cs) = S union cs;
   755 
   756 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (Ts, c ins cs)
   757   | add_typ_tycons (_, cs) = cs;
   758 
   759 val add_term_classes = it_term_types add_typ_classes;
   760 val add_term_tycons = it_term_types add_typ_tycons;
   761 
   762 fun add_term_consts (Const (c, _), cs) = c ins_string cs
   763   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   764   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   765   | add_term_consts (_, cs) = cs;
   766 
   767 fun term_consts t = add_term_consts(t,[]);
   768 
   769 fun exists_Const P t = let
   770         fun ex (Const c      ) = P c
   771         |   ex (t $ u        ) = ex t orelse ex u
   772         |   ex (Abs (_, _, t)) = ex t
   773         |   ex _               = false
   774     in ex t end;
   775 
   776 fun exists_subterm P =
   777   let fun ex t = P t orelse
   778                  (case t of
   779                     u $ v        => ex u orelse ex v
   780                   | Abs(_, _, u) => ex u
   781                   | _            => false)
   782   in ex end;
   783 
   784 (*map classes, tycons*)
   785 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   786   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   787   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
   788 
   789 (*map classes, tycons, consts*)
   790 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
   791   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
   792   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
   793   | map_term _ _ _ (t as Bound _) = t
   794   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   795   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   796 
   797 
   798 
   799 (** TFrees and TVars **)
   800 
   801 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   802 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   803 
   804 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   805 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   806   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   807   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   808   | add_term_free_names (_, bs) = bs;
   809 
   810 (*Accumulates the names in the term, suppressing duplicates.
   811   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   812 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   813   | add_term_names (Free(a,_), bs) = a ins_string bs
   814   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   815   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   816   | add_term_names (_, bs) = bs;
   817 
   818 (*Accumulates the TVars in a type, suppressing duplicates. *)
   819 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)
   820   | add_typ_tvars(TFree(_),vs) = vs
   821   | add_typ_tvars(TVar(v),vs) = v ins vs;
   822 
   823 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   824 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)
   825   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   826   | add_typ_tfree_names(TVar(_),fs) = fs;
   827 
   828 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)
   829   | add_typ_tfrees(TFree(f),fs) = f ins fs
   830   | add_typ_tfrees(TVar(_),fs) = fs;
   831 
   832 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms)
   833   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   834   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   835 
   836 (*Accumulates the TVars in a term, suppressing duplicates. *)
   837 val add_term_tvars = it_term_types add_typ_tvars;
   838 
   839 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   840 val add_term_tfrees = it_term_types add_typ_tfrees;
   841 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   842 
   843 val add_term_tvarnames = it_term_types add_typ_varnames;
   844 
   845 (*Non-list versions*)
   846 fun typ_tfrees T = add_typ_tfrees(T,[]);
   847 fun typ_tvars T = add_typ_tvars(T,[]);
   848 fun term_tfrees t = add_term_tfrees(t,[]);
   849 fun term_tvars t = add_term_tvars(t,[]);
   850 
   851 (*special code to enforce left-to-right collection of TVar-indexnames*)
   852 
   853 fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
   854   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
   855                                      else ixns@[ixn]
   856   | add_typ_ixns(ixns,TFree(_)) = ixns;
   857 
   858 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
   859   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
   860   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
   861   | add_term_tvar_ixns(Bound _,ixns) = ixns
   862   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
   863       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
   864   | add_term_tvar_ixns(f$t,ixns) =
   865       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   866 
   867 (** Frees and Vars **)
   868 
   869 (*a partial ordering (not reflexive) for atomic terms*)
   870 fun atless (Const (a,_), Const (b,_))  =  a<b
   871   | atless (Free (a,_), Free (b,_)) =  a<b
   872   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   873   | atless (Bound i, Bound j)  =   i<j
   874   | atless _  =  false;
   875 
   876 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   877 fun insert_aterm (t,us) =
   878   let fun inserta [] = [t]
   879         | inserta (us as u::us') =
   880               if atless(t,u) then t::us
   881               else if t=u then us (*duplicate*)
   882               else u :: inserta(us')
   883   in  inserta us  end;
   884 
   885 (*Accumulates the Vars in the term, suppressing duplicates*)
   886 fun add_term_vars (t, vars: term list) = case t of
   887     Var   _ => insert_aterm(t,vars)
   888   | Abs (_,_,body) => add_term_vars(body,vars)
   889   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   890   | _ => vars;
   891 
   892 fun term_vars t = add_term_vars(t,[]);
   893 
   894 (*Accumulates the Frees in the term, suppressing duplicates*)
   895 fun add_term_frees (t, frees: term list) = case t of
   896     Free   _ => insert_aterm(t,frees)
   897   | Abs (_,_,body) => add_term_frees(body,frees)
   898   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   899   | _ => frees;
   900 
   901 fun term_frees t = add_term_frees(t,[]);
   902 
   903 (*Given an abstraction over P, replaces the bound variable by a Free variable
   904   having a unique name. *)
   905 fun variant_abs (a,T,P) =
   906   let val b = variant (add_term_names(P,[])) a
   907   in  (b,  subst_bound (Free(b,T), P))  end;
   908 
   909 (* renames and reverses the strings in vars away from names *)
   910 fun rename_aTs names vars : (string*typ)list =
   911   let fun rename_aT (vars,(a,T)) =
   912                 (variant (map #1 vars @ names) a, T) :: vars
   913   in foldl rename_aT ([],vars) end;
   914 
   915 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   916 
   917 
   918 (* left-ro-right traversal *)
   919 
   920 (*foldl atoms of type*)
   921 fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts)
   922   | foldl_atyps f x_atom = f x_atom;
   923 
   924 (*foldl atoms of term*)
   925 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
   926   | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
   927   | foldl_aterms f x_atom = f x_atom;
   928 
   929 fun foldl_map_aterms f (x, t $ u) =
   930       let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
   931       in (x'', t' $ u') end
   932   | foldl_map_aterms f (x, Abs (a, T, t)) =
   933       let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
   934   | foldl_map_aterms f x_atom = f x_atom;
   935 
   936 (*foldl types of term*)
   937 fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
   938   | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
   939   | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
   940   | foldl_term_types f (x, Bound _) = x
   941   | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
   942   | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
   943 
   944 fun foldl_types f = foldl_term_types (fn _ => f);
   945 
   946 (*collect variables*)
   947 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
   948 val add_tvars = foldl_types add_tvarsT;
   949 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
   950 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   951 
   952 
   953 
   954 (** type and term orders **)
   955 
   956 fun indexname_ord ((x, i), (y, j)) =
   957   (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
   958 
   959 val sort_ord = list_ord String.compare;
   960 
   961 
   962 (* typ_ord *)
   963 
   964 fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
   965   | typ_ord (Type _, _) = GREATER
   966   | typ_ord (TFree _, Type _) = LESS
   967   | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
   968   | typ_ord (TFree _, TVar _) = GREATER
   969   | typ_ord (TVar _, Type _) = LESS
   970   | typ_ord (TVar _, TFree _) = LESS
   971   | typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y)
   972 and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
   973 
   974 
   975 (* term_ord *)
   976 
   977 (*a linear well-founded AC-compatible ordering for terms:
   978   s < t <=> 1. size(s) < size(t) or
   979             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   980             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   981                (s1..sn) < (t1..tn) (lexicographically)*)
   982 
   983 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   984   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   985   | dest_hd (Var v) = (v, 2)
   986   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   987   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   988 
   989 fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
   990       (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   991   | term_ord (t, u) =
   992       (case Int.compare (size_of_term t, size_of_term u) of
   993         EQUAL =>
   994           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   995             (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
   996           end
   997       | ord => ord)
   998 and hd_ord (f, g) =
   999   prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
  1000 and terms_ord (ts, us) = list_ord term_ord (ts, us);
  1001 
  1002 fun termless tu = (term_ord tu = LESS);
  1003 
  1004 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
  1005 structure Typtab = TableFun(type key = typ val ord = typ_ord);
  1006 structure Termtab = TableFun(type key = term val ord = term_ord);
  1007 
  1008 (*Substitute for type Vars in a type, version using Vartab*)
  1009 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
  1010   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
  1011         | subst(T as TFree _) = T
  1012         | subst(T as TVar(ixn, _)) =
  1013             (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U)
  1014   in subst T end;
  1015 
  1016 (*Substitute for type Vars in a term, version using Vartab*)
  1017 val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
  1018 
  1019 
  1020 (*** Compression of terms and types by sharing common subtrees.
  1021      Saves 50-75% on storage requirements.  As it is a bit slow,
  1022      it should be called only for axioms, stored theorems, etc.
  1023      Recorded term and type fragments are never disposed. ***)
  1024 
  1025 (** Sharing of types **)
  1026 
  1027 val memo_types = ref (Typtab.empty: typ Typtab.table);
  1028 
  1029 fun compress_type T =
  1030   (case Typtab.lookup (! memo_types, T) of
  1031     Some T' => T'
  1032   | None =>
  1033       let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
  1034       in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
  1035 
  1036 
  1037 (** Sharing of atomic terms **)
  1038 
  1039 val memo_terms = ref (Termtab.empty : term Termtab.table);
  1040 
  1041 fun share_term (t $ u) = share_term t $ share_term u
  1042   | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
  1043   | share_term t =
  1044       (case Termtab.lookup (! memo_terms, t) of
  1045         Some t' => t'
  1046       | None => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
  1047 
  1048 val compress_term = share_term o map_term_types compress_type;
  1049 
  1050 
  1051 (* dummy patterns *)
  1052 
  1053 val dummy_patternN = "dummy_pattern";
  1054 
  1055 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1056   | is_dummy_pattern _ = false;
  1057 
  1058 fun no_dummy_patterns tm =
  1059   if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
  1060   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1061 
  1062 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1063       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1064   | replace_dummy Ts (i, Abs (x, T, t)) =
  1065       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1066       in (i', Abs (x, T, t')) end
  1067   | replace_dummy Ts (i, t $ u) =
  1068       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1069       in (i'', t' $ u') end
  1070   | replace_dummy _ (i, a) = (i, a);
  1071 
  1072 val replace_dummy_patterns = replace_dummy [];
  1073 
  1074 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1075   | is_replaced_dummy_pattern _ = false;
  1076 
  1077 
  1078 (* adhoc freezing *)
  1079 
  1080 fun adhoc_freeze_vars tm =
  1081   let
  1082     fun mk_inst (var as Var ((a, i), T)) =
  1083       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1084       in ((var,  Free(x, T)), x) end;
  1085     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1086   in (subst_atomic insts tm, xs) end;
  1087 
  1088 
  1089 (* string_of_vname *)
  1090 
  1091 fun string_of_vname (x, i) =
  1092   let
  1093     val si = string_of_int i;
  1094     val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true;
  1095   in
  1096     if dot then "?" ^ x ^ "." ^ si
  1097     else if i = 0 then "?" ^ x
  1098     else "?" ^ x ^ si
  1099   end;
  1100 
  1101 fun string_of_vname' (x, ~1) = x
  1102   | string_of_vname' xi = string_of_vname xi;
  1103 
  1104 end;
  1105 
  1106 structure BasicTerm: BASIC_TERM = Term;
  1107 open BasicTerm;