Changes to rewrite_term:
authorberghofe
Fri May 31 18:47:11 2002 +0200 (2002-05-31)
changeset 1319598975cc13d28
parent 13194 812b00ed1c03
child 13196 08c42252346f
Changes to rewrite_term:
- now uses skeletons to speed up rewriting
- added interface for rewriting procedures
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Fri May 31 15:06:06 2002 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri May 31 18:47:11 2002 +0200
     1.3 @@ -32,7 +32,8 @@
     1.4    val unify             : sg * env * (term * term)list -> env
     1.5    val first_order       : term -> bool
     1.6    val pattern           : term -> bool
     1.7 -  val rewrite_term      : type_sig -> (term * term) list -> term -> term
     1.8 +  val rewrite_term      : type_sig -> (term * term) list -> (term -> term option) list
     1.9 +                          -> term -> term
    1.10    exception Unif
    1.11    exception MATCH
    1.12    exception Pattern
    1.13 @@ -409,10 +410,13 @@
    1.14  
    1.15  (* rewriting -- simple but fast *)
    1.16  
    1.17 -fun rewrite_term tsig rules tm =
    1.18 +fun rewrite_term tsig rules procs tm =
    1.19    let
    1.20 +    val skel0 = Bound 0;
    1.21 +
    1.22      val rhs_names =
    1.23        foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
    1.24 +
    1.25      fun variant_absfree (x, T, t) =
    1.26        let
    1.27          val x' = variant (add_term_free_names (t, rhs_names)) x;
    1.28 @@ -420,38 +424,51 @@
    1.29        in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
    1.30  
    1.31      fun match_rew tm (tm1, tm2) =
    1.32 -      Some (subst_vars (match tsig (tm1, tm)) (if_none (Term.rename_abs tm1 tm tm2) tm2))
    1.33 -        handle MATCH => None;
    1.34 -    fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
    1.35 -      | rew tm = get_first (match_rew tm) rules;
    1.36 +      let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2
    1.37 +      in Some (subst_vars (match tsig (tm1, tm)) rtm, rtm)
    1.38 +        handle MATCH => None
    1.39 +      end;
    1.40  
    1.41 -    fun rew1 tm = (case rew2 tm of
    1.42 +    fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body), skel0)
    1.43 +      | rew tm = (case get_first (match_rew tm) rules of
    1.44 +          None => apsome (rpair skel0) (get_first (fn p => p tm) procs)
    1.45 +        | x => x);
    1.46 +
    1.47 +    fun rew1 (Var _) _ = None
    1.48 +      | rew1 skel tm = (case rew2 skel tm of
    1.49            Some tm1 => (case rew tm1 of
    1.50 -              Some tm2 => Some (if_none (rew1 tm2) tm2)
    1.51 +              Some (tm2, skel') => Some (if_none (rew1 skel' tm2) tm2)
    1.52              | None => Some tm1)
    1.53          | None => (case rew tm of
    1.54 -              Some tm1 => Some (if_none (rew1 tm1) tm1)
    1.55 +              Some (tm1, skel') => Some (if_none (rew1 skel' tm1) tm1)
    1.56              | None => None))
    1.57  
    1.58 -    and rew2 (tm1 $ tm2) = (case tm1 of
    1.59 +    and rew2 skel (tm1 $ tm2) = (case tm1 of
    1.60              Abs (_, _, body) =>
    1.61                let val tm' = subst_bound (tm2, body)
    1.62 -              in Some (if_none (rew2 tm') tm') end
    1.63 -          | _ => (case rew1 tm1 of
    1.64 -              Some tm1' => (case rew1 tm2 of
    1.65 -                  Some tm2' => Some (tm1' $ tm2')
    1.66 -                | None => Some (tm1' $ tm2))
    1.67 -            | None => (case rew1 tm2 of
    1.68 -                  Some tm2' => Some (tm1 $ tm2')
    1.69 -                | None => None)))
    1.70 -      | rew2 (Abs (x, T, tm)) =
    1.71 -          let val (abs, tm') = variant_absfree (x, T, tm) in
    1.72 -            (case rew1 tm' of
    1.73 +              in Some (if_none (rew2 skel0 tm') tm') end
    1.74 +          | _ => 
    1.75 +            let val (skel1, skel2) = (case skel of
    1.76 +                skel1 $ skel2 => (skel1, skel2)
    1.77 +              | _ => (skel0, skel0))
    1.78 +            in case rew1 skel1 tm1 of
    1.79 +                Some tm1' => (case rew1 skel2 tm2 of
    1.80 +                    Some tm2' => Some (tm1' $ tm2')
    1.81 +                  | None => Some (tm1' $ tm2))
    1.82 +              | None => (case rew1 skel2 tm2 of
    1.83 +                    Some tm2' => Some (tm1 $ tm2')
    1.84 +                  | None => None)
    1.85 +            end)
    1.86 +      | rew2 skel (Abs (x, T, tm)) =
    1.87 +          let
    1.88 +            val (abs, tm') = variant_absfree (x, T, tm);
    1.89 +            val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
    1.90 +          in case rew1 skel' tm' of
    1.91                Some tm'' => Some (abs tm'')
    1.92 -            | None => None)
    1.93 +            | None => None
    1.94            end
    1.95 -      | rew2 _ = None
    1.96 +      | rew2 _ _ = None
    1.97  
    1.98 -  in if_none (rew1 tm) tm end;
    1.99 +  in if_none (rew1 skel0 tm) tm end;
   1.100  
   1.101  end;