MLIR Dialect Domain Specific Language

This file sets up generic glue meta-code to tie together the generic MLIR parser with the Transform mechanism, to obtain an easy way to specify a DSL that elaborates into Com/Expr instances for a specific dialect.

partial def SSA.ctxtNf (as : Lean.Expr) : Lean.MetaM Lean.Expr

ctxtNf reduces an expression of type Ctxt _ to something in between whnf and normal form. ctxtNf recursively calls whnf on the tail of the list, so that the result is of the form a₀ :: a₁ :: ... :: aₙ :: [] where each element aᵢ is not further reduced

partial def SSA.comNf (com : Lean.Expr) : Lean.MetaM Lean.Expr

comNf reduces an expression of type Com to something in between whnf and normal form. comNf recursively calls whnf on the expression and body of a Com.var, resulting in Com.var (Expr.mk ...) <| Com.var (Expr.mk ...) <| Com.var (Expr.mk ...) <| ... <| Com.rete _ where the arguments to Expr.mk are not reduced

def SSA.elabIntoCom (region : Lean.TSyntax `mlir_region) (d : Q(Dialect)) {φ : Q(ℕ)} (_dialectSignature : autoParam Q(DialectSignature «$d») _auto✝) (_transformTy : autoParam Q(MLIR.AST.TransformTy «$d» «$φ») _auto✝) (_transformExpr : autoParam Q(MLIR.AST.TransformExpr «$d» «$φ») _auto✝) (_transformReturn : autoParam Q(MLIR.AST.TransformReturn «$d» «$φ») _auto✝) : Lean.Elab.TermElabM Lean.Expr

elabIntoCom is a building block for defining a dialect-specific DSL based on the geneeric MLIR syntax parser.

For example, if FooOp is the type of operations of a "Foo" dialect, we can build a term elaborator for this dialect as follows:

elab "[foo_com| " reg:mlir_region "]" : term => SSA.elabIntoCom reg q(FooOp)
--     ^^^^^^^                                                        ^^^^^

Equations

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