Documentation

SSA.Core.MLIRSyntax.AST

MLIR Syntax AST #

This file contains the AST datastructures for generic MLIR syntax

inductive MLIR.AST.AffineExpr :

Var: String → MLIR.AST.AffineExpr

Instances For

instance MLIR.AST.instDecidableEqAffineExpr :

DecidableEq MLIR.AST.AffineExpr

Equations

MLIR.AST.instDecidableEqAffineExpr = MLIR.AST.decEqAffineExpr✝

instance MLIR.AST.instReprAffineExpr :

Repr MLIR.AST.AffineExpr

Equations

MLIR.AST.instReprAffineExpr = { reprPrec := MLIR.AST.reprAffineExpr✝ }

inductive MLIR.AST.AffineTuple :

mk: List MLIR.AST.AffineExpr → MLIR.AST.AffineTuple

Instances For

instance MLIR.AST.instDecidableEqAffineTuple :

DecidableEq MLIR.AST.AffineTuple

Equations

MLIR.AST.instDecidableEqAffineTuple = MLIR.AST.decEqAffineTuple✝

instance MLIR.AST.instReprAffineTuple :

Repr MLIR.AST.AffineTuple

Equations

MLIR.AST.instReprAffineTuple = { reprPrec := MLIR.AST.reprAffineTuple✝ }

inductive MLIR.AST.AffineMap :

mk: MLIR.AST.AffineTuple → MLIR.AST.AffineTuple → MLIR.AST.AffineMap

Instances For

instance MLIR.AST.instDecidableEqAffineMap :

DecidableEq MLIR.AST.AffineMap

Equations

MLIR.AST.instDecidableEqAffineMap = MLIR.AST.decEqAffineMap✝

instance MLIR.AST.instReprAffineMap :

Repr MLIR.AST.AffineMap

Equations

MLIR.AST.instReprAffineMap = { reprPrec := MLIR.AST.reprAffineMap✝ }

inductive MLIR.AST.BBName :

mk: String → MLIR.AST.BBName

Instances For

instance MLIR.AST.instDecidableEqBBName :

DecidableEq MLIR.AST.BBName

Equations

MLIR.AST.instDecidableEqBBName = MLIR.AST.decEqBBName✝

instance MLIR.AST.instReprBBName :

Repr MLIR.AST.BBName

Equations

MLIR.AST.instReprBBName = { reprPrec := MLIR.AST.reprBBName✝ }

inductive MLIR.AST.SSAVal :

An ssa value is a variable name

SSAVal: String → MLIR.AST.SSAVal

Instances For

instance MLIR.AST.instDecidableEqSSAVal :

DecidableEq MLIR.AST.SSAVal

Equations

MLIR.AST.instDecidableEqSSAVal = MLIR.AST.decEqSSAVal✝

instance MLIR.AST.instReprSSAVal :

Repr MLIR.AST.SSAVal

Equations

MLIR.AST.instReprSSAVal = { reprPrec := MLIR.AST.reprSSAVal✝ }

def MLIR.AST.SSAValToString (s : MLIR.AST.SSAVal) :

Equations

MLIR.AST.SSAValToString (MLIR.AST.SSAVal.SSAVal a) = a

Instances For

instance MLIR.AST.instToStringSSAVal :

ToString MLIR.AST.SSAVal

Equations

MLIR.AST.instToStringSSAVal = { toString := MLIR.AST.SSAValToString }

inductive MLIR.AST.Signedness :

Instances For

instance MLIR.AST.instDecidableEqSignedness :

DecidableEq MLIR.AST.Signedness

Equations

MLIR.AST.instDecidableEqSignedness x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance MLIR.AST.instReprSignedness :

Repr MLIR.AST.Signedness

Equations

MLIR.AST.instReprSignedness = { reprPrec := MLIR.AST.reprSignedness✝ }

@[reducible, inline]

abbrev MLIR.AST.Width (φ : ℕ) :

Equations

MLIR.AST.Width φ = ConcreteOrMVar ℕ φ

Instances For

@[reducible, inline]

