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