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