abbrev MLIR.AST.Width.concrete {φ : ℕ} :

ℕ → MLIR.AST.Width φ

Equations

MLIR.AST.Width.concrete = ConcreteOrMVar.concrete

Instances For

@[reducible, inline]

abbrev MLIR.AST.Width.mvar {φ : ℕ} :

Fin φ → MLIR.AST.Width φ

Equations

MLIR.AST.Width.mvar = ConcreteOrMVar.mvar

Instances For

inductive MLIR.AST.MLIRType (φ : ℕ) :

int: {φ : ℕ} → MLIR.AST.Signedness → MLIR.AST.Width φ → MLIR.AST.MLIRType φ
float: {φ : ℕ} → ℕ → MLIR.AST.MLIRType φ
tensor1d: {φ : ℕ} → MLIR.AST.MLIRType φ
tensor2d: {φ : ℕ} → MLIR.AST.MLIRType φ
tensor4d: {φ : ℕ} → MLIR.AST.MLIRType φ
index: {φ : ℕ} → MLIR.AST.MLIRType φ
undefined: {φ : ℕ} → String → MLIR.AST.MLIRType φ

Instances For

instance MLIR.AST.instReprMLIRType :

{φ : ℕ} → Repr (MLIR.AST.MLIRType φ)

Equations

MLIR.AST.instReprMLIRType = { reprPrec := MLIR.AST.reprMLIRType✝ }

instance MLIR.AST.instDecidableEqMLIRType :

{φ : ℕ} → DecidableEq (MLIR.AST.MLIRType φ)

Equations

MLIR.AST.instDecidableEqMLIRType = MLIR.AST.decEqMLIRType✝

instance MLIR.AST.instToFormatWidth (φ : ℕ) :

Lean.ToFormat (MLIR.AST.Width φ)

Equations

MLIR.AST.instToFormatWidth φ = { format := repr }

instance MLIR.AST.instToFormatMLIRType (φ : ℕ) :

Lean.ToFormat (MLIR.AST.MLIRType φ)

Equations

MLIR.AST.instToFormatMLIRType φ = { format := repr }

@[reducible, inline]

abbrev MLIR.AST.MLIRTy (φ : optParam ℕ 0) :

Equations

MLIR.AST.MLIRTy φ = MLIR.AST.MLIRType φ

Instances For

def MLIR.AST.MLIRTy.i (φ : ℕ) (width : ℕ) :

MLIR.AST.MLIRTy φ

Shorthand to build <iN>

Equations

MLIR.AST.MLIRTy.i φ width = MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless (ConcreteOrMVar.concrete width)

Instances For

@[reducible, inline]

abbrev MLIR.AST.MLIRType.i1 (φ : ℕ) :

MLIR.AST.MLIRType φ

Equations

MLIR.AST.MLIRType.i1 φ = MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless 1

Instances For

@[reducible, inline]

abbrev MLIR.AST.MLIRType.i32 (φ : ℕ) :

MLIR.AST.MLIRType φ

Equations

MLIR.AST.MLIRType.i32 φ = MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless 32

Instances For

def MLIR.AST.MLIRType.i (φ : ℕ) (width : ℕ) :

MLIR.AST.MLIRTy φ

Equations

MLIR.AST.MLIRType.i φ width = MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless (ConcreteOrMVar.concrete width)

Instances For

@[reducible, inline]

abbrev MLIR.AST.TypedSSAVal (φ : ℕ) :

An ssa value (variable name) with a type

Equations

MLIR.AST.TypedSSAVal φ = (MLIR.AST.SSAVal × MLIR.AST.MLIRType φ)

Instances For

inductive MLIR.AST.AttrValue (φ : ℕ) :

