Transform* typeclasses

This file defines TransformTy, TransformExpr, and TransformReturn typeclasses, which dictate how generic MLIR syntax (as defined in MLIRSyntax.AST) can be transformed into an instance of Com or Expr for a specific dialect.

instance MLIR.AST.instCoeExprCtxtTy {eff : EffectKind} {d : Dialect} [DialectSignature d] {t : d.Ty} {Γ : Ctxt d.Ty} {Γ' : Γ.DerivedCtxt} : Coe (Expr d Γ eff t) (Expr d Γ'.ctxt eff t)

Equations

• MLIR.AST.instCoeExprCtxtTy = { coe := fun (e : Expr d Γ eff t) => Expr.changeVars Γ'.diff.toHom e }

Even though we technically only need to know the Ty type, our typeclass hierarchy is fully based on Op. It is thus more convenient to incorporate Op in these types, so that there will be no ambiguity errors.

@[reducible, inline]

abbrev MLIR.AST.ExceptM (d : Dialect) (α : Type u_1) : Type u_1

Equations

• MLIR.AST.ExceptM d = Except (MLIR.AST.TransformError d.Ty)

@[reducible, inline]

abbrev MLIR.AST.BuilderM (d : Dialect) (α : Type) : Type

Equations

• MLIR.AST.BuilderM d = StateT MLIR.AST.NameMapping (MLIR.AST.ExceptM d)

@[reducible, inline]

abbrev MLIR.AST.ReaderM (d : Dialect) (α : Type) : Type

Equations

• MLIR.AST.ReaderM d = ReaderT MLIR.AST.NameMapping (MLIR.AST.ExceptM d)

instance MLIR.AST.instMonadLiftReaderMBuilderM {d : Dialect} : MonadLift (MLIR.AST.ReaderM d) (MLIR.AST.BuilderM d)

Equations

• MLIR.AST.instMonadLiftReaderMBuilderM = { monadLift := fun {α : Type} (x : MLIR.AST.ReaderM d α) => do let __do_lift ← get liftM (ReaderT.run x __do_lift) }

instance MLIR.AST.instMonadLiftExceptMReaderM {d : Dialect} : MonadLift (MLIR.AST.ExceptM d) (MLIR.AST.ReaderM d)

Equations

• MLIR.AST.instMonadLiftExceptMReaderM = { monadLift := fun {α : Type} (x : MLIR.AST.ExceptM d α) => do let __do_lift ← liftM x pure __do_lift }

def MLIR.AST.BuilderM.runWithEmptyMapping {d : Dialect} {α : Type} (k : MLIR.AST.BuilderM d α) : MLIR.AST.ExceptM d α

Equations

• k.runWithEmptyMapping = Prod.fst <$> StateT.run k []

These typeclasses provide a natural flow to how users should implement TransformDialect.

• First declare how to transform types with TransformTy.
• Second, using TransformTy, declare how to transform expressions with TransformExpr.
• Third, using both type and expression conversion, declare how to transform returns with TransformReturn.
• These three automatically give an instance of TransformDialect.

class MLIR.AST.TransformTy (d : Dialect) (φ : outParam ℕ) [DialectSignature d] : Type

• mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM d d.Ty

class MLIR.AST.TransformExpr (d : Dialect) (φ : outParam ℕ) [DialectSignature d] [MLIR.AST.TransformTy d φ] : Type

• mkExpr : (Γ : List d.Ty) → MLIR.AST.Op φ → MLIR.AST.ReaderM d ((eff : EffectKind) × (ty : d.Ty) × Expr d Γ eff ty)

class MLIR.AST.TransformReturn (d : Dialect) (φ : outParam ℕ) [DialectSignature d] [MLIR.AST.TransformTy d φ] : Type

• mkReturn : (Γ : List d.Ty) → MLIR.AST.Op φ → MLIR.AST.ReaderM d ((eff : EffectKind) × (ty : d.Ty) × Com d Γ eff ty)

def MLIR.AST.addValToMapping {d : Dialect} (Γ : Ctxt d.Ty) (name : String) (ty : d.Ty) : MLIR.AST.BuilderM d ((Γ' : Γ.DerivedCtxt) × Γ'.ctxt.Var ty)

Add a new variable to the context, and record it's (absolute) index in the name mapping

Throws an error if the variable name already exists in the mapping, essentially disallowing shadowing

Equations

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

def MLIR.AST.getValFromCtxt {d : Dialect} [DecidableEq d.Ty] (Γ : Ctxt d.Ty) (name : String) (expectedType : d.Ty) : MLIR.AST.ReaderM d (Γ.Var expectedType)

Look up a name from the name mapping, and return the corresponding variable in the given context.

Throws an error if the name is not present in the mapping (this indicates the name may be free), or if the type of the variable in the context is different from expectedType

Equations

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

def MLIR.AST.BuilderM.isOk {d : Dialect} {α : Type} (x : MLIR.AST.BuilderM d α) : Bool

Equations

• x.isOk = match StateT.run x [] with | Except.ok a => true | Except.error a => false

def MLIR.AST.BuilderM.isErr {d : Dialect} {α : Type} (x : MLIR.AST.BuilderM d α) : Bool

Equations

• x.isErr = match StateT.run x [] with | Except.ok a => true | Except.error a => false

def MLIR.AST.TypedSSAVal.mkTy {d : Dialect} {φ : ℕ} [DialectSignature d] [MLIR.AST.TransformTy d φ] : MLIR.AST.TypedSSAVal φ → MLIR.AST.ExceptM d d.Ty

Equations

• MLIR.AST.TypedSSAVal.mkTy (MLIR.AST.SSAVal.SSAVal a, ty) = MLIR.AST.TransformTy.mkTy ty

def MLIR.AST.TypedSSAVal.mkVal {d : Dialect} {φ : ℕ} [DialectSignature d] [DecidableEq d.Ty] [instTransformTy : MLIR.AST.TransformTy d φ] (Γ : Ctxt d.Ty) : MLIR.AST.TypedSSAVal φ → MLIR.AST.ReaderM d ((ty : d.Ty) × Γ.Var ty)

Translate a TypedSSAVal (a name with an expected type), to a variable in the context. This expects the name to have already been declared before

Equations

• MLIR.AST.TypedSSAVal.mkVal Γ (MLIR.AST.SSAVal.SSAVal a, ty) = do let ty ← liftM (MLIR.AST.TransformTy.mkTy ty) let var ← MLIR.AST.getValFromCtxt Γ a ty pure ⟨ty, var⟩

def MLIR.AST.TypedSSAVal.mkVal' {d : Dialect} {φ : ℕ} [DialectSignature d] [DecidableEq d.Ty] [instTransformTy : MLIR.AST.TransformTy d φ] (Γ : Ctxt d.Ty) : MLIR.AST.TypedSSAVal φ → MLIR.AST.ReaderM d ((ty : d.Ty) × Γ.Var ty)

A variant of TypedSSAVal.mkVal that takes the function mkTy as an argument instead of using the typeclass TransformDialect. This is useful when trying to implement an instance of TransformDialect itself, to cut infinite regress.

Equations

• MLIR.AST.TypedSSAVal.mkVal' Γ (MLIR.AST.SSAVal.SSAVal a, ty) = do let ty ← liftM (MLIR.AST.TransformTy.mkTy ty) let var ← MLIR.AST.getValFromCtxt Γ a ty pure ⟨ty, var⟩

def MLIR.AST.TypedSSAVal.newVal {d : Dialect} {φ : ℕ} [DialectSignature d] [instTransformTy : MLIR.AST.TransformTy d φ] (Γ : Ctxt d.Ty) : MLIR.AST.TypedSSAVal φ → MLIR.AST.BuilderM d ((Γ' : Γ.DerivedCtxt) × (ty : d.Ty) × Γ'.ctxt.Var ty)

Declare a new variable, by adding the passed name to the name mapping stored in the monad state

Equations

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

def MLIR.AST.mkCom {d : Dialect} {φ : ℕ} [DialectSignature d] [MLIR.AST.TransformTy d φ] [MLIR.AST.TransformExpr d φ] [MLIR.AST.TransformReturn d φ] (reg : MLIR.AST.Region φ) : MLIR.AST.ExceptM d ((Γ : Ctxt d.Ty) × (eff : EffectKind) × (ty : d.Ty) × Com d Γ eff ty)

Equations

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