From 6283edb10c91e0d8082e38a3e52d8b50206cd60f Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 16 Nov 2023 02:48:55 +0000
Subject: [PATCH] feat: add rewriter that's based on fuel, which tries applying
 the rewriter at every 'ix' until it runs out of fuel

---
 SSA/Core/Framework.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean
index bdd2c2a06..e68f56795 100644
--- a/SSA/Core/Framework.lean
+++ b/SSA/Core/Framework.lean
@@ -1180,6 +1180,7 @@ def rewritePeepholeAt (pr : PeepholeRewrite Op Γ t)
         | none => target
       else target
 
+
 theorem denote_rewritePeepholeAt (pr : PeepholeRewrite Op Γ t)
     (pos : ℕ) (target : Com Op Γ₂ t₂) :
     (rewritePeepholeAt pr pos target).denote = target.denote := by
@@ -1196,6 +1197,23 @@ theorem denote_rewritePeepholeAt (pr : PeepholeRewrite Op Γ t)
 section SimpPeephole
 
 
+/- repeatedly apply peephole on program. -/
+section SimpPeepholeApplier
+
+/-- rewrite with `pr` to `target` program, at location `ix` and later, running at most `fuel` steps. -/
+def rewritePeephole_go (fuel : ℕ) (pr : PeepholeRewrite Op Γ t) (ix : ℕ) (target : Com Op Γ₂ t₂) :
+    (Com Op Γ₂ t₂) := 
+  match fuel with
+  | 0 => target
+  | fuel' + 1 => 
+     let target' := rewritePeepholeAt pr ix target
+     rewritePeephole_go fuel' pr (ix + 1) target'
+
+/-- rewrite with `pr` to `target` program, running at most `fuel` steps. -/
+def rewritePeephole (fuel : ℕ) (pr : PeepholeRewrite Op Γ t) (target : Com Op Γ₂ t₂) :
+    (Com Op Γ₂ t₂) := rewritePeephole_go fuel pr 0 target
+end SimpPeepholeApplier
+
 /--
 `simp_peephole [t1, t2, ... tn]` at Γ simplifies the evaluation of the context Γ,
 leaving behind a bare Lean level proposition to be proven.