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