def MLIR.VarName : Type

VarName is the type of (human-readable) variable names

Equations

• MLIR.VarName = String

def MLIR.BlockLabel : Type

BlockLabel is the type of (human-readable) basic block labels

Equations

• MLIR.BlockLabel = String

instance MLIR.instDecidableEqVarName : DecidableEq MLIR.VarName

Equations

• MLIR.instDecidableEqVarName = id inferInstance

instance MLIR.instDecidableEqBlockLabel : DecidableEq MLIR.BlockLabel

Equations

• MLIR.instDecidableEqBlockLabel = id inferInstance

inductive MLIR.UnTyped.Expr (Op : Type) (T : Type) : Type

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

• mk: {Op T : Type} → MLIR.VarName → Op → List MLIR.VarName → List (MLIR.UnTyped.Region Op T) → MLIR.UnTyped.Expr Op T

inductive MLIR.UnTyped.Lets (Op : Type) (T : Type) : Type

Lets is a sequence of operations (without terminator), which grows downwards. That is, the head of the list represents the first operation to be executed

• mk: {Op T : Type} → List (MLIR.UnTyped.Expr Op T) → MLIR.UnTyped.Lets Op T

inductive MLIR.UnTyped.Body (Op : Type) (T : Type) : Type

The Body of a basic block is a sequence of operations, followed by a terminator

• mk: {Op T : Type} → MLIR.UnTyped.Lets Op T → T → MLIR.UnTyped.Body Op T

inductive MLIR.UnTyped.BasicBlock (Op : Type) (T : Type) : Type

A basic block has a label, a set of arguments, and then a program

• mk: {Op T : Type} → MLIR.BlockLabel → List MLIR.VarName → MLIR.UnTyped.Body Op T → MLIR.UnTyped.BasicBlock Op T

inductive MLIR.UnTyped.Region (Op : Type) (T : Type) : Type

A region consists of one or more basic blocks, where the first basic block is known as the entry block

• mk: {Op T : Type} → MLIR.UnTyped.BasicBlock Op T → List (MLIR.UnTyped.BasicBlock Op T) → MLIR.UnTyped.Region Op T

Projections

def MLIR.UnTyped.Expr.varName {Op : Type} {T : Type} : MLIR.UnTyped.Expr Op T → MLIR.VarName

Equations

• (MLIR.UnTyped.Expr.mk varName op args regions).varName = varName

def MLIR.UnTyped.Expr.op {Op : Type} {T : Type} : MLIR.UnTyped.Expr Op T → Op

Equations

• (MLIR.UnTyped.Expr.mk varName op args regions).op = op

@[simp]

theorem MLIR.UnTyped.Expr.op_mk {Op : Type} {T : Type} {varName : MLIR.VarName} {op : Op} {args : List MLIR.VarName} {regions : List (MLIR.UnTyped.Region Op T)} : (MLIR.UnTyped.Expr.mk varName op args regions).op = op

@[simp]

theorem MLIR.UnTyped.Expr.varName_mk {Op : Type} {T : Type} {varName : MLIR.VarName} {op : Op} {args : List MLIR.VarName} {regions : List (MLIR.UnTyped.Region Op T)} : (MLIR.UnTyped.Expr.mk varName op args regions).varName = varName

def MLIR.UnTyped.Lets.inner {Op : Type} {T : Type} : MLIR.UnTyped.Lets Op T → List (MLIR.UnTyped.Expr Op T)

Equations

• (MLIR.UnTyped.Lets.mk inner).inner = inner

@[simp]

theorem MLIR.UnTyped.Lets.mk_inner {Op : Type} {T : Type} (lets : MLIR.UnTyped.Lets Op T) : MLIR.UnTyped.Lets.mk lets.inner = lets

@[simp]

theorem MLIR.UnTyped.Lets.inner_mk {Op : Type} {T : Type} (lets : List (MLIR.UnTyped.Expr Op T)) : (MLIR.UnTyped.Lets.mk lets).inner = lets

def MLIR.UnTyped.BasicBlock.args {Op : Type} {T : Type} : MLIR.UnTyped.BasicBlock Op T → List MLIR.VarName

Equations

• (MLIR.UnTyped.BasicBlock.mk label args body).args = args

def MLIR.UnTyped.BasicBlock.body {Op : Type} {T : Type} : MLIR.UnTyped.BasicBlock Op T → MLIR.UnTyped.Body Op T

Equations

• (MLIR.UnTyped.BasicBlock.mk label args body).body = body