Added function rewrite_term_top for top-down rewriting.
authorberghofe
Thu Feb 18 17:27:18 2010 +0100 (2010-02-18)
changeset 352106e45e4c94751
parent 35198 f95c6440c1c7
child 35211 5d2fe4e09354
Added function rewrite_term_top for top-down rewriting.
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Thu Feb 18 11:23:03 2010 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Feb 18 17:27:18 2010 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4    val pattern: term -> bool
     1.5    val match_rew: theory -> term -> term * term -> (term * term) option
     1.6    val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
     1.7 +  val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
     1.8    exception Unif
     1.9    exception MATCH
    1.10    exception Pattern
    1.11 @@ -432,7 +433,7 @@
    1.12        handle MATCH => NONE
    1.13    end;
    1.14  
    1.15 -fun rewrite_term thy rules procs tm =
    1.16 +fun gen_rewrite_term bot thy rules procs tm =
    1.17    let
    1.18      val skel0 = Bound 0;
    1.19  
    1.20 @@ -448,42 +449,53 @@
    1.21              NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
    1.22            | x => x);
    1.23  
    1.24 -    fun rew1 bounds (Var _) _ = NONE
    1.25 -      | rew1 bounds skel tm = (case rew2 bounds skel tm of
    1.26 -          SOME tm1 => (case rew tm1 of
    1.27 -              SOME (tm2, skel') => SOME (the_default tm2 (rew1 bounds skel' tm2))
    1.28 -            | NONE => SOME tm1)
    1.29 -        | NONE => (case rew tm of
    1.30 -              SOME (tm1, skel') => SOME (the_default tm1 (rew1 bounds skel' tm1))
    1.31 -            | NONE => NONE))
    1.32 -
    1.33 -    and rew2 bounds skel (tm1 $ tm2) = (case tm1 of
    1.34 +    fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
    1.35              Abs (_, _, body) =>
    1.36                let val tm' = subst_bound (tm2, body)
    1.37 -              in SOME (the_default tm' (rew2 bounds skel0 tm')) end
    1.38 +              in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
    1.39            | _ =>
    1.40              let val (skel1, skel2) = (case skel of
    1.41                  skel1 $ skel2 => (skel1, skel2)
    1.42                | _ => (skel0, skel0))
    1.43 -            in case rew1 bounds skel1 tm1 of
    1.44 -                SOME tm1' => (case rew1 bounds skel2 tm2 of
    1.45 +            in case r bounds skel1 tm1 of
    1.46 +                SOME tm1' => (case r bounds skel2 tm2 of
    1.47                      SOME tm2' => SOME (tm1' $ tm2')
    1.48                    | NONE => SOME (tm1' $ tm2))
    1.49 -              | NONE => (case rew1 bounds skel2 tm2 of
    1.50 +              | NONE => (case r bounds skel2 tm2 of
    1.51                      SOME tm2' => SOME (tm1 $ tm2')
    1.52                    | NONE => NONE)
    1.53              end)
    1.54 -      | rew2 bounds skel (Abs body) =
    1.55 +      | rew_sub r bounds skel (Abs body) =
    1.56            let
    1.57              val (abs, tm') = variant_absfree bounds body;
    1.58              val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
    1.59 -          in case rew1 (bounds + 1) skel' tm' of
    1.60 +          in case r (bounds + 1) skel' tm' of
    1.61                SOME tm'' => SOME (abs tm'')
    1.62              | NONE => NONE
    1.63            end
    1.64 -      | rew2 _ _ _ = NONE;
    1.65 +      | rew_sub _ _ _ _ = NONE;
    1.66 +
    1.67 +    fun rew_bot bounds (Var _) _ = NONE
    1.68 +      | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
    1.69 +          SOME tm1 => (case rew tm1 of
    1.70 +              SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
    1.71 +            | NONE => SOME tm1)
    1.72 +        | NONE => (case rew tm of
    1.73 +              SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
    1.74 +            | NONE => NONE));
    1.75  
    1.76 -  in the_default tm (rew1 0 skel0 tm) end;
    1.77 +    fun rew_top bounds _ tm = (case rew tm of
    1.78 +          SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
    1.79 +              SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
    1.80 +            | NONE => SOME tm1)
    1.81 +        | NONE => (case rew_sub rew_top bounds skel0 tm of
    1.82 +              SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
    1.83 +            | NONE => NONE));
    1.84 +
    1.85 +  in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
    1.86 +
    1.87 +val rewrite_term = gen_rewrite_term true;
    1.88 +val rewrite_term_top = gen_rewrite_term false;
    1.89  
    1.90  end;
    1.91