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