feat: add simple example of using new object level translation

opencompl · Oct 9, 2023 · e458ed8 · e458ed8
1 parent e4260e4
commit e458ed8
Show file tree

Hide file tree

Showing 2 changed files with 58 additions and 3 deletions.
diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean
@@ -7,6 +7,61 @@ abbrev ICom.Refinement (src tgt : Com (φ:=0) Γ t) (h : Goedel.toType t = Optio
 
 infixr:90 " ⊑ "  => ICom.Refinement
 
+namespace OnlyReturn
+def lhs (w : Nat) :=
+[mlir_icom (w)| {
+^bb0(%C1 : _):
+  "llvm.return" (%C1) : (_) -> ()
+}]
+
+def rhs (w : Nat):=
+[mlir_icom (w)| {
+^bb0(%C1 : _):
+  "llvm.return" (%C1) : (_) -> ()
+}]
+
+open Ctxt (Var) in
+theorem refinement (w : Nat) : lhs w ⊑ rhs w := by
+  unfold lhs rhs
+  intro (Γv : ([.bitvec w] : List InstCombine.Ty) |> Ctxt.Valuation)
+  simp [ICom.denote, IExpr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
+        Ctxt.snoc, Ctxt.Valuation.snoc_last, Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc,
+        HVector.map, OpDenote.denote, IExpr.op_mk, IExpr.args_mk, ICom.Refinement,
+        Bind.bind, DialectMorphism.mapTy, MOp.instantiateCom,
+        InstCombine.MTy.instantiate, ConcreteOrMVar.instantiate, Vector.get, List.get]
+  generalize Γv (Var.last [] (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) = x
+  -- simp_alive
+  apply Bitvec.Refinement.refl
+end OnlyReturn
+
+
+namespace AddCommutative
+def lhs (w : Nat) :=
+[mlir_icom (w)| {
+^bb0(%X : _, %Y: _):
+  %Z = "llvm.add" (%X, %Y) : (_, _) -> (_)
+  "llvm.return" (%Z) : (_) -> ()
+}]
+
+def rhs (w : Nat):=
+[mlir_icom (w)| {
+^bb0(%X : _, %Y: _):
+  %Z = "llvm.add" (%Y, %X) : (_, _) -> (_)
+  "llvm.return" (%Z) : (_) -> ()
+}]
+
+open Ctxt (Var) in
+theorem refinement (w : Nat) : lhs w ⊑ rhs w := by
+  unfold lhs rhs
+  intro (Γv : ([.bitvec w, .bitvec w] : List InstCombine.Ty) |> Ctxt.Valuation)
+  simp [ICom.denote, IExpr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
+        Ctxt.snoc, Ctxt.Valuation.snoc_last, Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc,
+        HVector.map, OpDenote.denote, IExpr.op_mk, IExpr.args_mk, ICom.Refinement,
+        Bind.bind, DialectMorphism.mapTy, MOp.instantiateCom,
+        InstCombine.MTy.instantiate, ConcreteOrMVar.instantiate, Vector.get, List.get]
+  sorry
+end AddCommutative
+
 
 -- Name:AddSub:1043
 -- precondition: true

diff --git a/SSA/Projects/InstCombine/ForMathlib.lean b/SSA/Projects/InstCombine/ForMathlib.lean
@@ -475,16 +475,16 @@ theorem Refinement.some_some {α : Type u} {x y : α} :
 
 namespace Refinement
 
-theorem Refinement.refl {α: Type u} : ∀ x : Option α, Refinement x x := by 
+theorem refl {α: Type u} : ∀ x : Option α, Refinement x x := by
   intro x ; cases x
   apply Refinement.noneAny
   apply Refinement.bothSome; rfl
 
-theorem Refinement.trans {α : Type u} : ∀ x y z : Option α, Refinement x y → Refinement y z → Refinement x z := by
+theorem trans {α : Type u} : ∀ x y z : Option α, Refinement x y → Refinement y z → Refinement x z := by
   intro x y z h₁ h₂
   cases h₁ <;> cases h₂ <;> try { apply Refinement.noneAny } ; try {apply Refinement.bothSome; assumption}
   rename_i x y hxy y h 
-  rw [hxy, h]; apply Refinement.refl
+  rw [hxy, h]; apply refl
 
 instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by
   intro x y