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