fix: make simp_alive_peephole work

opencompl · Mar 26, 2024 · 5a03bfe · 5a03bfe
1 parent 31d4e53
commit 5a03bfe
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
@@ -32,7 +32,7 @@ macro "simp_alive_peephole" : tactic =>
         simp (config := {unfoldPartialApp := true, zetaDelta := true}) only [OpDenote.denote,
           InstCombine.Op.denote, HVector.toPair, HVector.toTriple, pairMapM, BitVec.Refinement,
           bind, Option.bind, pure, Ctxt.DerivedCtxt.ofCtxt, Ctxt.DerivedCtxt.snoc,
-          Ctxt.snoc,
+          Ctxt.snoc, Valuation.snoc,
           ConcreteOrMVar.instantiate, Vector.get, HVector.toSingle,
           LLVM.and?, LLVM.or?, LLVM.xor?, LLVM.add?, LLVM.sub?,
           LLVM.mul?, LLVM.udiv?, LLVM.sdiv?, LLVM.urem?, LLVM.srem?,
@@ -52,6 +52,7 @@ macro "simp_alive_peephole" : tactic =>
         try intros v3
         try intros v4
         try intros v5
+        simp only [Option.bind, bind, Monad.toBind, Var.casesOn, cast, pairBind, Option.bind_eq_bind]
         try cases' v0 with x0 <;> simp[Option.bind, bind, Monad.toBind]
           <;> try cases' v1 with x1 <;> simp[Option.bind, bind, Monad.toBind]
           <;> try cases' v2 with x2 <;> simp[Option.bind, bind, Monad.toBind]