@[reducible, inline]

abbrev ParseError : Type

Equations

• ParseError = String

@[reducible, inline]

abbrev ParseFun {ParseOutput : Type} : Type

Equations

• ParseFun = (Lean.Environment → String → EIO ParseError ParseOutput)

unsafe def elabIntoTermTactic {α : Type} (expectedType : Lean.Expr) (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM α

unsafe def elabIntoTermElab {α : Type} (expectedType : Lean.Expr) (stx : Lean.Syntax) : Lean.Elab.TermElabM α

unsafe def elabIntoMeta {α : Type} (expectedType : Lean.Expr) (stx : Lean.Syntax) : Lean.MetaM α

unsafe def elabIntoCore {α : Type} (expectedType : Lean.Expr) (stx : Lean.Syntax) : Lean.CoreM α

def printException {α : Type u_1} : Except Lean.Exception α → IO String

Equations

• printException (Except.ok a) = throw (IO.userError "printException called on Except.ok")
• printException (Except.error e) = e.toMessageData.toString

unsafe def elabIntoEIO {α : Type} (env : Lean.Environment) (typeName : Lean.Expr) (stx : Lean.Syntax) : EIO ParseError α

def region0Expr : Lean.Expr

Equations

• region0Expr = (Lean.Expr.const `MLIR.AST.Region []).app (Lean.Expr.const `Nat.zero [])

def op0Expr : Lean.Expr

Equations

• op0Expr = (Lean.Expr.const `MLIR.AST.Op []).app (Lean.Expr.const `Nat.zero [])

def elabRegion (env : Lean.Environment) (stx : Lean.Syntax) : EIO ParseError (MLIR.AST.Region 0)

Parse Lean.Syntax into MLIR.AST.Region.

This runs the Lean frontend stack and adds it to the TCB. It should be safe (if we trust the lean parser) since we ensure that the types match: see https://leanprover-community.github.io/mathlib4_docs/Std/Util/TermUnsafe.html#Std.TermUnsafe.termUnsafe_

Equations

• elabRegion env stx = do let reg ← elabRegion.unsafe_impl_1 env stx pure reg

def elabOp (env : Lean.Environment) (stx : Lean.Syntax) : EIO ParseError (MLIR.AST.Op 0)

Parse Lean.Syntax into MLIR.AST.Op.

This runs the Lean frontend stack and adds it to the TCB. It should be safe (if we trust the lean parser) since we ensure that the types match: see https://leanprover-community.github.io/mathlib4_docs/Std/Util/TermUnsafe.html#Std.TermUnsafe.termUnsafe_

Equations

• elabOp env stx = elabOp.unsafe_impl_1 env stx

def mkParseFun {ParseOutput : Type} (syntaxcat : Lean.Name) (ntparser : Lean.Syntax → EIO ParseError ParseOutput) (s : String) (env : Lean.Environment) : EIO ParseError ParseOutput

Equations

• mkParseFun syntaxcat ntparser s env = match Lean.Parser.runParserCategory env syntaxcat s with | Except.error msg => throw msg | Except.ok syn => ntparser syn

def regionParser : ParseFun

Equations

• regionParser env = mkNonTerminalParser `mlir_region (elabRegion env) env

def runParser {ParseOutput : Type} (parser : ParseFun) (fileName : String) : IO (Option ParseOutput)

Equations

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

def parseRegionFromFile {α : Type} (fileName : String) (regionParseFun : MLIR.AST.Region 0 → Except ParseError α) : IO (Option α)

Equations

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