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