def Ctxt.delete {Ty : Type} {α : Ty} (Γ : Ctxt Ty) (v : Γ.Var α) : Ctxt Ty

Delete a variable from a list.

Equations

• Γ.delete v = List.eraseIdx Γ ↑v

def Deleted {Ty : Type} {α : Ty} (Γ : Ctxt Ty) (v : Γ.Var α) (Γ' : Ctxt Ty) : Prop

Witness that Γ' is Γ without v

Equations

• Deleted Γ v Γ' = (Γ' = Γ.delete v)

def Deleted.deleteSnoc {Ty : Type} (Γ : Ctxt Ty) (α : Ty) : Deleted (Γ.snoc α) (Ctxt.Var.last Γ α) Γ

build a Deleted for a (Γ.snoc α) → Γ

Equations

• ⋯ = ⋯

theorem List.eraseIdx_succ : ∀ {α : Type u_1} {x : α} {xs : List α} {n : ℕ}, (x :: xs).eraseIdx n.succ = x :: xs.eraseIdx n

theorem List.eraseIdx_eq_len_concat : ∀ {α : Type u_1} {xs : List α} {x : α}, (xs ++ [x]).eraseIdx xs.length = xs

theorem List.get?_eraseIdx_of_lt {k : ℕ} {n : ℕ} : ∀ {α : Type u_1} {xs : List α}, k < n → (xs.eraseIdx n).get? k = xs.get? k

theorem List.get?_eraseIdx_of_le {α : Type u_1} {xs : List α} {n : ℕ} {k : ℕ} (hk : n ≤ k) : (xs.eraseIdx n).get? k = xs.get? (k + 1)

Removing index n shifts entires of k ≥ n by 1.

def Deleted.pullback_var : {Ty : Type} → {Γ : Ctxt Ty} → {t : Ty} → {delv : Γ.Var t} → {Γ' : Ctxt Ty} → {β : Ty} → Deleted Γ delv Γ' → Γ'.Var β → Γ.Var β

Given Γ' := Γ /delv, transport a variable from Γ' to Γ.

Equations

• DEL.pullback_var v = if DELV : ↑v < ↑delv then ⟨↑v, ⋯⟩ else ⟨↑v + 1, ⋯⟩

def Deleted.pushforward_Valuation {Ty : Type} [TyDenote Ty] {α : Ty} {Γ : Ctxt Ty} {Γ' : Ctxt Ty} {delv : Γ.Var α} (DEL : Deleted Γ delv Γ') (vΓ : Γ.Valuation) : Γ'.Valuation

Equations

• DEL.pushforward_Valuation vΓ v' = vΓ (DEL.pullback_var v')

