src/Pure/term.ML
author wenzelm
Tue Jan 31 18:19:26 2006 +0100 (2006-01-31)
changeset 18871 ca48320f6619
parent 18847 5fac129ae936
child 18893 2dbf73278b0e
permissions -rw-r--r--
lambda: abstract over TYPE argument, too;
     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 as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t))
   899   | lambda v t = raise TERM ("lambda", [v, t]);
   900 
   901 (*Form an abstraction over a free variable.*)
   902 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   903 fun absdummy (T, body) = Abs ("uu", T, body);
   904 
   905 (*Abstraction over a list of free variables*)
   906 fun list_abs_free ([ ] ,     t) = t
   907   | list_abs_free ((a,T)::vars, t) =
   908       absfree(a, T, list_abs_free(vars,t));
   909 
   910 (*Quantification over a list of free variables*)
   911 fun list_all_free ([], t: term) = t
   912   | list_all_free ((a,T)::vars, t) =
   913         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   914 
   915 (*Quantification over a list of variables (already bound in body) *)
   916 fun list_all ([], t) = t
   917   | list_all ((a,T)::vars, t) =
   918         (all T) $ (Abs(a, T, list_all(vars,t)));
   919 
   920 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   921   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   922 fun subst_atomic [] tm = tm
   923   | subst_atomic inst tm =
   924       let
   925         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   926           | subst (t $ u) = subst t $ subst u
   927           | subst t = if_none (AList.lookup (op aconv) inst t) t;
   928       in subst tm end;
   929 
   930 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   931 fun typ_subst_atomic [] ty = ty
   932   | typ_subst_atomic inst ty =
   933       let
   934         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   935           | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
   936       in subst ty end;
   937 
   938 fun subst_atomic_types [] tm = tm
   939   | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
   940 
   941 fun typ_subst_TVars [] ty = ty
   942   | typ_subst_TVars inst ty =
   943       let
   944         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   945           | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
   946           | subst T = T;
   947       in subst ty end;
   948 
   949 fun subst_TVars [] tm = tm
   950   | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
   951 
   952 (*see also Envir.norm_term*)
   953 fun subst_Vars [] tm = tm
   954   | subst_Vars inst tm =
   955       let
   956         fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
   957           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   958           | subst (t $ u) = subst t $ subst u
   959           | subst t = t;
   960       in subst tm end;
   961 
   962 (*see also Envir.norm_term*)
   963 fun subst_vars ([], []) tm = tm
   964   | subst_vars ([], inst) tm = subst_Vars inst tm
   965   | subst_vars (instT, inst) tm =
   966       let
   967         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   968           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   969           | subst (t as Var (xi, T)) =
   970               (case AList.lookup (op =) inst xi of
   971                 NONE => Var (xi, typ_subst_TVars instT T)
   972               | SOME t => t)
   973           | subst (t as Bound _) = t
   974           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   975           | subst (t $ u) = subst t $ subst u;
   976       in subst tm end;
   977 
   978 
   979 (* instantiation of schematic variables (types before terms) *)
   980 
   981 local exception SAME in
   982 
   983 fun instantiateT_same [] _ = raise SAME
   984   | instantiateT_same instT ty =
   985       let
   986         fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
   987           | subst_typ (TVar v) =
   988               (case AList.lookup eq_tvar instT v of
   989                 SOME T => T
   990               | NONE => raise SAME)
   991           | subst_typ _ = raise SAME
   992         and subst_typs (T :: Ts) =
   993             (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   994               handle SAME => T :: subst_typs Ts)
   995           | subst_typs [] = raise SAME;
   996       in subst_typ ty end;
   997 
   998 fun instantiate ([], []) tm = tm
   999   | instantiate (instT, inst) tm =
  1000       let
  1001         val substT = instantiateT_same instT;
  1002         fun subst (Const (c, T)) = Const (c, substT T)
  1003           | subst (Free (x, T)) = Free (x, substT T)
  1004           | subst (Var (xi, T)) =
  1005               let val (T', same) = (substT T, false) handle SAME => (T, true) in
  1006                 (case AList.lookup eq_var inst (xi, T') of
  1007                    SOME t => t
  1008                  | NONE => if same then raise SAME else Var (xi, T'))
  1009               end
  1010           | subst (Bound _) = raise SAME
  1011           | subst (Abs (x, T, t)) =
  1012               (Abs (x, substT T, subst t handle SAME => t)
  1013                 handle SAME => Abs (x, T, subst t))
  1014           | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
  1015       in subst tm handle SAME => tm end;
  1016 
  1017 fun instantiateT instT ty =
  1018   instantiateT_same instT ty handle SAME => ty;
  1019 
  1020 end;
  1021 
  1022 
  1023 (** Identifying first-order terms **)
  1024 
  1025 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
  1026 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
  1027 
  1028 (*First order means in all terms of the form f(t1,...,tn) no argument has a
  1029   function type. The supplied quantifiers are excluded: their argument always
  1030   has a function type through a recursive call into its body.*)
  1031 fun is_first_order quants =
  1032   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
  1033         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
  1034             q mem_string quants  andalso   (*it is a known quantifier*)
  1035             not (is_funtype T)   andalso first_order1 (T::Ts) body
  1036         | first_order1 Ts t =
  1037             case strip_comb t of
  1038                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1039                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1040                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1041                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1042                | (Abs _, ts) => false (*not in beta-normal form*)
  1043                | _ => error "first_order: unexpected case"
  1044     in  first_order1 []  end;
  1045 
  1046 
  1047 (* maximum index of typs and terms *)
  1048 
  1049 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
  1050   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
  1051   | maxidx_typ (TFree _) i = i
  1052 and maxidx_typs [] i = i
  1053   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
  1054 
  1055 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
  1056   | maxidx_term (Const (_, T)) i = maxidx_typ T i
  1057   | maxidx_term (Free (_, T)) i = maxidx_typ T i
  1058   | maxidx_term (Bound _) i = i
  1059   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
  1060   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
  1061 
  1062 fun maxidx_of_typ T = maxidx_typ T ~1;
  1063 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
  1064 fun maxidx_of_term t = maxidx_term t ~1;
  1065 
  1066 
  1067 
  1068 (**** Syntax-related declarations ****)
  1069 
  1070 (*** Printing ***)
  1071 
  1072 (*Makes a variant of a name distinct from the names in 'used'.
  1073   First attaches the suffix and then increments this;
  1074   preserves a suffix of underscores "_". *)
  1075 fun variant used name =
  1076   let
  1077     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
  1078     fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
  1079     fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
  1080   in vary1 (if c = "" then "u" else c) ^ u end;
  1081 
  1082 (*Create variants of the list of names, with priority to the first ones*)
  1083 fun variantlist ([], used) = []
  1084   | variantlist(b::bs, used) =
  1085       let val b' = variant used b
  1086       in  b' :: variantlist (bs, b'::used)  end;
  1087 
  1088 (*Invent fresh names*)
  1089 fun invent_names _ _ 0 = []
  1090   | invent_names used a n =
  1091       let val b = Symbol.bump_string a in
  1092         if a mem_string used then invent_names used b n
  1093         else a :: invent_names used b (n - 1)
  1094       end;
  1095 
  1096 
  1097 (** Consts etc. **)
  1098 
  1099 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
  1100   | add_typ_classes (TFree (_, S), cs) = S union cs
  1101   | add_typ_classes (TVar (_, S), cs) = S union cs;
  1102 
  1103 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
  1104   | add_typ_tycons (_, cs) = cs;
  1105 
  1106 val add_term_classes = it_term_types add_typ_classes;
  1107 val add_term_tycons = it_term_types add_typ_tycons;
  1108 
  1109 fun add_term_consts (Const (c, _), cs) = c ins_string cs
  1110   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
  1111   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
  1112   | add_term_consts (_, cs) = cs;
  1113 
  1114 fun term_consts t = add_term_consts(t,[]);
  1115 
  1116 fun exists_subterm P =
  1117   let
  1118     fun ex tm = P tm orelse
  1119       (case tm of
  1120         t $ u => ex t orelse ex u
  1121       | Abs (_, _, t) => ex t
  1122       | _ => false);
  1123   in ex end;
  1124 
  1125 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
  1126 
  1127 (*map classes, tycons*)
  1128 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
  1129   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
  1130   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
  1131 
  1132 (*map classes, tycons, consts*)
  1133 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
  1134   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
  1135   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
  1136   | map_term _ _ _ (t as Bound _) = t
  1137   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
  1138   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
  1139 
  1140 
  1141 (** TFrees and TVars **)
  1142 
  1143 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
  1144 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
  1145   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  1146   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  1147   | add_term_free_names (_, bs) = bs;
  1148 
  1149 (*Accumulates the names in the term, suppressing duplicates.
  1150   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  1151 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
  1152   | add_term_names (Free(a,_), bs) = a ins_string bs
  1153   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  1154   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  1155   | add_term_names (_, bs) = bs;
  1156 
  1157 (*Accumulates the TVars in a type, suppressing duplicates. *)
  1158 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
  1159   | add_typ_tvars(TFree(_),vs) = vs
  1160   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  1161 
  1162 (*Accumulates the TFrees in a type, suppressing duplicates. *)
  1163 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
  1164   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
  1165   | add_typ_tfree_names(TVar(_),fs) = fs;
  1166 
  1167 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
  1168   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  1169   | add_typ_tfrees(TVar(_),fs) = fs;
  1170 
  1171 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
  1172   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
  1173   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
  1174 
  1175 (*Accumulates the TVars in a term, suppressing duplicates. *)
  1176 val add_term_tvars = it_term_types add_typ_tvars;
  1177 
  1178 (*Accumulates the TFrees in a term, suppressing duplicates. *)
  1179 val add_term_tfrees = it_term_types add_typ_tfrees;
  1180 val add_term_tfree_names = it_term_types add_typ_tfree_names;
  1181 
  1182 val add_term_tvarnames = it_term_types add_typ_varnames;
  1183 
  1184 (*Non-list versions*)
  1185 fun typ_tfrees T = add_typ_tfrees(T,[]);
  1186 fun typ_tvars T = add_typ_tvars(T,[]);
  1187 fun term_tfrees t = add_term_tfrees(t,[]);
  1188 fun term_tvars t = add_term_tvars(t,[]);
  1189 
  1190 (*special code to enforce left-to-right collection of TVar-indexnames*)
  1191 
  1192 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
  1193   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
  1194                                      else ixns@[ixn]
  1195   | add_typ_ixns(ixns,TFree(_)) = ixns;
  1196 
  1197 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1198   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1199   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1200   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1201   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1202       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1203   | add_term_tvar_ixns(f$t,ixns) =
  1204       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1205 
  1206 
  1207 (** Frees and Vars **)
  1208 
  1209 (*Accumulates the Vars in the term, suppressing duplicates*)
  1210 fun add_term_vars (t, vars: term list) = case t of
  1211     Var   _ => OrdList.insert term_ord t vars
  1212   | Abs (_,_,body) => add_term_vars(body,vars)
  1213   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1214   | _ => vars;
  1215 
  1216 fun term_vars t = add_term_vars(t,[]);
  1217 
  1218 (*Accumulates the Frees in the term, suppressing duplicates*)
  1219 fun add_term_frees (t, frees: term list) = case t of
  1220     Free   _ => OrdList.insert term_ord t frees
  1221   | Abs (_,_,body) => add_term_frees(body,frees)
  1222   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1223   | _ => frees;
  1224 
  1225 fun term_frees t = add_term_frees(t,[]);
  1226 
  1227 (*Given an abstraction over P, replaces the bound variable by a Free variable
  1228   having a unique name -- SLOW!*)
  1229 fun variant_abs (a,T,P) =
  1230   let val b = variant (add_term_names(P,[])) a
  1231   in  (b,  subst_bound (Free(b,T), P))  end;
  1232 
  1233 fun dest_abs (x, T, body) =
  1234   let
  1235     fun name_clash (Free (y, _)) = (x = y)
  1236       | name_clash (t $ u) = name_clash t orelse name_clash u
  1237       | name_clash (Abs (_, _, t)) = name_clash t
  1238       | name_clash _ = false;
  1239   in
  1240     if name_clash body then
  1241       dest_abs (variant [x] x, T, body)    (*potentially slow, but rarely happens*)
  1242     else (x, subst_bound (Free (x, T), body))
  1243   end;
  1244 
  1245 (*names for numbered variables --
  1246   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
  1247 local
  1248   val small_int = Vector.tabulate (1000, fn i =>
  1249     let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
  1250     in ":" ^ leading ^ string_of_int i end);
  1251 in
  1252   fun bound n =
  1253     if n < 1000 then Vector.sub (small_int, n)
  1254     else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
  1255 end;
  1256 
  1257 val is_bound = String.isPrefix ":";
  1258 
  1259 (* renames and reverses the strings in vars away from names *)
  1260 fun rename_aTs names vars : (string*typ)list =
  1261   let fun rename_aT (vars,(a,T)) =
  1262                 (variant (map #1 vars @ names) a, T) :: vars
  1263   in Library.foldl rename_aT ([],vars) end;
  1264 
  1265 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
  1266 
  1267 
  1268 (* zero var indexes *)
  1269 
  1270 fun zero_var_inst vars =
  1271   fold (fn v as ((x, i), X) => fn (used, inst) =>
  1272     let
  1273       val x' = variant used (if is_bound x then "u" else x);
  1274       val used' = x' :: used;
  1275     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
  1276   vars ([], []) |> #2;
  1277 
  1278 fun zero_var_indexesT ty =
  1279   instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
  1280 
  1281 fun zero_var_indexes_inst tm =
  1282   let
  1283     val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
  1284     val inst =
  1285       add_vars tm [] |> map (apsnd (instantiateT instT))
  1286       |> sort var_ord |> zero_var_inst |> map (apsnd Var);
  1287   in (instT, inst) end;
  1288 
  1289 fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
  1290 
  1291 
  1292 (* dummy patterns *)
  1293 
  1294 val dummy_patternN = "dummy_pattern";
  1295 
  1296 fun dummy_pattern T = Const (dummy_patternN, T);
  1297 
  1298 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1299   | is_dummy_pattern _ = false;
  1300 
  1301 fun no_dummy_patterns tm =
  1302   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  1303   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1304 
  1305 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1306       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1307   | replace_dummy Ts (i, Abs (x, T, t)) =
  1308       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1309       in (i', Abs (x, T, t')) end
  1310   | replace_dummy Ts (i, t $ u) =
  1311       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1312       in (i'', t' $ u') end
  1313   | replace_dummy _ (i, a) = (i, a);
  1314 
  1315 val replace_dummy_patterns = replace_dummy [];
  1316 
  1317 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1318   | is_replaced_dummy_pattern _ = false;
  1319 
  1320 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1321   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1322   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1323   | show_dummy_patterns a = a;
  1324 
  1325 
  1326 (* adhoc freezing *)
  1327 
  1328 fun adhoc_freeze_vars tm =
  1329   let
  1330     fun mk_inst (var as Var ((a, i), T)) =
  1331       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1332       in ((var,  Free(x, T)), x) end;
  1333     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1334   in (subst_atomic insts tm, xs) end;
  1335 
  1336 
  1337 (* string_of_vname *)
  1338 
  1339 val show_question_marks = ref true;
  1340 
  1341 fun string_of_vname (x, i) =
  1342   let
  1343     val question_mark = if ! show_question_marks then "?" else "";
  1344     val idx = string_of_int i;
  1345     val dot =
  1346       (case rev (Symbol.explode x) of
  1347         _ :: "\\<^isub>" :: _ => false
  1348       | _ :: "\\<^isup>" :: _ => false
  1349       | c :: _ => Symbol.is_digit c
  1350       | _ => true);
  1351   in
  1352     if dot then question_mark ^ x ^ "." ^ idx
  1353     else if i <> 0 then question_mark ^ x ^ idx
  1354     else question_mark ^ x
  1355   end;
  1356 
  1357 fun string_of_vname' (x, ~1) = x
  1358   | string_of_vname' xi = string_of_vname xi;
  1359 
  1360 
  1361 (* str_of_term *)
  1362 
  1363 fun str_of_term (Const (c, _)) = c
  1364   | str_of_term (Free (x, _)) = x
  1365   | str_of_term (Var (xi, _)) = string_of_vname xi
  1366   | str_of_term (Bound i) = string_of_int i
  1367   | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
  1368   | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
  1369 
  1370 end;
  1371 
  1372 structure BasicTerm: BASIC_TERM = Term;
  1373 open BasicTerm;