Types

def MLIR.SimplyTyped.Var {Ty : Type} (Γ : MLIR.SimplyTyped.Context Ty) (ty : Ty) : Type

An instrinsically well-typed variable

Equations

• MLIR.SimplyTyped.Var Γ ty = { v : MLIR.VarName // Γ.hasType v ty }

def MLIR.SimplyTyped.VarList {Ty : Type} (Γ : MLIR.SimplyTyped.Context Ty) (tys : List Ty) : Type

A list of instrinsically well-typed variables

Equations

• MLIR.SimplyTyped.VarList Γ tys = { vs : List MLIR.VarName // vs.length = tys.length ∧ ∀ v ∈ vs.zip tys, Γ.hasType v.1 v.2 }

def MLIR.SimplyTyped.Expr (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ : MLIR.SimplyTyped.Context Ty) (ty : Ty) : Type

An Expr binds the result of a single operation to a new variable. Morally, it represents $varName = $op($args) { $regions }

Equations

• MLIR.SimplyTyped.Expr Op Γ ty = { expr : MLIR.UnTyped.Expr Op MLIR.VarName // MLIR.SimplyTyped.Expr.WellTyped Γ expr ty }

def MLIR.SimplyTyped.Lets (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ_in : MLIR.SimplyTyped.Context Ty) (Γ_out : MLIR.SimplyTyped.Context Ty) : Type

Lets is an intrinsically well-typed sequence of operations, which grows downwards. That is, the head of the list represents the first operation to be executed

Equations

• MLIR.SimplyTyped.Lets Op Γ_in Γ_out = { lets : MLIR.UnTyped.Lets Op MLIR.VarName // MLIR.SimplyTyped.Lets.WellTyped Γ_in lets Γ_out }

def MLIR.SimplyTyped.RevLets (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ_in : MLIR.SimplyTyped.Context Ty) (Γ_out : MLIR.SimplyTyped.Context Ty) : Type

RevLets is an intrinsically well-typed sequence of operations, which grows upwards. That is, the head of the list represents the last operation to be executed, and in particular, may refer to any variables defined in the tail of the list

Equations

• MLIR.SimplyTyped.RevLets Op Γ_in Γ_out = { lets : MLIR.UnTyped.Lets Op MLIR.VarName // MLIR.SimplyTyped.Lets.WellTyped Γ_in (MLIR.UnTyped.Lets.mk lets.inner.reverse) Γ_out }

def MLIR.SimplyTyped.Body (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ : MLIR.SimplyTyped.Context Ty) (ty : Ty) : Type

Equations

• MLIR.SimplyTyped.Body Op Γ ty = { body : MLIR.UnTyped.Body Op MLIR.VarName // MLIR.SimplyTyped.Body.WellTyped Γ body ty }

def MLIR.SimplyTyped.BasicBlock (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (ty : MLIR.SimplyTyped.RegionType Ty) : Type

Equations

• MLIR.SimplyTyped.BasicBlock Op ty = { block : MLIR.UnTyped.BasicBlock Op MLIR.VarName // MLIR.SimplyTyped.BasicBlock.WellTyped block ty }

def MLIR.SimplyTyped.Region (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (ty : MLIR.SimplyTyped.RegionType Ty) : Type

Equations

• MLIR.SimplyTyped.Region Op ty = { region : MLIR.UnTyped.Region Op MLIR.VarName // MLIR.SimplyTyped.Region.WellTyped region ty }

def MLIR.SimplyTyped.RegionList (Op : Type) {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (tys : List (MLIR.SimplyTyped.RegionType Ty)) : Type

Equations

• MLIR.SimplyTyped.RegionList Op tys = { regions : List (MLIR.UnTyped.Region Op MLIR.VarName) // MLIR.SimplyTyped.RegionList.WellTyped regions tys }

Projections

@[reducible, inline]

abbrev MLIR.SimplyTyped.Expr.varName {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (e : MLIR.SimplyTyped.Expr Op Γ ty) : MLIR.VarName

Equations

• e.varName = (↑e).varName

@[reducible, inline]

abbrev MLIR.SimplyTyped.Expr.op {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (e : MLIR.SimplyTyped.Expr Op Γ ty) : Op

Equations

• e.op = (↑e).op

theorem MLIR.SimplyTyped.Expr.ty_eq {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (e : MLIR.SimplyTyped.Expr Op Γ ty) : ty = (MLIR.SimplyTyped.OpSignature.signature e.op).returnType

@[reducible, inline]

abbrev MLIR.SimplyTyped.Lets.inner {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ_in : MLIR.SimplyTyped.Context Ty} {Γ_out : MLIR.SimplyTyped.Context Ty} (l : MLIR.SimplyTyped.Lets Op Γ_in Γ_out) : List (MLIR.UnTyped.Expr Op MLIR.VarName)

Equations

• l.inner = (↑l).inner

def MLIR.SimplyTyped.Lets.ofUnTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (lets : MLIR.UnTyped.Lets Op MLIR.VarName) {Γ_in : MLIR.SimplyTyped.Context Ty} (h : ∃ (Γ_out : MLIR.SimplyTyped.Context Ty), MLIR.SimplyTyped.Lets.WellTyped Γ_in lets Γ_out) : MLIR.SimplyTyped.Lets Op Γ_in (MLIR.SimplyTyped.Lets.outContext lets Γ_in)

Equations

• MLIR.SimplyTyped.Lets.ofUnTyped lets h = ⟨lets, ⋯⟩

theorem MLIR.SimplyTyped.Lets.Γ_out_eq {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ_in : MLIR.SimplyTyped.Context Ty} {Γ_out : MLIR.SimplyTyped.Context Ty} (l : MLIR.SimplyTyped.Lets Op Γ_in Γ_out) : Γ_out = MLIR.SimplyTyped.Lets.outContext (↑l) Γ_in

def MLIR.SimplyTyped.Body.returnContext {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} : MLIR.SimplyTyped.Body Op Γ ty → MLIR.SimplyTyped.Context Ty

The context under which the return statement of a body is typed

Equations

• MLIR.SimplyTyped.Body.returnContext ⟨MLIR.UnTyped.Body.mk lets terminator, property⟩ = MLIR.SimplyTyped.Lets.outContext lets Γ

def MLIR.SimplyTyped.Body.lets {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (body : MLIR.SimplyTyped.Body Op Γ ty) : MLIR.SimplyTyped.Lets Op Γ body.returnContext

Equations

• MLIR.SimplyTyped.Body.lets ⟨MLIR.UnTyped.Body.mk lets terminator, property⟩ = ⟨lets, ⋯⟩

def MLIR.SimplyTyped.Body.return {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (body : MLIR.SimplyTyped.Body Op Γ ty) : MLIR.SimplyTyped.Var body.returnContext ty

Equations

• MLIR.SimplyTyped.Body.return ⟨MLIR.UnTyped.Body.mk lets terminator, property⟩ = ⟨terminator, ⋯⟩

Constructors

def MLIR.SimplyTyped.Expr.mk {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (varName : MLIR.VarName) (op : Op) (ty_eq : ty = (MLIR.SimplyTyped.OpSignature.signature op).returnType) (args : MLIR.SimplyTyped.VarList Γ (MLIR.SimplyTyped.OpSignature.signature op).arguments) (regions : MLIR.SimplyTyped.RegionList Op (MLIR.SimplyTyped.OpSignature.signature op).regions) : MLIR.SimplyTyped.Expr Op Γ ty

Equations

• MLIR.SimplyTyped.Expr.mk varName op ty_eq args regions = ⟨MLIR.UnTyped.Expr.mk varName op ↑args ↑regions, ⋯⟩

def MLIR.SimplyTyped.Lets.nil {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} : MLIR.SimplyTyped.Lets Op Γ Γ

The empty sequence of operations

Equations

• MLIR.SimplyTyped.Lets.nil = ⟨MLIR.UnTyped.Lets.mk [], ⋯⟩

def MLIR.SimplyTyped.Lets.lete {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ_in : MLIR.SimplyTyped.Context Ty} {ty : Ty} {Γ_out : MLIR.SimplyTyped.Context Ty} (e : MLIR.SimplyTyped.Expr Op Γ_in ty) (lets : MLIR.SimplyTyped.Lets Op (Γ_in.push e.varName ty) Γ_out) : MLIR.SimplyTyped.Lets Op Γ_in Γ_out

Add a new operation to the top of the sequence, abstracting over a previously free variable

Equations

• MLIR.SimplyTyped.Lets.lete e lets = ⟨MLIR.UnTyped.Lets.mk (↑e :: lets.inner), ⋯⟩

def MLIR.SimplyTyped.Body.mk {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ_in : MLIR.SimplyTyped.Context Ty} {Γ_out : MLIR.SimplyTyped.Context Ty} {ty : Ty} (lets : MLIR.SimplyTyped.Lets Op Γ_in Γ_out) (ret : MLIR.SimplyTyped.Var Γ_out ty) : MLIR.SimplyTyped.Body Op Γ_in ty

Equations

• MLIR.SimplyTyped.Body.mk lets ret = ⟨MLIR.UnTyped.Body.mk ↑lets ↑ret, ⋯⟩

def MLIR.SimplyTyped.Body.mkReturn {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} (v : MLIR.SimplyTyped.Var Γ ty) : MLIR.SimplyTyped.Body Op Γ ty

Return an empty Body, whose terminator is "return v"

Equations

• MLIR.SimplyTyped.Body.mkReturn v = MLIR.SimplyTyped.Body.mk MLIR.SimplyTyped.Lets.nil v

def MLIR.SimplyTyped.Body.lete {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {eTy : Ty} {ty : Ty} (e : MLIR.SimplyTyped.Expr Op Γ eTy) : MLIR.SimplyTyped.Body Op (Γ.push e.varName eTy) ty → MLIR.SimplyTyped.Body Op Γ ty

Add a new operation to the top of a Body, abstracting over a previously free variable

Equations

• MLIR.SimplyTyped.Body.lete e ⟨MLIR.UnTyped.Body.mk lets ret, h_body⟩ = MLIR.SimplyTyped.Body.mk (MLIR.SimplyTyped.Lets.lete e ⟨lets, ⋯⟩) ⟨ret, ⋯⟩

Eliminators / Induction Principles

def MLIR.SimplyTyped.Expr.recOn {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {ty : Ty} {motive : MLIR.SimplyTyped.Expr Op Γ ty → Sort u} (mk : (varName : MLIR.VarName) → (op : Op) → (ty_eq : ty = (MLIR.SimplyTyped.OpSignature.signature op).returnType) → (args : MLIR.SimplyTyped.VarList Γ (MLIR.SimplyTyped.OpSignature.signature op).arguments) → (regions : MLIR.SimplyTyped.RegionList Op (MLIR.SimplyTyped.OpSignature.signature op).regions) → motive (MLIR.SimplyTyped.Expr.mk varName op ty_eq args regions)) (e : MLIR.SimplyTyped.Expr Op Γ ty) : motive e

Equations

• MLIR.SimplyTyped.Expr.recOn mk ⟨MLIR.UnTyped.Expr.mk varName op args regions, h⟩ = cast ⋯ (mk varName op ⋯ ⟨args, ⋯⟩ ⟨regions, ⋯⟩)

def MLIR.SimplyTyped.Lets.recOn {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ_out : MLIR.SimplyTyped.Context Ty} {motive : {Γ_in : MLIR.SimplyTyped.Context Ty} → MLIR.SimplyTyped.Lets Op Γ_in Γ_out → Sort u} (nil : motive MLIR.SimplyTyped.Lets.nil) (lete : {Γ_in : MLIR.SimplyTyped.Context Ty} → {ty : Ty} → (e : MLIR.SimplyTyped.Expr Op Γ_in ty) → (lets : MLIR.SimplyTyped.Lets Op (Γ_in.push e.varName ty) Γ_out) → motive (MLIR.SimplyTyped.Lets.lete e lets)) {Γ_in : MLIR.SimplyTyped.Context Ty} (lets : MLIR.SimplyTyped.Lets Op Γ_in Γ_out) : motive lets

Equations

• One or more equations did not get rendered due to their size.
• MLIR.SimplyTyped.Lets.recOn nil lete ⟨MLIR.UnTyped.Lets.mk (e :: lets), h⟩ = cast ⋯ (lete ⟨e, ⋯⟩ ⟨MLIR.UnTyped.Lets.mk lets, ⋯⟩)