NOTE: Monadic Code Needs Pointfree Theorems

It is always best to write theorems in unapplied fashion, since a monadic function is often used in chains of binds.

A theorem of the form 'f1 x = f2 x'cannot be used in a context 'f1 >>= g', but a pointfree theorem of the form 'f = g'permits rewriting everywhere, even in 'f1 >>= g'.

This is not a problem in pure code, since we rarely use poinfree style with (f ∘ g), but this is much more pervasive in monadic code, where 'f >>= g' is common.

Thus, the rule is that ALL rewrite rules are written pointfree in the last argument.

NOTE: Normal form for monadic code

We never use functor and applicative instances. Rather, we always write definitions in terms of monadic code, using 'non-canonical' haskell code such as mv >>= (fun v => return (g v)) rather than writing the more natural g <$> mv since it is much easier to design simp sets and tactics that consistenty simplify monadic bind, instead of a combination of: <$>, <*>, return, pure, >>=.

Furthermore, consistent use of >>= simplifes reasoning about information flow, where left-to-right order clearly implies the direction of information flow.

theorem Pure.pure_cast {β : Type u_1} {α : Type u_1} {f : Type u_1 → Type u_2} [inst : Pure f] (b : β) (h : β = α) : pure (cast h b) = cast ⋯ (pure b)

@[reducible, inline]

abbrev RegionSignature (Ty : Type) : Type

Equations

• RegionSignature Ty = List (Ctxt Ty × Ty)

structure Signature (Ty : Type) : Type

• mkEffectful :: (
• sig : List Ty
• regSig : RegionSignature Ty
• outTy : Ty
• effectKind : EffectKind
• )

@[reducible, inline]

abbrev Signature.mk {Ty : Type} (sig : List Ty) (regSig : RegionSignature Ty) (outTy : Ty) : Signature Ty

Equations

• Signature.mk sig regSig outTy = { sig := sig, regSig := regSig, outTy := outTy, effectKind := EffectKind.pure }

class DialectSignature (d : Dialect) : Type

• signature : d.Op → Signature d.Ty

def DialectSignature.sig {d : Dialect} [s : DialectSignature d] : d.Op → List d.Ty

Equations

• DialectSignature.sig = Signature.sig ∘ signature

def DialectSignature.regSig {d : Dialect} [s : DialectSignature d] : d.Op → RegionSignature d.Ty

Equations

• DialectSignature.regSig = Signature.regSig ∘ signature

def DialectSignature.outTy {d : Dialect} [s : DialectSignature d] : d.Op → d.Ty

Equations

• DialectSignature.outTy = Signature.outTy ∘ signature

def DialectSignature.effectKind {d : Dialect} [s : DialectSignature d] : d.Op → EffectKind

Equations

• DialectSignature.effectKind = Signature.effectKind ∘ signature

class DialectDenote (d : Dialect) [TyDenote d.Ty] [DialectSignature d] : Type

• denote : (op : d.Op) → HVector TyDenote.toType (DialectSignature.sig op) → HVector (fun (t : Ctxt d.Ty × d.Ty) => t.1.Valuation → EffectKind.impure.toMonad d.m ⟦t.2⟧) (DialectSignature.regSig op) → (DialectSignature.effectKind op).toMonad d.m ⟦DialectSignature.outTy op⟧

inductive Expr (d : Dialect) [DialectSignature d] (Γ : Ctxt d.Ty) (eff : EffectKind) (ty : d.Ty) : Type

An intrinsically typed expression whose effect is at most EffectKind

• mk: {d : Dialect} → [inst : DialectSignature d] → {eff : EffectKind} → {Γ : Ctxt d.Ty} → {ty : d.Ty} → (op : d.Op) → ty = DialectSignature.outTy op → DialectSignature.effectKind op ≤ eff → HVector Γ.Var (DialectSignature.sig op) → HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op) → Expr d Γ eff ty

inductive Com (d : Dialect) [DialectSignature d] : Ctxt d.Ty → EffectKind → d.Ty → Type

A very simple intrinsically typed program: a sequence of let bindings. Note that the EffectKind is uniform: if a Com is pure, then the expression and its body are pure, and if a Com is impure, then both the expression and the body are impure!

• ret: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → {t : d.Ty} → {eff : EffectKind} → Γ.Var t → Com d Γ eff t
• var: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → {eff : EffectKind} → {α β : d.Ty} → Expr d Γ eff α → Com d (Γ.snoc α) eff β → Com d Γ eff β

inductive Lets (d : Dialect) [DialectSignature d] (Γ_in : Ctxt d.Ty) (eff : EffectKind) (Γ_out : Ctxt d.Ty) : Type

Lets d Γ_in Γ_out is a sequence of lets which are well-formed under context Γ_out and result in context Γ_in.

• nil: {d : Dialect} → [inst : DialectSignature d] → {Γ_in : Ctxt d.Ty} → {eff : EffectKind} → Lets d Γ_in eff Γ_in
• var: {d : Dialect} → [inst : DialectSignature d] → {Γ_in : Ctxt d.Ty} → {eff : EffectKind} → {Γ_out : Ctxt d.Ty} → {t : d.Ty} → Lets d Γ_in eff Γ_out → Expr d Γ_out eff t → Lets d Γ_in eff (Γ_out.snoc t)

structure Zipper (d : Dialect) [DialectSignature d] (Γ_in : Ctxt d.Ty) (eff : EffectKind) (Γ_mid : Ctxt d.Ty) (ty : d.Ty) : Type

Zipper d Γ_in eff Γ_mid ty represents a particular position in a program, by storing the Lets that come before this position separately from the Com that represents the rest. Thus, Γ_in is the context of the program as a whole, while Γ_mid is the context at the current position.

While technically the position is in between two let-bindings, by convention we say that the first binding of top : Lets .. is the current binding of a particular zipper.

• top : Lets d Γ_in eff Γ_mid

  The let-bindings at the top of the zipper

• bot : Com d Γ_mid eff ty

  The program at the bottom of the zipper

partial def reprRegArgsAux {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] [Repr d.Ty] {ts : List (Ctxt d.Ty × d.Ty)} (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts) : List Lean.Format

Convert a HVector of region arguments into a List of format strings.

