src/Pure/pattern.ML
changeset 12797 4de06a8f67ef
parent 12784 bab3b002cbbb
child 12817 fcbb6ad5c790
     1.1 --- a/src/Pure/pattern.ML	Thu Jan 17 20:59:46 2002 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Jan 17 21:00:38 2002 +0100
     1.3 @@ -228,15 +228,26 @@
     1.4  
     1.5  (*Eta-contract a term (fully)*)
     1.6  
     1.7 -(* copying: *)
     1.8 -fun eta_contract (Abs(a,T,body)) =
     1.9 -      (case  eta_contract body  of
    1.10 -        body' as (f $ Bound 0) =>
    1.11 -          if loose_bvar1(f,0) then Abs(a,T,body')
    1.12 -          else incr_boundvars ~1 f
    1.13 -      | body' => Abs(a,T,body'))
    1.14 -  | eta_contract(f$t) = eta_contract f $ eta_contract t
    1.15 -  | eta_contract t = t;
    1.16 +fun eta_contract t =
    1.17 +  let
    1.18 +    exception SAME;
    1.19 +    fun eta (Abs (a, T, body)) = 
    1.20 +      ((case eta body of
    1.21 +          body' as (f $ Bound 0) => 
    1.22 +	    if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.23 +	    else incr_boundvars ~1 f
    1.24 +        | body' => Abs (a, T, body')) handle SAME =>
    1.25 +       (case body of
    1.26 +          (f $ Bound 0) => 
    1.27 +	    if loose_bvar1 (f, 0) then raise SAME
    1.28 +	    else incr_boundvars ~1 f
    1.29 +        | _ => raise SAME))
    1.30 +      | eta (f $ t) =
    1.31 +          (let val f' = eta f
    1.32 +           in f' $ etah t end handle SAME => f $ eta t)
    1.33 +      | eta _ = raise SAME
    1.34 +    and etah t = (eta t handle SAME => t)
    1.35 +  in etah t end;
    1.36  
    1.37  val beta_eta_contract = eta_contract o Envir.beta_norm;
    1.38  
    1.39 @@ -400,9 +411,16 @@
    1.40  
    1.41  fun rewrite_term tsig rules tm =
    1.42    let
    1.43 +    val rhs_names =
    1.44 +      foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
    1.45 +    fun variant_absfree (x, T, t) =
    1.46 +      let
    1.47 +        val x' = variant (add_term_free_names (t, rhs_names)) x;
    1.48 +        val t' = subst_bound (Free (x', T), t);
    1.49 +      in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
    1.50 +
    1.51      fun match_rew tm (tm1, tm2) =
    1.52        Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
    1.53 -
    1.54      fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
    1.55        | rew tm = get_first (match_rew tm) rules;
    1.56  
    1.57 @@ -432,11 +450,14 @@
    1.58              | None => (case rew1 tm2 of
    1.59                    Some tm2' => Some (tm1 $ tm2')
    1.60                  | None => None)))
    1.61 -      | rew2 (Abs (x, T, tm)) = (case rew1 tm of
    1.62 -            Some tm' => Some (Abs (x, T, tm'))
    1.63 -          | None => None)
    1.64 +      | rew2 (Abs (x, T, tm)) =
    1.65 +          let val (abs, tm') = variant_absfree (x, T, tm) in
    1.66 +            (case rew1 tm' of
    1.67 +              Some tm'' => Some (abs tm'')
    1.68 +            | None => None)
    1.69 +          end
    1.70        | rew2 _ = None
    1.71  
    1.72 -  in if_none (rew1 tm) tm end;
    1.73 +  in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end;
    1.74  
    1.75  end;