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