From 5a03bfe300deb4905c383f6bc0daec09f790d8a3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 26 Mar 2024 06:06:39 +0000 Subject: [PATCH] fix: make simp_alive_peephole work --- SSA/Projects/InstCombine/Tactic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 60af38859..91e3b5497 100644 --- 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]