theorem Deleted.pushforward_Valuation_denote {Ty : Type} [TyDenote Ty] {α : Ty} {Γ : Ctxt Ty} {Γ' : Ctxt Ty} {delv : Γ.Var α} (DEL : Deleted Γ delv Γ') (vΓ : Γ.Valuation) (v' : Γ'.Var α) : vΓ (DEL.pullback_var v') = DEL.pushforward_Valuation vΓ v'

def Var.tryDelete? {Ty : Type} {α : Ty} {β : Ty} [TyDenote Ty] {Γ : Ctxt Ty} {Γ' : Ctxt Ty} {delv : Γ.Var α} (DEL : Deleted Γ delv Γ') (v : Γ.Var β) : Option { v' : Γ'.Var β // ∀ (V : Γ.Valuation), V.eval v = (DEL.pushforward_Valuation V).eval v' }

Given Γ' := Γ/delv, transport a variable from Γ to Γ', if v ≠ delv`.

Equations

• Var.tryDelete? DEL v = if VEQ : ↑v = ↑delv then none else if VLT : ↑v < ↑delv then some ⟨⟨↑v, ⋯⟩, ⋯⟩ else some ⟨⟨↑v - 1, ⋯⟩, ⋯⟩

theorem DCE.Deleted.pushforward_Valuation_snoc {d : Dialect} [TyDenote d.Ty] {α : d.Ty} {Γ : Ctxt d.Ty} {Γ' : Ctxt d.Ty} {ω : d.Ty} {delv : Γ.Var α} (DEL : Deleted Γ delv Γ') (DELω : Deleted (Γ.snoc ω) (↑delv) (Γ'.snoc ω)) (V : Γ.Valuation) {newv : ⟦ω⟧} : DELω.pushforward_Valuation (V::ᵥnewv) = (DEL.pushforward_Valuation V::ᵥnewv)

pushforward (V :: newv) = (pushforward V) :: newv

def DCE.arglistDeleteVar? {d : Dialect} [TyDenote d.Ty] {α : d.Ty} {Γ : Ctxt d.Ty} {delv : Γ.Var α} {Γ' : Ctxt d.Ty} {ts : List d.Ty} (DEL : Deleted Γ delv Γ') (as : HVector Γ.Var ts) : Option { as' : HVector Γ'.Var ts // ∀ (V : Γ.Valuation), HVector.map V.eval as = HVector.map (DEL.pushforward_Valuation V).eval as' }

Try to delete the variable from the argument list. Succeeds if variable does not occur in the argument list. Fails otherwise.

Equations

• One or more equations did not get rendered due to their size.
• DCE.arglistDeleteVar? DEL HVector.nil = some ⟨HVector.nil, ⋯⟩

def DCE.Expr.deleteVar? {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} : {t : d.Ty} → {delv : Γ.Var t} → {Γ' : Ctxt d.Ty} → {t_1 : d.Ty} → (DEL : Deleted Γ delv Γ') → (e : Expr d Γ EffectKind.pure t_1) → Option { e' : Expr d Γ' EffectKind.pure t_1 // ∀ (V : Γ.Valuation), e.denote V = e'.denote (DEL.pushforward_Valuation V) }

Equations

• DCE.Expr.deleteVar? DEL (Expr.mk op ty_eq eff_le args regArgs) = match DCE.arglistDeleteVar? DEL args with | none => none | some args' => some ⟨Expr.mk op ty_eq eff_le (↑args') regArgs, ⋯⟩

def DCE.Deleted.snoc {d : Dialect} {Γ' : Ctxt d.Ty} {ω : d.Ty} {α : d.Ty} {Γ : Ctxt d.Ty} {v : Γ.Var α} (DEL : Deleted Γ v Γ') : Deleted (Γ.snoc ω) (↑v) (Γ'.snoc ω)

snoc an ω to both the input and output contexts of Deleted Γ v Γ'

Equations

• ⋯ = ⋯

@[irreducible]

def DCE.Com.deleteVar? {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} : {t : d.Ty} → {delv : Γ.Var t} → {Γ' : Ctxt d.Ty} → {t_1 : d.Ty} → (DEL : Deleted Γ delv Γ') → (com : Com d Γ EffectKind.pure t_1) → Option { com' : Com d Γ' EffectKind.pure t_1 // ∀ (V : Γ.Valuation), com.denote V = com'.denote (DEL.pushforward_Valuation V) }

Delete a variable from an Com.

Equations

• One or more equations did not get rendered due to their size.
• DCE.Com.deleteVar? DEL (Com.ret v) = match Var.tryDelete? DEL v with | none => none | some ⟨v_1, hv⟩ => some ⟨Com.ret v_1, ⋯⟩

def DCE.DCEType {d : Dialect} [TyDenote d.Ty] [Monad d.m] [DialectSignature d] [DialectDenote d] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : Type

Declare the type of DCE up-front, so we can declare an Inhabited instance. This is necessary so that we can mark the DCE implementation as a partial def and ensure that Lean does not freak out on us, since it's indeed unclear to Lean that the output type of dce is always inhabited.

Equations

• DCE.DCEType com = ((Γ' : Ctxt d.Ty) × (hom : Γ'.Hom Γ) × { com' : Com d Γ' EffectKind.pure t // ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom) })

instance DCE.instInhabitedDCEType {d : Dialect} [TyDenote d.Ty] [Monad d.m] [SIG : DialectSignature d] [DENOTE : DialectDenote d] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : Inhabited (DCE.DCEType com)

Show that DCEType in inhabited.

Equations

• DCE.instInhabitedDCEType com = { default := ⟨Γ, ⟨Ctxt.Hom.id, ⟨com, ⋯⟩⟩⟩ }

partial def DCE.dce_ {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : DCE.DCEType com

walk the list of bindings, and for each let, try to delete the variable defined by the let in the body/ Note that this is O(n^2), for an easy proofs, as it is written as a forward pass. The fast O(n) version is a backward pass.

def DCE.dce {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : (Γ' : Ctxt d.Ty) × (hom : Γ'.Hom Γ) × { com' : Com d Γ' EffectKind.pure t // ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom) }

This is the real entrypoint to dce which unfolds the type of dce_, where we play the DCEType trick to convince Lean that the output type is in fact inhabited.

Equations

• DCE.dce com = DCE.dce_ com

def DCE.dce' {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : { com' : Com d Γ EffectKind.pure t // ∀ (V : Γ.Valuation), com.denote V = com'.denote V }

A version of DCE that returns an output program with the same context. It uses the context morphism of dce to adapt the result of DCE to work with the original context

Equations

• DCE.dce' com = match DCE.dce_ com with | ⟨Γ', ⟨hom, ⟨com', hcom'⟩⟩⟩ => ⟨com'.changeVars hom, ⋯⟩

inductive DCE.Examples.ExTy : Type

A very simple type universe.

• nat: DCE.Examples.ExTy
• bool: DCE.Examples.ExTy

instance DCE.Examples.instDecidableEqExTy : DecidableEq DCE.Examples.ExTy

Equations

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

instance DCE.Examples.instReprExTy : Repr DCE.Examples.ExTy

Equations

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

@[reducible]

instance DCE.Examples.instTyDenoteExTy : TyDenote DCE.Examples.ExTy

Equations

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

inductive DCE.Examples.ExOp : Type

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

instance DCE.Examples.instDecidableEqExOp : DecidableEq DCE.Examples.ExOp

Equations

• DCE.Examples.instDecidableEqExOp = DCE.Examples.decEqExOp✝

@[reducible, inline]

abbrev DCE.Examples.Ex : Dialect

Equations

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

instance DCE.Examples.instDialectSignatureEx : DialectSignature DCE.Examples.Ex

Equations

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

@[reducible]

instance DCE.Examples.instDialectDenoteEx : DialectDenote DCE.Examples.Ex

Equations

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

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

Equations

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

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

Equations

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

def DCE.Examples.ex1_pre_dce : Com DCE.Examples.Ex ∅ EffectKind.pure DCE.Examples.ExTy.nat

Equations

• DCE.Examples.ex1_pre_dce = Com.var (DCE.Examples.cst 1) (Com.var (DCE.Examples.cst 2) (Com.ret ⟨0, DCE.Examples.ex1_pre_dce.proof_1⟩))

def DCE.Examples.ex1_post_dce : Com DCE.Examples.Ex ∅ EffectKind.pure DCE.Examples.ExTy.nat

TODO: how do we evaluate 'ex1_post_dce' within Lean? :D

Equations

• DCE.Examples.ex1_post_dce = ↑(DCE.dce' DCE.Examples.ex1_pre_dce)

def DCE.Examples.ex1_post_dce_expected : Com DCE.Examples.Ex ∅ EffectKind.pure DCE.Examples.ExTy.nat

Equations

• DCE.Examples.ex1_post_dce_expected = Com.var (DCE.Examples.cst 1) (Com.ret ⟨0, DCE.Examples.ex1_post_dce_expected.proof_1⟩)