partial def Expr.repr {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : ℕ → Expr d Γ eff t → Lean.Format

partial def Com.repr {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (prec : ℕ) (com : Com d Γ eff t) : Lean.Format

Format string for a Com, with the region parentheses and formal argument list.

partial def comReprAux {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (prec : ℕ) : Com d Γ eff t → Lean.Format

Format string for sequence of assignments and return in a Com.

def Lets.repr {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {eff : Ctxt d.Ty} {Γ : EffectKind} {t : Ctxt d.Ty} (prec : ℕ) : Lets d eff Γ t → Lean.Format

Equations

• Lets.repr prec Lets.nil = Lean.Format.align false ++ Lean.format ";"
• Lets.repr prec (body.var e) = Lets.repr prec body ++ (Lean.Format.align false ++ (Lean.format "" ++ Lean.format (Expr.repr prec e) ++ Lean.format ""))

instance instReprExpr {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Repr (Expr d Γ eff t)

Equations

• instReprExpr = { reprPrec := flip Expr.repr }

instance instReprCom {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Repr (Com d Γ eff t)

Equations

• instReprCom = { reprPrec := flip Com.repr }

instance instReprLets {d : Dialect} [DialectSignature d] [Repr d.Op] [Repr d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : Ctxt d.Ty} : Repr (Lets d Γ eff t)

Equations

• instReprLets = { reprPrec := flip Lets.repr }

@[irreducible]

instance HVector.decidableEqReg {d : Dialect} [DialectSignature d] [DecidableEq d.Op] [DecidableEq d.Ty] {l : List (Ctxt d.Ty × d.Ty)} : DecidableEq (HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) l)

Equations

• HVector.nil.decidableEqReg HVector.nil = isTrue ⋯
• (x₁::ₕv₁).decidableEqReg (x₂::ₕv₂) = decidable_of_iff (x₁ = x₂ ∧ v₁ = v₂) ⋯

@[irreducible]

instance Expr.decidableEq {d : Dialect} [DialectSignature d] {eff : EffectKind} [DecidableEq d.Op] [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {ty : d.Ty} : DecidableEq (Expr d Γ eff ty)

Equations

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

@[irreducible]

instance Com.decidableEq {d : Dialect} [DialectSignature d] [DecidableEq d.Op] [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : DecidableEq (Com d Γ eff ty)

Equations

• One or more equations did not get rendered due to their size.
• (Com.ret v₁).decidableEq (Com.ret v₂) = decidable_of_iff (v₁ = v₂) ⋯
• (Com.ret v).decidableEq (Com.var e body) = isFalse ⋯
• (Com.var e body).decidableEq (Com.ret v) = isFalse ⋯

def Com.recAux' {d : Dialect} [DialectSignature d] {motive : {Γ : Ctxt d.Ty} → {eff : EffectKind} → {t : d.Ty} → Com d Γ eff t → Sort u} (ret : {Γ : Ctxt d.Ty} → {t : d.Ty} → {eff : EffectKind} → (v : Γ.Var t) → motive (Com.ret v)) (var : {Γ : Ctxt d.Ty} → {t u : d.Ty} → {eff : EffectKind} → (e : Expr d Γ eff t) → (body : Com d (Γ.snoc t) eff u) → motive body → motive (Com.var e body)) {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : motive com

Equations

• One or more equations did not get rendered due to their size.
• Com.recAux' ret var (Com.ret v) = ret v

@[implemented_by Com.recAux']

def Com.rec' {d : Dialect} [DialectSignature d] {motive : {Γ : Ctxt d.Ty} → {eff : EffectKind} → {t : d.Ty} → Com d Γ eff t → Sort u} (ret : {Γ : Ctxt d.Ty} → {t : d.Ty} → {eff : EffectKind} → (v : Γ.Var t) → motive (Com.ret v)) (var : {Γ : Ctxt d.Ty} → {t u : d.Ty} → {eff : EffectKind} → (e : Expr d Γ eff t) → (body : Com d (Γ.snoc t) eff u) → motive body → motive (Com.var e body)) {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : motive com

Equations

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

@[simp]

theorem Com.rec'_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (v : Γ.Var t) {motive : {Γ : Ctxt d.Ty} → {eff : EffectKind} → {t : d.Ty} → Com d Γ eff t → Sort u_1} {eff : EffectKind} {ret : {Γ : Ctxt d.Ty} → {t : d.Ty} → {eff : EffectKind} → (v : Γ.Var t) → motive (Com.ret v)} {var : {Γ : Ctxt d.Ty} → {t u : d.Ty} → {eff : EffectKind} → (e : Expr d Γ eff t) → (body : Com d (Γ.snoc t) eff u) → motive body → motive (Com.var e body)} : Com.rec' ret var (Com.ret v) = ret v

@[simp]

theorem Com.rec'_var {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {u : d.Ty} (e : Expr d Γ eff t) (body : Com d (Γ.snoc t) eff u) {motive : {Γ : Ctxt d.Ty} → {eff : EffectKind} → {t : d.Ty} → Com d Γ eff t → Sort u_1} {ret : {Γ : Ctxt d.Ty} → {t : d.Ty} → {eff : EffectKind} → (v : Γ.Var t) → motive (Com.ret v)} {var : {Γ : Ctxt d.Ty} → {t u : d.Ty} → {eff : EffectKind} → (e : Expr d Γ eff t) → (body : Com d (Γ.snoc t) eff u) → motive body → motive (Com.var e body)} : Com.rec' ret var (Com.var e body) = var e body (Com.rec' (fun {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} => ret) (fun {Γ : Ctxt d.Ty} {t u : d.Ty} {eff : EffectKind} => var) body)

theorem Com.recAux'_eq {d : Dialect} [DialectSignature d] {motive : {Γ : Ctxt d.Ty} → {eff : EffectKind} → {t : d.Ty} → Com d Γ eff t → Sort u} : Com.recAux' = Com.rec'

def Com.recPure {d : Dialect} [DialectSignature d] {motive : {Γ : Ctxt d.Ty} → {t : d.Ty} → Com d Γ EffectKind.pure t → Sort u} (ret : {Γ : Ctxt d.Ty} → {t : d.Ty} → (v : Γ.Var t) → motive (Com.ret v)) (var : {Γ : Ctxt d.Ty} → {t u : d.Ty} → (e : Expr d Γ EffectKind.pure t) → (body : Com d (Γ.snoc t) EffectKind.pure u) → motive body → motive (Com.var e body)) {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : motive com

Alternative recursion principle for known-pure Coms

Equations

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

def Expr.op {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) : d.Op

Equations

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

theorem Expr.eff_le {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ : Ctxt d.Ty} {ty : d.Ty} (e : Expr d Γ eff ty) : DialectSignature.effectKind e.op ≤ eff

theorem Expr.ty_eq {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ : Ctxt d.Ty} {ty : d.Ty} (e : Expr d Γ eff ty) : ty = DialectSignature.outTy e.op

def Expr.args {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ : Ctxt d.Ty} {ty : d.Ty} (e : Expr d Γ eff ty) : HVector Γ.Var (DialectSignature.sig e.op)

Equations

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

def Expr.regArgs {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ : Ctxt d.Ty} {ty : d.Ty} (e : Expr d Γ eff ty) : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig e.op)

Equations

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

Projection equations for Expr

@[simp]

theorem Expr.op_mk {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) : (Expr.mk op ty_eq eff_le args regArgs).op = op

@[simp]

theorem Expr.args_mk {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) : (Expr.mk op ty_eq eff_le args regArgs).args = args

@[simp]

theorem Expr.regArgs_mk {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) : (Expr.mk op ty_eq eff_le args regArgs).regArgs = regArgs

size

def Com.size {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Com d Γ eff t → ℕ

The size of a Com is given by the number of let-bindings it contains

Equations

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

@[simp]

theorem Com.size_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {v : Γ.Var t} : (Com.ret v).size = 0

@[simp]

theorem Com.size_var {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : ∀ {ty : d.Ty} {e : Expr d Γ eff ty} {body : Com d (Γ.snoc ty) eff t}, (Com.var e body).size = body.size + 1

Com projections and simple conversions

def Com.outContext {d : Dialect} [DialectSignature d] {eff : EffectKind} {t : d.Ty} {Γ : Ctxt d.Ty} : Com d Γ eff t → Ctxt d.Ty

The outContext of a program is a context which includes variables for all let-bindings of the program. That is, it is the context under which the return value is typed

Equations

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

def Com.outContextDiff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : Γ.Diff com.outContext

The difference between the context Γ under which com is typed, and the output context of that same com

Equations

• com.outContextDiff = ⟨com.size, ⋯⟩

def Com.outContextHom {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : Γ.Hom com.outContext

com.outContextHom is the canonical homorphism from free variables of com to those same variables in the output context of com

Equations

• com.outContextHom = com.outContextDiff.toHom

def Com.returnVar {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : com.outContext.Var t

The return variable of a program

Equations

• (Com.ret v).returnVar = v
• (Com.var e body).returnVar = body.returnVar

@[simp]

theorem Com.outContext_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} (v : Γ.Var t) : (Com.ret v).outContext = Γ

@[simp]

theorem Com.outContext_var {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {u : d.Ty} {eff : EffectKind} (e : Expr d Γ eff t) (body : Com d (Γ.snoc t) eff u) : (Com.var e body).outContext = body.outContext

@[simp]

theorem Com.outContextHom_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} (v : Γ.Var t) : (Com.ret v).outContextHom = Ctxt.Hom.id

@[simp]

theorem Com.outContextHom_var {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : ∀ {ty : d.Ty} {e : Expr d Γ eff ty} {body : Com d (Γ.snoc ty) eff t}, (Com.var e body).outContextHom = body.outContextHom.unSnoc

@[simp]

theorem Com.returnVar_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {v : Γ.Var t} : (Com.ret v).returnVar = v

@[simp]

theorem Com.returnVar_var {d : Dialect} [DialectSignature d] {eff : EffectKind} : ∀ {Γ : Ctxt d.Ty} {ty : d.Ty} {e : Expr d Γ eff ty} {a : d.Ty} {body : Com d (Γ.snoc ty) eff a}, (Com.var e body).returnVar = body.returnVar

Lets.addComToEnd and Com.toLets

@[irreducible]

def Lets.addComToEnd {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {ty : d.Ty} {Γ_out : Ctxt d.Ty} {eff : EffectKind} (lets : Lets d Γ_in eff Γ_out) (com : Com d Γ_out eff ty) : Lets d Γ_in eff com.outContext

Add a Com to the end of a sequence of lets

Equations

• lets.addComToEnd (Com.ret v) = lets
• lets.addComToEnd (Com.var e body) = (lets.var e).addComToEnd body

def Com.toLets {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (com : Com d Γ eff t) : Lets d Γ eff com.outContext

The let-bindings of a program

Equations

• com.toLets = Lets.nil.addComToEnd com

@[simp]

theorem Lets.addComToEnd_ret {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} {v : Γ_out.Var t} {lets : Lets d Γ_in eff Γ_out} : lets.addComToEnd (Com.ret v) = lets

@[simp]

theorem Lets.addComToEnd_var {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} : ∀ {ty : d.Ty} {e : Expr d Γ_out eff ty} {lets : Lets d Γ_in eff Γ_out} {com : Com d (Γ_out.snoc ty) eff t}, lets.addComToEnd (Com.var e com) = (lets.var e).addComToEnd com

@[simp]

theorem Com.toLets_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {v : Γ.Var t} : (Com.ret v).toLets = Lets.nil

denote

Denote expressions, programs, and sequences of lets

def HVector.denote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {l : List (Ctxt d.Ty × d.Ty)} (T : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) l) : HVector (fun (t : Ctxt d.Ty × d.Ty) => t.1.Valuation → EffectKind.impure.toMonad d.m ⟦t.2⟧) l

Equations

• HVector.nil.denote = HVector.nil
• (v::ₕvs).denote = (v.denote::ₕvs.denote)

def Expr.denote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) (Γv : Γ.Valuation) : eff.toMonad d.m ⟦ty⟧

Equations

• (Expr.mk op ⋯ heff args regArgs).denote Γv = EffectKind.liftEffect heff (DialectDenote.denote op (HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) args) regArgs.denote)

def Com.denote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : Com d Γ eff ty → Γ.Valuation → eff.toMonad d.m ⟦ty⟧

Equations

• (Com.ret e).denote x = pure (x e)
• (Com.var e_2 body_2).denote x = body_2.denote (x::ᵥe_2.denote x)
• (Com.var e_2 body_2).denote x = do let x_1 ← e_2.denote x body_2.denote (x::ᵥx_1)

def Com.denoteLets {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (com : Com d Γ eff ty) (Γv : Γ.Valuation) : eff.toMonad d.m com.outContext.Valuation

Denote just the let bindings of com, transforming a valuation for Γ into a valuation for the output context of com

Equations

• (Com.ret e).denoteLets x = pure x
• (Com.var e body).denoteLets x = do let Ve ← e.denote x let V ← body.denoteLets (x::ᵥVe) pure (Ctxt.Valuation.cast ⋯ V)

def Expr.denoteImpure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) (Γv : Γ.Valuation) : EffectKind.impure.toMonad d.m ⟦ty⟧

Denote an Expr in an unconditionally impure fashion

Equations

• e.denoteImpure Γv = liftM (e.denote Γv)

def Com.denoteImpure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : Com d Γ eff ty → Γ.Valuation → EffectKind.impure.toMonad d.m ⟦ty⟧

Denote a Com in an unconditionally impure fashion

Equations

• (Com.ret e).denoteImpure x = pure (x e)
• (Com.var e body).denoteImpure x = do let x_1 ← e.denoteImpure x liftM (body.denote (x::ᵥx_1))
• (Com.var e body).denoteImpure x = do let x_1 ← e.denoteImpure x liftM (body.denote (x::ᵥx_1))

def Lets.denote {d : Dialect} [TyDenote d.Ty] [Monad d.m] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} [DialectSignature d] [DialectDenote d] {Γ₂ : Ctxt d.Ty} (lets : Lets d Γ₁ eff Γ₂) (Γ₁'v : Γ₁.Valuation) : eff.toMonad d.m Γ₂.Valuation

Equations

• Lets.nil.denote Γ₁'v = pure Γ₁'v
• (lets'.var e).denote Γ₁'v = do let Γ₂'v ← lets'.denote Γ₁'v let v ← e.denote Γ₂'v pure (Γ₂'v::ᵥv)

@[reducible, inline]

abbrev Lets.denotePure {d : Dialect} [TyDenote d.Ty] [Monad d.m] {Γ₁ : Ctxt d.Ty} {Γ₂ : Ctxt d.Ty} [DialectSignature d] [DialectDenote d] : Lets d Γ₁ EffectKind.pure Γ₂ → Γ₁.Valuation → Γ₂.Valuation

denotePure is a specialization of denote for pure Lets. Theorems and definitions should always be phrased in terms of the latter.

However, denotePure behaves slighly better when it comes to congruences, since congr does not realize that pure.toMonad d.m (Valuation _) is just Valuation _, and thus a function. Therefore, if a goalstate is ⊢ lets.denote ... = lets.denote ..., and lets is pure, then to use the congruence, you can do: rw [← Lets.denotePure]; congr

Equations

• Lets.denotePure = Lets.denote

def Lets.denoteImpure {d : Dialect} [TyDenote d.Ty] [Monad d.m] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} [DialectSignature d] [DialectDenote d] {Γ₂ : Ctxt d.Ty} (lets : Lets d Γ₁ eff Γ₂) (Γ₁'v : Γ₁.Valuation) : EffectKind.impure.toMonad d.m Γ₂.Valuation

Denote a Lets in an unconditionally impure fashion

Equations

• Lets.nil.denoteImpure Γ₁'v = EffectKind.impure.return Γ₁'v
• (lets'.var e).denoteImpure Γ₁'v = do let Γ₂'v ← liftM (lets'.denote Γ₁'v) let v ← liftM (e.denote Γ₂'v) pure (Γ₂'v::ᵥv)
• (lets'.var e).denoteImpure Γ₁'v = do let Γ₂'v ← liftM (lets'.denote Γ₁'v) let v ← liftM (e.denote Γ₂'v) pure (Γ₂'v::ᵥv)

def Zipper.denote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {ty : d.Ty} (zip : Zipper d Γ_in eff Γ_out ty) (V_in : Γ_in.Valuation) : eff.toMonad d.m ⟦ty⟧

The denotation of a zipper is a composition of the denotations of the constituent Lets and Com

Equations

• zip.denote V_in = zip.top.denote V_in >>= zip.bot.denote

theorem Expr.denote_unfold {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {ty : d.Ty} {eff : EffectKind} {Γ : Ctxt d.Ty} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) (Γv : Γ.Valuation) : (Expr.mk op ty_eq eff_le args regArgs).denote Γv = ⋯ ▸ EffectKind.liftEffect eff_le (DialectDenote.denote op (HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) args) regArgs.denote)

theorem Com.denote_unfold {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {ty : d.Ty} {eff : EffectKind} {Γ : Ctxt d.Ty} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) (Γv : Γ.Valuation) : (Expr.mk op ty_eq eff_le args regArgs).denote Γv = ⋯ ▸ EffectKind.liftEffect eff_le (DialectDenote.denote op (HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) args) regArgs.denote)

Equation lemma to unfold denote, which does not unfold correctly due to the presence of the coercion ty_eq and the mutual definition.

simp-lemmas about denote functions

@[simp]

theorem HVector.denote_nil {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] (T : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) []) : T.denote = HVector.nil

@[simp]

theorem HVector.denote_cons {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] (t : Ctxt d.Ty × d.Ty) (ts : List (Ctxt d.Ty × d.Ty)) (a : Com d t.1 EffectKind.impure t.2) (as : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts) : (a::ₕas).denote = (a.denote::ₕas.denote)

@[simp]

theorem Com.denote_ret {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {t : d.Ty} {eff : EffectKind} (Γ : Ctxt d.Ty) (x : Γ.Var t) : (Com.ret x).denote = fun (Γv : Γ.Valuation) => pure (Γv x)

@[simp]

theorem Com.denote_var {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {α : d.Ty} : ∀ {a : d.Ty} {body : Com d (Γ.snoc α) eff a} [inst : LawfulMonad d.m] {e : Expr d Γ eff α}, (Com.var e body).denote = fun (Γv : Γ.Valuation) => do let v ← e.denote Γv body.denote (Γv::ᵥv)

@[simp]

theorem Com.denoteLets_var {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {u : d.Ty} (e : Expr d Γ eff t) (body : Com d (Γ.snoc t) eff u) [LawfulMonad d.m] : (Com.var e body).denoteLets = fun (V : Γ.Valuation) => do let Ve ← e.denote V body.denoteLets (V::ᵥVe)

@[simp]

theorem Com.denoteImpure_ret {d : Dialect} [DialectSignature d] [TyDenote d.Ty] {t : d.Ty} {eff : EffectKind} [Monad d.m] [DialectDenote d] {Γ : Ctxt d.Ty} (x : Γ.Var t) : (Com.ret x).denoteImpure = fun (Γv : Γ.Valuation) => pure (Γv x)

@[simp]

theorem Com.denoteImpure_body {d : Dialect} [DialectSignature d] [TyDenote d.Ty] {eff : EffectKind} {te : d.Ty} {tbody : d.Ty} [Monad d.m] [DialectDenote d] {Γ : Ctxt d.Ty} (e : Expr d Γ eff te) (body : Com d (Γ.snoc te) eff tbody) : (Com.var e body).denoteImpure = fun (Γv : Γ.Valuation) => do let x ← e.denoteImpure Γv liftM (body.denote (Γv::ᵥx))

@[simp]

theorem Lets.denote_nil {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {eff : EffectKind} {Γ : Ctxt d.Ty} : Lets.nil.denote = fun (x : Γ.Valuation) => pure x

@[simp]

theorem Lets.denote_var {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} {lets : Lets d Γ_in eff Γ_out} {e : Expr d Γ_out eff t} : (lets.var e).denote = fun (V_in : Γ_in.Valuation) => do let V_out ← lets.denote V_in let x ← e.denote V_out pure (V_out::ᵥx)

@[simp]

theorem Lets.denote_addComToEnd {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} {lets : Lets d Γ_in eff Γ_out} {com : Com d Γ_out eff t} : (lets.addComToEnd com).denote = fun (V : Γ_in.Valuation) => do let Vlets ← lets.denote V let Vbody ← com.denoteLets Vlets pure Vbody

@[simp]

theorem Com.denoteLets_ret {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {v : Γ.Var t} : (Com.ret v).denoteLets = fun (V : Γ.Valuation) => pure V

theorem Com.denoteLets_eq {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {com : Com d Γ eff t} : com.denoteLets = com.toLets.denote

changeVars

Map a context homomorphism over a Expr/Com. That is, substitute variables.

def Expr.changeVars {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {Γ' : Ctxt d.Ty} (varsMap : Γ.Hom Γ') {ty : d.Ty} (e : Expr d Γ eff ty) : Expr d Γ' eff ty

Equations

• Expr.changeVars varsMap (Expr.mk op sig_eq eff_leq args regArgs) = Expr.mk op sig_eq eff_leq (HVector.map varsMap args) regArgs

def Com.changeVars {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Γ' : Ctxt d.Ty} : Com d Γ eff ty → Γ.Hom Γ' → Com d Γ' eff ty

Equations

• (Com.ret v).changeVars = fun (varsMap : Γ.Hom Γ') => Com.ret (varsMap v)
• (Com.var e body).changeVars = fun (varsMap : Γ.Hom Γ') => Com.var (Expr.changeVars varsMap e) (body.changeVars fun (x : d.Ty) (v : (Γ.snoc α).Var x) => varsMap.snocMap v)

simp-lemmas about changeVars

@[simp]

theorem Expr.denote_changeVars {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {eff : EffectKind} {ty : d.Ty} {Γ : Ctxt d.Ty} {Γ' : Ctxt d.Ty} (varsMap : Γ.Hom Γ') (e : Expr d Γ eff ty) : (Expr.changeVars varsMap e).denote = fun (Γ'v : Γ'.Valuation) => e.denote (Γ'v.comap varsMap)

@[simp]

theorem Com.changeVars_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} {Δ : Ctxt d.Ty} (v : Γ.Var t) : (Com.ret v).changeVars = fun (map : Γ.Hom Δ) => Com.ret (map v)

@[simp]

theorem Com.changeVars_var {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {u : d.Ty} {Δ : Ctxt d.Ty} (e : Expr d Γ eff t) (body : Com d (Γ.snoc t) eff u) : (Com.var e body).changeVars = fun (map : Γ.Hom Δ) => Com.var (Expr.changeVars map e) (body.changeVars map.snocMap)

@[simp]

theorem Com.outContext_changeVars_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : ∀ {t : d.Ty} {v : Γ.Var t} {Γ' : Ctxt d.Ty} (varsMap : Γ.Hom Γ'), Com d Γ eff ty → ((Com.ret v).changeVars varsMap).outContext = Γ'

@[simp]

theorem Com.denote_changeVars {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Γ' : Ctxt d.Ty} (varsMap : Γ.Hom Γ') (c : Com d Γ eff ty) : (c.changeVars varsMap).denote = c.denote ∘ fun (V : Γ'.Valuation) => V.comap varsMap

@[simp]

theorem Com.denote_changeVars' {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Γ' : Ctxt d.Ty} (varsMap : Γ.Hom Γ') (c : Com d Γ eff ty) : (c.changeVars varsMap).denote = fun (V : Γ'.Valuation) => c.denote (V.comap varsMap)

def Com.outContext_changeVars_hom {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Δ : Ctxt d.Ty} {map : Γ.Hom Δ} (map_inv : Δ.Hom Γ) {c : Com d Γ eff ty} : (c.changeVars map).outContext.Hom c.outContext

Equations

• Com.outContext_changeVars_hom map_inv = cast ⋯ map_inv
• Com.outContext_changeVars_hom map_inv = cast ⋯ (Com.outContext_changeVars_hom map_inv.snocMap)

@[simp]

theorem Com.denoteLets_returnVar_pure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {ty : d.Ty} (c : Com d Γ EffectKind.pure ty) (Γv : Γ.Valuation) : c.denoteLets Γv c.returnVar = c.denote Γv

@[simp]

theorem Expr.changeVars_changeVars {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Δ : Ctxt d.Ty} {Ξ : Ctxt d.Ty} (e : Expr d Γ eff ty) (f : Γ.Hom Δ) (g : Δ.Hom Ξ) : Expr.changeVars g (Expr.changeVars f e) = Expr.changeVars (f.comp g) e

FlatCom

An alternative representation of a program as a Lets with a return Var

structure FlatCom (d : Dialect) [DialectSignature d] (Γ_in : Ctxt d.Ty) (eff : EffectKind) (Γ_out : Ctxt d.Ty) (ty : d.Ty) : Type

FlatCom Γ eff Δ ty represents a program as a sequence Lets Γ eff Δ and a Var Δ ty. This is isomorphic to Com Γ eff ty, where Δ is com.outContext

• lets : Lets d Γ_in eff Γ_out
• ret : Γ_out.Var ty

def FlatCom.denoteLets {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} (flatCom : FlatCom d Γ eff Γ_out t) (Γv : Γ.Valuation) : eff.toMonad d.m Γ_out.Valuation

Denote the Lets of the FlatICom

Equations

• flatCom.denoteLets Γv = flatCom.lets.denote Γv

@[reducible, inline]

abbrev FlatCom.denote {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} [DialectDenote d] (flatCom : FlatCom d Γ eff Γ_out t) (Γv : Γ.Valuation) : eff.toMonad d.m ⟦t⟧

Denote the lets and the ret of the FlatCom. This is equal to denoting the Com

Equations

• flatCom.denote Γv = do let Γ'v ← flatCom.lets.denote Γv pure (Γ'v flatCom.ret)

theorem FlatCom.denoteLets_eq {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} [DialectDenote d] (flatCom : FlatCom d Γ eff Γ_out t) : flatCom.denoteLets = fun (Γv : Γ.Valuation) => flatCom.lets.denote Γv

theorem FlatCom.denote_eq {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} [DialectDenote d] (flatCom : FlatCom d Γ eff Γ_out t) : flatCom.denote = fun (Γv : Γ.Valuation) => do let Γ'v ← flatCom.lets.denote Γv pure (Γ'v flatCom.ret)

casting of expressions and purity

castPureToEff

def Expr.changeEffect {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff₁ : EffectKind} {eff₂ : EffectKind} (h : eff₁ ≤ eff₂) : Expr d Γ eff₁ t → Expr d Γ eff₂ t

Change the effect of an expression into another effect that is "higher" in the hierarchy. Generally used to change a pure expression into an impure one, but it is useful to have this phrased more generically

Equations

• Expr.changeEffect h (Expr.mk op ty_eq eff_le args regArgs) = Expr.mk op ty_eq ⋯ args regArgs

def Com.changeEffect {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff₁ : EffectKind} {eff₂ : EffectKind} (h : eff₁ ≤ eff₂) : Com d Γ eff₁ t → Com d Γ eff₂ t

Change the effect of a program into another effect that is "higher" in the hierarchy. Generally used to change a pure program into an impure one, but it is useful to have this phrased more generically

Equations

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

def Lets.changeEffect {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {eff₁ : EffectKind} {eff₂ : EffectKind} (h : eff₁ ≤ eff₂) : Lets d Γ_in eff₁ Γ_out → Lets d Γ_in eff₂ Γ_out

Change the effect of a sequence of lets into another effect that is "higher" in the hierarchy. Generally used to change pure into impure, but it is useful to have this phrased more generically

def Expr.castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (eff : EffectKind) : Expr d Γ EffectKind.pure t → Expr d Γ eff t

cast a pure Expr into a possibly impure expression

Equations

• Expr.castPureToEff eff = Expr.changeEffect ⋯

def Com.castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (eff : EffectKind) : Com d Γ EffectKind.pure t → Com d Γ eff t

Equations

• Com.castPureToEff eff = Com.changeEffect ⋯

def Lets.castPureToEff {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} (eff : EffectKind) : Lets d Γ_in EffectKind.pure Γ_out → Lets d Γ_in eff Γ_out

Equations

• Lets.castPureToEff eff Lets.nil = Lets.nil
• Lets.castPureToEff eff (body.var e) = (Lets.castPureToEff eff body).var (Expr.castPureToEff eff e)

def Com.letPure {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} {u : d.Ty} (e : Expr d Γ EffectKind.pure t) (body : Com d (Γ.snoc t) eff u) : Com d Γ eff u

A wrapper around Com.var that allows for a pure expression to be added to an otherwise impure program, using Expr.castPureToEff

Equations

• Com.letPure e body = Com.var (Expr.castPureToEff eff e) body

def Com.letSup {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff₁ : EffectKind} {t : d.Ty} {eff₂ : EffectKind} {u : d.Ty} (e : Expr d Γ eff₁ t) (body : Com d (Γ.snoc t) eff₂ u) : Com d Γ (eff₁ ⊔ eff₂) u

letSup e body allows us to combine an expression and body with different effects, by returning a Com whose effect is their join/supremum

Equations

• Com.letSup e body = Com.var (Expr.changeEffect ⋯ e) (Com.changeEffect ⋯ body)

@[simp]

theorem Com.castPureToEff_ret {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {v : Γ.Var ty} {eff : EffectKind} : Com.castPureToEff eff (Com.ret v) = Com.ret v

@[simp]

theorem Com.castPureToEff_var {d : Dialect} [DialectSignature d] {ty : d.Ty} {Γ : Ctxt d.Ty} {eTy : d.Ty} {eff : EffectKind} {com : Com d (Γ.snoc eTy) EffectKind.pure ty} {e : Expr d Γ EffectKind.pure eTy} : Com.castPureToEff eff (Com.var e com) = Com.var (Expr.castPureToEff eff e) (Com.castPureToEff eff com)

@[simp]

theorem Lets.castPureToEff_nil {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} : Lets.castPureToEff eff Lets.nil = Lets.nil

@[simp]

theorem Lets.castPureToEff_var {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {eTy : d.Ty} {eff : EffectKind} {lets : Lets d Γ_in EffectKind.pure Γ_out} {e : Expr d Γ_out EffectKind.pure eTy} : Lets.castPureToEff eff (lets.var e) = (Lets.castPureToEff eff lets).var (Expr.castPureToEff eff e)

@[simp]

theorem Com.outContext_castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).outContext = com.outContext

@[simp]

theorem Com.size_castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).size = com.size

castPureToEff does not change the size of a Com

@[simp]

theorem Lets.addComToEnd_castPureToEff {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {lets : Lets d Γ_in EffectKind.pure Γ_out} {com : Com d Γ_out EffectKind.pure ty} : (Lets.castPureToEff eff lets).addComToEnd (Com.castPureToEff eff com) = cast ⋯ (Lets.castPureToEff eff (lets.addComToEnd com))

@[simp]

theorem Com.toLets_castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).toLets = cast ⋯ (Lets.castPureToEff eff com.toLets)

@[simp]

theorem Com.returnVar_castPureToEff {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).returnVar = Ctxt.Var.castCtxt ⋯ com.returnVar

denotations of castPureToEff

@[simp]

theorem Expr.denote_castPureToEff {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} {e : Expr d Γ EffectKind.pure t} : (Expr.castPureToEff eff e).denote = fun (V : Γ.Valuation) => pure (e.denote V)

@[simp]

theorem Com.denote_castPureToEff {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).denote = fun (V : Γ.Valuation) => pure (com.denote V)

@[simp]

theorem Com.denoteLets_castPureToEff {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} {com : Com d Γ EffectKind.pure ty} : (Com.castPureToEff eff com).denoteLets = fun (V : Γ.Valuation) => pure (Ctxt.Valuation.comap (com.denoteLets V) fun (x : d.Ty) (v : (Com.castPureToEff eff com).outContext.Var x) => Ctxt.Var.castCtxt ⋯ v)

Expr.HasPureOp and Expr.toPure?

def Expr.HasPureOp {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) : Prop

Whether the operation of an expression is pure (which might be evaluated impurely)

Equations

• e.HasPureOp = (DialectSignature.effectKind e.op = EffectKind.pure)

instance instDecidableHasPureOp {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (e : Expr d Γ eff t) : Decidable e.HasPureOp

e.HasPureOp is decidable

Equations

• instDecidableHasPureOp e = inferInstanceAs (Decidable (DialectSignature.effectKind e.op = EffectKind.pure))

@[simp]

theorem Expr.castPureToEff_pure_eq {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (e : Expr d Γ EffectKind.pure t) : Expr.castPureToEff EffectKind.pure e = e

def Expr.toPure? {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) : Option (Expr d Γ EffectKind.pure ty)

Attempt to convert a possibly impure expression into a pure expression. If the expression's operation is impure, return none

Equations

• (Expr.mk op ty_eq eff_le args regArgs).toPure? = match h : DialectSignature.effectKind op with | EffectKind.pure => some (Expr.mk op ty_eq ⋯ args regArgs) | EffectKind.impure => none

theorem Expr.HasPureOp_of_pure {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (e : Expr d Γ EffectKind.pure t) : e.HasPureOp

The operation of a pure expression is necessarily pure

theorem Expr.denote_mk_of_pure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {ty : d.Ty} {eff₂ : EffectKind} {Γ : Ctxt d.Ty} {op : d.Op} (eff_eq : DialectSignature.effectKind op = EffectKind.pure) (ty_eq : ty = DialectSignature.outTy op) (eff_le : DialectSignature.effectKind op ≤ eff₂) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) : (Expr.mk op ty_eq eff_le args regArgs).denote = fun (Γv : Γ.Valuation) => let d_1 := cast ⋯ (DialectDenote.denote op (HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) args) regArgs.denote); match eff₂, eff_le with | EffectKind.pure, eff_le => d_1 | EffectKind.impure, eff_le => pure d_1

Rewrite theorem for an expression with a pure operation (which might be evaluated impurely)

theorem Expr.denote_of_pure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {e : Expr d Γ eff ty} (eff_eq : e.HasPureOp) : e.denote = fun (Γv : Γ.Valuation) => let d_1 := cast ⋯ (DialectDenote.denote e.op (HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) e.args) e.regArgs.denote); match eff, e, eff_eq with | EffectKind.pure, e, eff_eq => d_1 | EffectKind.impure, e, eff_eq => pure d_1

@[simp]

theorem Expr.denote_castPureToEff_impure_eq {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} [LawfulMonad d.m] (e : Expr d Γ EffectKind.pure t) : (Expr.castPureToEff EffectKind.impure e).denote = fun (Γv : Γ.Valuation) => pure (e.denote Γv)

casting an expr to an impure expr and running it equals running it purely and returning the value

theorem Expr.hasPureOp_of_toPure?_isSome {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {e : Expr d Γ eff ty} (h : e.toPure?.isSome = true) : e.HasPureOp

theorem Expr.denote_toPure? {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {e : Expr d Γ eff ty} {e' : Expr d Γ EffectKind.pure ty} (he : e.toPure? = some e') : e.denote = match (motive := (eff : EffectKind) → {e : Expr d Γ eff ty} → e.toPure? = some e' → Γ.Valuation → eff.toMonad d.m ⟦ty⟧) eff, e, he with | EffectKind.pure, e, he => e'.denote | EffectKind.impure, e, he => pure ∘ e'.denote

The denotation of toPure?

Combining Lets and Com

Various machinery to combine Lets and Coms in various ways.

def Com.toFlatCom {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {t : d.Ty} (com : Com d Γ EffectKind.pure t) : FlatCom d Γ EffectKind.pure com.outContext t

Convert a Com into a FlatCom

Equations

• com.toFlatCom = { lets := com.toLets, ret := com.returnVar }

def Zipper.toCom {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty : d.Ty} (zip : Zipper d Γ_in eff Γ_mid ty) : Com d Γ_in eff ty

Recombine a zipper into a single program by adding the lets to the beginning of the com

Equations

• zip.toCom = Zipper.toCom.go zip.top zip.bot

def Zipper.toCom.go {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Γ_mid : Ctxt d.Ty} : Lets d Γ_in eff Γ_mid → Com d Γ_mid eff ty → Com d Γ_in eff ty

Equations

• Zipper.toCom.go Lets.nil com = com
• Zipper.toCom.go (body.var e) com = Zipper.toCom.go body (Com.var e com)

def Zipper.insertCom {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty : d.Ty} {newTy : d.Ty} (zip : Zipper d Γ_in eff Γ_mid ty) (v : Γ_mid.Var newTy) (newCom : Com d Γ_mid eff newTy) : Zipper d Γ_in eff newCom.outContext ty

Add a Com directly before the current position of a zipper, while reassigning every occurence of a given free variable (v) of zip.com to the output of the new Com

Equations

• zip.insertCom v newCom = { top := zip.top.addComToEnd newCom, bot := zip.bot.changeVars (newCom.outContextHom.with v newCom.returnVar) }

def Zipper.insertPureCom {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty : d.Ty} {newTy : d.Ty} (zip : Zipper d Γ_in eff Γ_mid ty) (v : Γ_mid.Var newTy) (newCom : Com d Γ_mid EffectKind.pure newTy) : Zipper d Γ_in eff newCom.outContext ty

Add a pure Com directly before the current position of a possibly impure zipper, while r eassigning every occurence of a given free variable (v) of zip.com to the output of the new Com

This is a wrapper around insertCom (which expects newCom to have the same effect as zip) and castPureToEff

Equations

• zip.insertPureCom v newCom = ⋯ ▸ zip.insertCom v (Com.castPureToEff eff newCom)

simp-lemmas

@[simp]

theorem Zipper.toCom_nil {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {com : Com d Γ eff ty} : { top := Lets.nil, bot := com }.toCom = com

@[simp]

theorem Zipper.toCom_var {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} : ∀ {ty : d.Ty} {e : Expr d Γ_mid eff ty} {a : d.Ty} {com : Com d (Γ_mid.snoc ty) eff a} {lets : Lets d Γ_in eff Γ_mid}, { top := lets.var e, bot := com }.toCom = { top := lets, bot := Com.var e com }.toCom

@[simp]

theorem Zipper.denote_toCom {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty : d.Ty} [LawfulMonad d.m] (zip : Zipper d Γ_in eff Γ_mid ty) : zip.toCom.denote = zip.denote

@[simp]

theorem Zipper.denote_mk {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {ty : d.Ty} {lets : Lets d Γ_in eff Γ_out} {com : Com d Γ_out eff ty} : { top := lets, bot := com }.denote = fun (V : Γ_in.Valuation) => lets.denote V >>= com.denote

theorem Zipper.denote_insertCom {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty₁ : d.Ty} {newTy : d.Ty} {v : Γ_mid.Var newTy} {zip : Zipper d Γ_in eff Γ_mid ty₁} {newCom : Com d Γ_mid eff newTy} [LawfulMonad d.m] : (zip.insertCom v newCom).denote = fun (V_in : Γ_in.Valuation) => do let V_mid ← zip.top.denote V_in let V_newMid ← newCom.denoteLets V_mid zip.bot.denote (V_newMid.comap (newCom.outContextHom.with v newCom.returnVar))

@[simp]

theorem Zipper.denoteLets_eqRec_Γ_mid {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty : d.Ty} {Γ_mid' : Ctxt d.Ty} {zip : Zipper d Γ_in eff Γ_mid ty} (h : Γ_mid = Γ_mid') : (h ▸ zip).denote = zip.denote

Casting the intermediate context is not relevant for the denotation

theorem Zipper.denote_insertPureCom {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_mid : Ctxt d.Ty} {ty₁ : d.Ty} {newTy : d.Ty} {v : Γ_mid.Var newTy} {zip : Zipper d Γ_in eff Γ_mid ty₁} {newCom : Com d Γ_mid EffectKind.pure newTy} [LawfulMonad d.m] : (zip.insertPureCom v newCom).denote = fun (V_in : Γ_in.Valuation) => do let V_mid ← zip.top.denote V_in zip.bot.denote (Ctxt.Valuation.comap (newCom.denoteLets V_mid) (newCom.outContextHom.with v newCom.returnVar))

Semantic preservation of Zipper.insertPureCom

Generally, we don't intend for insertPureCom to change the semantics of the zipper'd program. We characterize the condition for this intended property by proving denote_insertPureCom_eq_of, which states that if the reassigned variable v in the original top of the zipper is semantically equivalent to the return value of the inserted program newCom, then the denotation of the zipper after insertion agrees with the original zipper.

@[simp]

theorem Com.denoteLets_outContextHom {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {ty : d.Ty} (com : Com d Γ EffectKind.pure ty) (V : Γ.Valuation) {vTy : d.Ty} (v : Γ.Var vTy) : com.denoteLets V (com.outContextHom v) = V v

Denoting any of the free variables of a program through Com.denoteLets just returns the assignment of that variable in the input valuation

@[simp]

theorem Ctxt.Valuation.comap_outContextHom_denoteLets {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {ty : d.Ty} {com : Com d Γ EffectKind.pure ty} {V : Γ.Valuation} : Ctxt.Valuation.comap (com.denoteLets V) com.outContextHom = V

Inserting multiple programs with Zipper.foldInsert

Random Access for Lets

Get the let-binding that correponds to a given variable v, so long as the binding's operation is pure

def Lets.getPureExprAux {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ₁ : Ctxt d.Ty} {Γ₂ : Ctxt d.Ty} {t : d.Ty} : Lets d Γ₁ eff Γ₂ → (v : Γ₂.Var t) → Option (Expr d (Γ₂.dropUntil v) EffectKind.pure t)

Get the Expr that a var v is assigned to in a sequence of Lets, without adjusting variables, assuming that this expression has a pure operation. If the expression has an impure operation, or there is no binding corresponding to v (i.e., v comes from Γ_in), return none

Equations

• One or more equations did not get rendered due to their size.
• Lets.nil.getPureExprAux x_2 = none

def Lets.getPureExpr {d : Dialect} [DialectSignature d] {eff : EffectKind} {Γ₁ : Ctxt d.Ty} {Γ₂ : Ctxt d.Ty} (lets : Lets d Γ₁ eff Γ₂) {t : d.Ty} (v : Γ₂.Var t) : Option (Expr d Γ₂ EffectKind.pure t)

Get the Expr that a var v is assigned to in a sequence of Lets. The variables are adjusted so that they are variables in the output context of a lets, not the local context where the variable appears.

Equations

• lets.getPureExpr v = Expr.changeVars Ctxt.dropUntilHom <$> lets.getPureExprAux v

@[simp]

theorem Lets.getPureExpr_nil {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} : ∀ {t : d.Ty} {v : Γ.Var t}, Lets.nil.getPureExpr v = none

@[simp]

theorem Lets.getPureExpr_var_last {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {ty : d.Ty} (lets : Lets d Γ_in eff Γ_out) (e : Expr d Γ_out eff ty) : (lets.var e).getPureExpr (Ctxt.Var.last Γ_out ty) = Expr.changeVars Ctxt.Hom.id.snocRight <$> e.toPure?

@[simp]

theorem Lets.getPureExprAux_var_toSnoc {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {ty₁ : d.Ty} {ty₂ : d.Ty} (lets : Lets d Γ_in eff Γ_out) (e : Expr d Γ_out eff ty₁) (v : Γ_out.Var ty₂) : (lets.var e).getPureExprAux ↑v = lets.getPureExprAux v

@[simp]

theorem Lets.getPureExpr_var_toSnoc {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {ty₁ : d.Ty} {ty₂ : d.Ty} (lets : Lets d Γ_in eff Γ_out) (e : Expr d Γ_out eff ty₁) (v : Γ_out.Var ty₂) : (lets.var e).getPureExpr ↑v = Expr.changeVars Ctxt.Hom.id.snocRight <$> lets.getPureExpr v

theorem Lets.denote_getPureExprAux {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {eff : EffectKind} {α : Type} [LawfulMonad d.m] {Γ₁ : Ctxt d.Ty} {Γ₂ : Ctxt d.Ty} {t : d.Ty} {lets : Lets d Γ₁ eff Γ₂} {v : Γ₂.Var t} {ePure : Expr d (Γ₂.dropUntil v) EffectKind.pure t} (he : lets.getPureExprAux v = some ePure) (s : Γ₁.Valuation) (f : Γ₂.Valuation → ⟦t⟧ → eff.toMonad d.m α) : (do let Γv ← lets.denote s f Γv ((Expr.changeVars Ctxt.dropUntilHom ePure).denote Γv)) = do let Γv ← lets.denote s f Γv (Γv v)

theorem Lets.denote_getExpr {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {eff : EffectKind} {α : Type} [LawfulMonad d.m] {Γ₁ : Ctxt d.Ty} {Γ₂ : Ctxt d.Ty} {lets : Lets d Γ₁ eff Γ₂} {t : d.Ty} {v : Γ₂.Var t} {e : Expr d Γ₂ EffectKind.pure t} (he : lets.getPureExpr v = some e) (s : Γ₁.Valuation) (f : Γ₂.Valuation → ⟦t⟧ → eff.toMonad d.m α) : (do let Γv ← lets.denote s f Γv (e.denote Γv)) = do let Γv ← lets.denote s f Γv (Γv v)

Mapping

We can map between different dialects

def RegionSignature.map {Ty : Type} {Ty' : Type} (f : Ty → Ty') : RegionSignature Ty → RegionSignature Ty'

Equations

• RegionSignature.map f = List.map fun (x : Ctxt Ty × Ty) => match x with | (Γ, ty) => (Ctxt.map f Γ, f ty)

instance instFunctorRegionSignature : Functor RegionSignature

Equations

• instFunctorRegionSignature = { map := fun {α β : Type} => RegionSignature.map, mapConst := fun {α β : Type} => RegionSignature.map ∘ Function.const β }

def Signature.map {Ty : Type} {Ty' : Type} (f : Ty → Ty') : Signature Ty → Signature Ty'

Equations

• Signature.map f sig = { sig := List.map f sig.sig, regSig := RegionSignature.map f sig.regSig, outTy := f sig.outTy, effectKind := EffectKind.pure }

instance instFunctorSignature : Functor Signature

Equations

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

structure DialectMorphism (d : Dialect) (d' : Dialect) [DialectSignature d] [DialectSignature d'] : Type

A dialect morphism consists of a map between operations and a map between types, such that the signature of operations is respected

• mapOp : d.Op → d'.Op
• mapTy : d.Ty → d'.Ty
• preserves_signature : ∀ (op : d.Op), signature (self.mapOp op) = self.mapTy <$> signature op

theorem DialectMorphism.preserves_signature {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (self : DialectMorphism d d') (op : d.Op) : signature (self.mapOp op) = self.mapTy <$> signature op

def DialectMorphism.preserves_sig {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') (op : d.Op) : DialectSignature.sig (f.mapOp op) = List.map f.mapTy (DialectSignature.sig op)

Equations

• ⋯ = ⋯

def DialectMorphism.preserves_regSig {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') (op : d.Op) : DialectSignature.regSig (f.mapOp op) = RegionSignature.map f.mapTy (DialectSignature.regSig op)

Equations

• ⋯ = ⋯

def DialectMorphism.preserves_outTy {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') (op : d.Op) : DialectSignature.outTy (f.mapOp op) = f.mapTy (DialectSignature.outTy op)

Equations

• ⋯ = ⋯

theorem DialectMorphism.preserves_effectKind {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') (op : d.Op) : DialectSignature.effectKind (f.mapOp op) = DialectSignature.effectKind op

@[irreducible]

def Com.changeDialect {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : Com d Γ eff ty → Com d' (f.mapTy <$> Γ) eff (f.mapTy ty)

Equations

• Com.changeDialect f (Com.ret v) = Com.ret v.toMap
• Com.changeDialect f (Com.var e body) = Com.var (Expr.changeDialect f e) (Com.changeDialect f body)

@[irreducible]

def Expr.changeDialect {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} : Expr d Γ eff ty → Expr d' (Ctxt.map f.mapTy Γ) eff (f.mapTy ty)

Equations

• Expr.changeDialect f (Expr.mk op ⋯ heff args regArgs) = Expr.mk (f.mapOp op) ⋯ ⋯ (⋯ ▸ HVector.map' f.mapTy (fun (x : d.Ty) => Ctxt.Var.toMap) args) (⋯ ▸ HVector.changeDialect f regArgs)

@[irreducible]

def HVector.changeDialect {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') {eff : EffectKind} {regSig : RegionSignature d.Ty} : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 eff t.2) regSig → HVector (fun (t : Ctxt d'.Ty × d'.Ty) => Com d' t.1 eff t.2) (f.mapTy <$> regSig)

Inline of HVector.map' for the termination checker

Equations

• HVector.changeDialect f HVector.nil = HVector.nil
• HVector.changeDialect f (a::ₕas) = (Com.changeDialect f a::ₕHVector.changeDialect f as)

def Lets.changeDialect {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] (f : DialectMorphism d d') {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} : Lets d Γ_in eff Γ_out → Lets d' (f.mapTy <$> Γ_in) eff (f.mapTy <$> Γ_out)

Equations

• Lets.changeDialect f Lets.nil = Lets.nil
• Lets.changeDialect f (body.var e) = (Lets.changeDialect f body).var (Expr.changeDialect f e)

@[simp]

theorem Com.changeDialect_ret {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] {Γ : Ctxt d.Ty} {t : d.Ty} {eff : EffectKind} (f : DialectMorphism d d') (v : Γ.Var t) : Com.changeDialect f (Com.ret v) = Com.ret v.toMap

@[simp]

theorem Com.changeDialect_var {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {u : d.Ty} (f : DialectMorphism d d') (e : Expr d Γ eff t) (body : Com d (Γ.snoc t) eff u) : Com.changeDialect f (Com.var e body) = Com.var (Expr.changeDialect f e) (Com.changeDialect f body)

@[simp]

theorem HVector.changeDialect_nil {d : Dialect} {d' : Dialect} [DialectSignature d] [DialectSignature d'] {eff : EffectKind} (f : DialectMorphism d d') : HVector.changeDialect f HVector.nil = HVector.nil

Mapping

@[reducible, inline]

abbrev Mapping {d : Dialect} (Γ : Ctxt d.Ty) (Δ : Ctxt d.Ty) : Type

Mapping Γ Δ represents a partial homomorphism from context Γ to Δ. It's used to incrementally build a total homorphism

Equations

• Mapping Γ Δ = AList fun (x : (t : d.Ty) × Γ.Var t) => Δ.Var x.fst

theorem AList.mem_of_mem_entries {α : Type u_1} {β : α → Type u_2} {s : AList β} {k : α} {v : β k} : ⟨k, v⟩ ∈ s.entries → k ∈ s

if (k, v) is in s.entries then k is in s.

For mathlib

theorem AList.mem_entries_of_mem {α : Type u_1} {β : α → Type u_2} {s : AList β} {k : α} : k ∈ s → ∃ (v : β k), ⟨k, v⟩ ∈ s.entries

if k is in s, then there is v such that (k, v) is in s.entries.

Free Variables

def HVector.toVarSet {d : Dialect} [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {l : List d.Ty} (T : HVector Γ.Var l) : Γ.VarSet

Convert a heterogenous vector of variables into a homogeneous VarSet

Equations

• HVector.nil.toVarSet = ∅
• (v::ₕvs).toVarSet = insert ⟨head, v⟩ vs.toVarSet

def HVector.vars {d : Dialect} [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {l : List d.Ty} (T : HVector Γ.Var l) : Γ.VarSet

Equations

• T.vars = HVector.foldl (fun (x : d.Ty) (s : Γ.VarSet) (a : Γ.Var x) => insert ⟨x, a⟩ s) ∅ T

def Lets.vars {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} : Lets d Γ_in eff Γ_out → Γ_out.Var t → Γ_in.VarSet

The free variables of lets that are (transitively) referred to by some variable v. Also known as the uses of var.

Equations

• One or more equations did not get rendered due to their size.
• Lets.nil.vars v = Ctxt.VarSet.ofVar v

def Com.vars {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {t : d.Ty} : Com d Γ EffectKind.pure t → Γ.VarSet

com.vars is the set of free variables from Γ that are (transitively) used by the return variable of com

Equations

• com.vars = com.toFlatCom.lets.vars com.toFlatCom.ret

theorem Lets.vars_var_eq {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {lets : Lets d Γ_in eff Γ_out} {t : d.Ty} {e : Expr d Γ_out eff t} {w : ℕ} {tw : d.Ty} {wh : Γ_out.get? w = some tw} : (lets.var e).vars ⟨w + 1, ⋯⟩ = lets.vars ⟨w, wh⟩

@[simp]

theorem HVector.vars_nil {d : Dialect} [DecidableEq d.Ty] {Γ : Ctxt d.Ty} : HVector.nil.vars = ∅

@[simp]

theorem HVector.vars_cons {d : Dialect} [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {t : d.Ty} {l : List d.Ty} (v : Γ.Var t) (T : HVector Γ.Var l) : (v::ₕT).vars = insert ⟨t, v⟩ T.vars

theorem HVector.map_eq_of_eq_on_vars {d : Dialect} [DecidableEq d.Ty] {Γ : Ctxt d.Ty} {l : List d.Ty} {A : d.Ty → Type u_1} {T : HVector Γ.Var l} {s₁ : (t : d.Ty) → Γ.Var t → A t} {s₂ : (t : d.Ty) → Γ.Var t → A t} (h : ∀ v ∈ T.vars, s₁ v.fst v.snd = s₂ v.fst v.snd) : HVector.map s₁ T = HVector.map s₂ T

For a vector of variables T, let s₁ and s₂ be two maps from variables to A t. If s₁ and s₂ agree on all variables in T (which is a VarSet), then T.map s₁ = T.map s₂

Expression Trees

Morally, a pure Com can be represented as just a tree of expressions. We use this intuition to explain what matchVar does, but first we give a semi-formal definition of ExprTree and its operations.

inductive ExprTree (d : Dialect) [DialectSignature d] (Γ : Ctxt d.Ty) (ty : d.Ty) : Type

A tree of pure expressions

• mk: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → {ty : d.Ty} → (op : d.Op) → ty = DialectSignature.outTy op → DialectSignature.effectKind op = EffectKind.pure → ExprTreeBranches d Γ (DialectSignature.sig op) → ExprTree d Γ ty
• fvar: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → {ty : d.Ty} → Γ.Var ty → ExprTree d Γ ty

inductive ExprTreeBranches (d : Dialect) [DialectSignature d] (Γ : Ctxt d.Ty) : List d.Ty → Type

• nil: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → ExprTreeBranches d Γ []
• cons: {d : Dialect} → [inst : DialectSignature d] → {Γ : Ctxt d.Ty} → {t : d.Ty} → {ts : List d.Ty} → ExprTree d Γ t → ExprTreeBranches d Γ ts → ExprTreeBranches d Γ (t :: ts)

def ExprTreeBranches.ofHVector {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ts : List d.Ty} : HVector (ExprTree d Γ) ts → ExprTreeBranches d Γ ts

Equations

• ↑HVector.nil = ExprTreeBranches.nil
• ↑(v::ₕvs) = ExprTreeBranches.cons v ↑vs

@[irreducible]

def Lets.exprTreeAt {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {ty : d.Ty} (lets : Lets d Γ_in EffectKind.pure Γ_out) (v : Γ_out.Var ty) : ExprTree d Γ_in ty

lets.exprTreeAt v follows the def-use chain of v in lets to produce an ExprTree whose free variables are only the free variables of lets as a whole

Equations

• Lets.nil.exprTreeAt v = ExprTree.fvar v
• (body.var e).exprTreeAt ⟨0, ⋯⟩ = Expr.toExprTree body e
• (body.var e).exprTreeAt ⟨v.succ, h⟩ = body.exprTreeAt ⟨v, h⟩

@[irreducible]

def Expr.toExprTree {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {ty : d.Ty} (lets : Lets d Γ_in EffectKind.pure Γ_out) (e : Expr d Γ_out EffectKind.pure ty) : ExprTree d Γ_in ty

e.toExprTree lets converts a single expression e into an expression tree by looking up the arguments to e in lets

Equations

• Expr.toExprTree lets e = ExprTree.mk e.op ⋯ ⋯ (Expr.toExprTree.argsToBranches lets e.args)

@[irreducible]

def Expr.toExprTree.argsToBranches {d : Dialect} [DialectSignature d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} (lets : Lets d Γ_in EffectKind.pure Γ_out) {ts : List d.Ty} : HVector Γ_out.Var ts → ExprTreeBranches d Γ_in ts

Equations

• Expr.toExprTree.argsToBranches lets HVector.nil = ExprTreeBranches.nil
• Expr.toExprTree.argsToBranches lets (v::ₕvs) = ExprTreeBranches.cons (lets.exprTreeAt v) (Expr.toExprTree.argsToBranches lets vs)

TermModel

We can syntactically give semantics to any dialect by denoting it with ExprTrees

structure TermModelTy (Ty : Type) : Type

A wrapper around the Ty universe of a term model, to prevent the instance of TyDenote leaking to the original type.

• ty : Ty

def TermModel (d : Dialect) (_Γ : Ctxt d.Ty) : Dialect

The Term Model of a dialect d is a dialect with the exact same operations, types, and signature as the original dialect d, but whose denotation exists of expression trees.

Equations

• TermModel d _Γ = { Op := d.Op, Ty := TermModelTy d.Ty, m := d.m }

class PureDialect (d : Dialect) [DialectSignature d] : Prop

• allPure : ∀ (op : d.Op), DialectSignature.effectKind op = EffectKind.pure

theorem PureDialect.allPure {d : Dialect} : ∀ {inst : DialectSignature d} [self : PureDialect d] (op : d.Op), DialectSignature.effectKind op = EffectKind.pure

instance instMonadMTermModel {d : Dialect} {Γ : Ctxt d.Ty} [Monad d.m] : Monad (TermModel d Γ).m

Equations

• instMonadMTermModel = inferInstanceAs (Monad d.m)

instance instDialectSignatureTermModel {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} : DialectSignature (TermModel d Γ)

Equations

• instDialectSignatureTermModel = { signature := fun (op : (TermModel d Γ).Op) => TermModelTy.mk <$> signature op }

instance instTyDenoteTyTermModel {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} : TyDenote (TermModel d Γ).Ty

Equations

• instTyDenoteTyTermModel = { toType := fun (ty : (TermModel d Γ).Ty) => ExprTree d Γ ty.ty }

instance instDialectDenoteTermModelOfPureDialect {d : Dialect} [DialectSignature d] [Monad d.m] {Γ : Ctxt d.Ty} [p : PureDialect d] : DialectDenote (TermModel d Γ)

Equations

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

def instDialectDenoteTermModelOfPureDialect.argsToBranches {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ts : List d.Ty} : HVector TyDenote.toType (TermModelTy.mk <$> ts) → ExprTreeBranches d Γ ts

Equations

• instDialectDenoteTermModelOfPureDialect.argsToBranches HVector.nil = ExprTreeBranches.nil
• instDialectDenoteTermModelOfPureDialect.argsToBranches (a_1::ₕas) = ExprTreeBranches.cons a_1 (instDialectDenoteTermModelOfPureDialect.argsToBranches as)

def Ctxt.Substitution (d : Dialect) [DialectSignature d] (Γ : Ctxt d.Ty) (Δ : Ctxt d.Ty) : Type

A substitution in context Γ maps variables of Γ to expression trees in Δ, in a type-preserving manner

Equations

• Ctxt.Substitution d Γ Δ = ({ty : d.Ty} → Γ.Var ty → ExprTree d Δ ty)

def Ctxt.Substitution.ofValuation {d : Dialect} [DialectSignature d] {Δ : Ctxt d.Ty} {Γ : Ctxt d.Ty} (V : (TermModelTy.mk <$> Γ).Valuation) : Ctxt.Substitution d Γ Δ

A valuation of the term model w.r.t context Δ is exactly a substitution

Equations

• ↑V ⟨v, h⟩ = V ⟨v, ⋯⟩

def Ctxt.Substitution.ofHom {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {Δ : Ctxt d.Ty} (f : Γ.Hom Δ) : Ctxt.Substitution d Γ Δ

A context homomorphism trivially induces a substitution

Equations

• ↑f v = ExprTree.fvar (f v)

def TermModel.morphism {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} : DialectMorphism d (TermModel d Γ)

Equations

• TermModel.morphism = { mapOp := id, mapTy := TermModelTy.mk, preserves_signature := ⋯ }

def Lets.toSubstitution {d : Dialect} [DialectSignature d] [Monad d.m] [PureDialect d] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} (lets : Lets d Γ_in EffectKind.pure Γ_out) : Ctxt.Substitution d Γ_out Γ_in

lets.toSubstitution gives a substitution from each variable in the output context to an expression tree with variables in the input context by following the def-use chain

Equations

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

def ExprTree.applySubstitution {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : d.Ty} {Δ : Ctxt d.Ty} (σ : Ctxt.Substitution d Γ Δ) : ExprTree d Γ ty → ExprTree d Δ ty

e.applySubstitution σ replaces occurences of v in e with σ v

Equations

• ExprTree.applySubstitution σ (ExprTree.fvar v) = σ v
• ExprTree.applySubstitution σ (ExprTree.mk op ⋯ eff_eq args) = ExprTree.mk op ⋯ eff_eq (ExprTreeBranches.applySubstitution (fun {ty : d.Ty} => σ) args)

def ExprTreeBranches.applySubstitution {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {ty : List d.Ty} {Δ : Ctxt d.Ty} (σ : Ctxt.Substitution d Γ Δ) : ExprTreeBranches d Γ ty → ExprTreeBranches d Δ ty

es.applySubstitution σ maps ExprTree.applySubstution over es

Equations

• One or more equations did not get rendered due to their size.
• ExprTreeBranches.applySubstitution σ ExprTreeBranches.nil = ExprTreeBranches.nil

Matching

@[irreducible]

def matchArg {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} [DecidableEq d.Op] (lets : Lets d Γ_in eff Γ_out) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) {l : List d.Ty} : HVector Γ_out.Var l → HVector Δ_out.Var l → Mapping Δ_in Γ_out → Option (Mapping Δ_in Γ_out)

matchArg lets matchLets args matchArgs map tries to extends the partial substition map by calling matchVar lets args[i] matchLets matchArgs[i] for each pair of corresponding variables, returning the final partial substiution, or none on conflicting assigments

Equations

• matchArg lets matchLets HVector.nil HVector.nil x = some x
• matchArg lets matchLets (vₗ::ₕvsₗ) (vᵣ::ₕvsᵣ) x = do let ma ← matchVar lets vₗ matchLets vᵣ x matchArg lets matchLets vsₗ vsᵣ ma

@[irreducible]

def matchVar {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {eff : EffectKind} {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {t : d.Ty} [DecidableEq d.Op] (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (w : Δ_out.Var t) (ma : optParam (Mapping Δ_in Γ_out) ∅) : Option (Mapping Δ_in Γ_out)

matchVar lets v matchLets w map tries to extend the partial substition map, such that the transitive expression trees represented by variables v and w become syntactically equal, returning the final partial substitution map' on success , or none on conflicting assignments.

Diagramatically, the contexts are related as follows: Γ_in --[lets]--> Γ_out <--[map]-- Δ_in --[matchLets]--> Δ_out [v] [w]

Informally, we want to find a map that glues the program matchLets to the end of lets such that the expression tree of v (in lets) is syntactically unified with the expression tree of w (in matchLets).

This obeys the hypothetical equation: (matchLets.exprTreeAt w).changeVars map = lets.exprTreeAt v where exprTreeAt is a hypothetical definition that gives the expression tree.

NOTE: this only matches on pure let bindings in both matchLets and lets.

Equations

• One or more equations did not get rendered due to their size.
• matchVar lets v (matchLets.var e) ⟨w.succ, h⟩ x = matchVar lets v matchLets ⟨w, ⋯⟩ x
• matchVar lets v Lets.nil w x = match AList.lookup ⟨t, w⟩ x with | some v₂ => if v = v₂ then some x else none | none => some (AList.insert ⟨t, w⟩ v x)

theorem matchVar_var_succ_eq {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {eff : EffectKind} {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {t : d.Ty} {te : d.Ty} [DecidableEq d.Op] (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (matchE : Expr d Δ_out EffectKind.pure te) (w : ℕ) (hw : Δ_out.get? w = some t) (ma : Mapping Δ_in Γ_out) : matchVar lets v (matchLets.var matchE) ⟨w + 1, ⋯⟩ ma = matchVar lets v matchLets ⟨w, hw⟩ ma

how matchVar behaves on var at a successor variable

theorem matchVar_var_last_eq {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {eff : EffectKind} {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {t : d.Ty} [DecidableEq d.Op] (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (matchE : Expr d Δ_out EffectKind.pure t) (ma : Mapping Δ_in Γ_out) : matchVar lets v (matchLets.var matchE) (Ctxt.Var.last Δ_out t) ma = do let ie ← lets.getPureExpr v if hs : ∃ (h : ie.op = matchE.op), ie.regArgs = ⋯ ▸ matchE.regArgs then matchArg lets matchLets ie.args (⋯ ▸ matchE.args) ma else none

how matchVar behaves on var at the last variable.

theorem subset_entries {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] : (∀ (Γ_in : Ctxt d.Ty) (eff : EffectKind) (Γ_out Δ_in Δ_out : Ctxt d.Ty) (inst : DecidableEq d.Op) (lets : Lets d Γ_in eff Γ_out) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (l : List d.Ty) (argsl : HVector Γ_out.Var l) (argsr : HVector Δ_out.Var l) (ma varMap : Mapping Δ_in Γ_out), varMap ∈ matchArg lets matchLets argsl argsr ma → ma.entries ⊆ varMap.entries) ∧ ∀ (eff : EffectKind) (Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty) (t : d.Ty) (inst : DecidableEq d.Op) (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (w : Δ_out.Var t) (ma varMap : Mapping Δ_in Γ_out), varMap ∈ matchVar lets v matchLets w ma → ma.entries ⊆ varMap.entries

theorem subset_entries_matchArg {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ_in : Ctxt d.Ty} {eff : EffectKind} [DecidableEq d.Op] {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {lets : Lets d Γ_in eff Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {l : List d.Ty} {argsl : HVector Γ_out.Var l} {argsr : HVector Δ_out.Var l} {ma : Mapping Δ_in Γ_out} {varMap : Mapping Δ_in Γ_out} (hvarMap : varMap ∈ matchArg lets matchLets argsl argsr ma) : ma.entries ⊆ varMap.entries

theorem subset_entries_matchVar {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Δ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Γ_in : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {Δ_out : Ctxt d.Ty} [DecidableEq d.Op] {varMap : Mapping Δ_in Γ_out} {ma : Mapping Δ_in Γ_out} {lets : Lets d Γ_in eff Γ_out} {v : Γ_out.Var t} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {w : Δ_out.Var t} (hvarMap : varMap ∈ matchVar lets v matchLets w ma) : ma.entries ⊆ varMap.entries

matchVar only adds new entries: if matchVar lets v matchLets w ma = .some varMap, then ma is a subset of varMap. Said differently, The output mapping of matchVar extends the input mapping when it succeeds.

theorem denote_matchVar_matchArg {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DecidableEq d.Ty] [DecidableEq d.Op] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {lets : Lets d Γ_in eff Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {l : List d.Ty} {args₁ : HVector Γ_out.Var l} {args₂ : HVector Δ_out.Var l} {ma : Mapping Δ_in Γ_out} {varMap₁ : Mapping Δ_in Γ_out} {varMap₂ : Mapping Δ_in Γ_out} (h_sub : varMap₁.entries ⊆ varMap₂.entries) (f₁ : (t : d.Ty) → Γ_out.Var t → ⟦t⟧) (f₂ : (t : d.Ty) → Δ_out.Var t → ⟦t⟧) (hf : ∀ (t : d.Ty) (v₁ : Γ_out.Var t) (v₂ : Δ_out.Var t) (ma ma' : Mapping Δ_in Γ_out), ma ∈ matchVar lets v₁ matchLets v₂ ma' → ma.entries ⊆ varMap₂.entries → f₂ t v₂ = f₁ t v₁) (hmatchVar : ∀ (vMap : Mapping Δ_in Γ_out) (t : d.Ty) (vₗ : Γ_out.Var t) (vᵣ : Δ_out.Var t) (ma : Mapping Δ_in Γ_out), vMap ∈ matchVar lets vₗ matchLets vᵣ ma → ma.entries ⊆ vMap.entries) (hvarMap : varMap₁ ∈ matchArg lets matchLets args₁ args₂ ma) : HVector.map f₂ args₂ = HVector.map f₁ args₁

@[reducible, inline]

abbrev Expr.IsDenotationForPureE {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) (Γv : Γ.Valuation) (x : ⟦ty⟧) : Prop

e.IsDenotationForPureE Γv x holds if x is the pure value obtained from e under valuation Γv, assuming that e has a pure operation. If e has an impure operation, the property holds vacuously.

Equations

• e.IsDenotationForPureE Γv x = ∀ (ePure : Expr d Γ EffectKind.pure ty), e.toPure? = some ePure → ePure.denote Γv = x

def Expr.denoteIntoSubtype {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ_in eff ty) (Γv : Γ_in.Valuation) : eff.toMonad d.m { x : ⟦ty⟧ // e.IsDenotationForPureE Γv x }

Equations

• e.denoteIntoSubtype Γv = match h_pure : e.toPure? with | some ePure => pure ⟨ePure.denote Γv, ⋯⟩ | none => (fun (x : ⟦ty⟧) => ⟨x, ⋯⟩) <$> e.denote Γv

def Lets.denoteIntoSubtype {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} (lets : Lets d Γ_in eff Γ_out) (Γv : Γ_in.Valuation) : eff.toMonad d.m { V : Γ_out.Valuation // ∀ {t : d.Ty} (v : Γ_out.Var t) (e : Expr d Γ_out EffectKind.pure t), lets.getPureExpr v = some e → e.denote V = V v }

An alternative version of Lets.denote, whose returned type carries a proof that the valuation agrees with the denotation of every pure expression in lets.

Strongly prefer using Lets.denote in definitions, but you can use denoteIntoSubtype in proofs. The subtype allows us to carry the property with us when doing congruence proofs inside a bind.

Equations

• Lets.nil.denoteIntoSubtype Γv = pure ⟨Γv, ⋯⟩
• (body.var e).denoteIntoSubtype Γv = do let __discr ← body.denoteIntoSubtype Γv match __discr with | ⟨Vout, h⟩ => do let v ← e.denoteIntoSubtype Vout pure ⟨Vout::ᵥ↑v, ⋯⟩

theorem Expr.denote_eq_denoteIntoSubtype {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} (e : Expr d Γ eff ty) (Γv : Γ.Valuation) : e.denote Γv = Subtype.val <$> e.denoteIntoSubtype Γv

theorem Lets.denote_eq_denoteIntoSubtype {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} (lets : Lets d Γ_in eff Γ_out) (Γv : Γ_in.Valuation) : lets.denote Γv = Subtype.val <$> lets.denoteIntoSubtype Γv

theorem matchVar_nil {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} : ∀ {t : d.Ty} {v : Γ_out.Var t} {Δ : Ctxt d.Ty} {w : Δ.Var t} {ma ma' : Mapping Δ Γ_out} {lets : Lets d Γ_in eff Γ_out}, matchVar lets v Lets.nil w ma = some ma' → AList.lookup ⟨t, w⟩ ma' = some v

theorem matchVar_var_last {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {ty : d.Ty} {v : Γ_out.Var ty} {ma : Mapping Δ_in Γ_out} {ma' : Mapping Δ_in Γ_out} {lets : Lets d Γ_in eff Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {matchExpr : Expr d Δ_out EffectKind.pure ty} : matchVar lets v (matchLets.var matchExpr) (Ctxt.Var.last Δ_out ty) ma = some ma' → ∃ (args : HVector Γ_out.Var (DialectSignature.sig matchExpr.op)), lets.getPureExpr v = some (Expr.mk matchExpr.op ⋯ ⋯ args matchExpr.regArgs) ∧ matchArg lets matchLets args matchExpr.args ma = some ma'

@[simp]

theorem Lets.denote_var_last_pure {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {ty : d.Ty} (lets : Lets d Γ_in EffectKind.pure Γ_out) (e : Expr d Γ_out EffectKind.pure ty) (V_in : Γ_in.Valuation) : (lets.var e).denote V_in (Ctxt.Var.last Γ_out ty) = e.denote (lets.denote V_in)

@[simp]

theorem Expr.denote_eq_denote_of {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {eff : EffectKind} {ty : d.Ty} {Δ : Ctxt d.Ty} {e₁ : Expr d Γ eff ty} {e₂ : Expr d Δ eff ty} {Γv : Γ.Valuation} {Δv : Δ.Valuation} (op_eq : e₁.op = e₂.op) (h_regArgs : HEq e₁.regArgs e₂.regArgs) (h_args : HVector.map (fun (x : d.Ty) (v : Γ.Var x) => Γv v) (op_eq ▸ e₁.args) = HVector.map (fun (x : d.Ty) (v : Δ.Var x) => Δv v) e₂.args) : e₁.denote Γv = e₂.denote Δv

theorem denote_matchVar2_of_subset {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {α : Type} {lets : Lets d Γ_in eff Γ_out} {v : Γ_out.Var t} {varMap₁ : Mapping Δ_in Γ_out} {varMap₂ : Mapping Δ_in Γ_out} {s₁ : Γ_in.Valuation} {ma : Mapping Δ_in Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {w : Δ_out.Var t} (h_sub : varMap₁.entries ⊆ varMap₂.entries) (h_matchVar : varMap₁ ∈ matchVar lets v matchLets w ma) (f : Γ_out.Valuation → ⟦t⟧ → eff.toMonad d.m α) : (do let Γ_out_lets ← lets.denote s₁ f Γ_out_lets (matchLets.denote (fun (t' : d.Ty) (v' : Δ_in.Var t') => match AList.lookup ⟨t', v'⟩ varMap₂ with | some mappedVar => Γ_out_lets mappedVar | none => default) w)) = do let Γ_out_lets ← lets.denote s₁ f Γ_out_lets (Γ_out_lets v)

theorem denote_matchVar2 {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {eff : EffectKind} {Γ_out : Ctxt d.Ty} {t : d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {α : Type} {lets : Lets d Γ_in eff Γ_out} {v : Γ_out.Var t} {varMap : Mapping Δ_in Γ_out} {s₁ : Γ_in.Valuation} {ma : Mapping Δ_in Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {w : Δ_out.Var t} {f : Γ_out.Valuation → ⟦t⟧ → eff.toMonad d.m α} : varMap ∈ matchVar lets v matchLets w ma → (do let Γvlets ← lets.denote s₁ f Γvlets (matchLets.denote (fun (t' : d.Ty) (v' : Δ_in.Var t') => match AList.lookup ⟨t', v'⟩ varMap with | some mappedVar => Γvlets mappedVar | none => default) w)) = do let Γv ← lets.denote s₁ f Γv (Γv v)

if matchVar lets v matchLets w ma = .some varMap, then informally:

Γ_in --⟦lets⟧--> Γ_out --comap ma--> Δ_in --⟦matchLets⟧ --> Δ_out --w--> t = Γ_in ⟦lets⟧ --> Γ_out --v--> t

@[simp]

theorem lt_one_add_add (a : ℕ) (b : ℕ) : b < 1 + a + b

@[simp]

theorem zero_eq_zero : Zero.zero = 0

@[irreducible]

theorem mem_matchVar_matchArg {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {eff : EffectKind} {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {lets : Lets d Γ_in eff Γ_out} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {l : List d.Ty} {argsₗ : HVector Γ_out.Var l} {argsᵣ : HVector Δ_out.Var l} {ma : Mapping Δ_in Γ_out} {varMap : Mapping Δ_in Γ_out} (hvarMap : varMap ∈ matchArg lets matchLets argsₗ argsᵣ ma) {t' : d.Ty} {v' : Δ_in.Var t'} : (⟨t', v'⟩ ∈ Finset.biUnion argsᵣ.vars fun (v : (t : d.Ty) × Δ_out.Var t) => matchLets.vars v.snd) → ⟨t', v'⟩ ∈ varMap

@[irreducible]

theorem mem_matchVar {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {Δ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Γ_in : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} {Δ_out : Ctxt d.Ty} {varMap : Mapping Δ_in Γ_out} {ma : Mapping Δ_in Γ_out} {lets : Lets d Γ_in eff Γ_out} {v : Γ_out.Var t} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {w : Δ_out.Var t} (hvarMap : varMap ∈ matchVar lets v matchLets w ma) {t' : d.Ty} {v' : Δ_in.Var t'} (hMatchLets : ⟨t', v'⟩ ∈ matchLets.vars w) : ⟨t', v'⟩ ∈ varMap

All variables containing in matchExpr are assigned by matchVar.

def matchVarMap {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {eff : EffectKind} {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {t : d.Ty} (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t) (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (w : Δ_out.Var t) (hvars : ∀ (t_1 : d.Ty) (v : Δ_in.Var t_1), ⟨t_1, v⟩ ∈ matchLets.vars w) : Option (Δ_in.Hom Γ_out)

A version of matchVar that returns a Hom of Ctxts instead of the AList, provided every variable in the context appears as a free variable in matchExpr.

Equations

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

theorem denote_matchVarMap2 {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] {eff : EffectKind} {α : Type} [LawfulMonad d.m] {Γ_in : Ctxt d.Ty} {Γ_out : Ctxt d.Ty} {Δ_in : Ctxt d.Ty} {Δ_out : Ctxt d.Ty} {lets : Lets d Γ_in eff Γ_out} {t : d.Ty} {v : Γ_out.Var t} {matchLets : Lets d Δ_in EffectKind.pure Δ_out} {w : Δ_out.Var t} {hvars : ∀ (t_1 : d.Ty) (v : Δ_in.Var t_1), ⟨t_1, v⟩ ∈ matchLets.vars w} {map : Δ_in.Hom Γ_out} (hmap : map ∈ matchVarMap lets v matchLets w hvars) (s₁ : Γ_in.Valuation) (f : Γ_out.Valuation → ⟦t⟧ → eff.toMonad d.m α) : (do let Γ_out_v ← lets.denote s₁ f Γ_out_v (matchLets.denote (Γ_out_v.comap map) w)) = do let Γ_out_v ← lets.denote s₁ f Γ_out_v (Γ_out_v v)

if matchVarMap lets v matchLets w hvars = .some map, then ⟦lets; matchLets⟧ = ⟦lets⟧(v)

def splitProgramAtAux {d : Dialect} [DialectSignature d] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} {Γ₂ : Ctxt d.Ty} {t : d.Ty} (pos : ℕ) (lets : Lets d Γ₁ eff Γ₂) (prog : Com d Γ₂ eff t) : Option ((Γ₃ : Ctxt d.Ty) × Lets d Γ₁ eff Γ₃ × Com d Γ₃ eff t × (t' : d.Ty) × Γ₃.Var t')

splitProgramAtAux pos lets prog, will return a Lets ending with the posth variable in prog, and an Com starting with the next variable. It also returns, the type of this variable and the variable itself as an element of the output Ctxt of the returned Lets.

Equations

• splitProgramAtAux 0 x (Com.var e body) = some ⟨Γ₂.snoc α, (x.var e, body, ⟨α, Ctxt.Var.last Γ₂ α⟩)⟩
• splitProgramAtAux x✝ x (Com.ret v) = none
• splitProgramAtAux n.succ x (Com.var e body) = splitProgramAtAux n (x.var e) body

theorem denote_splitProgramAtAux {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} {Γ₂ : Ctxt d.Ty} {t : d.Ty} [LawfulMonad d.m] {pos : ℕ} {lets : Lets d Γ₁ eff Γ₂} {prog : Com d Γ₂ eff t} {res : (Γ₃ : Ctxt d.Ty) × Lets d Γ₁ eff Γ₃ × Com d Γ₃ eff t × (t' : d.Ty) × Γ₃.Var t'} (hres : res ∈ splitProgramAtAux pos lets prog) (s : Γ₁.Valuation) : res.snd.1.denote s >>= res.snd.2.1.denote = lets.denote s >>= prog.denote

def splitProgramAt {d : Dialect} [DialectSignature d] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} (pos : ℕ) (prog : Com d Γ₁ eff t) : Option ((Γ₂ : Ctxt d.Ty) × Lets d Γ₁ eff Γ₂ × Com d Γ₂ eff t × (t' : d.Ty) × Γ₂.Var t')

splitProgramAt pos prog, will return a Lets ending with the posth variable in prog, and an Com starting with the next variable. It also returns, the type of this variable and the variable itself as an element of the output Ctxt of the returned Lets.

Equations

• splitProgramAt pos prog = splitProgramAtAux pos Lets.nil prog

theorem denote_splitProgramAt {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ₁ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} [LawfulMonad d.m] {pos : ℕ} {prog : Com d Γ₁ eff t} {res : (Γ₂ : Ctxt d.Ty) × Lets d Γ₁ eff Γ₂ × Com d Γ₂ eff t × (t' : d.Ty) × Γ₂.Var t'} (hres : res ∈ splitProgramAt pos prog) (s : Γ₁.Valuation) : res.snd.1.denote s >>= res.snd.2.1.denote = prog.denote s

def rewriteAt {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] [DecidableEq d.Op] {Γ₁ : Ctxt d.Ty} {t₁ : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (lhs : Com d Γ₁ EffectKind.pure t₁) (rhs : Com d Γ₁ EffectKind.pure t₁) (hlhs : ∀ (t : d.Ty) (v : Γ₁.Var t), ⟨t, v⟩ ∈ lhs.vars) (pos : ℕ) (target : Com d Γ₂ eff t₂) : Option (Com d Γ₂ eff t₂)

rewriteAt lhs rhs hlhs pos target, searches for lhs at position pos of target. If it can match the variables, it inserts rhs into the program with the correct assignment of variables, and then replaces occurences of the variable at position pos in target with the output of rhs.

Equations

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

@[simp]

theorem Com.denote_toFlatCom_lets {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} [LawfulMonad d.m] (com : Com d Γ EffectKind.pure t) : com.toFlatCom.lets.denote = com.denoteLets

@[simp]

theorem Com.toFlatCom_ret {d : Dialect} [DialectSignature d] [Monad d.m] {Γ : Ctxt d.Ty} {t : d.Ty} [LawfulMonad d.m] (com : Com d Γ EffectKind.pure t) : com.toFlatCom.ret = com.returnVar

theorem denote_rewriteAt {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] {Γ₁ : Ctxt d.Ty} {t₁ : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} [LawfulMonad d.m] (lhs : Com d Γ₁ EffectKind.pure t₁) (rhs : Com d Γ₁ EffectKind.pure t₁) (hlhs : ∀ (t : d.Ty) (v : Γ₁.Var t), ⟨t, v⟩ ∈ lhs.vars) (pos : ℕ) (target : Com d Γ₂ eff t₂) (hl : lhs.denote = rhs.denote) (rew : Com d Γ₂ eff t₂) (hrew : rew ∈ rewriteAt lhs rhs hlhs pos target) : rew.denote = target.denote

structure PeepholeRewrite (d : Dialect) [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] (Γ : List d.Ty) (t : d.Ty) : Type

Rewrites are indexed with a concrete list of types, rather than an (erased) context, so that the required variable checks become decidable

• lhs : Com d (↑Γ) EffectKind.pure t
• rhs : Com d (↑Γ) EffectKind.pure t
• correct : self.lhs.denote = self.rhs.denote

theorem PeepholeRewrite.correct {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {Γ : List d.Ty} {t : d.Ty} (self : PeepholeRewrite d Γ t) : self.lhs.denote = self.rhs.denote

instance instDecidableForallForallMemSigmaTyVarOfListVarSetVars {d : Dialect} [DialectSignature d] [DecidableEq d.Ty] {Γ : List d.Ty} {t' : d.Ty} {lhs : Com d (↑Γ) EffectKind.pure t'} : Decidable (∀ (t : d.Ty) (v : (↑Γ).Var t), ⟨t, v⟩ ∈ lhs.vars)

Equations

• instDecidableForallForallMemSigmaTyVarOfListVarSetVars = decidable_of_iff (∀ (i : Fin Γ.length), let v := ⟨↑i, ⋯⟩; ⟨Γ.get i, v⟩ ∈ lhs.vars) ⋯

def rewritePeepholeAt {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [DecidableEq d.Op] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (pr : PeepholeRewrite d Γ t) (pos : ℕ) (target : Com d Γ₂ eff t₂) : Com d Γ₂ eff t₂

Equations

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

theorem denote_rewritePeepholeAt {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (pr : PeepholeRewrite d Γ t) (pos : ℕ) (target : Com d Γ₂ eff t₂) : (rewritePeepholeAt pr pos target).denote = target.denote

def rewritePeephole_go {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [DecidableEq d.Op] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) (ix : ℕ) (target : Com d Γ₂ eff t₂) : Com d Γ₂ eff t₂

rewrite with pr to target program, at location ix and later, running at most fuel steps.

Equations

• rewritePeephole_go 0 pr ix target = target
• rewritePeephole_go fuel'.succ pr ix target = rewritePeephole_go fuel' pr (ix + 1) (rewritePeepholeAt pr ix target)

def rewritePeephole {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [DecidableEq d.Op] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) (target : Com d Γ₂ eff t₂) : Com d Γ₂ eff t₂

rewrite with pr to target program, running at most fuel steps.

Equations

• rewritePeephole fuel pr target = rewritePeephole_go fuel pr 0 target

theorem denote_rewritePeephole_go {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} {fuel : ℕ} (pr : PeepholeRewrite d Γ t) (pos : ℕ) (target : Com d Γ₂ eff t₂) : (rewritePeephole_go fuel pr pos target).denote = target.denote

rewritePeephole_go preserve semantics

theorem denote_rewritePeephole {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) (target : Com d Γ₂ eff t₂) : (rewritePeephole fuel pr target).denote = target.denote

rewritePeephole preserves semantics.

theorem Expr.denote_eq_of_region_denote_eq {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [Monad d.m] {ty : d.Ty} {eff : EffectKind} {Γ : Ctxt d.Ty} (op : d.Op) (ty_eq : ty = DialectSignature.outTy op) (eff' : DialectSignature.effectKind op ≤ eff) (args : HVector Γ.Var (DialectSignature.sig op)) (regArgs : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) (regArgs' : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) (DialectSignature.regSig op)) (hregArgs' : regArgs'.denote = regArgs.denote) : (Expr.mk op ty_eq eff' args regArgs').denote = (Expr.mk op ty_eq eff' args regArgs).denote

@[irreducible]

def rewritePeepholeRecursivelyRegArgs {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) {ts : List (Ctxt d.Ty × d.Ty)} (args : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts) : { out : HVector (fun (t : Ctxt d.Ty × d.Ty) => Com d t.1 EffectKind.impure t.2) ts // out.denote = args.denote }

Equations

• One or more equations did not get rendered due to their size.
• rewritePeepholeRecursivelyRegArgs fuel pr HVector.nil = ⟨HVector.nil, ⋯⟩

@[irreducible]

def rewritePeepholeRecursivelyExpr {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) {ty : d.Ty} (e : Expr d Γ₂ eff ty) : { out : Expr d Γ₂ eff ty // out.denote = e.denote }

Equations

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

@[irreducible]

def rewritePeepholeRecursively {d : Dialect} [DialectSignature d] [TyDenote d.Ty] [DialectDenote d] [DecidableEq d.Ty] [Monad d.m] [(t : d.Ty) → Inhabited ⟦t⟧] [DecidableEq d.Op] [LawfulMonad d.m] {Γ : List d.Ty} {t : d.Ty} {Γ₂ : Ctxt d.Ty} {eff : EffectKind} {t₂ : d.Ty} (fuel : ℕ) (pr : PeepholeRewrite d Γ t) (target : Com d Γ₂ eff t₂) : { out : Com d Γ₂ eff t₂ // out.denote = target.denote }

A peephole rewriter that recurses into regions, allowing peephole rewriting into nested code.

Equations

• One or more equations did not get rendered due to their size.
• rewritePeepholeRecursively 0 pr target = ⟨target, ⋯⟩

def Com.getTy {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Com d Γ eff t → Type

Equations

• x.getTy = d.Ty

def Com.ty {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Com d Γ eff t → d.Ty

Equations

• x.ty = t

def Com.ctxt {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Com d Γ eff t → Ctxt d.Ty

Equations

• x.ctxt = Γ

def Expr.getTy {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Expr d Γ eff t → Type

Equations

• x.getTy = d.Ty

def Expr.ty {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Expr d Γ eff t → d.Ty

Equations

• x.ty = t

def Expr.ctxt {d : Dialect} [DialectSignature d] {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty} : Expr d Γ eff t → Ctxt d.Ty

Equations

• x.ctxt = Γ