Merge pull request #131 from opencompl/instcombine-paper-example

Add alive example from paper

SSA/Projects/InstCombine/AliveHandwrittenExamples.lean

@@ -0,0 +1,40 @@
+
+import SSA.Projects.InstCombine.LLVM.EDSL
+import SSA.Projects.InstCombine.AliveStatements
+import SSA.Projects.InstCombine.Refinement
+import SSA.Projects.InstCombine.Tactic
+
+open MLIR AST
+open Std (BitVec)
+open Ctxt (Var)
+
+namespace AliveAutoGenerated
+set_option pp.proofs false
+set_option pp.proofs.withType false
+
+
+/-
+Name: SimplifyDivRemOfSelect
+
+%sel = select %c, %Y, 0
+%r = udiv %X, %sel
+  =>
+%r = udiv %X, %Y
+
+-/
+
+def alive_simplifyDivRemOfSelect (w : Nat) :
+[mlir_icom ( w )| {
+^bb0(%c : i1, %X : _, %Y : _):
+  %v0  = "llvm.mlir.constant" () { value = 0 : _ } :() -> (_)
+  %sel = "llvm.select" (%c,%Y,%v0) : (i1, _, _) -> (_)
+  %r   = "llvm.udiv" (%X,%sel) : (_, _) -> (_)
+  "llvm.return" (%r) : (_) -> ()
+}] ⊑ [mlir_icom ( w )| {
+^bb0(%c : i1, %X : _, %Y : _):
+  %r = "llvm.udiv" (%X,%Y) : (_, _) -> (_)
+  "llvm.return" (%r) : (_) -> ()
+}] := by
+  simp_alive_peephole
+  -- goal: ⊢ BitVec.udiv? x1✝ (BitVec.select x2✝ x0✝ (BitVec.ofInt w 0)) ⊑ BitVec.udiv? x1✝ x0✝
+  sorry