src/Pure/term.ML
author haftmann
Fri Feb 19 11:06:22 2010 +0100 (2010-02-19)
changeset 35227 d67857e3a8c0
parent 34922 e35f608f81a2
child 35986 b7fcca3d9a44
permissions -rw-r--r--
added dest_comb
     1 (*  Title:      Pure/term.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Simply typed lambda-calculus: types, terms, and basic operations.
     6 *)
     7 
     8 infix 9 $;
     9 infixr 5 -->;
    10 infixr --->;
    11 infix aconv;
    12 
    13 signature BASIC_TERM =
    14 sig
    15   type indexname = string * int
    16   type class = string
    17   type sort = class list
    18   type arity = string * sort list * sort
    19   datatype typ =
    20     Type  of string * typ list |
    21     TFree of string * sort |
    22     TVar  of indexname * sort
    23   datatype term =
    24     Const of string * typ |
    25     Free of string * typ |
    26     Var of indexname * typ |
    27     Bound of int |
    28     Abs of string * typ * term |
    29     $ of term * term
    30   exception TYPE of string * typ list * term list
    31   exception TERM of string * term list
    32   val dummyS: sort
    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 dest_Const: term -> string * typ
    46   val dest_Free: term -> string * typ
    47   val dest_Var: term -> indexname * typ
    48   val dest_comb: term -> term * term
    49   val domain_type: typ -> typ
    50   val range_type: typ -> typ
    51   val binder_types: typ -> typ list
    52   val body_type: typ -> typ
    53   val strip_type: typ -> typ list * typ
    54   val type_of1: typ list * term -> typ
    55   val type_of: term -> typ
    56   val fastype_of1: typ list * term -> typ
    57   val fastype_of: term -> typ
    58   val list_abs: (string * typ) list * term -> term
    59   val strip_abs: term -> (string * typ) list * term
    60   val strip_abs_body: term -> term
    61   val strip_abs_vars: term -> (string * typ) list
    62   val strip_qnt_body: string -> term -> term
    63   val strip_qnt_vars: string -> term -> (string * typ) list
    64   val list_comb: term * term list -> term
    65   val strip_comb: term -> term * term list
    66   val head_of: term -> term
    67   val size_of_term: term -> int
    68   val size_of_typ: typ -> int
    69   val map_atyps: (typ -> typ) -> typ -> typ
    70   val map_aterms: (term -> term) -> term -> term
    71   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    72   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    73   val map_types: (typ -> typ) -> term -> term
    74   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    75   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    76   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    77   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    78   val burrow_types: (typ list -> typ list) -> term list -> term list
    79   val aconv: term * term -> bool
    80   val propT: typ
    81   val strip_all_body: term -> term
    82   val strip_all_vars: term -> (string * typ) list
    83   val incr_bv: int * int * term -> term
    84   val incr_boundvars: int -> term -> term
    85   val add_loose_bnos: term * int * int list -> int list
    86   val loose_bnos: term -> int list
    87   val loose_bvar: term * int -> bool
    88   val loose_bvar1: term * int -> bool
    89   val subst_bounds: term list * term -> term
    90   val subst_bound: term * term -> term
    91   val betapply: term * term -> term
    92   val betapplys: term * term list -> term
    93   val subst_free: (term * term) list -> term -> term
    94   val abstract_over: term * term -> term
    95   val lambda: term -> term -> term
    96   val absfree: string * typ * term -> term
    97   val absdummy: typ * term -> term
    98   val list_abs_free: (string * typ) list * term -> term
    99   val list_all_free: (string * typ) list * term -> term
   100   val list_all: (string * typ) list * term -> term
   101   val subst_atomic: (term * term) list -> term -> term
   102   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   103   val subst_atomic_types: (typ * typ) list -> term -> term
   104   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   105   val subst_TVars: (indexname * typ) list -> term -> term
   106   val subst_Vars: (indexname * term) list -> term -> term
   107   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   108   val is_first_order: string list -> term -> bool
   109   val maxidx_of_typ: typ -> int
   110   val maxidx_of_typs: typ list -> int
   111   val maxidx_of_term: term -> int
   112   val exists_subtype: (typ -> bool) -> typ -> bool
   113   val exists_type: (typ -> bool) -> term -> bool
   114   val exists_subterm: (term -> bool) -> term -> bool
   115   val exists_Const: (string * typ -> bool) -> term -> bool
   116   val show_question_marks: bool Unsynchronized.ref
   117 end;
   118 
   119 signature TERM =
   120 sig
   121   include BASIC_TERM
   122   val aT: sort -> typ
   123   val itselfT: typ -> typ
   124   val a_itselfT: typ
   125   val all: typ -> term
   126   val argument_type_of: term -> int -> typ
   127   val add_tvar_namesT: typ -> indexname list -> indexname list
   128   val add_tvar_names: term -> indexname list -> indexname list
   129   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   130   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   131   val add_var_names: term -> indexname list -> indexname list
   132   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   133   val add_tfree_namesT: typ -> string list -> string list
   134   val add_tfree_names: term -> string list -> string list
   135   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   136   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   137   val add_free_names: term -> string list -> string list
   138   val add_frees: term -> (string * typ) list -> (string * typ) list
   139   val add_const_names: term -> string list -> string list
   140   val add_consts: term -> (string * typ) list -> (string * typ) list
   141   val hidden_polymorphism: term -> (indexname * sort) list
   142   val declare_typ_names: typ -> Name.context -> Name.context
   143   val declare_term_names: term -> Name.context -> Name.context
   144   val declare_term_frees: term -> Name.context -> Name.context
   145   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   146   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   147   val eq_ix: indexname * indexname -> bool
   148   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   149   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   150   val aconv_untyped: term * term -> bool
   151   val could_unify: term * term -> bool
   152   val strip_abs_eta: int -> term -> (string * typ) list * term
   153   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   154   val map_abs_vars: (string -> string) -> term -> term
   155   val rename_abs: term -> term -> term -> term option
   156   val lambda_name: string * term -> term -> term
   157   val close_schematic_term: term -> term
   158   val maxidx_typ: typ -> int -> int
   159   val maxidx_typs: typ list -> int -> int
   160   val maxidx_term: term -> int -> int
   161   val has_abs: term -> bool
   162   val dest_abs: string * typ * term -> string * term
   163   val dummy_patternN: string
   164   val dummy_pattern: typ -> term
   165   val is_dummy_pattern: term -> bool
   166   val free_dummy_patterns: term -> Name.context -> term * Name.context
   167   val no_dummy_patterns: term -> term
   168   val replace_dummy_patterns: term -> int -> term * int
   169   val is_replaced_dummy_pattern: indexname -> bool
   170   val show_dummy_patterns: term -> term
   171   val string_of_vname: indexname -> string
   172   val string_of_vname': indexname -> string
   173 end;
   174 
   175 structure Term: TERM =
   176 struct
   177 
   178 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   179   for resolution.*)
   180 type indexname = string * int;
   181 
   182 (* Types are classified by sorts. *)
   183 type class = string;
   184 type sort  = class list;
   185 type arity = string * sort list * sort;
   186 
   187 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   188 datatype typ = Type  of string * typ list
   189              | TFree of string * sort
   190              | TVar  of indexname * sort;
   191 
   192 (*Terms.  Bound variables are indicated by depth number.
   193   Free variables, (scheme) variables and constants have names.
   194   An term is "closed" if every bound variable of level "lev"
   195   is enclosed by at least "lev" abstractions.
   196 
   197   It is possible to create meaningless terms containing loose bound vars
   198   or type mismatches.  But such terms are not allowed in rules. *)
   199 
   200 datatype term =
   201     Const of string * typ
   202   | Free  of string * typ
   203   | Var   of indexname * typ
   204   | Bound of int
   205   | Abs   of string*typ*term
   206   | op $  of term*term;
   207 
   208 (*Errors involving type mismatches*)
   209 exception TYPE of string * typ list * term list;
   210 
   211 (*Errors errors involving terms*)
   212 exception TERM of string * term list;
   213 
   214 (*Note variable naming conventions!
   215     a,b,c: string
   216     f,g,h: functions (including terms of function type)
   217     i,j,m,n: int
   218     t,u: term
   219     v,w: indexnames
   220     x,y: any
   221     A,B,C: term (denoting formulae)
   222     T,U: typ
   223 *)
   224 
   225 
   226 (** Types **)
   227 
   228 (*dummies for type-inference etc.*)
   229 val dummyS = [""];
   230 val dummyT = Type ("dummy", []);
   231 
   232 fun no_dummyT typ =
   233   let
   234     fun check (T as Type ("dummy", _)) =
   235           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   236       | check (Type (_, Ts)) = List.app check Ts
   237       | check _ = ();
   238   in check typ; typ end;
   239 
   240 fun S --> T = Type("fun",[S,T]);
   241 
   242 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   243 val op ---> = Library.foldr (op -->);
   244 
   245 fun dest_Type (Type x) = x
   246   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   247 fun dest_TVar (TVar x) = x
   248   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   249 fun dest_TFree (TFree x) = x
   250   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   251 
   252 
   253 (** Discriminators **)
   254 
   255 fun is_Bound (Bound _) = true
   256   | is_Bound _         = false;
   257 
   258 fun is_Const (Const _) = true
   259   | is_Const _ = false;
   260 
   261 fun is_Free (Free _) = true
   262   | is_Free _ = false;
   263 
   264 fun is_Var (Var _) = true
   265   | is_Var _ = false;
   266 
   267 fun is_TVar (TVar _) = true
   268   | is_TVar _ = false;
   269 
   270 
   271 (** Destructors **)
   272 
   273 fun dest_Const (Const x) =  x
   274   | dest_Const t = raise TERM("dest_Const", [t]);
   275 
   276 fun dest_Free (Free x) =  x
   277   | dest_Free t = raise TERM("dest_Free", [t]);
   278 
   279 fun dest_Var (Var x) =  x
   280   | dest_Var t = raise TERM("dest_Var", [t]);
   281 
   282 fun dest_comb (t1 $ t2) = (t1, t2)
   283   | dest_comb t = raise TERM("dest_comb", [t]);
   284 
   285 
   286 fun domain_type (Type("fun", [T,_])) = T
   287 and range_type  (Type("fun", [_,T])) = T;
   288 
   289 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   290 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   291   | binder_types _   =  [];
   292 
   293 (* maps  [T1,...,Tn]--->T  to T*)
   294 fun body_type (Type("fun",[S,T])) = body_type T
   295   | body_type T   =  T;
   296 
   297 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   298 fun strip_type T : typ list * typ =
   299   (binder_types T, body_type T);
   300 
   301 
   302 (*Compute the type of the term, checking that combinations are well-typed
   303   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   304 fun type_of1 (Ts, Const (_,T)) = T
   305   | type_of1 (Ts, Free  (_,T)) = T
   306   | type_of1 (Ts, Bound i) = (nth Ts i
   307         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   308   | type_of1 (Ts, Var (_,T)) = T
   309   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   310   | type_of1 (Ts, f$u) =
   311       let val U = type_of1(Ts,u)
   312           and T = type_of1(Ts,f)
   313       in case T of
   314             Type("fun",[T1,T2]) =>
   315               if T1=U then T2  else raise TYPE
   316                     ("type_of: type mismatch in application", [T1,U], [f$u])
   317           | _ => raise TYPE
   318                     ("type_of: function type is expected in application",
   319                      [T,U], [f$u])
   320       end;
   321 
   322 fun type_of t : typ = type_of1 ([],t);
   323 
   324 (*Determines the type of a term, with minimal checking*)
   325 fun fastype_of1 (Ts, f$u) =
   326     (case fastype_of1 (Ts,f) of
   327         Type("fun",[_,T]) => T
   328         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   329   | fastype_of1 (_, Const (_,T)) = T
   330   | fastype_of1 (_, Free (_,T)) = T
   331   | fastype_of1 (Ts, Bound i) = (nth Ts i
   332          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   333   | fastype_of1 (_, Var (_,T)) = T
   334   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   335 
   336 fun fastype_of t : typ = fastype_of1 ([],t);
   337 
   338 (*Determine the argument type of a function*)
   339 fun argument_type_of tm k =
   340   let
   341     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   342       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   343 
   344     fun arg 0 _ (Abs (_, T, _)) = T
   345       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   346       | arg i Ts (t $ _) = arg (i + 1) Ts t
   347       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   348   in arg k [] tm end;
   349 
   350 
   351 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
   352 
   353 fun strip_abs (Abs (a, T, t)) =
   354       let val (a', t') = strip_abs t
   355       in ((a, T) :: a', t') end
   356   | strip_abs t = ([], t);
   357 
   358 (* maps  (x1,...,xn)t   to   t  *)
   359 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   360   | strip_abs_body u  =  u;
   361 
   362 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   363 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   364   | strip_abs_vars u  =  [] : (string*typ) list;
   365 
   366 
   367 fun strip_qnt_body qnt =
   368 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   369       | strip t = t
   370 in strip end;
   371 
   372 fun strip_qnt_vars qnt =
   373 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   374       | strip t  =  [] : (string*typ) list
   375 in strip end;
   376 
   377 
   378 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   379 val list_comb : term * term list -> term = Library.foldl (op $);
   380 
   381 
   382 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   383 fun strip_comb u : term * term list =
   384     let fun stripc (f$t, ts) = stripc (f, t::ts)
   385         |   stripc  x =  x
   386     in  stripc(u,[])  end;
   387 
   388 
   389 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   390 fun head_of (f$t) = head_of f
   391   | head_of u = u;
   392 
   393 (*number of atoms and abstractions in a term*)
   394 fun size_of_term tm =
   395   let
   396     fun add_size (t $ u) n = add_size t (add_size u n)
   397       | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
   398       | add_size _ n = n + 1;
   399   in add_size tm 0 end;
   400 
   401 (*number of atoms and constructors in a type*)
   402 fun size_of_typ ty =
   403   let
   404     fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
   405       | add_size _ n = n + 1;
   406   in add_size ty 0 end;
   407 
   408 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   409   | map_atyps f T = f T;
   410 
   411 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   412   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   413   | map_aterms f t = f t;
   414 
   415 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   416 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   417 
   418 fun map_types f =
   419   let
   420     fun map_aux (Const (a, T)) = Const (a, f T)
   421       | map_aux (Free (a, T)) = Free (a, f T)
   422       | map_aux (Var (v, T)) = Var (v, f T)
   423       | map_aux (t as Bound _)  = t
   424       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   425       | map_aux (t $ u) = map_aux t $ map_aux u;
   426   in map_aux end;
   427 
   428 
   429 (* fold types and terms *)
   430 
   431 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   432   | fold_atyps f T = f T;
   433 
   434 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   435   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   436   | fold_aterms f a = f a;
   437 
   438 fun fold_term_types f (t as Const (_, T)) = f t T
   439   | fold_term_types f (t as Free (_, T)) = f t T
   440   | fold_term_types f (t as Var (_, T)) = f t T
   441   | fold_term_types f (Bound _) = I
   442   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   443   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   444 
   445 fun fold_types f = fold_term_types (K f);
   446 
   447 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
   448   | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
   449   | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
   450   | replace_types (Bound i) Ts = (Bound i, Ts)
   451   | replace_types (Abs (x, _, b)) (T :: Ts) =
   452       let val (b', Ts') = replace_types b Ts
   453       in (Abs (x, T, b'), Ts') end
   454   | replace_types (t $ u) Ts =
   455       let
   456         val (t', Ts') = replace_types t Ts;
   457         val (u', Ts'') = replace_types u Ts';
   458       in (t' $ u', Ts'') end;
   459 
   460 fun burrow_types f ts =
   461   let
   462     val Ts = rev (fold (fold_types cons) ts []);
   463     val Ts' = f Ts;
   464     val (ts', []) = fold_map replace_types ts Ts';
   465   in ts' end;
   466 
   467 (*collect variables*)
   468 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
   469 val add_tvar_names = fold_types add_tvar_namesT;
   470 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   471 val add_tvars = fold_types add_tvarsT;
   472 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   473 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   474 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
   475 val add_tfree_names = fold_types add_tfree_namesT;
   476 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   477 val add_tfrees = fold_types add_tfreesT;
   478 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
   479 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   480 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
   481 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
   482 
   483 (*extra type variables in a term, not covered by its type*)
   484 fun hidden_polymorphism t =
   485   let
   486     val T = fastype_of t;
   487     val tvarsT = add_tvarsT T [];
   488     val extra_tvars = fold_types (fold_atyps
   489       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   490   in extra_tvars end;
   491 
   492 
   493 (* renaming variables *)
   494 
   495 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   496 
   497 fun declare_term_names tm =
   498   fold_aterms
   499     (fn Const (a, _) => Name.declare (Long_Name.base_name a)
   500       | Free (a, _) => Name.declare a
   501       | _ => I) tm #>
   502   fold_types declare_typ_names tm;
   503 
   504 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
   505 
   506 fun variant_frees t frees =
   507   fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
   508 
   509 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   510 
   511 
   512 
   513 (** Comparing terms **)
   514 
   515 (* variables *)
   516 
   517 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   518 
   519 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   520 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   521 
   522 
   523 (* alpha equivalence *)
   524 
   525 fun tm1 aconv tm2 =
   526   pointer_eq (tm1, tm2) orelse
   527     (case (tm1, tm2) of
   528       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
   529     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
   530     | (a1, a2) => a1 = a2);
   531 
   532 fun aconv_untyped (tm1, tm2) =
   533   pointer_eq (tm1, tm2) orelse
   534     (case (tm1, tm2) of
   535       (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
   536     | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
   537     | (Const (a, _), Const (b, _)) => a = b
   538     | (Free (x, _), Free (y, _)) => x = y
   539     | (Var (xi, _), Var (yj, _)) => xi = yj
   540     | (Bound i, Bound j) => i = j
   541     | _ => false);
   542 
   543 
   544 (*A fast unification filter: true unless the two terms cannot be unified.
   545   Terms must be NORMAL.  Treats all Vars as distinct. *)
   546 fun could_unify (t, u) =
   547   let
   548     fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
   549       | matchrands _ _ = true;
   550   in
   551     case (head_of t, head_of u) of
   552       (_, Var _) => true
   553     | (Var _, _) => true
   554     | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
   555     | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
   556     | (Bound i, Bound j) => i = j andalso matchrands t u
   557     | (Abs _, _) => true   (*because of possible eta equality*)
   558     | (_, Abs _) => true
   559     | _ => false
   560   end;
   561 
   562 
   563 
   564 (** Connectives of higher order logic **)
   565 
   566 fun aT S = TFree (Name.aT, S);
   567 
   568 fun itselfT ty = Type ("itself", [ty]);
   569 val a_itselfT = itselfT (TFree (Name.aT, []));
   570 
   571 val propT : typ = Type("prop",[]);
   572 
   573 fun all T = Const("all", (T-->propT)-->propT);
   574 
   575 (* maps  !!x1...xn. t   to   t  *)
   576 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   577   | strip_all_body t  =  t;
   578 
   579 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   580 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   581                 (a,T) :: strip_all_vars t
   582   | strip_all_vars t  =  [] : (string*typ) list;
   583 
   584 (*increments a term's non-local bound variables
   585   required when moving a term within abstractions
   586      inc is  increment for bound variables
   587      lev is  level at which a bound variable is considered 'loose'*)
   588 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   589   | incr_bv (inc, lev, Abs(a,T,body)) =
   590         Abs(a, T, incr_bv(inc,lev+1,body))
   591   | incr_bv (inc, lev, f$t) =
   592       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   593   | incr_bv (inc, lev, u) = u;
   594 
   595 fun incr_boundvars  0  t = t
   596   | incr_boundvars inc t = incr_bv(inc,0,t);
   597 
   598 (*Scan a pair of terms; while they are similar,
   599   accumulate corresponding bound vars in "al"*)
   600 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   601       match_bvs(s, t, if x="" orelse y="" then al
   602                                           else (x,y)::al)
   603   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   604   | match_bvs(_,_,al) = al;
   605 
   606 (* strip abstractions created by parameters *)
   607 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   608 
   609 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   610   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   611   | map_abs_vars f t = t;
   612 
   613 fun rename_abs pat obj t =
   614   let
   615     val ren = match_bvs (pat, obj, []);
   616     fun ren_abs (Abs (x, T, b)) =
   617           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   618       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   619       | ren_abs t = t
   620   in if null ren then NONE else SOME (ren_abs t) end;
   621 
   622 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   623    (Bound 0) is loose at level 0 *)
   624 fun add_loose_bnos (Bound i, lev, js) =
   625         if i<lev then js else insert (op =) (i - lev) js
   626   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   627   | add_loose_bnos (f$t, lev, js) =
   628         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   629   | add_loose_bnos (_, _, js) = js;
   630 
   631 fun loose_bnos t = add_loose_bnos (t, 0, []);
   632 
   633 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   634    level k or beyond. *)
   635 fun loose_bvar(Bound i,k) = i >= k
   636   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   637   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   638   | loose_bvar _ = false;
   639 
   640 fun loose_bvar1(Bound i,k) = i = k
   641   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   642   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   643   | loose_bvar1 _ = false;
   644 
   645 (*Substitute arguments for loose bound variables.
   646   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   647   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   648         and the appropriate call is  subst_bounds([b,a], c) .
   649   Loose bound variables >=n are reduced by "n" to
   650      compensate for the disappearance of lambdas.
   651 *)
   652 fun subst_bounds (args: term list, t) : term =
   653   let
   654     val n = length args;
   655     fun subst (t as Bound i, lev) =
   656          (if i < lev then raise Same.SAME   (*var is locally bound*)
   657           else incr_boundvars lev (nth args (i - lev))
   658             handle Subscript => Bound (i - n))  (*loose: change it*)
   659       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   660       | subst (f $ t, lev) =
   661           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   662             handle Same.SAME => f $ subst (t, lev))
   663       | subst _ = raise Same.SAME;
   664   in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
   665 
   666 (*Special case: one argument*)
   667 fun subst_bound (arg, t) : term =
   668   let
   669     fun subst (Bound i, lev) =
   670           if i < lev then raise Same.SAME   (*var is locally bound*)
   671           else if i = lev then incr_boundvars lev arg
   672           else Bound (i - 1)   (*loose: change it*)
   673       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   674       | subst (f $ t, lev) =
   675           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   676             handle Same.SAME => f $ subst (t, lev))
   677       | subst _ = raise Same.SAME;
   678   in subst (t, 0) handle Same.SAME => t end;
   679 
   680 (*beta-reduce if possible, else form application*)
   681 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   682   | betapply (f,u) = f$u;
   683 
   684 val betapplys = Library.foldl betapply;
   685 
   686 
   687 (*unfolding abstractions with substitution
   688   of bound variables and implicit eta-expansion*)
   689 fun strip_abs_eta k t =
   690   let
   691     val used = fold_aterms declare_term_frees t Name.context;
   692     fun strip_abs t (0, used) = (([], t), (0, used))
   693       | strip_abs (Abs (v, T, t)) (k, used) =
   694           let
   695             val ([v'], used') = Name.variants [v] used;
   696             val t' = subst_bound (Free (v', T), t);
   697             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   698           in (((v', T) :: vs, t''), (k', used'')) end
   699       | strip_abs t (k, used) = (([], t), (k, used));
   700     fun expand_eta [] t _ = ([], t)
   701       | expand_eta (T::Ts) t used =
   702           let
   703             val ([v], used') = Name.variants [""] used;
   704             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   705           in ((v, T) :: vs, t') end;
   706     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   707     val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
   708     val (vs2, t'') = expand_eta Ts t' used';
   709   in (vs1 @ vs2, t'') end;
   710 
   711 
   712 (*Substitute new for free occurrences of old in a term*)
   713 fun subst_free [] = I
   714   | subst_free pairs =
   715       let fun substf u =
   716             case AList.lookup (op aconv) pairs u of
   717                 SOME u' => u'
   718               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   719                                  | t$u' => substf t $ substf u'
   720                                  | _ => u)
   721       in  substf  end;
   722 
   723 (*Abstraction of the term "body" over its occurrences of v,
   724     which must contain no loose bound variables.
   725   The resulting term is ready to become the body of an Abs.*)
   726 fun abstract_over (v, body) =
   727   let
   728     fun abs lev tm =
   729       if v aconv tm then Bound lev
   730       else
   731         (case tm of
   732           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   733         | t $ u =>
   734             (abs lev t $ (abs lev u handle Same.SAME => u)
   735               handle Same.SAME => t $ abs lev u)
   736         | _ => raise Same.SAME);
   737   in abs 0 body handle Same.SAME => body end;
   738 
   739 fun term_name (Const (x, _)) = Long_Name.base_name x
   740   | term_name (Free (x, _)) = x
   741   | term_name (Var ((x, _), _)) = x
   742   | term_name _ = Name.uu;
   743 
   744 fun lambda_name (x, v) t =
   745   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
   746 
   747 fun lambda v t = lambda_name ("", v) t;
   748 
   749 (*Form an abstraction over a free variable.*)
   750 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
   751 fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
   752 
   753 (*Abstraction over a list of free variables*)
   754 fun list_abs_free ([ ] ,     t) = t
   755   | list_abs_free ((a,T)::vars, t) =
   756       absfree(a, T, list_abs_free(vars,t));
   757 
   758 (*Quantification over a list of free variables*)
   759 fun list_all_free ([], t: term) = t
   760   | list_all_free ((a,T)::vars, t) =
   761         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   762 
   763 (*Quantification over a list of variables (already bound in body) *)
   764 fun list_all ([], t) = t
   765   | list_all ((a,T)::vars, t) =
   766         (all T) $ (Abs(a, T, list_all(vars,t)));
   767 
   768 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   769   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   770 fun subst_atomic [] tm = tm
   771   | subst_atomic inst tm =
   772       let
   773         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   774           | subst (t $ u) = subst t $ subst u
   775           | subst t = the_default t (AList.lookup (op aconv) inst t);
   776       in subst tm end;
   777 
   778 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   779 fun typ_subst_atomic [] ty = ty
   780   | typ_subst_atomic inst ty =
   781       let
   782         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   783           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   784       in subst ty end;
   785 
   786 fun subst_atomic_types [] tm = tm
   787   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   788 
   789 fun typ_subst_TVars [] ty = ty
   790   | typ_subst_TVars inst ty =
   791       let
   792         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   793           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   794           | subst T = T;
   795       in subst ty end;
   796 
   797 fun subst_TVars [] tm = tm
   798   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   799 
   800 fun subst_Vars [] tm = tm
   801   | subst_Vars inst tm =
   802       let
   803         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   804           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   805           | subst (t $ u) = subst t $ subst u
   806           | subst t = t;
   807       in subst tm end;
   808 
   809 fun subst_vars ([], []) tm = tm
   810   | subst_vars ([], inst) tm = subst_Vars inst tm
   811   | subst_vars (instT, inst) tm =
   812       let
   813         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   814           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   815           | subst (Var (xi, T)) =
   816               (case AList.lookup (op =) inst xi of
   817                 NONE => Var (xi, typ_subst_TVars instT T)
   818               | SOME t => t)
   819           | subst (t as Bound _) = t
   820           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   821           | subst (t $ u) = subst t $ subst u;
   822       in subst tm end;
   823 
   824 fun close_schematic_term t =
   825   let
   826     val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
   827     val extra_terms = map Var (add_vars t []);
   828   in fold lambda (extra_terms @ extra_types) t end;
   829 
   830 
   831 
   832 (** Identifying first-order terms **)
   833 
   834 (*Differs from proofterm/is_fun in its treatment of TVar*)
   835 fun is_funtype (Type ("fun", [_, _])) = true
   836   | is_funtype _ = false;
   837 
   838 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   839 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
   840 
   841 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   842   function type. The supplied quantifiers are excluded: their argument always
   843   has a function type through a recursive call into its body.*)
   844 fun is_first_order quants =
   845   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   846         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   847             member (op =) quants q  andalso   (*it is a known quantifier*)
   848             not (is_funtype T)   andalso first_order1 (T::Ts) body
   849         | first_order1 Ts t =
   850             case strip_comb t of
   851                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   852                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   853                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   854                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   855                | (Abs _, ts) => false (*not in beta-normal form*)
   856                | _ => error "first_order: unexpected case"
   857     in  first_order1 []  end;
   858 
   859 
   860 (* maximum index of typs and terms *)
   861 
   862 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   863   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   864   | maxidx_typ (TFree _) i = i
   865 and maxidx_typs [] i = i
   866   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
   867 
   868 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   869   | maxidx_term (Const (_, T)) i = maxidx_typ T i
   870   | maxidx_term (Free (_, T)) i = maxidx_typ T i
   871   | maxidx_term (Bound _) i = i
   872   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   873   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
   874 
   875 fun maxidx_of_typ T = maxidx_typ T ~1;
   876 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
   877 fun maxidx_of_term t = maxidx_term t ~1;
   878 
   879 
   880 
   881 (** misc syntax operations **)
   882 
   883 (* substructure *)
   884 
   885 fun exists_subtype P =
   886   let
   887     fun ex ty = P ty orelse
   888       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   889   in ex end;
   890 
   891 fun exists_type P =
   892   let
   893     fun ex (Const (_, T)) = P T
   894       | ex (Free (_, T)) = P T
   895       | ex (Var (_, T)) = P T
   896       | ex (Bound _) = false
   897       | ex (Abs (_, T, t)) = P T orelse ex t
   898       | ex (t $ u) = ex t orelse ex u;
   899   in ex end;
   900 
   901 fun exists_subterm P =
   902   let
   903     fun ex tm = P tm orelse
   904       (case tm of
   905         t $ u => ex t orelse ex u
   906       | Abs (_, _, t) => ex t
   907       | _ => false);
   908   in ex end;
   909 
   910 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   911 
   912 fun has_abs (Abs _) = true
   913   | has_abs (t $ u) = has_abs t orelse has_abs u
   914   | has_abs _ = false;
   915 
   916 
   917 (* dest abstraction *)
   918 
   919 fun dest_abs (x, T, body) =
   920   let
   921     fun name_clash (Free (y, _)) = (x = y)
   922       | name_clash (t $ u) = name_clash t orelse name_clash u
   923       | name_clash (Abs (_, _, t)) = name_clash t
   924       | name_clash _ = false;
   925   in
   926     if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
   927     else (x, subst_bound (Free (x, T), body))
   928   end;
   929 
   930 
   931 (* dummy patterns *)
   932 
   933 val dummy_patternN = "dummy_pattern";
   934 
   935 fun dummy_pattern T = Const (dummy_patternN, T);
   936 
   937 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
   938   | is_dummy_pattern _ = false;
   939 
   940 fun no_dummy_patterns tm =
   941   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   942   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   943 
   944 fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
   945       let val [x] = Name.invents used Name.uu 1
   946       in (Free (Name.internal x, T), Name.declare x used) end
   947   | free_dummy_patterns (Abs (x, T, b)) used =
   948       let val (b', used') = free_dummy_patterns b used
   949       in (Abs (x, T, b'), used') end
   950   | free_dummy_patterns (t $ u) used =
   951       let
   952         val (t', used') = free_dummy_patterns t used;
   953         val (u', used'') = free_dummy_patterns u used';
   954       in (t' $ u', used'') end
   955   | free_dummy_patterns a used = (a, used);
   956 
   957 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
   958       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   959   | replace_dummy Ts (Abs (x, T, t)) i =
   960       let val (t', i') = replace_dummy (T :: Ts) t i
   961       in (Abs (x, T, t'), i') end
   962   | replace_dummy Ts (t $ u) i =
   963       let
   964         val (t', i') = replace_dummy Ts t i;
   965         val (u', i'') = replace_dummy Ts u i';
   966       in (t' $ u', i'') end
   967   | replace_dummy _ a i = (a, i);
   968 
   969 val replace_dummy_patterns = replace_dummy [];
   970 
   971 fun is_replaced_dummy_pattern ("_dummy_", _) = true
   972   | is_replaced_dummy_pattern _ = false;
   973 
   974 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
   975   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   976   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   977   | show_dummy_patterns a = a;
   978 
   979 
   980 (* display variables *)
   981 
   982 val show_question_marks = Unsynchronized.ref true;
   983 
   984 fun string_of_vname (x, i) =
   985   let
   986     val question_mark = if ! show_question_marks then "?" else "";
   987     val idx = string_of_int i;
   988     val dot =
   989       (case rev (Symbol.explode x) of
   990         _ :: "\\<^isub>" :: _ => false
   991       | _ :: "\\<^isup>" :: _ => false
   992       | c :: _ => Symbol.is_digit c
   993       | _ => true);
   994   in
   995     if dot then question_mark ^ x ^ "." ^ idx
   996     else if i <> 0 then question_mark ^ x ^ idx
   997     else question_mark ^ x
   998   end;
   999 
  1000 fun string_of_vname' (x, ~1) = x
  1001   | string_of_vname' xi = string_of_vname xi;
  1002 
  1003 end;
  1004 
  1005 structure BasicTerm: BASIC_TERM = Term;
  1006 open BasicTerm;