src/Pure/term.ML
changeset 20109 47fef41c68fb
parent 20100 c96cb48eef53
child 20116 f2aecd6e58ec
     1.1 --- a/src/Pure/term.ML	Wed Jul 12 17:00:32 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 12 17:00:33 2006 +0200
     1.3 @@ -163,6 +163,7 @@
     1.4    val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
     1.5    val add_tfrees: term -> (string * sort) list -> (string * sort) list
     1.6    val add_frees: term -> (string * typ) list -> (string * typ) list
     1.7 +  val strip_abs_eta: int -> term -> (string * typ) list * term
     1.8    val fast_indexname_ord: indexname * indexname -> order
     1.9    val indexname_ord: indexname * indexname -> order
    1.10    val sort_ord: sort * sort -> order
    1.11 @@ -812,6 +813,31 @@
    1.12  val betapplys = Library.foldl betapply;
    1.13  
    1.14  
    1.15 +(*unfolding abstractions with substitution
    1.16 +  of bound variables and implicit eta-expansion*)
    1.17 +fun strip_abs_eta k t =
    1.18 +  let
    1.19 +    val used = fold_aterms (fn Free (v, _) => cons v | _ => I) t [];
    1.20 +    fun strip_abs t (0, used) = (([], t), (0, used))
    1.21 +      | strip_abs (Abs (v, T, t)) (k, used) =
    1.22 +          let
    1.23 +            val v' = Name.variant used v;
    1.24 +            val t' = subst_bound (Free (v, T), t);
    1.25 +            val ((vs, t''), (k', used')) = strip_abs t' (k - 1, v' :: used);
    1.26 +          in (((v', T) :: vs, t''), (k', used')) end
    1.27 +      | strip_abs t (k, used) = (([], t), (k, used));
    1.28 +    fun expand_eta [] t _ = ([], t)
    1.29 +      | expand_eta (T::Ts) t used =
    1.30 +          let
    1.31 +            val v = hd (Name.invent_list used "a" 1)
    1.32 +            val (vs, t') = expand_eta Ts (t $ Free (v, T)) (v :: used);
    1.33 +          in ((v, T) :: vs, t') end;
    1.34 +    val ((vs1, t'), (k', used')) = strip_abs t (k, used);
    1.35 +    val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
    1.36 +    val (vs2, t'') = expand_eta Ts t' used';
    1.37 +  in (vs1 @ vs2, t'') end;
    1.38 +
    1.39 +
    1.40  (** Specialized equality, membership, insertion etc. **)
    1.41  
    1.42  (* variables *)