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