src/Pure/term.ML
author nipkow
Sat Jun 25 16:07:55 2005 +0200 (2005-06-25)
changeset 16570 861b9fa2c98c
parent 16537 954495db0f07
child 16589 24c32abc8b84
permissions -rw-r--r--
Added term_lpo
     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: 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 (Abs (_,_,body)) = 1 + size_of_term body
   408   | size_of_term (f$t) = size_of_term f  +  size_of_term t
   409   | size_of_term _ = 1;
   410 
   411 fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
   412   | map_type_tvar f (T as TFree _) = T
   413   | map_type_tvar f (TVar x) = f x;
   414 
   415 fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
   416   | map_type_tfree f (TFree x) = f x
   417   | map_type_tfree f (T as TVar _) = T;
   418 
   419 (* apply a function to all types in a term *)
   420 fun map_term_types f =
   421 let fun map(Const(a,T)) = Const(a, f T)
   422       | map(Free(a,T)) = Free(a, f T)
   423       | map(Var(v,T)) = Var(v, f T)
   424       | map(t as Bound _)  = t
   425       | map(Abs(a,T,t)) = Abs(a, f T, map t)
   426       | map(f$t) = map f $ map t;
   427 in map end;
   428 
   429 (* iterate a function over all types in a term *)
   430 fun it_term_types f =
   431 let fun iter(Const(_,T), a) = f(T,a)
   432       | iter(Free(_,T), a) = f(T,a)
   433       | iter(Var(_,T), a) = f(T,a)
   434       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   435       | iter(f$u, a) = iter(f, iter(u, a))
   436       | iter(Bound _, a) = a
   437 in iter end
   438 
   439 
   440 (** Comparing terms, types etc. **)
   441 
   442 fun indexname_ord ((x, i), (y, j)) =
   443   (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   444 
   445 val sort_ord = list_ord string_ord;
   446 
   447 
   448 (* typ_ord *)
   449 
   450 fun typ_ord TU =
   451   if pointer_eq TU then EQUAL
   452   else
   453     (case TU of
   454       (Type x, Type y) => prod_ord string_ord typs_ord (x, y)
   455     | (Type _, _) => GREATER
   456     | (TFree _, Type _) => LESS
   457     | (TFree x, TFree y) => prod_ord string_ord sort_ord (x, y)
   458     | (TFree _, TVar _) => GREATER
   459     | (TVar _, Type _) => LESS
   460     | (TVar _, TFree _) => LESS
   461     | (TVar x, TVar y) => prod_ord indexname_ord sort_ord (x, y))
   462 and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
   463 
   464 
   465 (* term_ord *)
   466 
   467 (*a linear well-founded AC-compatible ordering for terms:
   468   s < t <=> 1. size(s) < size(t) or
   469             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   470             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   471                (s1..sn) < (t1..tn) (lexicographically)*)
   472 
   473 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   474   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   475   | dest_hd (Var v) = (v, 2)
   476   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   477   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   478 
   479 fun term_ord tu =
   480   if pointer_eq tu then EQUAL
   481   else
   482     (case tu of
   483       (Abs (_, T, t), Abs(_, U, u)) =>
   484         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   485       | (t, u) =>
   486         (case int_ord (size_of_term t, size_of_term u) of
   487           EQUAL =>
   488             let
   489               val (f, ts) = strip_comb t
   490               and (g, us) = strip_comb u
   491             in case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord end
   492         | ord => ord))
   493 and hd_ord (f, g) =
   494   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   495 and terms_ord (ts, us) = list_ord term_ord (ts, us);
   496 
   497 fun op aconv tu = (term_ord tu = EQUAL);
   498 fun aconvs ts_us = (list_ord term_ord ts_us = EQUAL);
   499 fun termless tu = (term_ord tu = LESS);
   500 
   501 (*** Lexicographic path order on terms.
   502 
   503   See Baader & Nipkow, Term rewriting, CUP 1998.
   504   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   505   constants.
   506 
   507   f_ord maps strings to integers and serves two purposes:
   508   - Predicate on constant symbols.  Those that are not recognised by f_ord
   509     must be mapped to ~1.
   510   - Order on the recognised symbols.  These must be mapped to distinct
   511     integers >= 0.
   512 
   513 ***)
   514 
   515 local
   516 fun dest_hd f_ord (Const (a, T)) = 
   517       let val ord = f_ord a in
   518         if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
   519       end
   520   | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
   521   | dest_hd _ (Var v) = ((1, v), 1)
   522   | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
   523   | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
   524 
   525 fun term_lpo f_ord (s, t) =
   526   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
   527     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
   528     then case hd_ord f_ord (f, g) of
   529 	GREATER =>
   530 	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   531 	  then GREATER else LESS
   532       | EQUAL =>
   533 	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   534 	  then list_ord (term_lpo f_ord) (ss, ts)
   535 	  else LESS
   536       | LESS => LESS
   537     else GREATER
   538   end
   539 and hd_ord f_ord (f, g) = case (f, g) of
   540     (Abs (_, T, t), Abs (_, U, u)) =>
   541       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   542   | (_, _) => prod_ord (prod_ord int_ord
   543                   (prod_ord indexname_ord typ_ord)) int_ord
   544                 (dest_hd f_ord f, dest_hd f_ord g)
   545 in
   546 val term_lpo = term_lpo
   547 end;
   548 
   549 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
   550 structure Typtab = TableFun(type key = typ val ord = typ_ord);
   551 structure Termtab = TableFun(type key = term val ord = term_ord);
   552 
   553 
   554 (** Connectives of higher order logic **)
   555 
   556 fun itselfT ty = Type ("itself", [ty]);
   557 val a_itselfT = itselfT (TFree ("'a", []));
   558 
   559 val propT : typ = Type("prop",[]);
   560 
   561 val implies = Const("==>", propT-->propT-->propT);
   562 
   563 fun all T = Const("all", (T-->propT)-->propT);
   564 
   565 fun equals T = Const("==", T-->T-->propT);
   566 
   567 (* maps  !!x1...xn. t   to   t  *)
   568 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   569   | strip_all_body t  =  t;
   570 
   571 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   572 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   573                 (a,T) :: strip_all_vars t
   574   | strip_all_vars t  =  [] : (string*typ) list;
   575 
   576 (*increments a term's non-local bound variables
   577   required when moving a term within abstractions
   578      inc is  increment for bound variables
   579      lev is  level at which a bound variable is considered 'loose'*)
   580 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   581   | incr_bv (inc, lev, Abs(a,T,body)) =
   582         Abs(a, T, incr_bv(inc,lev+1,body))
   583   | incr_bv (inc, lev, f$t) =
   584       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   585   | incr_bv (inc, lev, u) = u;
   586 
   587 fun incr_boundvars  0  t = t
   588   | incr_boundvars inc t = incr_bv(inc,0,t);
   589 
   590 (*Scan a pair of terms; while they are similar,
   591   accumulate corresponding bound vars in "al"*)
   592 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   593       match_bvs(s, t, if x="" orelse y="" then al
   594                                           else (x,y)::al)
   595   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   596   | match_bvs(_,_,al) = al;
   597 
   598 (* strip abstractions created by parameters *)
   599 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   600 
   601 fun rename_abs pat obj t =
   602   let
   603     val ren = match_bvs (pat, obj, []);
   604     fun ren_abs (Abs (x, T, b)) =
   605           Abs (getOpt (assoc_string (ren, x), x), T, ren_abs b)
   606       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   607       | ren_abs t = t
   608   in if null ren then NONE else SOME (ren_abs t) end;
   609 
   610 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   611    (Bound 0) is loose at level 0 *)
   612 fun add_loose_bnos (Bound i, lev, js) =
   613         if i<lev then js  else  (i-lev) ins_int js
   614   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   615   | add_loose_bnos (f$t, lev, js) =
   616         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   617   | add_loose_bnos (_, _, js) = js;
   618 
   619 fun loose_bnos t = add_loose_bnos (t, 0, []);
   620 
   621 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   622    level k or beyond. *)
   623 fun loose_bvar(Bound i,k) = i >= k
   624   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   625   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   626   | loose_bvar _ = false;
   627 
   628 fun loose_bvar1(Bound i,k) = i = k
   629   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   630   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   631   | loose_bvar1 _ = false;
   632 
   633 (*Substitute arguments for loose bound variables.
   634   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   635   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   636         and the appropriate call is  subst_bounds([b,a], c) .
   637   Loose bound variables >=n are reduced by "n" to
   638      compensate for the disappearance of lambdas.
   639 *)
   640 fun subst_bounds (args: term list, t) : term =
   641   let val n = length args;
   642       fun subst (t as Bound i, lev) =
   643            (if i<lev then  t    (*var is locally bound*)
   644             else  incr_boundvars lev (List.nth(args, i-lev))
   645                     handle Subscript => Bound(i-n)  (*loose: change it*))
   646         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   647         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   648         | subst (t,lev) = t
   649   in   case args of [] => t  | _ => subst (t,0)  end;
   650 
   651 (*Special case: one argument*)
   652 fun subst_bound (arg, t) : term =
   653   let fun subst (t as Bound i, lev) =
   654             if i<lev then  t    (*var is locally bound*)
   655             else  if i=lev then incr_boundvars lev arg
   656                            else Bound(i-1)  (*loose: change it*)
   657         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   658         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   659         | subst (t,lev) = t
   660   in  subst (t,0)  end;
   661 
   662 (*beta-reduce if possible, else form application*)
   663 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   664   | betapply (f,u) = f$u;
   665 
   666 
   667 (** Equality, membership and insertion of indexnames (string*ints) **)
   668 
   669 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
   670 fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
   671 
   672 (*membership in a list, optimized version for indexnames*)
   673 fun mem_ix (_, []) = false
   674   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
   675 
   676 (*insertion into list, optimized version for indexnames*)
   677 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   678 
   679 
   680 (** Membership, insertion, union for terms **)
   681 
   682 fun mem_term (_, []) = false
   683   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   684 
   685 fun subset_term ([], ys) = true
   686   | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
   687 
   688 fun eq_set_term (xs, ys) =
   689     xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
   690 
   691 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   692 
   693 fun union_term (xs, []) = xs
   694   | union_term ([], ys) = ys
   695   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   696 
   697 fun inter_term ([], ys) = []
   698   | inter_term (x::xs, ys) =
   699       if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
   700 
   701 (*A fast unification filter: true unless the two terms cannot be unified.
   702   Terms must be NORMAL.  Treats all Vars as distinct. *)
   703 fun could_unify (t,u) =
   704   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   705         | matchrands _ = true
   706   in case (head_of t , head_of u) of
   707         (_, Var _) => true
   708       | (Var _, _) => true
   709       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   710       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   711       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   712       | (Abs _, _) =>  true   (*because of possible eta equality*)
   713       | (_, Abs _) =>  true
   714       | _ => false
   715   end;
   716 
   717 (*Substitute new for free occurrences of old in a term*)
   718 fun subst_free [] = (fn t=>t)
   719   | subst_free pairs =
   720       let fun substf u =
   721             case gen_assoc (op aconv) (pairs, u) of
   722                 SOME u' => u'
   723               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   724                                  | t$u' => substf t $ substf u'
   725                                  | _ => u)
   726       in  substf  end;
   727 
   728 (*a total, irreflexive ordering on index names*)
   729 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   730 
   731 
   732 (*Abstraction of the term "body" over its occurrences of v,
   733     which must contain no loose bound variables.
   734   The resulting term is ready to become the body of an Abs.*)
   735 fun abstract_over (v,body) =
   736   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   737       (case u of
   738           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   739         | f$rand => abst(lev,f) $ abst(lev,rand)
   740         | _ => u)
   741   in  abst(0,body)  end;
   742 
   743 fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   744   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   745   | lambda v t = raise TERM ("lambda", [v, t]);
   746 
   747 (*Form an abstraction over a free variable.*)
   748 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   749 
   750 (*Abstraction over a list of free variables*)
   751 fun list_abs_free ([ ] ,     t) = t
   752   | list_abs_free ((a,T)::vars, t) =
   753       absfree(a, T, list_abs_free(vars,t));
   754 
   755 (*Quantification over a list of free variables*)
   756 fun list_all_free ([], t: term) = t
   757   | list_all_free ((a,T)::vars, t) =
   758         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   759 
   760 (*Quantification over a list of variables (already bound in body) *)
   761 fun list_all ([], t) = t
   762   | list_all ((a,T)::vars, t) =
   763         (all T) $ (Abs(a, T, list_all(vars,t)));
   764 
   765 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)].
   766   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   767 fun subst_atomic [] t = t : term
   768   | subst_atomic (instl: (term*term) list) t =
   769       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   770             | subst (f$t') = subst f $ subst t'
   771             | subst t = getOpt (assoc(instl,t),t)
   772       in  subst t  end;
   773 
   774 (*Replace the ATOMIC type Ti by Ui;    instl = [(T1,U1), ..., (Tn,Un)].*)
   775 fun typ_subst_atomic [] T = T
   776   | typ_subst_atomic instl (Type (s, Ts)) =
   777       Type (s, map (typ_subst_atomic instl) Ts)
   778   | typ_subst_atomic instl T = getOpt (assoc (instl, T), T);
   779 
   780 (*Substitute for type Vars in a type*)
   781 fun typ_subst_TVars iTs T = if null iTs then T else
   782   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   783         | subst(T as TFree _) = T
   784         | subst(T as TVar(ixn,_)) = getOpt (assoc(iTs,ixn),T)
   785   in subst T end;
   786 
   787 (*Substitute for type Vars in a term*)
   788 val subst_TVars = map_term_types o typ_subst_TVars;
   789 
   790 (*Substitute for Vars in a term; see also envir/norm_term*)
   791 fun subst_Vars itms t = if null itms then t else
   792   let fun subst(v as Var(ixn,_)) = getOpt (assoc(itms,ixn),v)
   793         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   794         | subst(f$t) = subst f $ subst t
   795         | subst(t) = t
   796   in subst t end;
   797 
   798 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
   799 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   800   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   801         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   802         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   803             NONE   => Var(ixn,typ_subst_TVars iTs T)
   804           | SOME t => t)
   805         | subst(b as Bound _) = b
   806         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   807         | subst(f$t) = subst f $ subst t
   808   in subst end;
   809 
   810 
   811 (** Identifying first-order terms **)
   812 
   813 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   814 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
   815 
   816 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   817   function type. The meta-quantifier "all" is excluded--its argument always
   818   has a function type--through a recursive call into its body.*)
   819 fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   820   | first_order1 Ts (Const("all",_)$Abs(a,T,body)) =
   821       not (is_funtype T) andalso first_order1 (T::Ts) body
   822   | first_order1 Ts t =
   823       case strip_comb t of
   824                (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   825              | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   826              | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   827              | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   828              | (Abs _, ts) => false (*not in beta-normal form*)
   829              | _ => error "first_order: unexpected case";
   830 
   831 val is_first_order = first_order1 [];
   832 
   833 (*Computing the maximum index of a typ*)
   834 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   835   | maxidx_of_typ(TFree _) = ~1
   836   | maxidx_of_typ(TVar((_,i),_)) = i
   837 and maxidx_of_typs [] = ~1
   838   | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   839 
   840 
   841 (*Computing the maximum index of a term*)
   842 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   843   | maxidx_of_term (Bound _) = ~1
   844   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   845   | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   846   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   847   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   848 
   849 fun maxidx_of_terms ts = Library.foldl Int.max (~1, map maxidx_of_term ts);
   850 
   851 
   852 (* Increment the index of all Poly's in T by k *)
   853 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
   854 
   855 
   856 (**** Syntax-related declarations ****)
   857 
   858 (*** Printing ***)
   859 
   860 (*Makes a variant of a name distinct from the names in bs.
   861   First attaches the suffix and then increments this;
   862   preserves a suffix of underscores "_". *)
   863 fun variant bs name =
   864   let
   865     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
   866     fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
   867     fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
   868   in vary1 (if c = "" then "u" else c) ^ u end;
   869 
   870 (*Create variants of the list of names, with priority to the first ones*)
   871 fun variantlist ([], used) = []
   872   | variantlist(b::bs, used) =
   873       let val b' = variant used b
   874       in  b' :: variantlist (bs, b'::used)  end;
   875 
   876 (*Invent fresh names*)
   877 fun invent_names _ _ 0 = []
   878   | invent_names used a n =
   879       let val b = Symbol.bump_string a in
   880         if a mem_string used then invent_names used b n
   881         else a :: invent_names used b (n - 1)
   882       end;
   883 
   884 
   885 (** Consts etc. **)
   886 
   887 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
   888   | add_typ_classes (TFree (_, S), cs) = S union cs
   889   | add_typ_classes (TVar (_, S), cs) = S union cs;
   890 
   891 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
   892   | add_typ_tycons (_, cs) = cs;
   893 
   894 val add_term_classes = it_term_types add_typ_classes;
   895 val add_term_tycons = it_term_types add_typ_tycons;
   896 
   897 fun add_term_consts (Const (c, _), cs) = c ins_string cs
   898   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   899   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   900   | add_term_consts (_, cs) = cs;
   901 
   902 fun add_term_constsT (Const c, cs) = c::cs
   903   | add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs))
   904   | add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs)
   905   | add_term_constsT (_, cs) = cs;
   906 
   907 fun term_consts t = add_term_consts(t,[]);
   908 
   909 fun term_constsT t = add_term_constsT(t,[]);
   910 
   911 fun exists_Const P t = let
   912         fun ex (Const c      ) = P c
   913         |   ex (t $ u        ) = ex t orelse ex u
   914         |   ex (Abs (_, _, t)) = ex t
   915         |   ex _               = false
   916     in ex t end;
   917 
   918 fun exists_subterm P =
   919   let fun ex t = P t orelse
   920                  (case t of
   921                     u $ v        => ex u orelse ex v
   922                   | Abs(_, _, u) => ex u
   923                   | _            => false)
   924   in ex end;
   925 
   926 (*map classes, tycons*)
   927 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   928   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   929   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
   930 
   931 (*map classes, tycons, consts*)
   932 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
   933   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
   934   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
   935   | map_term _ _ _ (t as Bound _) = t
   936   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   937   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   938 
   939 
   940 (** TFrees and TVars **)
   941 
   942 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   943 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   944 
   945 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   946 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   947   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   948   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   949   | add_term_free_names (_, bs) = bs;
   950 
   951 (*Accumulates the names in the term, suppressing duplicates.
   952   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   953 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   954   | add_term_names (Free(a,_), bs) = a ins_string bs
   955   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   956   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   957   | add_term_names (_, bs) = bs;
   958 
   959 (*Accumulates the TVars in a type, suppressing duplicates. *)
   960 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
   961   | add_typ_tvars(TFree(_),vs) = vs
   962   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
   963 
   964 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   965 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
   966   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   967   | add_typ_tfree_names(TVar(_),fs) = fs;
   968 
   969 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
   970   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   971   | add_typ_tfrees(TVar(_),fs) = fs;
   972 
   973 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
   974   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   975   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   976 
   977 (*Accumulates the TVars in a term, suppressing duplicates. *)
   978 val add_term_tvars = it_term_types add_typ_tvars;
   979 
   980 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   981 val add_term_tfrees = it_term_types add_typ_tfrees;
   982 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   983 
   984 val add_term_tvarnames = it_term_types add_typ_varnames;
   985 
   986 (*Non-list versions*)
   987 fun typ_tfrees T = add_typ_tfrees(T,[]);
   988 fun typ_tvars T = add_typ_tvars(T,[]);
   989 fun term_tfrees t = add_term_tfrees(t,[]);
   990 fun term_tvars t = add_term_tvars(t,[]);
   991 
   992 (*special code to enforce left-to-right collection of TVar-indexnames*)
   993 
   994 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
   995   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
   996                                      else ixns@[ixn]
   997   | add_typ_ixns(ixns,TFree(_)) = ixns;
   998 
   999 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1000   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1001   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1002   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1003   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1004       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1005   | add_term_tvar_ixns(f$t,ixns) =
  1006       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1007 
  1008 
  1009 (** Frees and Vars **)
  1010 
  1011 (*a partial ordering (not reflexive) for atomic terms*)
  1012 fun atless (Const (a,_), Const (b,_))  =  a<b
  1013   | atless (Free (a,_), Free (b,_)) =  a<b
  1014   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
  1015   | atless (Bound i, Bound j)  =   i<j
  1016   | atless _  =  false;
  1017 
  1018 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
  1019 fun insert_aterm (t,us) =
  1020   let fun inserta [] = [t]
  1021         | inserta (us as u::us') =
  1022               if atless(t,u) then t::us
  1023               else if t=u then us (*duplicate*)
  1024               else u :: inserta(us')
  1025   in  inserta us  end;
  1026 
  1027 (*Accumulates the Vars in the term, suppressing duplicates*)
  1028 fun add_term_vars (t, vars: term list) = case t of
  1029     Var   _ => insert_aterm(t,vars)
  1030   | Abs (_,_,body) => add_term_vars(body,vars)
  1031   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1032   | _ => vars;
  1033 
  1034 fun term_vars t = add_term_vars(t,[]);
  1035 
  1036 (*Accumulates the Frees in the term, suppressing duplicates*)
  1037 fun add_term_frees (t, frees: term list) = case t of
  1038     Free   _ => insert_aterm(t,frees)
  1039   | Abs (_,_,body) => add_term_frees(body,frees)
  1040   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1041   | _ => frees;
  1042 
  1043 fun term_frees t = add_term_frees(t,[]);
  1044 
  1045 (*Given an abstraction over P, replaces the bound variable by a Free variable
  1046   having a unique name. *)
  1047 fun variant_abs (a,T,P) =
  1048   let val b = variant (add_term_names(P,[])) a
  1049   in  (b,  subst_bound (Free(b,T), P))  end;
  1050 
  1051 (* renames and reverses the strings in vars away from names *)
  1052 fun rename_aTs names vars : (string*typ)list =
  1053   let fun rename_aT (vars,(a,T)) =
  1054                 (variant (map #1 vars @ names) a, T) :: vars
  1055   in Library.foldl rename_aT ([],vars) end;
  1056 
  1057 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
  1058 
  1059 
  1060 (* left-ro-right traversal *)
  1061 
  1062 (*foldl atoms of type*)
  1063 fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
  1064   | foldl_atyps f x_atom = f x_atom;
  1065 
  1066 (*foldl atoms of term*)
  1067 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
  1068   | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
  1069   | foldl_aterms f x_atom = f x_atom;
  1070 
  1071 fun foldl_map_aterms f (x, t $ u) =
  1072       let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
  1073       in (x'', t' $ u') end
  1074   | foldl_map_aterms f (x, Abs (a, T, t)) =
  1075       let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
  1076   | foldl_map_aterms f x_atom = f x_atom;
  1077 
  1078 (*foldl types of term*)
  1079 fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
  1080   | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
  1081   | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
  1082   | foldl_term_types f (x, Bound _) = x
  1083   | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
  1084   | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
  1085 
  1086 fun foldl_types f = foldl_term_types (fn _ => f);
  1087 
  1088 (*collect variables*)
  1089 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
  1090 val add_tvars = foldl_types add_tvarsT;
  1091 val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
  1092 val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
  1093 
  1094 (*collect variable names*)
  1095 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
  1096 fun term_varnames t = add_term_varnames ([], t);
  1097 
  1098 
  1099 
  1100 (*** Compression of terms and types by sharing common subtrees.
  1101      Saves 50-75% on storage requirements.  As it is a bit slow,
  1102      it should be called only for axioms, stored theorems, etc.
  1103      Recorded term and type fragments are never disposed. ***)
  1104 
  1105 
  1106 (** Sharing of types **)
  1107 
  1108 val memo_types = ref (Typtab.empty: typ Typtab.table);
  1109 
  1110 fun compress_type T =
  1111   (case Typtab.lookup (! memo_types, T) of
  1112     SOME T' => T'
  1113   | NONE =>
  1114       let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
  1115       in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
  1116 
  1117 
  1118 (** Sharing of atomic terms **)
  1119 
  1120 val memo_terms = ref (Termtab.empty : term Termtab.table);
  1121 
  1122 fun share_term (t $ u) = share_term t $ share_term u
  1123   | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
  1124   | share_term t =
  1125       (case Termtab.lookup (! memo_terms, t) of
  1126         SOME t' => t'
  1127       | NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
  1128 
  1129 val compress_term = share_term o map_term_types compress_type;
  1130 
  1131 
  1132 (* dummy patterns *)
  1133 
  1134 val dummy_patternN = "dummy_pattern";
  1135 
  1136 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1137   | is_dummy_pattern _ = false;
  1138 
  1139 fun no_dummy_patterns tm =
  1140   if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
  1141   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1142 
  1143 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1144       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1145   | replace_dummy Ts (i, Abs (x, T, t)) =
  1146       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1147       in (i', Abs (x, T, t')) end
  1148   | replace_dummy Ts (i, t $ u) =
  1149       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1150       in (i'', t' $ u') end
  1151   | replace_dummy _ (i, a) = (i, a);
  1152 
  1153 val replace_dummy_patterns = replace_dummy [];
  1154 
  1155 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1156   | is_replaced_dummy_pattern _ = false;
  1157 
  1158 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1159   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1160   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1161   | show_dummy_patterns a = a;
  1162 
  1163 
  1164 (* adhoc freezing *)
  1165 
  1166 fun adhoc_freeze_vars tm =
  1167   let
  1168     fun mk_inst (var as Var ((a, i), T)) =
  1169       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1170       in ((var,  Free(x, T)), x) end;
  1171     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1172   in (subst_atomic insts tm, xs) end;
  1173 
  1174 
  1175 (* string_of_vname *)
  1176 
  1177 val show_question_marks = ref true;
  1178 
  1179 fun string_of_vname (x, i) =
  1180   let
  1181     val question_mark = if ! show_question_marks then "?" else "";
  1182     val idx = string_of_int i;
  1183     val dot =
  1184       (case rev (Symbol.explode x) of
  1185         _ :: "\\<^isub>" :: _ => false
  1186       | _ :: "\\<^isup>" :: _ => false
  1187       | c :: _ => Symbol.is_digit c
  1188       | _ => true);
  1189   in
  1190     if dot then question_mark ^ x ^ "." ^ idx
  1191     else if i <> 0 then question_mark ^ x ^ idx
  1192     else question_mark ^ x
  1193   end;
  1194 
  1195 fun string_of_vname' (x, ~1) = x
  1196   | string_of_vname' xi = string_of_vname xi;
  1197 
  1198 fun string_of_term (Const(s,_)) = s
  1199   | string_of_term (Free(s,_)) = s
  1200   | string_of_term (Var(ix,_)) = string_of_vname ix
  1201   | string_of_term (Bound i) = string_of_int i
  1202   | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
  1203   | string_of_term (s $ t) =
  1204       "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
  1205 
  1206 end;
  1207 
  1208 structure BasicTerm: BASIC_TERM = Term;
  1209 open BasicTerm;