Merge pull request #128 from opencompl/transform-dialect-generic-no-m…

…vars

Transform dialect generic no mvars

SSA/Core/Framework.lean

@@ -7,6 +7,8 @@ import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
+import SSA.Projects.MLIRSyntax.AST -- TODO post-merge: bring into Core
+import SSA.Projects.MLIRSyntax.EDSL -- TODO post-merge: bring into Core
 
 open Ctxt (Var VarSet Valuation)
 open Goedel (toType)
@@ -1196,32 +1198,31 @@ 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₂) := 
+    (ix : ℕ) (target : Com Op Γ₂ t₂) : (Com Op Γ₂ t₂) :=
   match fuel with
   | 0 => target
-  | fuel' + 1 => 
+  | 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₂) := 
+    (pr : PeepholeRewrite Op Γ t) (target : Com Op Γ₂ t₂) : (Com Op Γ₂ t₂) :=
   rewritePeephole_go fuel pr 0 target
 
 /-- `rewritePeephole_go` preserve semantics -/
 theorem denote_rewritePeephole_go (pr : PeepholeRewrite Op Γ t)
     (pos : ℕ) (target : Com Op Γ₂ t₂) :
     (rewritePeephole_go fuel pr pos target).denote = target.denote := by
   induction fuel generalizing pr pos target
-  case zero => 
+  case zero =>
     simp[rewritePeephole_go, denote_rewritePeepholeAt]
-  case succ fuel' hfuel => 
+  case succ fuel' hfuel =>
     simp[rewritePeephole_go, denote_rewritePeepholeAt, hfuel]
 
 /-- `rewritePeephole` preserves semantics. -/
@@ -1239,10 +1240,13 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
   `(tactic|
       (
       try simp (config := {decide := false}) only [
+        Int.ofNat_eq_coe, Nat.cast_zero, Ctxt.DerivedCtxt.snoc, Ctxt.DerivedCtxt.ofCtxt,
+        Ctxt.DerivedCtxt.ofCtxt_empty, Ctxt.Valuation.snoc_last,
         Com.denote, Expr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
         Ctxt.empty, Ctxt.empty_eq, Ctxt.snoc, Ctxt.Valuation.nil, Ctxt.Valuation.snoc_last,
         Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc,
         HVector.map, HVector.toPair, HVector.toTuple, OpDenote.denote, Expr.op_mk, Expr.args_mk,
+        DialectMorphism.mapOp, DialectMorphism.mapTy, List.map, Ctxt.snoc, List.map,
         $ts,*]
       generalize $ll { val := 0, property := _ } = a;
       generalize $ll { val := 1, property := _ } = b;
@@ -1270,7 +1274,6 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
 /-- `simp_peephole` with no extra user defined theorems. -/
 macro "simp_peephole" "at" ll:ident : tactic => `(tactic| simp_peephole [] at $ll)
 
-
 end SimpPeephole
 
 
@@ -1580,7 +1583,7 @@ instance : Goedel ExTy where
 inductive ExOp :  Type
   | add : ExOp
   | runK : ℕ → ExOp
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : OpSignature ExOp ExTy where
   signature
@@ -1631,6 +1634,15 @@ def p1 : PeepholeRewrite ExOp [.nat] .nat:=
       done
   }
 
+def p1_run : Com ExOp [.nat] .nat :=
+  rewritePeepholeAt p1 0 ex1_lhs
+
+/-
+RegionExamples.ExOp.runK 0[[%0]]
+return %1
+-/
+-- #eval p1_run
+
 /-- running `f(x) = x + x` 1 times does return `x + x`. -/
 def ex2_lhs : Com ExOp [.nat] .nat :=
   Com.lete (rgn (k := 1) ⟨0, by simp[Ctxt.snoc]⟩ (

SSA/Projects/InstCombine/AliveAutoGenerated.lean

@@ -12,7 +12,48 @@ namespace AliveAutoGenerated
 set_option pp.proofs false
 set_option pp.proofs.withType false
 
+def eg0  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%C0 : _):
+  "llvm.return" (%C0) : (_) -> ()
+}]
+
+def eg1  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%C0 : _):
+  "llvm.return" (%C0) : (_) -> ()
+}]
+
+theorem eg0_eq_eg1 : eg0 w ⊑ eg1 w := by
+  unfold eg0
+  unfold eg1
+  simp[DialectMorphism.mapTy,
+    InstcombineTransformDialect.MOp.instantiateCom,
+    InstcombineTransformDialect.instantiateMTy,
+    ConcreteOrMVar.instantiate, Com.Refinement]
+
+def eg2  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%C0 : _):
+  %v1 = "llvm.add" (%C0, %C0) : (_, _) -> (_)
+  "llvm.return" (%C0) : (_) -> ()
+}]
+
+
+def eg3  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%C0 : _):
+  %v1 = "llvm.mlir.constant" () { value = 2 : _ } :() -> (_)
+  %v2 = "llvm.mul" (%C0, %v1) : (_, _) -> (_)
+  "llvm.return" (%C0) : (_) -> ()
+}]
 
+open MLIR AST in
+theorem eg2_eq_eg3 : eg2 w ⊑ eg3 w := by
+  unfold eg2
+  unfold eg3
+  simp_alive_peephole
+  simp
 
 -- Name:AddSub:1043
 -- precondition: true
@@ -31,7 +72,7 @@ set_option pp.proofs.withType false
 
 -/
 def alive_AddSub_1043_src  (w : Nat)   :=
-[mlir_icom ( w )| {
+[alive_icom ( w )| {
 ^bb0(%C1 : _, %Z : _, %RHS : _):
   %v1 = "llvm.and" (%Z,%C1) : (_, _) -> (_)
   %v2 = "llvm.xor" (%v1,%C1) : (_, _) -> (_)
@@ -42,7 +83,7 @@ def alive_AddSub_1043_src  (w : Nat)   :=
 }]
 
 def alive_AddSub_1043_tgt  (w : Nat)  :=
-[mlir_icom ( w )| {
+[alive_icom ( w )| {
 ^bb0(%C1 : _, %Z : _, %RHS : _):
   %v1 = "llvm.not" (%C1) : (_) -> (_)
   %v2 = "llvm.or" (%Z,%v1) : (_, _) -> (_)
@@ -56,8 +97,13 @@ def alive_AddSub_1043_tgt  (w : Nat)  :=
 theorem alive_AddSub_1043  (w : Nat)   : alive_AddSub_1043_src w  ⊑ alive_AddSub_1043_tgt w  := by
   unfold alive_AddSub_1043_src alive_AddSub_1043_tgt
   simp_alive_peephole
-  apply bitvec_AddSub_1043
+  sorry
 
+/-# Early Exit
+delete this to check the rest of the file. The `#exit`
+  is an early exit to allow our `lake` builds to complete in sensible amounts of time.
+-/
+#exit
 
 /-# Early Exit
 delete this to check the rest of the file. The `#exit`

SSA/Projects/InstCombine/Base.lean

@@ -40,6 +40,9 @@ instance : Repr (MTy φ) where
     | .bitvec (.concrete w), _ => "i" ++ repr w
     | .bitvec (.mvar ⟨i, _⟩), _ => f!"i$\{%{i}}"
 
+instance : Lean.ToFormat (MTy φ) where
+  format := repr
+
 instance : ToString (MTy φ) where
   toString t := repr t |>.pretty