symbol: {φ : ℕ} → String → MLIR.AST.AttrValue φ
str: {φ : ℕ} → String → MLIR.AST.AttrValue φ
int: {φ : ℕ} → ℤ → MLIR.AST.MLIRType φ → MLIR.AST.AttrValue φ
nat: {φ : ℕ} → ℕ → MLIR.AST.AttrValue φ
bool: {φ : ℕ} → Bool → MLIR.AST.AttrValue φ
float: {φ : ℕ} → Float → MLIR.AST.MLIRType φ → MLIR.AST.AttrValue φ
type: {φ : ℕ} → MLIR.AST.MLIRType φ → MLIR.AST.AttrValue φ
affine: {φ : ℕ} → MLIR.AST.AffineMap → MLIR.AST.AttrValue φ
permutation: {φ : ℕ} → List ℕ → MLIR.AST.AttrValue φ
list: {φ : ℕ} → List (MLIR.AST.AttrValue φ) → MLIR.AST.AttrValue φ
nestedsymbol: {φ : ℕ} → MLIR.AST.AttrValue φ → MLIR.AST.AttrValue φ → MLIR.AST.AttrValue φ
alias: {φ : ℕ} → String → MLIR.AST.AttrValue φ
dict: {φ : ℕ} → MLIR.AST.AttrDict φ → MLIR.AST.AttrValue φ
opaque_: {φ : ℕ} → String → String → MLIR.AST.AttrValue φ
opaqueElements: {φ : ℕ} → String → String → MLIR.AST.MLIRType φ → MLIR.AST.AttrValue φ
unit: {φ : ℕ} → MLIR.AST.AttrValue φ

Instances For

inductive MLIR.AST.AttrEntry (φ : ℕ) :

mk: {φ : ℕ} → String → MLIR.AST.AttrValue φ → MLIR.AST.AttrEntry φ

Instances For

inductive MLIR.AST.AttrDict (φ : ℕ) :

mk: {φ : ℕ} → List (MLIR.AST.AttrEntry φ) → MLIR.AST.AttrDict φ

Instances For

def MLIR.AST.AttrEntry.destructure {φ : ℕ} :

MLIR.AST.AttrEntry φ → String × MLIR.AST.AttrValue φ

Equations

(MLIR.AST.AttrEntry.mk name value).destructure = (name, value)

Instances For

def MLIR.AST.AttrDict.getAttr {φ : ℕ} :

MLIR.AST.AttrDict φ → String → Option (MLIR.AST.AttrValue φ)

Equations

(MLIR.AST.AttrDict.mk attrs).getAttr x = List.lookup x (List.map MLIR.AST.AttrEntry.destructure attrs)

Instances For

@[reducible, inline]

abbrev MLIR.AST.AttrVal (φ : optParam ℕ 0) :

Equations

MLIR.AST.AttrVal φ = MLIR.AST.AttrValue φ

Instances For

inductive MLIR.AST.Op (φ : ℕ) :

mk: {φ : ℕ} → String → List (MLIR.AST.TypedSSAVal φ) → List (MLIR.AST.TypedSSAVal φ) → List (MLIR.AST.Region φ) → MLIR.AST.AttrDict φ → MLIR.AST.Op φ

Instances For

inductive MLIR.AST.Region (φ : ℕ) :

mk: {φ : ℕ} → String → List (MLIR.AST.TypedSSAVal φ) → List (MLIR.AST.Op φ) → MLIR.AST.Region φ

Instances For

inductive MLIR.AST.AttrDefn (φ : ℕ) :

mk: {φ : ℕ} → String → MLIR.AST.AttrValue φ → MLIR.AST.AttrDefn φ

Instances For

inductive MLIR.AST.Module (φ : ℕ) :

mk: {φ : ℕ} → List (MLIR.AST.Op φ) → List (MLIR.AST.AttrDefn φ) → MLIR.AST.Module φ

Instances For

def MLIR.AST.Op.name {φ : ℕ} :

MLIR.AST.Op φ → String

Equations

(MLIR.AST.Op.mk name res args regions attrs).name = name

Instances For

def MLIR.AST.Op.res {φ : ℕ} :

MLIR.AST.Op φ → List (MLIR.AST.TypedSSAVal φ)

Equations

(MLIR.AST.Op.mk name res args regions attrs).res = res

Instances For

def MLIR.AST.Op.resNames {φ : ℕ} :

MLIR.AST.Op φ → List MLIR.AST.SSAVal

Equations

