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