@[simp]

theorem BitVec.ofInt_zero (w : ℕ) : BitVec.ofInt w 0 = 0

inductive ToyNoRegion.Ty : Type

• int: ToyNoRegion.Ty

instance ToyNoRegion.instDecidableEqTy : DecidableEq ToyNoRegion.Ty

Equations

• ToyNoRegion.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance ToyNoRegion.instReprTy : Repr ToyNoRegion.Ty

Equations

• ToyNoRegion.instReprTy = { reprPrec := ToyNoRegion.reprTy✝ }

@[reducible]

instance ToyNoRegion.instTyDenoteTy : TyDenote ToyNoRegion.Ty

Equations

• ToyNoRegion.instTyDenoteTy = { toType := fun (x : ToyNoRegion.Ty) => match x with | ToyNoRegion.Ty.int => BitVec 32 }

inductive ToyNoRegion.Op : Type

• add: ToyNoRegion.Op
• const: ℤ → ToyNoRegion.Op

instance ToyNoRegion.instDecidableEqOp : DecidableEq ToyNoRegion.Op

Equations

• ToyNoRegion.instDecidableEqOp = ToyNoRegion.decEqOp✝

instance ToyNoRegion.instReprOp : Repr ToyNoRegion.Op

Equations

• ToyNoRegion.instReprOp = { reprPrec := ToyNoRegion.reprOp✝ }

@[reducible, inline]

abbrev ToyNoRegion.Simple : Dialect

Simple is a very basic example dialect

Equations

• ToyNoRegion.Simple = { Op := ToyNoRegion.Op, Ty := ToyNoRegion.Ty, m := Id }

instance ToyNoRegion.instDialectSignatureSimple : DialectSignature ToyNoRegion.Simple

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

instance ToyNoRegion.instDialectDenoteSimple : DialectDenote ToyNoRegion.Simple

Equations

• One or more equations did not get rendered due to their size.

def ToyNoRegion.cst {Γ : Ctxt ToyNoRegion.Simple.Ty} (n : ℤ) : Expr ToyNoRegion.Simple Γ EffectKind.pure ToyNoRegion.Ty.int

Equations

• ToyNoRegion.cst n = Expr.mk (ToyNoRegion.Op.const n) ToyNoRegion.cst.proof_1 ⋯ HVector.nil HVector.nil

def ToyNoRegion.add {Γ : Ctxt ToyNoRegion.Simple.Ty} (e₁ : Γ.Var ToyNoRegion.Ty.int) (e₂ : Γ.Var ToyNoRegion.Ty.int) : Expr ToyNoRegion.Simple Γ EffectKind.pure ToyNoRegion.Ty.int

Equations

• ToyNoRegion.add e₁ e₂ = Expr.mk ToyNoRegion.Op.add ToyNoRegion.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def ToyNoRegion.MLIR2Simple.mkTy {φ : ℕ} : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM ToyNoRegion.Simple ToyNoRegion.Ty

Equations

• ToyNoRegion.MLIR2Simple.mkTy (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless a) = pure ToyNoRegion.Ty.int
• ToyNoRegion.MLIR2Simple.mkTy x = throw MLIR.AST.TransformError.unsupportedType

instance ToyNoRegion.MLIR2Simple.instTransformTy : MLIR.AST.TransformTy ToyNoRegion.Simple 0

Equations

• ToyNoRegion.MLIR2Simple.instTransformTy = { mkTy := ToyNoRegion.MLIR2Simple.mkTy }

def ToyNoRegion.MLIR2Simple.mkExpr (Γ : Ctxt ToyNoRegion.Simple.Ty) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM ToyNoRegion.Simple ((eff : EffectKind) × (ty : ToyNoRegion.Simple.Ty) × Expr ToyNoRegion.Simple Γ eff ty)

Equations

• One or more equations did not get rendered due to their size.

instance ToyNoRegion.MLIR2Simple.instTransformExprSimpleOfNatNat : MLIR.AST.TransformExpr ToyNoRegion.Simple 0

Equations

• ToyNoRegion.MLIR2Simple.instTransformExprSimpleOfNatNat = { mkExpr := ToyNoRegion.MLIR2Simple.mkExpr }

def ToyNoRegion.MLIR2Simple.mkReturn (Γ : Ctxt ToyNoRegion.Simple.Ty) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM ToyNoRegion.Simple ((eff : EffectKind) × (ty : ToyNoRegion.Simple.Ty) × Com ToyNoRegion.Simple Γ eff ty)

Equations

• One or more equations did not get rendered due to their size.

