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