src/Pure/term.ML
author wenzelm
Sun Sep 25 23:36:14 2005 +0200 (2005-09-25)
changeset 17642 e063c0403650
parent 17314 04e21a27c0ad
child 17756 d4a35f82fbb4
permissions -rw-r--r--
zero_var_inst: replace loose bounds :000 etc.;
     1 (*  Title:      Pure/term.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Simply typed lambda-calculus: types, terms, and basic operations.
     7 *)
     8 
     9 infix 9  $;
    10 infixr 5 -->;
    11 infixr --->;
    12 infix aconv;
    13 
    14 signature BASIC_TERM =
    15 sig
    16   type indexname
    17   type class
    18   type sort
    19   type arity
    20   datatype typ =
    21     Type  of string * typ list |
    22     TFree of string * sort |
    23     TVar  of indexname * sort
    24   datatype term =
    25     Const of string * typ |
    26     Free of string * typ |
    27     Var of indexname * typ |
    28     Bound of int |
    29     Abs of string * typ * term |
    30     op $ of term * term
    31   exception TYPE of string * typ list * term list
    32   exception TERM of string * term list
    33   val dummyT: typ
    34   val no_dummyT: typ -> typ
    35   val --> : typ * typ -> typ
    36   val ---> : typ list * typ -> typ
    37   val dest_Type: typ -> string * typ list
    38   val dest_TVar: typ -> indexname * sort
    39   val dest_TFree: typ -> string * sort
    40   val is_Bound: term -> bool
    41   val is_Const: term -> bool
    42   val is_Free: term -> bool
    43   val is_Var: term -> bool
    44   val is_TVar: typ -> bool
    45   val is_funtype: typ -> bool
    46   val dest_Const: term -> string * typ
    47   val dest_Free: term -> string * typ
    48   val dest_Var: term -> indexname * typ
    49   val domain_type: typ -> typ
    50   val range_type: typ -> typ
    51   val binder_types: typ -> typ list
    52   val body_type: typ -> typ
    53   val strip_type: typ -> typ list * typ
    54   val type_of1: typ list * term -> typ
    55   val type_of: term -> typ
    56   val fastype_of1: typ list * term -> typ
    57   val fastype_of: term -> typ
    58   val list_abs: (string * typ) list * term -> term
    59   val strip_abs_body: term -> term
    60   val strip_abs_vars: term -> (string * typ) list
    61   val strip_qnt_body: string -> term -> term
    62   val strip_qnt_vars: string -> term -> (string * typ) list
    63   val list_comb: term * term list -> term
    64   val strip_comb: term -> term * term list
    65   val head_of: term -> term
    66   val size_of_term: term -> int
    67   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    68   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    69   val map_term_types: (typ -> typ) -> term -> term
    70   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    71   val 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 list_abs_free: (string * typ) list * term -> term
   116   val list_all_free: (string * typ) list * term -> term
   117   val list_all: (string * typ) list * term -> term
   118   val subst_atomic: (term * term) list -> term -> term
   119   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   120   val subst_atomic_types: (typ * typ) list -> term -> term
   121   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   122   val subst_TVars: (indexname * typ) list -> term -> term
   123   val subst_Vars: (indexname * term) list -> term -> term
   124   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   125   val is_first_order: string list -> term -> bool
   126   val maxidx_of_typ: typ -> int
   127   val maxidx_of_typs: typ list -> int
   128   val maxidx_of_term: term -> int
   129   val variant: string list -> string -> string
   130   val variantlist: string list * string list -> string list
   131     (*note reversed order of args wrt. variant!*)
   132   val add_typ_classes: typ * class list -> class list
   133   val add_typ_tycons: typ * string list -> string list
   134   val add_term_classes: term * class list -> class list
   135   val add_term_tycons: term * string list -> string list
   136   val add_term_consts: term * string list -> string list
   137   val term_consts: term -> string list
   138   val exists_subterm: (term -> bool) -> term -> bool
   139   val exists_Const: (string * typ -> bool) -> term -> bool
   140   val add_term_free_names: term * string list -> string list
   141   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   142   val add_typ_tfree_names: typ * string list -> string list
   143   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   144   val add_typ_varnames: typ * string list -> string list
   145   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   146   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   147   val add_term_tfree_names: term * string list -> string list
   148   val add_term_tvarnames: term * string list -> string list
   149   val typ_tfrees: typ -> (string * sort) list
   150   val typ_tvars: typ -> (indexname * sort) list
   151   val term_tfrees: term -> (string * sort) list
   152   val term_tvars: term -> (indexname * sort) list
   153   val add_typ_ixns: indexname list * typ -> indexname list
   154   val add_term_tvar_ixns: term * indexname list -> indexname list
   155   val add_term_vars: term * term list -> term list
   156   val term_vars: term -> term list
   157   val add_term_frees: term * term list -> term list
   158   val term_frees: term -> term list
   159   val variant_abs: string * typ * term -> string * term
   160   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   161   val show_question_marks: bool ref
   162 end;
   163 
   164 signature TERM =
   165 sig
   166   include BASIC_TERM
   167   val argument_type_of: term -> typ
   168   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   169   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   170   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   171   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   172   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   173   val add_frees: term -> (string * typ) list -> (string * typ) list
   174   val fast_indexname_ord: indexname * indexname -> order
   175   val indexname_ord: indexname * indexname -> order
   176   val sort_ord: sort * sort -> order
   177   val typ_ord: typ * typ -> order
   178   val fast_term_ord: term * term -> order
   179   val term_ord: term * term -> order
   180   val hd_ord: term * term -> order
   181   val termless: term * term -> bool
   182   val term_lpo: (string -> int) -> term * term -> order
   183   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   184   val rename_abs: term -> term -> term -> term option
   185   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   186   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   187   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   188   val var_ord: (indexname * typ) * (indexname * typ) -> order
   189   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   190     -> term -> term
   191   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
   192   val maxidx_typ: typ -> int -> int
   193   val maxidx_typs: typ list -> int -> int
   194   val maxidx_term: term -> int -> int
   195   val invent_names: string list -> string -> int -> string list
   196   val map_typ: (string -> string) -> (string -> string) -> typ -> typ
   197   val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   198   val dest_abs: string * typ * term -> string * term
   199   val bound: int -> string
   200   val is_bound: string -> bool
   201   val zero_var_indexesT: typ -> typ
   202   val zero_var_indexes: term -> term
   203   val zero_var_indexes_inst: term ->
   204     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   205   val dummy_patternN: string
   206   val no_dummy_patterns: term -> term
   207   val replace_dummy_patterns: int * term -> int * term
   208   val is_replaced_dummy_pattern: indexname -> bool
   209   val show_dummy_patterns: term -> term
   210   val adhoc_freeze_vars: term -> term * string list
   211   val string_of_vname: indexname -> string
   212   val string_of_vname': indexname -> 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 
   506 (** Comparing terms, types, sorts etc. **)
   507 
   508 (* fast syntactic comparison *)
   509 
   510 fun fast_indexname_ord ((x, i), (y, j)) =
   511   (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   512 
   513 fun sort_ord SS =
   514   if pointer_eq SS then EQUAL
   515   else dict_ord fast_string_ord SS;
   516 
   517 local
   518 
   519 fun cons_nr (TVar _) = 0
   520   | cons_nr (TFree _) = 1
   521   | cons_nr (Type _) = 2;
   522 
   523 in
   524 
   525 fun typ_ord TU =
   526   if pointer_eq TU then EQUAL
   527   else
   528     (case TU of
   529       (Type (a, Ts), Type (b, Us)) =>
   530         (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   531     | (TFree (a, S), TFree (b, S')) =>
   532         (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   533     | (TVar (xi, S), TVar (yj, S')) =>
   534         (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
   535     | (T, U) => int_ord (cons_nr T, cons_nr U));
   536 
   537 end;
   538 
   539 local
   540 
   541 fun cons_nr (Const _) = 0
   542   | cons_nr (Free _) = 1
   543   | cons_nr (Var _) = 2
   544   | cons_nr (Bound _) = 3
   545   | cons_nr (Abs _) = 4
   546   | cons_nr (_ $ _) = 5;
   547 
   548 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   549   | struct_ord (t1 $ t2, u1 $ u2) =
   550       (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   551   | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
   552 
   553 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   554   | atoms_ord (t1 $ t2, u1 $ u2) =
   555       (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   556   | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   557   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   558   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   559   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   560   | atoms_ord _ = sys_error "atoms_ord";
   561 
   562 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
   563       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   564   | types_ord (t1 $ t2, u1 $ u2) =
   565       (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   566   | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   567   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   568   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   569   | types_ord (Bound _, Bound _) = EQUAL
   570   | types_ord _ = sys_error "types_ord";
   571 
   572 in
   573 
   574 fun fast_term_ord tu =
   575   if pointer_eq tu then EQUAL
   576   else
   577     (case struct_ord tu of
   578       EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
   579     | ord => ord);
   580 
   581 fun op aconv tu = (fast_term_ord tu = EQUAL);
   582 fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL);
   583 
   584 structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
   585 structure Typtab = TableFun(type key = typ val ord = typ_ord);
   586 structure Termtab = TableFun(type key = term val ord = fast_term_ord);
   587 
   588 end;
   589 
   590 
   591 (* term_ord *)
   592 
   593 (*a linear well-founded AC-compatible ordering for terms:
   594   s < t <=> 1. size(s) < size(t) or
   595             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   596             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   597                (s1..sn) < (t1..tn) (lexicographically)*)
   598 
   599 fun indexname_ord ((x, i), (y, j)) =
   600   (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   601 
   602 local
   603 
   604 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
   605   | hd_depth p = p;
   606 
   607 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   608   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   609   | dest_hd (Var v) = (v, 2)
   610   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   611   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   612 
   613 in
   614 
   615 fun term_ord tu =
   616   if pointer_eq tu then EQUAL
   617   else
   618     (case tu of
   619       (Abs (_, T, t), Abs(_, U, u)) =>
   620         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   621     | (t, u) =>
   622         (case int_ord (size_of_term t, size_of_term u) of
   623           EQUAL =>
   624             (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
   625               EQUAL => args_ord (t, u) | ord => ord)
   626         | ord => ord))
   627 and hd_ord (f, g) =
   628   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   629 and args_ord (f $ t, g $ u) =
   630       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   631   | args_ord _ = EQUAL;
   632 
   633 fun termless tu = (term_ord tu = LESS);
   634 
   635 end;
   636 
   637 
   638 (** Lexicographic path order on terms **)
   639 
   640 (*
   641   See Baader & Nipkow, Term rewriting, CUP 1998.
   642   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   643   constants.
   644 
   645   f_ord maps strings to integers and serves two purposes:
   646   - Predicate on constant symbols.  Those that are not recognised by f_ord
   647     must be mapped to ~1.
   648   - Order on the recognised symbols.  These must be mapped to distinct
   649     integers >= 0.
   650 
   651 *)
   652 
   653 local
   654 fun dest_hd f_ord (Const (a, T)) =
   655       let val ord = f_ord a in
   656         if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
   657       end
   658   | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
   659   | dest_hd _ (Var v) = ((1, v), 1)
   660   | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
   661   | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
   662 
   663 fun term_lpo f_ord (s, t) =
   664   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
   665     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
   666     then case hd_ord f_ord (f, g) of
   667         GREATER =>
   668           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   669           then GREATER else LESS
   670       | EQUAL =>
   671           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   672           then list_ord (term_lpo f_ord) (ss, ts)
   673           else LESS
   674       | LESS => LESS
   675     else GREATER
   676   end
   677 and hd_ord f_ord (f, g) = case (f, g) of
   678     (Abs (_, T, t), Abs (_, U, u)) =>
   679       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   680   | (_, _) => prod_ord (prod_ord int_ord
   681                   (prod_ord indexname_ord typ_ord)) int_ord
   682                 (dest_hd f_ord f, dest_hd f_ord g)
   683 in
   684 val term_lpo = term_lpo
   685 end;
   686 
   687 
   688 (** Connectives of higher order logic **)
   689 
   690 fun itselfT ty = Type ("itself", [ty]);
   691 val a_itselfT = itselfT (TFree ("'a", []));
   692 
   693 val propT : typ = Type("prop",[]);
   694 
   695 val implies = Const("==>", propT-->propT-->propT);
   696 
   697 fun all T = Const("all", (T-->propT)-->propT);
   698 
   699 fun equals T = Const("==", T-->T-->propT);
   700 
   701 (* maps  !!x1...xn. t   to   t  *)
   702 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   703   | strip_all_body t  =  t;
   704 
   705 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   706 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   707                 (a,T) :: strip_all_vars t
   708   | strip_all_vars t  =  [] : (string*typ) list;
   709 
   710 (*increments a term's non-local bound variables
   711   required when moving a term within abstractions
   712      inc is  increment for bound variables
   713      lev is  level at which a bound variable is considered 'loose'*)
   714 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   715   | incr_bv (inc, lev, Abs(a,T,body)) =
   716         Abs(a, T, incr_bv(inc,lev+1,body))
   717   | incr_bv (inc, lev, f$t) =
   718       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   719   | incr_bv (inc, lev, u) = u;
   720 
   721 fun incr_boundvars  0  t = t
   722   | incr_boundvars inc t = incr_bv(inc,0,t);
   723 
   724 (*Scan a pair of terms; while they are similar,
   725   accumulate corresponding bound vars in "al"*)
   726 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   727       match_bvs(s, t, if x="" orelse y="" then al
   728                                           else (x,y)::al)
   729   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   730   | match_bvs(_,_,al) = al;
   731 
   732 (* strip abstractions created by parameters *)
   733 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   734 
   735 fun rename_abs pat obj t =
   736   let
   737     val ren = match_bvs (pat, obj, []);
   738     fun ren_abs (Abs (x, T, b)) =
   739           Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b)
   740       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   741       | ren_abs t = t
   742   in if null ren then NONE else SOME (ren_abs t) end;
   743 
   744 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   745    (Bound 0) is loose at level 0 *)
   746 fun add_loose_bnos (Bound i, lev, js) =
   747         if i<lev then js  else  (i-lev) ins_int js
   748   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   749   | add_loose_bnos (f$t, lev, js) =
   750         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   751   | add_loose_bnos (_, _, js) = js;
   752 
   753 fun loose_bnos t = add_loose_bnos (t, 0, []);
   754 
   755 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   756    level k or beyond. *)
   757 fun loose_bvar(Bound i,k) = i >= k
   758   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   759   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   760   | loose_bvar _ = false;
   761 
   762 fun loose_bvar1(Bound i,k) = i = k
   763   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   764   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   765   | loose_bvar1 _ = false;
   766 
   767 (*Substitute arguments for loose bound variables.
   768   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   769   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   770         and the appropriate call is  subst_bounds([b,a], c) .
   771   Loose bound variables >=n are reduced by "n" to
   772      compensate for the disappearance of lambdas.
   773 *)
   774 fun subst_bounds (args: term list, t) : term =
   775   let val n = length args;
   776       fun subst (t as Bound i, lev) =
   777            (if i<lev then  t    (*var is locally bound*)
   778             else  incr_boundvars lev (List.nth(args, i-lev))
   779                     handle Subscript => Bound(i-n)  (*loose: change it*))
   780         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   781         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   782         | subst (t,lev) = t
   783   in   case args of [] => t  | _ => subst (t,0)  end;
   784 
   785 (*Special case: one argument*)
   786 fun subst_bound (arg, t) : term =
   787   let fun subst (t as Bound i, lev) =
   788             if i<lev then  t    (*var is locally bound*)
   789             else  if i=lev then incr_boundvars lev arg
   790                            else Bound(i-1)  (*loose: change it*)
   791         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   792         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   793         | subst (t,lev) = t
   794   in  subst (t,0)  end;
   795 
   796 (*beta-reduce if possible, else form application*)
   797 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   798   | betapply (f,u) = f$u;
   799 
   800 
   801 (** Specialized equality, membership, insertion etc. **)
   802 
   803 (* indexnames *)
   804 
   805 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   806 
   807 fun mem_ix (_, []) = false
   808   | mem_ix (x, y :: ys) = eq_ix (x, y) orelse mem_ix (x, ys);
   809 
   810 fun ins_ix (x, xs) = if mem_ix (x, xs) then xs else x :: xs;
   811 
   812 
   813 (* variables *)
   814 
   815 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   816 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   817 
   818 val tvar_ord = prod_ord indexname_ord sort_ord;
   819 val var_ord = prod_ord indexname_ord typ_ord;
   820 
   821 
   822 (* terms *)
   823 
   824 fun mem_term (_, []) = false
   825   | mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts);
   826 
   827 fun subset_term ([], ys) = true
   828   | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
   829 
   830 fun eq_set_term (xs, ys) =
   831     xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
   832 
   833 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   834 
   835 fun union_term (xs, []) = xs
   836   | union_term ([], ys) = ys
   837   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   838 
   839 fun inter_term ([], ys) = []
   840   | inter_term (x::xs, ys) =
   841       if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
   842 
   843 
   844 (*A fast unification filter: true unless the two terms cannot be unified.
   845   Terms must be NORMAL.  Treats all Vars as distinct. *)
   846 fun could_unify (t,u) =
   847   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   848         | matchrands _ = true
   849   in case (head_of t , head_of u) of
   850         (_, Var _) => true
   851       | (Var _, _) => true
   852       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   853       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   854       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   855       | (Abs _, _) =>  true   (*because of possible eta equality*)
   856       | (_, Abs _) =>  true
   857       | _ => false
   858   end;
   859 
   860 (*Substitute new for free occurrences of old in a term*)
   861 fun subst_free [] = (fn t=>t)
   862   | subst_free pairs =
   863       let fun substf u =
   864             case AList.lookup (op aconv) pairs u of
   865                 SOME u' => u'
   866               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   867                                  | t$u' => substf t $ substf u'
   868                                  | _ => u)
   869       in  substf  end;
   870 
   871 (*a total, irreflexive ordering on index names*)
   872 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   873 
   874 
   875 (*Abstraction of the term "body" over its occurrences of v,
   876     which must contain no loose bound variables.
   877   The resulting term is ready to become the body of an Abs.*)
   878 fun abstract_over (v, body) =
   879   let
   880     exception SAME;
   881     fun abs lev tm =
   882       if v aconv tm then Bound lev
   883       else
   884         (case tm of
   885           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   886         | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
   887         | _ => raise SAME);
   888   in abs 0 body handle SAME => body end;
   889 
   890 fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   891   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   892   | lambda v t = raise TERM ("lambda", [v, t]);
   893 
   894 (*Form an abstraction over a free variable.*)
   895 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   896 
   897 (*Abstraction over a list of free variables*)
   898 fun list_abs_free ([ ] ,     t) = t
   899   | list_abs_free ((a,T)::vars, t) =
   900       absfree(a, T, list_abs_free(vars,t));
   901 
   902 (*Quantification over a list of free variables*)
   903 fun list_all_free ([], t: term) = t
   904   | list_all_free ((a,T)::vars, t) =
   905         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   906 
   907 (*Quantification over a list of variables (already bound in body) *)
   908 fun list_all ([], t) = t
   909   | list_all ((a,T)::vars, t) =
   910         (all T) $ (Abs(a, T, list_all(vars,t)));
   911 
   912 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   913   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   914 fun subst_atomic [] tm = tm
   915   | subst_atomic inst tm =
   916       let
   917         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   918           | subst (t $ u) = subst t $ subst u
   919           | subst t = if_none (AList.lookup (op aconv) inst t) t;
   920       in subst tm end;
   921 
   922 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   923 fun typ_subst_atomic [] ty = ty
   924   | typ_subst_atomic inst ty =
   925       let
   926         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   927           | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
   928       in subst ty end;
   929 
   930 fun subst_atomic_types [] tm = tm
   931   | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
   932 
   933 fun typ_subst_TVars [] ty = ty
   934   | typ_subst_TVars inst ty =
   935       let
   936         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   937           | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
   938           | subst T = T;
   939       in subst ty end;
   940 
   941 fun subst_TVars [] tm = tm
   942   | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
   943 
   944 (*see also Envir.norm_term*)
   945 fun subst_Vars [] tm = tm
   946   | subst_Vars inst tm =
   947       let
   948         fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
   949           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   950           | subst (t $ u) = subst t $ subst u
   951           | subst t = t;
   952       in subst tm end;
   953 
   954 (*see also Envir.norm_term*)
   955 fun subst_vars ([], []) tm = tm
   956   | subst_vars ([], inst) tm = subst_Vars inst tm
   957   | subst_vars (instT, inst) tm =
   958       let
   959         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   960           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   961           | subst (t as Var (xi, T)) =
   962               (case AList.lookup (op =) inst xi of
   963                 NONE => Var (xi, typ_subst_TVars instT T)
   964               | SOME t => t)
   965           | subst (t as Bound _) = t
   966           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   967           | subst (t $ u) = subst t $ subst u;
   968       in subst tm end;
   969 
   970 
   971 (* instantiation of schematic variables (types before terms) *)
   972 
   973 local exception SAME in
   974 
   975 fun instantiateT_same [] _ = raise SAME
   976   | instantiateT_same instT ty =
   977       let
   978         fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
   979           | subst_typ (TVar v) =
   980               (case AList.lookup eq_tvar instT v of
   981                 SOME T => T
   982               | NONE => raise SAME)
   983           | subst_typ _ = raise SAME
   984         and subst_typs (T :: Ts) =
   985             (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   986               handle SAME => T :: subst_typs Ts)
   987           | subst_typs [] = raise SAME;
   988       in subst_typ ty end;
   989 
   990 fun instantiate ([], []) tm = tm
   991   | instantiate (instT, inst) tm =
   992       let
   993         val substT = instantiateT_same instT;
   994         fun subst (Const (c, T)) = Const (c, substT T)
   995           | subst (Free (x, T)) = Free (x, substT T)
   996           | subst (Var (xi, T)) =
   997               let val (T', same) = (substT T, false) handle SAME => (T, true) in
   998                 (case AList.lookup eq_var inst (xi, T') of
   999                    SOME t => t
  1000                  | NONE => if same then raise SAME else Var (xi, T'))
  1001               end
  1002           | subst (Bound _) = raise SAME
  1003           | subst (Abs (x, T, t)) =
  1004               (Abs (x, substT T, subst t handle SAME => t)
  1005                 handle SAME => Abs (x, T, subst t))
  1006           | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
  1007       in subst tm handle SAME => tm end;
  1008 
  1009 fun instantiateT instT ty =
  1010   instantiateT_same instT ty handle SAME => ty;
  1011 
  1012 end;
  1013 
  1014 
  1015 (** Identifying first-order terms **)
  1016 
  1017 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
  1018 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
  1019 
  1020 (*First order means in all terms of the form f(t1,...,tn) no argument has a
  1021   function type. The supplied quantifiers are excluded: their argument always
  1022   has a function type through a recursive call into its body.*)
  1023 fun is_first_order quants =
  1024   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
  1025         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
  1026             q mem_string quants  andalso   (*it is a known quantifier*)
  1027             not (is_funtype T)   andalso first_order1 (T::Ts) body
  1028         | first_order1 Ts t =
  1029             case strip_comb t of
  1030                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1031                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1032                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1033                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1034                | (Abs _, ts) => false (*not in beta-normal form*)
  1035                | _ => error "first_order: unexpected case"
  1036     in  first_order1 []  end;
  1037 
  1038 
  1039 (* maximum index of typs and terms *)
  1040 
  1041 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
  1042   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
  1043   | maxidx_typ (TFree _) i = i
  1044 and maxidx_typs [] i = i
  1045   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
  1046 
  1047 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
  1048   | maxidx_term (Const (_, T)) i = maxidx_typ T i
  1049   | maxidx_term (Free (_, T)) i = maxidx_typ T i
  1050   | maxidx_term (Bound _) i = i
  1051   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
  1052   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
  1053 
  1054 fun maxidx_of_typ T = maxidx_typ T ~1;
  1055 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
  1056 fun maxidx_of_term t = maxidx_term t ~1;
  1057 
  1058 
  1059 
  1060 (**** Syntax-related declarations ****)
  1061 
  1062 (*** Printing ***)
  1063 
  1064 (*Makes a variant of a name distinct from the names in 'used'.
  1065   First attaches the suffix and then increments this;
  1066   preserves a suffix of underscores "_". *)
  1067 fun variant used name =
  1068   let
  1069     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
  1070     fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
  1071     fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
  1072   in vary1 (if c = "" then "u" else c) ^ u end;
  1073 
  1074 (*Create variants of the list of names, with priority to the first ones*)
  1075 fun variantlist ([], used) = []
  1076   | variantlist(b::bs, used) =
  1077       let val b' = variant used b
  1078       in  b' :: variantlist (bs, b'::used)  end;
  1079 
  1080 (*Invent fresh names*)
  1081 fun invent_names _ _ 0 = []
  1082   | invent_names used a n =
  1083       let val b = Symbol.bump_string a in
  1084         if a mem_string used then invent_names used b n
  1085         else a :: invent_names used b (n - 1)
  1086       end;
  1087 
  1088 
  1089 (** Consts etc. **)
  1090 
  1091 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
  1092   | add_typ_classes (TFree (_, S), cs) = S union cs
  1093   | add_typ_classes (TVar (_, S), cs) = S union cs;
  1094 
  1095 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
  1096   | add_typ_tycons (_, cs) = cs;
  1097 
  1098 val add_term_classes = it_term_types add_typ_classes;
  1099 val add_term_tycons = it_term_types add_typ_tycons;
  1100 
  1101 fun add_term_consts (Const (c, _), cs) = c ins_string cs
  1102   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
  1103   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
  1104   | add_term_consts (_, cs) = cs;
  1105 
  1106 fun term_consts t = add_term_consts(t,[]);
  1107 
  1108 fun exists_subterm P =
  1109   let
  1110     fun ex tm = P tm orelse
  1111       (case tm of
  1112         t $ u => ex t orelse ex u
  1113       | Abs (_, _, t) => ex t
  1114       | _ => false);
  1115   in ex end;
  1116 
  1117 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
  1118 
  1119 (*map classes, tycons*)
  1120 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
  1121   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
  1122   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
  1123 
  1124 (*map classes, tycons, consts*)
  1125 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
  1126   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
  1127   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
  1128   | map_term _ _ _ (t as Bound _) = t
  1129   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
  1130   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
  1131 
  1132 
  1133 (** TFrees and TVars **)
  1134 
  1135 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
  1136 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
  1137   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  1138   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  1139   | add_term_free_names (_, bs) = bs;
  1140 
  1141 (*Accumulates the names in the term, suppressing duplicates.
  1142   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  1143 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
  1144   | add_term_names (Free(a,_), bs) = a ins_string bs
  1145   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  1146   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  1147   | add_term_names (_, bs) = bs;
  1148 
  1149 (*Accumulates the TVars in a type, suppressing duplicates. *)
  1150 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
  1151   | add_typ_tvars(TFree(_),vs) = vs
  1152   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  1153 
  1154 (*Accumulates the TFrees in a type, suppressing duplicates. *)
  1155 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
  1156   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
  1157   | add_typ_tfree_names(TVar(_),fs) = fs;
  1158 
  1159 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
  1160   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  1161   | add_typ_tfrees(TVar(_),fs) = fs;
  1162 
  1163 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
  1164   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
  1165   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
  1166 
  1167 (*Accumulates the TVars in a term, suppressing duplicates. *)
  1168 val add_term_tvars = it_term_types add_typ_tvars;
  1169 
  1170 (*Accumulates the TFrees in a term, suppressing duplicates. *)
  1171 val add_term_tfrees = it_term_types add_typ_tfrees;
  1172 val add_term_tfree_names = it_term_types add_typ_tfree_names;
  1173 
  1174 val add_term_tvarnames = it_term_types add_typ_varnames;
  1175 
  1176 (*Non-list versions*)
  1177 fun typ_tfrees T = add_typ_tfrees(T,[]);
  1178 fun typ_tvars T = add_typ_tvars(T,[]);
  1179 fun term_tfrees t = add_term_tfrees(t,[]);
  1180 fun term_tvars t = add_term_tvars(t,[]);
  1181 
  1182 (*special code to enforce left-to-right collection of TVar-indexnames*)
  1183 
  1184 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
  1185   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
  1186                                      else ixns@[ixn]
  1187   | add_typ_ixns(ixns,TFree(_)) = ixns;
  1188 
  1189 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1190   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1191   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1192   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1193   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1194       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1195   | add_term_tvar_ixns(f$t,ixns) =
  1196       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1197 
  1198 
  1199 (** Frees and Vars **)
  1200 
  1201 (*Accumulates the Vars in the term, suppressing duplicates*)
  1202 fun add_term_vars (t, vars: term list) = case t of
  1203     Var   _ => OrdList.insert term_ord t vars
  1204   | Abs (_,_,body) => add_term_vars(body,vars)
  1205   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1206   | _ => vars;
  1207 
  1208 fun term_vars t = add_term_vars(t,[]);
  1209 
  1210 (*Accumulates the Frees in the term, suppressing duplicates*)
  1211 fun add_term_frees (t, frees: term list) = case t of
  1212     Free   _ => OrdList.insert term_ord t frees
  1213   | Abs (_,_,body) => add_term_frees(body,frees)
  1214   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1215   | _ => frees;
  1216 
  1217 fun term_frees t = add_term_frees(t,[]);
  1218 
  1219 (*Given an abstraction over P, replaces the bound variable by a Free variable
  1220   having a unique name*)
  1221 fun variant_abs (a,T,P) =
  1222   let val b = variant (add_term_names(P,[])) a
  1223   in  (b,  subst_bound (Free(b,T), P))  end;
  1224 
  1225 fun dest_abs (x, T, body) =
  1226   let
  1227     fun name_clash (Free (y, _)) = (x = y)
  1228       | name_clash (t $ u) = name_clash t orelse name_clash u
  1229       | name_clash (Abs (_, _, t)) = name_clash t
  1230       | name_clash _ = false;
  1231   in
  1232     if name_clash body then
  1233       dest_abs (variant [x] x, T, body)    (*potentially slow, but rarely happens*)
  1234     else (x, subst_bound (Free (x, T), body))
  1235   end;
  1236 
  1237 (*names for numbered variables --
  1238   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
  1239 local
  1240   val small_int = Vector.tabulate (1000, fn i =>
  1241     let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
  1242     in ":" ^ leading ^ string_of_int i end);
  1243 in
  1244   fun bound n =
  1245     if n < 1000 then Vector.sub (small_int, n)
  1246     else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
  1247 end;
  1248 
  1249 val is_bound = String.isPrefix ":";
  1250 
  1251 (* renames and reverses the strings in vars away from names *)
  1252 fun rename_aTs names vars : (string*typ)list =
  1253   let fun rename_aT (vars,(a,T)) =
  1254                 (variant (map #1 vars @ names) a, T) :: vars
  1255   in Library.foldl rename_aT ([],vars) end;
  1256 
  1257 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
  1258 
  1259 
  1260 (* zero var indexes *)
  1261 
  1262 fun zero_var_inst vars =
  1263   fold (fn v as ((x, i), X) => fn (used, inst) =>
  1264     let
  1265       val x' = variant used (if is_bound x then "u" else x);
  1266       val used' = x' :: used;
  1267     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
  1268   vars ([], []) |> #2;
  1269 
  1270 fun zero_var_indexesT ty =
  1271   instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
  1272 
  1273 fun zero_var_indexes_inst tm =
  1274   let
  1275     val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
  1276     val inst =
  1277       add_vars tm [] |> map (apsnd (instantiateT instT))
  1278       |> sort var_ord |> zero_var_inst |> map (apsnd Var);
  1279   in (instT, inst) end;
  1280 
  1281 fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
  1282 
  1283 
  1284 (* dummy patterns *)
  1285 
  1286 val dummy_patternN = "dummy_pattern";
  1287 
  1288 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1289   | is_dummy_pattern _ = false;
  1290 
  1291 fun no_dummy_patterns tm =
  1292   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  1293   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1294 
  1295 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1296       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1297   | replace_dummy Ts (i, Abs (x, T, t)) =
  1298       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1299       in (i', Abs (x, T, t')) end
  1300   | replace_dummy Ts (i, t $ u) =
  1301       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1302       in (i'', t' $ u') end
  1303   | replace_dummy _ (i, a) = (i, a);
  1304 
  1305 val replace_dummy_patterns = replace_dummy [];
  1306 
  1307 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1308   | is_replaced_dummy_pattern _ = false;
  1309 
  1310 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1311   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1312   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1313   | show_dummy_patterns a = a;
  1314 
  1315 
  1316 (* adhoc freezing *)
  1317 
  1318 fun adhoc_freeze_vars tm =
  1319   let
  1320     fun mk_inst (var as Var ((a, i), T)) =
  1321       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1322       in ((var,  Free(x, T)), x) end;
  1323     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1324   in (subst_atomic insts tm, xs) end;
  1325 
  1326 
  1327 (* string_of_vname *)
  1328 
  1329 val show_question_marks = ref true;
  1330 
  1331 fun string_of_vname (x, i) =
  1332   let
  1333     val question_mark = if ! show_question_marks then "?" else "";
  1334     val idx = string_of_int i;
  1335     val dot =
  1336       (case rev (Symbol.explode x) of
  1337         _ :: "\\<^isub>" :: _ => false
  1338       | _ :: "\\<^isup>" :: _ => false
  1339       | c :: _ => Symbol.is_digit c
  1340       | _ => true);
  1341   in
  1342     if dot then question_mark ^ x ^ "." ^ idx
  1343     else if i <> 0 then question_mark ^ x ^ idx
  1344     else question_mark ^ x
  1345   end;
  1346 
  1347 fun string_of_vname' (x, ~1) = x
  1348   | string_of_vname' xi = string_of_vname xi;
  1349 
  1350 end;
  1351 
  1352 structure BasicTerm: BASIC_TERM = Term;
  1353 open BasicTerm;