instance ToyNoRegion.MLIR2Simple.instTransformReturnSimpleOfNatNat : MLIR.AST.TransformReturn ToyNoRegion.Simple 0

Equations

• ToyNoRegion.MLIR2Simple.instTransformReturnSimpleOfNatNat = { mkReturn := ToyNoRegion.MLIR2Simple.mkReturn }

def ToyNoRegion.MLIR2Simple.«term[simple_com|_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ToyNoRegion.eg₀ : Com ToyNoRegion.Simple (↑[]) EffectKind.pure ToyNoRegion.Ty.int

Equations

• One or more equations did not get rendered due to their size.

def ToyNoRegion.eg₀val : EffectKind.pure.toMonad ToyNoRegion.Simple.m ⟦ToyNoRegion.Ty.int⟧

Equations

• ToyNoRegion.eg₀val = ToyNoRegion.eg₀.denote Ctxt.Valuation.nil

def ToyNoRegion.lhs : Com ToyNoRegion.Simple (↑[ToyNoRegion.Ty.int]) EffectKind.pure ToyNoRegion.Ty.int

x + 0

Equations

• One or more equations did not get rendered due to their size.

def ToyNoRegion.rhs : Com ToyNoRegion.Simple (↑[ToyNoRegion.Ty.int]) EffectKind.pure ToyNoRegion.Ty.int

x

Equations

• ToyNoRegion.rhs = Com.ret ⟨0, ToyNoRegion.rhs.proof_1⟩

def ToyNoRegion.p1 : PeepholeRewrite ToyNoRegion.Simple [ToyNoRegion.Ty.int] ToyNoRegion.Ty.int

Equations

• ToyNoRegion.p1 = { lhs := ToyNoRegion.lhs, rhs := ToyNoRegion.rhs, correct := ToyNoRegion.p1.proof_1 }

def ToyNoRegion.ex1_rewritePeepholeAt : Com ToyNoRegion.Simple (↑[ToyNoRegion.Ty.int]) EffectKind.pure ToyNoRegion.Ty.int

Equations

• ToyNoRegion.ex1_rewritePeepholeAt = rewritePeepholeAt ToyNoRegion.p1 1 ToyNoRegion.lhs

theorem ToyNoRegion.hex1_rewritePeephole : ToyNoRegion.ex1_rewritePeepholeAt = Com.var (ToyNoRegion.cst 0) (Com.var (ToyNoRegion.add ⟨1, ⋯⟩ ⟨0, ⋯⟩) (Com.ret ⟨2, ⋯⟩))

def ToyNoRegion.ex1_rewritePeephole : Com ToyNoRegion.Simple (↑[ToyNoRegion.Ty.int]) EffectKind.pure ToyNoRegion.Ty.int

Equations

• ToyNoRegion.ex1_rewritePeephole = rewritePeephole 100 ToyNoRegion.p1 ToyNoRegion.lhs

theorem ToyNoRegion.Hex1_rewritePeephole : ToyNoRegion.ex1_rewritePeephole = Com.var (ToyNoRegion.cst 0) (Com.var (ToyNoRegion.add ⟨1, ⋯⟩ ⟨0, ⋯⟩) (Com.ret ⟨2, ⋯⟩))

inductive ToyRegion.Ty : Type

• int: ToyRegion.Ty

instance ToyRegion.instDecidableEqTy : DecidableEq ToyRegion.Ty

Equations

• ToyRegion.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance ToyRegion.instReprTy : Repr ToyRegion.Ty

Equations

• ToyRegion.instReprTy = { reprPrec := ToyRegion.reprTy✝ }

@[reducible]

instance ToyRegion.instTyDenoteTy : TyDenote ToyRegion.Ty

Equations

• ToyRegion.instTyDenoteTy = { toType := fun (x : ToyRegion.Ty) => match x with | ToyRegion.Ty.int => BitVec 32 }

instance ToyRegion.instInhabitedToTypeTy {t : ToyRegion.Ty} : Inhabited ⟦t⟧

Equations

• ToyRegion.instInhabitedToTypeTy = { default := ToyRegion.Ty.casesOn (motive := fun (t_1 : ToyRegion.Ty) => t = t_1 → ⟦t⟧) t (fun (h : t = ToyRegion.Ty.int) => ⋯ ▸ 0#32) ⋯ }

inductive ToyRegion.Op : Type

• add: ToyRegion.Op
• const: ℤ → ToyRegion.Op
• iterate: ℕ → ToyRegion.Op

instance ToyRegion.instDecidableEqOp : DecidableEq ToyRegion.Op

Equations

• ToyRegion.instDecidableEqOp = ToyRegion.decEqOp✝

instance ToyRegion.instReprOp : Repr ToyRegion.Op

Equations

• ToyRegion.instReprOp = { reprPrec := ToyRegion.reprOp✝ }

@[reducible, inline]

abbrev ToyRegion.SimpleReg : Dialect

A simple example dialect with regions

Equations

• ToyRegion.SimpleReg = { Op := ToyRegion.Op, Ty := ToyRegion.Ty, m := Id }

@[reducible, inline]

abbrev ToyRegion.SimpleReg.int : ToyRegion.SimpleReg.Ty

Equations

• ToyRegion.SimpleReg.int = ToyRegion.Ty.int

instance ToyRegion.instDialectSignatureSimpleReg : DialectSignature ToyRegion.SimpleReg

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

instance ToyRegion.instDialectDenoteSimpleReg : DialectDenote ToyRegion.SimpleReg

Equations

• One or more equations did not get rendered due to their size.

def ToyRegion.cst {Γ : Ctxt ToyRegion.SimpleReg.Ty} (n : ℤ) : Expr ToyRegion.SimpleReg Γ EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.cst n = Expr.mk (ToyRegion.Op.const n) ToyRegion.cst.proof_1 ⋯ HVector.nil HVector.nil

def ToyRegion.add {Γ : Ctxt ToyRegion.SimpleReg.Ty} (e₁ : Γ.Var ToyRegion.SimpleReg.int) (e₂ : Γ.Var ToyRegion.SimpleReg.int) : Expr ToyRegion.SimpleReg Γ EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.add e₁ e₂ = Expr.mk ToyRegion.Op.add ToyRegion.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def ToyRegion.iterate {Γ : Ctxt ToyRegion.SimpleReg.Ty} (k : ℕ) (input : Γ.Var ToyRegion.SimpleReg.int) (body : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.impure ToyRegion.SimpleReg.int) : Expr ToyRegion.SimpleReg Γ EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.iterate k input body = Expr.mk (ToyRegion.Op.iterate k) ToyRegion.iterate.proof_1 ⋯ (input::ₕHVector.nil) (body::ₕHVector.nil)

def ToyRegion.P1.lhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

running f(x) = x + x 0 times is the identity.

Equations

• One or more equations did not get rendered due to their size.

def ToyRegion.P1.rhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.P1.rhs = Com.ret ⟨0, ToyRegion.P1.rhs.proof_1⟩

def ToyRegion.P1.p1 : PeepholeRewrite ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] ToyRegion.SimpleReg.int

Equations

• ToyRegion.P1.p1 = { lhs := ToyRegion.P1.lhs, rhs := ToyRegion.P1.rhs, correct := ToyRegion.P1.p1.proof_1 }

def ToyRegion.P2.lhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

running f(x) = x + 0 0 times is the identity.

Equations

• ToyRegion.P2.lhs = Com.var (ToyRegion.cst 0) (Com.var (ToyRegion.add ⟨0, ToyRegion.P2.lhs.proof_1⟩ ⟨1, ToyRegion.P2.lhs.proof_2⟩) (Com.ret ⟨0, ToyRegion.P2.lhs.proof_3⟩))

def ToyRegion.P2.rhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.P2.rhs = Com.ret ⟨0, ToyRegion.P2.rhs.proof_1⟩

def ToyRegion.P2.p2 : PeepholeRewrite ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] ToyRegion.SimpleReg.int

Equations

• ToyRegion.P2.p2 = { lhs := ToyRegion.P2.lhs, rhs := ToyRegion.P2.rhs, correct := ToyRegion.P2.p2.proof_1 }

def ToyRegion.P2.egLhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

example program that has the pattern 'x + 0' both at the top level, and inside a region in an iterate.

Equations

• One or more equations did not get rendered due to their size.

def ToyRegion.P2.runRewriteOnLhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

Equations

• ToyRegion.P2.runRewriteOnLhs = ↑(rewritePeepholeRecursively 100 ToyRegion.P2.p2 ToyRegion.P2.egLhs)

def ToyRegion.P2.expectedRhs : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.pure ToyRegion.SimpleReg.int

Equations

• One or more equations did not get rendered due to their size.

theorem ToyRegion.P2.rewriteDidSomething : ToyRegion.P2.runRewriteOnLhs ≠ ToyRegion.P2.lhs

theorem ToyRegion.P2.rewriteCorrect : ToyRegion.P2.runRewriteOnLhs = ToyRegion.P2.expectedRhs