# HG changeset patch
# User wenzelm
# Date 1729713466 -7200
# Node ID 7d61f448f69388ba97768c316e78c8810ed488a5
# Parent  400be27520149af8c78308a8d4423b0304af90fb
provide rewrite_term_yoyo, which is analogous to Ast.normalize;

diff -r 400be2752014 -r 7d61f448f693 src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Wed Oct 23 15:09:02 2024 +0200
+++ b/src/Pure/more_pattern.ML	Wed Oct 23 21:57:46 2024 +0200
@@ -15,6 +15,7 @@
   val match_rew: theory -> term -> term * term -> (term * term) option
   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
   val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
+  val rewrite_term_yoyo: theory -> (term * term) list -> (term -> term option) list -> term -> term
 end;
 
 structure Pattern: PATTERN =
@@ -51,7 +52,7 @@
 val skel_arg = fn _ $ skel => skel | _ => skel0;
 val skel_body = fn Abs (_, _, skel) => skel | _ => skel0;
 
-datatype mode = Bottom | Top;
+datatype mode = Bottom | Top | Yoyo;
 
 fun rewrite_term_mode mode thy rules procs term =
   let
@@ -83,6 +84,9 @@
           in Option.map abs (rw (bounds + 1) (skel_body skel) t') end
       | rew_sub _ _ _ _ = NONE;
 
+
+    (* bottom-up with skeleton *)
+
     fun rew_bottom _ (Var _) _ = NONE
       | rew_bottom bounds skel t =
           (case rew_sub rew_bottom bounds skel t of
@@ -95,6 +99,9 @@
                 SOME (t1, skel') => SOME (the_default t1 (rew_bottom bounds skel' t1))
               | NONE => NONE));
 
+
+    (* top-down *)
+
     fun rew_top bounds _ t =
       (case rew t of
         SOME (t1, _) =>
@@ -106,13 +113,35 @@
             SOME t1 => SOME (the_default t1 (rew_top bounds skel0 t1))
           | NONE => NONE));
 
-    val rewrite = (case mode of Bottom => rew_bottom | Top => rew_top);
+
+    (* yoyo: see also Ast.normalize *)
+
+    fun rew_yoyo1 t =
+      rew t |> Option.map (fn (t', _) => the_default t' (rew_yoyo1 t'));
+
+    fun rew_yoyo2 bounds _ t =
+      (case rew_yoyo1 t of
+        SOME t1 =>
+          (case rew_sub rew_yoyo2 bounds skel0 t1 of
+            SOME t2 => SOME (the_default t2 (rew_yoyo1 t2))
+          | NONE => SOME t1)
+      | NONE =>
+          (case rew_sub rew_yoyo2 bounds skel0 t of
+            SOME t1 => SOME (the_default t1 (rew_yoyo1 t1))
+          | NONE => NONE));
+
+    fun rew_yoyo bounds skel t =
+      rew_yoyo2 bounds skel t |> Option.map (fn t' => the_default t' (rew_yoyo bounds skel0 t'));
+
+
+    val rewrite = (case mode of Bottom => rew_bottom | Top => rew_top | Yoyo => rew_yoyo);
   in the_default term (rewrite 0 skel0 term) end;
 
 in
 
 val rewrite_term = rewrite_term_mode Bottom;
 val rewrite_term_top = rewrite_term_mode Top;
+val rewrite_term_yoyo = rewrite_term_mode Yoyo;
 
 end;