Skip to content

Commit

Permalink
ICom/IExpr -> Com/Expr
Browse files Browse the repository at this point in the history
  • Loading branch information
@goens
goens committed Oct 26, 2023
1 parent a9d0d36 commit f04071c
Showing 1 changed file with 42 additions and 42 deletions.
84 changes: 42 additions & 42 deletions SSA/Projects/PaperExamples/PaperExamples.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,15 +35,15 @@ instance : OpDenote Op Ty where
| .const n, _, _ => BitVec.ofInt 32 n
| .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b

def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int :=
IExpr.mk
def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int :=
Expr.mk
(op := .const n)
(ty_eq := rfl)
(args := .nil)
(regArgs := .nil)

def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
IExpr.mk
def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int :=
Expr.mk
(op := .add)
(ty_eq := rfl)
(args := .cons e₁ <| .cons e₂ .nil)
Expand All @@ -52,28 +52,28 @@ def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
attribute [local simp] Ctxt.snoc

/-- x + 0 -/
def lhs : ICom Op (Ctxt.ofList [.int]) .int :=
def lhs : Com Op (Ctxt.ofList [.int]) .int :=
-- %c0 = 0
ICom.lete (cst 0) <|
Com.lete (cst 0) <|
-- %out = %x + %c0
ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <|
Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <|
-- return %out
ICom.ret ⟨0, by simp [Ctxt.snoc]⟩
Com.ret ⟨0, by simp [Ctxt.snoc]⟩

/-- x -/
def rhs : ICom Op (Ctxt.ofList [.int]) .int :=
ICom.ret ⟨0, by simp⟩
def rhs : Com Op (Ctxt.ofList [.int]) .int :=
Com.ret ⟨0, by simp⟩

def p1 : PeepholeRewrite Op [.int] .int :=
{ lhs := lhs, rhs := rhs, correct :=
by
rw [lhs, rhs]
/-
ICom.denote
(ICom.lete (cst 0)
(ICom.lete (add { val := 1, property := _ } { val := 0, property := _ })
(ICom.ret { val := 0, property := ex1.proof_3 }))) =
ICom.denote (ICom.ret { val := 0, property := _ })
Com.denote
(Com.lete (cst 0)
(Com.lete (add { val := 1, property := _ } { val := 0, property := _ })
(Com.ret { val := 0, property := ex1.proof_3 }))) =
Com.denote (Com.ret { val := 0, property := _ })
-/
funext Γv
simp_peephole [add, cst] at Γv
Expand All @@ -84,16 +84,16 @@ def p1 : PeepholeRewrite Op [.int] .int :=
sorry
}

def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
def ex1' : Com Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs


theorem EX1' : ex1' = (
-- %c0 = 0
ICom.lete (cst 0) <|
Com.lete (cst 0) <|
-- %out_dead = %x + %c0
ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
-- ret %c0
ICom.ret ⟨2, by simp [Ctxt.snoc]⟩)
Com.ret ⟨2, by simp [Ctxt.snoc]⟩)
:= by rfl

end ToyNoRegion
Expand Down Expand Up @@ -132,22 +132,22 @@ instance : OpDenote Op Ty where
-- let f_k := Nat.iterate f' k
-- f_k x

def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int :=
IExpr.mk
def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int :=
Expr.mk
(op := .const n)
(ty_eq := rfl)
(args := .nil)
(regArgs := .nil)

def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
IExpr.mk
def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int :=
Expr.mk
(op := .add)
(ty_eq := rfl)
(args := .cons e₁ <| .cons e₂ .nil)
(regArgs := .nil)

def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.int] .int) : IExpr Op Γ .int :=
IExpr.mk
def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : Com Op [.int] .int) : Expr Op Γ .int :=
Expr.mk
(op := .iterate k)
(ty_eq := rfl)
(args := .cons input .nil)
Expand All @@ -156,15 +156,15 @@ def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.in
attribute [local simp] Ctxt.snoc

/-- running `f(x) = x + x` 0 times is the identity. -/
def lhs : ICom Op [.int] .int :=
ICom.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ (
ICom.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x)
<| ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
def lhs : Com Op [.int] .int :=
Com.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ (
Com.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x)
<| Com.ret ⟨0, by simp[Ctxt.snoc]⟩
)) <|
ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
Com.ret ⟨0, by simp[Ctxt.snoc]⟩

def rhs : ICom Op [.int] .int :=
ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
def rhs : Com Op [.int] .int :=
Com.ret ⟨0, by simp[Ctxt.snoc]⟩

attribute [local simp] Ctxt.snoc

Expand All @@ -178,14 +178,14 @@ def p1 : PeepholeRewrite Op [.int] .int:=
rw [lhs, rhs]
funext Γv
/-
ICom.denote
(ICom.lete
Com.denote
(Com.lete
(iterate 0 { val := 0, property := lhs.proof_1 }
(ICom.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 })
(ICom.ret { val := 0, property := lhs.proof_2 })))
(ICom.ret { val := 0, property := lhs.proof_2 }))
(Com.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 })
(Com.ret { val := 0, property := lhs.proof_2 })))
(Com.ret { val := 0, property := lhs.proof_2 }))
Γv =
ICom.denote (ICom.ret { val := 0, property := rhs.proof_1 }) Γv
Com.denote (Com.ret { val := 0, property := rhs.proof_1 }) Γv
-/
simp_peephole [add, iterate] at Γv
/- ∀ (a : BitVec 32), (fun v => v + v)^[0] a = a -/
Expand All @@ -194,15 +194,15 @@ def p1 : PeepholeRewrite Op [.int] .int:=
}

/-
def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
def ex1' : Com Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
theorem EX1' : ex1' = (
-- %c0 = 0
ICom.lete (cst 0) <|
Com.lete (cst 0) <|
-- %out_dead = %x + %c0
ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
-- ret %c0
ICom.ret ⟨2, by simp [Ctxt.snoc]⟩)
Com.ret ⟨2, by simp [Ctxt.snoc]⟩)
:= by rfl
-/

Expand Down

0 comments on commit f04071c

Please sign in to comment.