moved (beta_)eta_contract to envir.ML;
authorwenzelm
Mon Feb 06 20:59:07 2006 +0100 (2006-02-06)
changeset 18940d8e12bf337a3
parent 18939 18e2a2676d80
child 18941 18cb1e2ab77d
moved (beta_)eta_contract to envir.ML;
tuned;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Mon Feb 06 20:59:06 2006 +0100
     1.2 +++ b/src/Pure/pattern.ML	Mon Feb 06 20:59:07 2006 +0100
     1.3 @@ -17,9 +17,7 @@
     1.4  sig
     1.5    val trace_unify_fail: bool ref
     1.6    val aeconv: term * term -> bool
     1.7 -  val eta_contract: term -> term
     1.8    val eta_long: typ list -> term -> term
     1.9 -  val beta_eta_contract: term -> term
    1.10    val eta_contract_atom: term -> term
    1.11    val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
    1.12    val first_order_match: theory -> term * term
    1.13 @@ -272,31 +270,6 @@
    1.14  fun unify thy = unif thy [];
    1.15  
    1.16  
    1.17 -(*Eta-contract a term (fully)*)
    1.18 -
    1.19 -fun eta_contract t =
    1.20 -  let
    1.21 -    exception SAME;
    1.22 -    fun eta (Abs (a, T, body)) =
    1.23 -      ((case eta body of
    1.24 -          body' as (f $ Bound 0) =>
    1.25 -            if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.26 -            else incr_boundvars ~1 f
    1.27 -        | body' => Abs (a, T, body')) handle SAME =>
    1.28 -       (case body of
    1.29 -          (f $ Bound 0) =>
    1.30 -            if loose_bvar1 (f, 0) then raise SAME
    1.31 -            else incr_boundvars ~1 f
    1.32 -        | _ => raise SAME))
    1.33 -      | eta (f $ t) =
    1.34 -          (let val f' = eta f
    1.35 -           in f' $ etah t end handle SAME => f $ eta t)
    1.36 -      | eta _ = raise SAME
    1.37 -    and etah t = (eta t handle SAME => t)
    1.38 -  in etah t end;
    1.39 -
    1.40 -val beta_eta_contract = eta_contract o Envir.beta_norm;
    1.41 -
    1.42  (*Eta-contract a term from outside: just enough to reduce it to an atom
    1.43  DOESN'T QUITE WORK!
    1.44  *)
    1.45 @@ -476,7 +449,7 @@
    1.46        in (abs, t') end;
    1.47  
    1.48      fun match_rew tm (tm1, tm2) =
    1.49 -      let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in
    1.50 +      let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
    1.51          SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
    1.52            handle MATCH => NONE
    1.53        end;
    1.54 @@ -489,16 +462,16 @@
    1.55      fun rew1 bounds (Var _) _ = NONE
    1.56        | rew1 bounds skel tm = (case rew2 bounds skel tm of
    1.57            SOME tm1 => (case rew tm1 of
    1.58 -              SOME (tm2, skel') => SOME (if_none (rew1 bounds skel' tm2) tm2)
    1.59 +              SOME (tm2, skel') => SOME (the_default tm2 (rew1 bounds skel' tm2))
    1.60              | NONE => SOME tm1)
    1.61          | NONE => (case rew tm of
    1.62 -              SOME (tm1, skel') => SOME (if_none (rew1 bounds skel' tm1) tm1)
    1.63 +              SOME (tm1, skel') => SOME (the_default tm1 (rew1 bounds skel' tm1))
    1.64              | NONE => NONE))
    1.65  
    1.66      and rew2 bounds skel (tm1 $ tm2) = (case tm1 of
    1.67              Abs (_, _, body) =>
    1.68                let val tm' = subst_bound (tm2, body)
    1.69 -              in SOME (if_none (rew2 bounds skel0 tm') tm') end
    1.70 +              in SOME (the_default tm' (rew2 bounds skel0 tm')) end
    1.71            | _ =>
    1.72              let val (skel1, skel2) = (case skel of
    1.73                  skel1 $ skel2 => (skel1, skel2)
    1.74 @@ -521,7 +494,7 @@
    1.75            end
    1.76        | rew2 _ _ _ = NONE;
    1.77  
    1.78 -  in if_none (rew1 0 skel0 tm) tm end;
    1.79 +  in the_default tm (rew1 0 skel0 tm) end;
    1.80  
    1.81  end;
    1.82