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