inductive StrataDDM.Elab.Header : Type

• dialect (loc : SourceRange) (name : DialectName) : Header
• program (loc : SourceRange) (name : DialectName) : Header

def StrataDDM.Elab.instInhabitedHeader.default : Header

Equations

• StrataDDM.Elab.instInhabitedHeader.default = StrataDDM.Elab.Header.dialect default default

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedHeader : Inhabited Header

Equations

• StrataDDM.Elab.instInhabitedHeader = { default := StrataDDM.Elab.instInhabitedHeader.default }

def StrataDDM.Elab.elabHeader (leanEnv : Lean.Environment) (inputContext : Parser.InputContext) (startPos : String.Pos.Raw := 0) (stopPos : String.Pos.Raw := inputContext.endPos) : Header × Array Lean.Message × String.Pos.Raw

Equations

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

def StrataDDM.Elab.elabProgramRest (loader : LoadedDialects) (leanEnv : Lean.Environment) (inputContext : Parser.InputContext) (dialect : DialectName) (known : dialect ∈ loader.dialects) (startPos : String.Pos.Raw) (stopPos : String.Pos.Raw := inputContext.endPos) : Except (Array Lean.Message) Program

Equations

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

def StrataDDM.Elab.elabProgram (loader : LoadedDialects) (leanEnv : Lean.Environment) (inputContext : Parser.InputContext) (startPos : String.Pos.Raw := 0) (stopPos : String.Pos.Raw := inputContext.endPos) : Except (Array Lean.Message) Program

Equations

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

def StrataDDM.Elab.mkErrorReport (errors : Array Lean.Message) : BaseIO String

Equations

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

partial def StrataDDM.Elab.loadDialectFromIonFragment (fm : DialectFileMap) (stk : Array DialectName) (dialect : DialectName) (frag : Ion.Fragment) : BaseIO (Except String Dialect)

partial def StrataDDM.Elab.elabDialectRest (fm : DialectFileMap) (inputContext : Parser.InputContext) (loc : SourceRange) (dialect : DialectName) (stk : Array DialectName := #[]) (startPos : String.Pos.Raw := 0) (stopPos : String.Pos.Raw := inputContext.endPos) : BaseIO (Dialect × DeclState)

Elaborate a dialect after the initial header with the name of dialect has been processed.

def StrataDDM.Elab.loadDialect (fm : DialectFileMap) (dialect : DialectName) : BaseIO (Except String Dialect)

Use fm to ensure dialect and all of its imports are loaded into ld.

This always returns a new loaded dialect map as some imports may be loaded successfully before a failure. It returns either an error message as a string or a dialect.

N.B. We may need to amend the error message in the future to provide more structure (such as error location information).

Equations

• StrataDDM.Elab.loadDialect fm dialect = StrataDDM.Elab.loadDialectRec✝ fm #[] dialect

def StrataDDM.Elab.loadDialectFromFile (fm : DialectFileMap) (path : System.FilePath) (actualPath : System.FilePath := path) : BaseIO (Except (Array Lean.Message) Dialect)

Load a dialect from a file, using actualPath for reading and path for error reporting. Returns the loaded dialect or an array of error messages.

Equations

• StrataDDM.Elab.loadDialectFromFile fm path actualPath = StrataDDM.Elab.loadDialectFromPath✝ fm #[] path actualPath

def StrataDDM.Elab.elabDialect (fm : DialectFileMap) (inputContext : Parser.InputContext) (startPos : String.Pos.Raw := 0) (stopPos : String.Pos.Raw := inputContext.endPos) : BaseIO (Dialect × DeclState)

Equations

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

def StrataDDM.Elab.parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (input : Parser.InputContext) : IO Program

Equations

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

def StrataDDM.Elab.parseCategoryFromDialect (dialects : LoadedDialects) (cat : QualifiedIdent) (input : Parser.InputContext) (startPos : String.Pos.Raw := 0) (stopPos : String.Pos.Raw := input.endPos) : IO Operation

Parse a single syntax category from a loaded dialect set.

Unlike parseStrataProgramFromDialect, this targets a specific syntax category (e.g. q\SMTResponse.GetValueResponse) rather than parsing a full program of Command`s. This avoids ambiguity issues that arise when multiple categories share the same surface syntax.

Returns the elaborated Operation on success.

Equations

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