(MLIR.AST.Op.mk name res args regions attrs).resNames = List.map Prod.fst res

Instances For

def MLIR.AST.Op.resTypes {φ : ℕ} :

MLIR.AST.Op φ → List (MLIR.AST.MLIRType φ)

Equations

(MLIR.AST.Op.mk name res args regions attrs).resTypes = List.map Prod.snd res

Instances For

def MLIR.AST.Op.args {φ : ℕ} :

MLIR.AST.Op φ → List (MLIR.AST.TypedSSAVal φ)

Equations

(MLIR.AST.Op.mk name res args regions attrs).args = args

Instances For

def MLIR.AST.Op.argNames {φ : ℕ} :

MLIR.AST.Op φ → List MLIR.AST.SSAVal

Equations

(MLIR.AST.Op.mk name res args regions attrs).argNames = List.map Prod.fst args

Instances For

def MLIR.AST.Op.argTypes {φ : ℕ} :

MLIR.AST.Op φ → List (MLIR.AST.MLIRType φ)

Equations

(MLIR.AST.Op.mk name res args regions attrs).argTypes = List.map Prod.snd args

Instances For

def MLIR.AST.Op.regions {φ : ℕ} :

MLIR.AST.Op φ → List (MLIR.AST.Region φ)

Equations

(MLIR.AST.Op.mk name res args regions attrs).regions = regions

Instances For

def MLIR.AST.Op.attrs {φ : ℕ} :

MLIR.AST.Op φ → MLIR.AST.AttrDict φ

Equations

(MLIR.AST.Op.mk name res args regions attrs).attrs = attrs

Instances For

instance MLIR.AST.instCoeStringSSAVal :

Coe String MLIR.AST.SSAVal

Equations

MLIR.AST.instCoeStringSSAVal = { coe := fun (s : String) => MLIR.AST.SSAVal.SSAVal s }

instance MLIR.AST.instCoeStringAttrValue (φ : ℕ) :

