def argVector.decEq : {Ty : Type} → {Γ : Ctxt Ty} → {ts : List Ty} → DecidableEq (HVector Γ.Var ts)

can decide equality on argument vectors.

Equations

• argVector.decEq = inferInstance

structure CSE.State (d : Dialect) [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} (lets : Lets d Γstart EffectKind.pure Γ) : Type

State stored by CSE pass.

• var2var : {α : d.Ty} → (v : Γ.Var α) → { v' : Γ.Var α // ∀ (V : Γstart.Valuation), lets.denote V v = lets.denote V v' }

  map variable to its canonical value

• expr2cache : (α : d.Ty) → (e : Expr d Γ EffectKind.pure α) → Option { v : Γ.Var α // ∀ (V : Γstart.Valuation), lets.denote V v = e.denote (lets.denote V) }

  map an Expr to its canonical variable

def CSE.State.empty {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} (lets : Lets d Γstart EffectKind.pure Γ) : CSE.State d lets

The empty CSEing state.

Equations

• CSE.State.empty lets = { var2var := fun {α : d.Ty} (v : Γ.Var α) => ⟨v, ⋯⟩, expr2cache := fun (α : d.Ty) (e : Expr d Γ EffectKind.pure α) => none }

def CSE.State.snocNewExpr2Cache {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} [DecidableEq d.Ty] [DecidableEq d.Op] {Γ : Ctxt d.Ty} {α : d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (s : CSE.State d lets) (e : Expr d Γ EffectKind.pure α) : CSE.State d (lets.var e)

Equations

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

@[simp]

theorem CSE.Lets.denote_var {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {α : d.Ty} {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (e : Expr d Γ EffectKind.pure α) (V : Γstart.Valuation) : (lets.var e).denote V = (lets.denote V::ᵥe.denote (lets.denote V))

denoting a var is the same as snocing the denotation of e onto the old valuation V.

def Ctxt.Hom.remapLast {d : Dialect} [TyDenote d.Ty] {α : d.Ty} (Γ : Ctxt d.Ty) (var : Γ.Var α) : (Γ.snoc α).Hom Γ

Remap the last variable in a context, to get a new context without the last variable

Equations

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

def CSE.VarRemapVar {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {β : d.Ty} [DecidableEq d.Ty] [DecidableEq d.Op] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {Γ' : Ctxt d.Ty} {α : d.Ty} (lets : Lets d Γstart EffectKind.pure Γ) (hom : Γ'.Hom Γ) (vold : Γ.Var α) (vnew : Γ'.Var α) (VNEW : ∀ (Vstart : Γstart.Valuation), lets.denote Vstart vold = Ctxt.Valuation.comap (lets.denote Vstart) hom vnew) (w' : Γ'.Var β) : { w : Γ.Var β // ∀ (Vstart : Γstart.Valuation), lets.denote Vstart w = Ctxt.Valuation.comap (lets.denote Vstart) hom w' }

Equations

• CSE.VarRemapVar lets hom vold vnew VNEW w' = if TY : β = α then if H : TY ▸ w' = vnew then ⟨⋯ ▸ vold, ⋯⟩ else ⟨hom w', ⋯⟩ else ⟨hom w', ⋯⟩

def CSE.arglistRemapVar {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [DecidableEq d.Ty] [DecidableEq d.Op] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {Γ' : Ctxt d.Ty} {α : d.Ty} (lets : Lets d Γstart EffectKind.pure Γ) (hom : Γ'.Hom Γ) (vold : Γ.Var α) (vnew : Γ'.Var α) (VNEW : ∀ (Vstart : Γstart.Valuation), lets.denote Vstart vold = Ctxt.Valuation.comap (lets.denote Vstart) hom vnew) {ts : List d.Ty} (as' : HVector Γ'.Var ts) : { as : HVector Γ.Var ts // ∀ (Vstart : Γstart.Valuation), HVector.map (fun (t : d.Ty) (v : Γ.Var t) => lets.denote Vstart v) as = HVector.map (fun (t : d.Ty) (v' : Γ'.Var t) => Ctxt.Valuation.comap (lets.denote Vstart) hom v') as' }

Equations

• One or more equations did not get rendered due to their size.
• CSE.arglistRemapVar lets hom vold vnew VNEW HVector.nil = ⟨HVector.nil, ⋯⟩

def CSE.ExprRemapVar {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {β : d.Ty} [DecidableEq d.Ty] [DecidableEq d.Op] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {Γ' : Ctxt d.Ty} {α : d.Ty} (lets : Lets d Γstart EffectKind.pure Γ) (hom : Γ'.Hom Γ) (vold : Γ.Var α) (vnew : Γ'.Var α) (VNEW : ∀ (Vstart : Γstart.Valuation), lets.denote Vstart vold = Ctxt.Valuation.comap (lets.denote Vstart) hom vnew) (e' : Expr d Γ' EffectKind.pure β) : { e : Expr d Γ EffectKind.pure β // ∀ (Vstart : Γstart.Valuation), e.denote (lets.denote Vstart) = e'.denote (Ctxt.Valuation.comap (lets.denote Vstart) hom) }

Equations

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

def CSE.State.snocOldExpr2Cache {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} [DecidableEq d.Ty] [DecidableEq d.Op] {Γ : Ctxt d.Ty} {α : d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (s : CSE.State d lets) (enew : Expr d Γ EffectKind.pure α) (eold : Expr d Γ EffectKind.pure α) (henew : ∀ (V : Γstart.Valuation), enew.denote (lets.denote V) = eold.denote (lets.denote V)) (vold : Γ.Var α) (hv : ∀ (V : Γstart.Valuation), eold.denote (lets.denote V) = lets.denote V vold) : CSE.State d (lets.var enew)

Equations

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

def CSE.State.cseArgList {d : Dialect} [Monad d.m] [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (s : CSE.State d lets) {ts : List d.Ty} (as : HVector Γ.Var ts) : { as' : HVector Γ.Var ts // ∀ (V : Γstart.Valuation), HVector.map (Ctxt.Valuation.eval (lets.denote V)) as = HVector.map (Ctxt.Valuation.eval (lets.denote V)) as' }

Replace the variables in as with new variables that have the same valuation

Equations

• s.cseArgList HVector.nil = ⟨HVector.nil, ⋯⟩
• s.cseArgList (a'::ₕas'_1) = match s.var2var a' with | ⟨a'_1, ha'⟩ => match s.cseArgList as'_1 with | ⟨as', has'⟩ => ⟨a'_1::ₕas', ⋯⟩

instance CSE.instInhabitedForallForallStateForallForallSubtypeHVectorProdCtxtTyComImpureEqForallValuationFstToMonadMToTypeSndDenote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} : Inhabited ({lets : Lets d Γstart EffectKind.pure Γ} → CSE.State d lets → {ts : List (Ctxt d.Ty × d.Ty)} → (rs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts) → { rs' : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts // rs.denote = rs'.denote })

Default instance for partial def to compile.

Equations

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

instance CSE.instInhabitedForallForallStateForallSubtypeComPureForallEqToMonadMToTypeTyDenote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {α : d.Ty} : Inhabited ({lets : Lets d Γstart EffectKind.pure Γ} → CSE.State d lets → (com : Com d Γ EffectKind.pure α) → { com' : Com d Γ EffectKind.pure α // ∀ (V : Γ.Valuation), com.denote V = com'.denote V })

Default instance for partial def to compile.

Equations

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

unsafe def CSE.State.cseRegionArgList {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [DecidableEq d.Ty] [DecidableEq d.Op] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} : CSE.State d lets → {ts : List (Ctxt d.Ty × d.Ty)} → (rs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts) → { rs' : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts // rs.denote = rs'.denote }

Replace the regions in rs with new regions that have the same valuation

unsafe def CSE.State.cseExpr {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [DecidableEq d.Ty] [DecidableEq d.Op] {α : d.Ty} {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (s : CSE.State d lets) (e : Expr d Γ EffectKind.pure α) : { e' : Expr d Γ EffectKind.pure α // ∀ (V : Γstart.Valuation), e'.denote (lets.denote V) = e.denote (lets.denote V) } × Option { v' : Γ.Var α // ∀ (V : Γstart.Valuation), lets.denote V v' = e.denote (lets.denote V) }

lookup an expression in the state and return a corresponding CSE'd variable for it, along with the CSE'd expression that was looked up in the map for the variable.

unsafe def CSE.State.cseCom {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [DecidableEq d.Ty] [DecidableEq d.Op] {Γstart : Ctxt d.Ty} {Γ : Ctxt d.Ty} {α : d.Ty} {lets : Lets d Γstart EffectKind.pure Γ} (s : CSE.State d lets) (com : Com d Γ EffectKind.pure α) : { com' : Com d Γ EffectKind.pure α // ∀ (V : Γstart.Valuation), com.denote (lets.denote V) = com'.denote (lets.denote V) }

unsafe def CSE.cse' {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [DecidableEq d.Ty] [DecidableEq d.Op] {α : d.Ty} {Γ : Ctxt d.Ty} (com : Com d Γ EffectKind.pure α) : { com' : Com d Γ EffectKind.pure α // ∀ (V : Γ.Valuation), com.denote V = com'.denote V }

common subexpression elimination entry point.

inductive CSE.Examples.ExTy : Type

A very simple type universe.

• nat: CSE.Examples.ExTy
• bool: CSE.Examples.ExTy

instance CSE.Examples.instDecidableEqExTy : DecidableEq CSE.Examples.ExTy

Equations

• CSE.Examples.instDecidableEqExTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CSE.Examples.instReprExTy : Repr CSE.Examples.ExTy

Equations

• CSE.Examples.instReprExTy = { reprPrec := CSE.Examples.reprExTy✝ }

@[reducible]

instance CSE.Examples.instTyDenoteExTy : TyDenote CSE.Examples.ExTy

Equations

• CSE.Examples.instTyDenoteExTy = { toType := fun (x : CSE.Examples.ExTy) => match x with | CSE.Examples.ExTy.nat => ℕ | CSE.Examples.ExTy.bool => Bool }

inductive CSE.Examples.ExOp : Type

• add: CSE.Examples.ExOp
• beq: CSE.Examples.ExOp
• cst: ℕ → CSE.Examples.ExOp

instance CSE.Examples.instDecidableEqExOp : DecidableEq CSE.Examples.ExOp

Equations

• CSE.Examples.instDecidableEqExOp = CSE.Examples.decEqExOp✝

instance CSE.Examples.instReprExOp : Repr CSE.Examples.ExOp

Equations

• CSE.Examples.instReprExOp = { reprPrec := CSE.Examples.reprExOp✝ }

@[reducible, inline]

abbrev CSE.Examples.Ex : Dialect

Equations

• CSE.Examples.Ex = { Op := CSE.Examples.ExOp, Ty := CSE.Examples.ExTy, m := Id }

instance CSE.Examples.instDialectSignatureEx : DialectSignature CSE.Examples.Ex

Equations

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

@[reducible]

instance CSE.Examples.instDialectDenoteEx : DialectDenote CSE.Examples.Ex

Equations

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

def CSE.Examples.cst {Γ : Ctxt CSE.Examples.Ex.Ty} (n : ℕ) : Expr CSE.Examples.Ex Γ EffectKind.pure CSE.Examples.ExTy.nat

Equations

• CSE.Examples.cst n = Expr.mk (CSE.Examples.ExOp.cst n) CSE.Examples.cst.proof_1 ⋯ HVector.nil HVector.nil

def CSE.Examples.add {Γ : Ctxt CSE.Examples.Ex.Ty} (e₁ : Γ.Var CSE.Examples.ExTy.nat) (e₂ : Γ.Var CSE.Examples.ExTy.nat) : Expr CSE.Examples.Ex Γ EffectKind.pure CSE.Examples.ExTy.nat

Equations

• CSE.Examples.add e₁ e₂ = Expr.mk CSE.Examples.ExOp.add CSE.Examples.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def CSE.Examples.ex1_pre_cse : Com CSE.Examples.Ex ∅ EffectKind.pure CSE.Examples.ExTy.nat

Equations

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

unsafe def CSE.Examples.ex1_post_cse : { com' : Com CSE.Examples.Ex ∅ EffectKind.pure CSE.Examples.ExTy.nat // ∀ (V : ∅.Valuation), CSE.Examples.ex1_pre_cse.denote V = com'.denote V }

unsafe def CSE.Examples.ex1_post_cse_post_dce : { com : Com CSE.Examples.Ex ∅ EffectKind.pure CSE.Examples.ExTy.nat // ∀ (V : ∅.Valuation), (↑CSE.Examples.ex1_post_cse).denote V = com.denote V }