Coe String (MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instCoeStringAttrValue φ = { coe := fun (s : String) => MLIR.AST.AttrValue.str s }

instance MLIR.AST.instCoeIntAttrValue (φ : ℕ) :

Coe ℤ (MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instCoeIntAttrValue φ = { coe := fun (i : ℤ) => MLIR.AST.AttrValue.int i (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless 64) }

instance MLIR.AST.instCoeMLIRTypeAttrValue (φ : ℕ) :

Coe (MLIR.AST.MLIRType φ) (MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instCoeMLIRTypeAttrValue φ = { coe := MLIR.AST.AttrValue.type }

instance MLIR.AST.instCoeProdStringAttrValueAttrEntry (φ : ℕ) :

Coe (String × MLIR.AST.AttrValue φ) (MLIR.AST.AttrEntry φ)

Equations

MLIR.AST.instCoeProdStringAttrValueAttrEntry φ = { coe := fun (v : String × MLIR.AST.AttrValue φ) => MLIR.AST.AttrEntry.mk v.1 v.2 }

instance MLIR.AST.instCoeProdStringMLIRTypeAttrEntry (φ : ℕ) :

Coe (String × MLIR.AST.MLIRType φ) (MLIR.AST.AttrEntry φ)

Equations

MLIR.AST.instCoeProdStringMLIRTypeAttrEntry φ = { coe := fun (v : String × MLIR.AST.MLIRType φ) => MLIR.AST.AttrEntry.mk v.1 (MLIR.AST.AttrValue.type v.2) }

instance MLIR.AST.instCoeAttrEntryProdStringAttrValue (φ : ℕ) :

Coe (MLIR.AST.AttrEntry φ) (String × MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instCoeAttrEntryProdStringAttrValue φ = { coe := fun (x : MLIR.AST.AttrEntry φ) => match x with | MLIR.AST.AttrEntry.mk key val => (key, val) }

instance MLIR.AST.instCoeListAttrEntryAttrDict (φ : ℕ) :

Coe (List (MLIR.AST.AttrEntry φ)) (MLIR.AST.AttrDict φ)

Equations

MLIR.AST.instCoeListAttrEntryAttrDict φ = { coe := fun (x : List (MLIR.AST.AttrEntry φ)) => let v := x; MLIR.AST.AttrDict.mk v }

instance MLIR.AST.instCoeAttrDictListAttrEntry (φ : ℕ) :

Coe (MLIR.AST.AttrDict φ) (List (MLIR.AST.AttrEntry φ))

Equations

MLIR.AST.instCoeAttrDictListAttrEntry φ = { coe := fun (x : MLIR.AST.AttrDict φ) => match x with | MLIR.AST.AttrDict.mk as => as }

def MLIR.AST.Region.name (φ : ℕ) (region : MLIR.AST.Region φ) :

MLIR.AST.BBName

Equations

MLIR.AST.Region.name φ (MLIR.AST.Region.mk name args ops) = MLIR.AST.BBName.mk name

Instances For

def MLIR.AST.Region.args (φ : ℕ) :

MLIR.AST.Region φ → List (MLIR.AST.TypedSSAVal φ)

Equations

MLIR.AST.Region.args φ (MLIR.AST.Region.mk name args ops) = args

Instances For

def MLIR.AST.Region.ops (φ : ℕ) (region : MLIR.AST.Region φ) :

List (MLIR.AST.Op φ)

Equations

MLIR.AST.Region.ops φ (MLIR.AST.Region.mk name args ops) = ops

Instances For

partial def MLIR.AST.docAttrVal {φ : ℕ} :

MLIR.AST.AttrValue φ → Lean.Format

partial def MLIR.AST.docAttrEntry {φ : ℕ} :

MLIR.AST.AttrEntry φ → Lean.Format

partial def MLIR.AST.docAttrDict {φ : ℕ} :

MLIR.AST.AttrDict φ → Lean.Format

instance MLIR.AST.instReprAttrValue (φ : ℕ) :

Repr (MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instReprAttrValue φ = { reprPrec := fun (x : MLIR.AST.AttrValue φ) (x_1 : ℕ) => MLIR.AST.docAttrVal x }

instance MLIR.AST.instReprAttrEntry (φ : ℕ) :

Repr (MLIR.AST.AttrEntry φ)

Equations

MLIR.AST.instReprAttrEntry φ = { reprPrec := fun (x : MLIR.AST.AttrEntry φ) (x_1 : ℕ) => MLIR.AST.docAttrEntry x }

instance MLIR.AST.instReprAttrDict (φ : ℕ) :

Repr (MLIR.AST.AttrDict φ)

Equations

MLIR.AST.instReprAttrDict φ = { reprPrec := fun (x : MLIR.AST.AttrDict φ) (x_1 : ℕ) => MLIR.AST.docAttrDict x }

instance MLIR.AST.instReprAttrDefn (φ : ℕ) :

Repr (MLIR.AST.AttrDefn φ)

Equations

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

instance MLIR.AST.instReprSSAVal_1 :

Repr MLIR.AST.SSAVal

Equations

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

instance MLIR.AST.instToFormatSSAVal :

Lean.ToFormat MLIR.AST.SSAVal

Equations

MLIR.AST.instToFormatSSAVal = { format := repr }

partial def MLIR.AST.op_to_format {φ : ℕ} :

MLIR.AST.Op φ → Lean.Format

partial def MLIR.AST.rgn_to_format {φ : ℕ} :

MLIR.AST.Region φ → Lean.Format

instance MLIR.AST.instReprOp (φ : ℕ) :

Repr (MLIR.AST.Op φ)

Equations

MLIR.AST.instReprOp φ = { reprPrec := fun (x : MLIR.AST.Op φ) (x_1 : ℕ) => MLIR.AST.op_to_format x }

instance MLIR.AST.instReprRegion (φ : ℕ) :

Repr (MLIR.AST.Region φ)

Equations

MLIR.AST.instReprRegion φ = { reprPrec := fun (x : MLIR.AST.Region φ) (x_1 : ℕ) => MLIR.AST.rgn_to_format x }

def MLIR.AST.AttrEntry.key {φ : ℕ} :

MLIR.AST.AttrEntry φ → String

Equations

(MLIR.AST.AttrEntry.mk name value).key = name

Instances For

def MLIR.AST.AttrEntry.value {φ : ℕ} :

MLIR.AST.AttrEntry φ → MLIR.AST.AttrValue φ

Equations

(MLIR.AST.AttrEntry.mk name value).value = value

Instances For

def MLIR.AST.AttrDict.empty {φ : ℕ} :

MLIR.AST.AttrDict φ

Equations

MLIR.AST.AttrDict.empty = MLIR.AST.AttrDict.mk []

Instances For

def MLIR.AST.Op.empty {φ : ℕ} (name : String) :

Equations

MLIR.AST.Op.empty name = MLIR.AST.Op.mk name [] [] [] MLIR.AST.AttrDict.empty

Instances For

def MLIR.AST.Op.addArg {φ : ℕ} (o : MLIR.AST.Op φ) (arg : MLIR.AST.TypedSSAVal φ) :

Equations

(MLIR.AST.Op.mk name res args regions attrs).addArg arg = MLIR.AST.Op.mk name res (args ++ [arg]) regions attrs

Instances For

def MLIR.AST.Op.addResult {φ : ℕ} (o : MLIR.AST.Op φ) (new_res : MLIR.AST.TypedSSAVal φ) :

Equations

(MLIR.AST.Op.mk name res args regions attrs).addResult new_res = MLIR.AST.Op.mk name (res ++ [new_res]) args regions attrs

Instances For

def MLIR.AST.Op.appendRegion {φ : ℕ} (o : MLIR.AST.Op φ) (r : MLIR.AST.Region φ) :

Equations

(MLIR.AST.Op.mk name res args regions attrs).appendRegion r = MLIR.AST.Op.mk name res args (regions ++ [r]) attrs

Instances For

def MLIR.AST.AttrDict.add {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (entry : MLIR.AST.AttrEntry φ) :

MLIR.AST.AttrDict φ

Equations

attrs.add entry = Coe.coe (entry :: Coe.coe attrs)

Instances For

def MLIR.AST.AttrDict.find {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (name : String) :

Option (MLIR.AST.AttrValue φ)

Equations

(MLIR.AST.AttrDict.mk as).find name = match List.find? (fun (entry : MLIR.AST.AttrEntry φ) => entry.key == name) as with | some v => some v.value | none => none

Instances For

def MLIR.AST.AttrDict.find_nat {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (name : String) :

Equations

attrs.find_nat name = match attrs.find name with | some (MLIR.AST.AttrValue.nat i) => some i | x => none

Instances For

def MLIR.AST.AttrDict.find_int {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (name : String) :

Option (ℤ × MLIR.AST.MLIRType φ)

Equations

attrs.find_int name = match attrs.find name with | some (MLIR.AST.AttrValue.int i ty) => some (i, ty) | x => none

Instances For

def MLIR.AST.AttrDict.find_str {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (name : String) :

Equations

attrs.find_str name = match attrs.find name with | some (MLIR.AST.AttrValue.str s) => some s | x => none

Instances For

def MLIR.AST.AttrDict.find_int' {φ : ℕ} (attrs : MLIR.AST.AttrDict φ) (name : String) :

Equations

attrs.find_int' name = match attrs.find name with | some (MLIR.AST.AttrValue.int i a) => some i | x => none

Instances For

@[simp]

theorem MLIR.AST.AttrDict.find_none (φ : ℕ) {n' : String} :

(MLIR.AST.AttrDict.mk []).find n' = none

@[simp]

theorem MLIR.AST.AttrDict.find_next (φ : ℕ) {n : String} {n' : String} (v : MLIR.AST.AttrValue φ) (l : List (MLIR.AST.AttrEntry φ)) :

(MLIR.AST.AttrDict.mk (MLIR.AST.AttrEntry.mk n v :: l)).find n' = if (n == n') = true then some v else (MLIR.AST.AttrDict.mk l).find n'

def MLIR.AST.AttrDict.addString (φ : ℕ) (attrs : MLIR.AST.AttrDict φ) (k : String) (v : String) :

MLIR.AST.AttrDict φ

Equations

MLIR.AST.AttrDict.addString φ (MLIR.AST.AttrDict.mk as) k v = MLIR.AST.AttrDict.mk (MLIR.AST.AttrEntry.mk k (MLIR.AST.AttrValue.str v) :: as)

Instances For

def MLIR.AST.AttrDict.addType (φ : ℕ) (attrs : MLIR.AST.AttrDict φ) (k : String) (v : MLIR.AST.MLIRType φ) :

MLIR.AST.AttrDict φ

Equations

MLIR.AST.AttrDict.addType φ (MLIR.AST.AttrDict.mk as) k v = MLIR.AST.AttrDict.mk (MLIR.AST.AttrEntry.mk k (MLIR.AST.AttrValue.type v) :: as)

Instances For

def MLIR.AST.Op.addAttr (φ : ℕ) (o : MLIR.AST.Op φ) (k : String) (v : MLIR.AST.AttrValue φ) :

Equations

MLIR.AST.Op.addAttr φ (MLIR.AST.Op.mk name res args regions attrs) k v = MLIR.AST.Op.mk name res args regions (attrs.add (MLIR.AST.AttrEntry.mk (k, v).1 (k, v).2))

Instances For

def MLIR.AST.Region.empty {φ : ℕ} (name : String) :

MLIR.AST.Region φ

Equations

MLIR.AST.Region.empty name = MLIR.AST.Region.mk name [] []

Instances For

def MLIR.AST.Region.appendOp (φ : ℕ) (bb : MLIR.AST.Region φ) (op : MLIR.AST.Op φ) :

MLIR.AST.Region φ

Equations

MLIR.AST.Region.appendOp φ (MLIR.AST.Region.mk name args ops) op = MLIR.AST.Region.mk name args (ops ++ [op])

Instances For

def MLIR.AST.Region.appendOps (φ : ℕ) (bb : MLIR.AST.Region φ) (ops : List (MLIR.AST.Op φ)) :

MLIR.AST.Region φ

Equations

MLIR.AST.Region.appendOps φ (MLIR.AST.Region.mk name args ops_1) ops = MLIR.AST.Region.mk name args (ops_1 ++ ops)

Instances For

instance MLIR.AST.instInhabitedMLIRType (φ : ℕ) :

Inhabited (MLIR.AST.MLIRType φ)

Equations

MLIR.AST.instInhabitedMLIRType φ = { default := MLIR.AST.MLIRType.undefined "INHABITANT" }

instance MLIR.AST.instInhabitedAttrValue (φ : ℕ) :

Inhabited (MLIR.AST.AttrValue φ)

Equations

MLIR.AST.instInhabitedAttrValue φ = { default := MLIR.AST.AttrValue.str "INHABITANT" }

instance MLIR.AST.instInhabitedOp (φ : ℕ) :

Inhabited (MLIR.AST.Op φ)

Equations

MLIR.AST.instInhabitedOp φ = { default := MLIR.AST.Op.empty "INHABITANT" }

instance MLIR.AST.instInhabitedRegion (φ : ℕ) :

Inhabited (MLIR.AST.Region φ)

Equations

MLIR.AST.instInhabitedRegion φ = { default := MLIR.AST.Region.empty "INHABITANT" }

instance MLIR.AST.instReprModule (φ : ℕ) :

Repr (MLIR.AST.Module φ)

Equations

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

def MLIR.AST.Region.fromOps {φ : ℕ} (os : List (MLIR.AST.Op φ)) (name : optParam String "entry") :

MLIR.AST.Region φ

Equations

MLIR.AST.Region.fromOps os name = MLIR.AST.Region.mk name [] os

Instances For

def MLIR.AST.Region.setArgs {φ : ℕ} (bb : MLIR.AST.Region φ) (args : List (MLIR.AST.SSAVal × MLIR.AST.MLIRType φ)) :

MLIR.AST.Region φ

Equations

(MLIR.AST.Region.mk name args_1 ops).setArgs args = MLIR.AST.Region.mk name args ops

Instances For