class StrataDDM.HasInputContext (m : Type → Type u_1) [Functor m] : Type u_1

• getInputContext : m Parser.InputContext
• getFileName : m System.FilePath

structure StrataDDM.SourcedProgram : Type

Bundle returned by the #strata term region. Carries:

• program: the parsed Strata.Program with file-global AST byte offsets, so Boole-style consumers (and any code that uses byte offsets in obligation labels or diagnostic ranges) keep their existing behavior.
• source: the raw snippet text between #strata and #end. Test helpers use this to build a snippet-local FileMap.
• basePos: byte offset in the Lean file where the snippet starts, so helpers can convert file-global pipeline diagnostics back to snippet-local positions when matching against inline annotations.
• baseLine / fileName: enough info for helpers to render <lean_file>:<line>:<col> in error messages so editors / quickfix lists can jump straight to the offending source.

• program : Program
• source : String
• basePos : Nat
• baseLine : Nat
• fileName : String

@[implicit_reducible]

instance StrataDDM.instInhabitedSourcedProgram : Inhabited SourcedProgram

Equations

• StrataDDM.instInhabitedSourcedProgram = { default := StrataDDM.instInhabitedSourcedProgram.default }

def StrataDDM.instInhabitedSourcedProgram.default : SourcedProgram

Equations

• StrataDDM.instInhabitedSourcedProgram.default = { program := default, source := default, basePos := default, baseLine := default, fileName := default }

@[implicit_reducible]

instance StrataDDM.instToStringSourcedProgram : ToString SourcedProgram

Forward ToString to the underlying Program so #eval printing keeps working at existing call sites.

Equations

• StrataDDM.instToStringSourcedProgram = { toString := fun (s : StrataDDM.SourcedProgram) => toString s.program }

@[implicit_reducible]

instance StrataDDM.instCoeSourcedProgramProgram : Coe SourcedProgram Program

Allow SourcedProgram to be used wherever a Program is expected; the source/positions are dropped. Removes ~200 explicit .program accessors at consumer call sites.

Equations

• StrataDDM.instCoeSourcedProgramProgram = { coe := fun (s : StrataDDM.SourcedProgram) => s.program }

@[reducible, inline]

abbrev StrataDDM.SourcedProgram.commands (s : SourcedProgram) : Array Operation

Equations

• s.commands = s.program.commands

@[reducible, inline]

abbrev StrataDDM.SourcedProgram.dialect (s : SourcedProgram) : DialectName

Equations

• s.dialect = s.program.dialect

@[reducible, inline]

abbrev StrataDDM.SourcedProgram.dialects (s : SourcedProgram) : DialectMap

Equations

• s.dialects = s.program.dialects

@[reducible, inline]

abbrev StrataDDM.SourcedProgram.globalContext (s : SourcedProgram) : GlobalContext

Equations

• s.globalContext = s.program.globalContext

@[reducible, inline]

abbrev StrataDDM.SourcedProgram.format (s : SourcedProgram) (opts : FormatOptions := { }) : Std.Format

Equations

• s.format opts = s.program.format opts

def StrataDDM.instToExprSourcedProgram.toExpr : SourcedProgram → Lean.Expr

Equations

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

@[implicit_reducible]

instance StrataDDM.instToExprSourcedProgram : Lean.ToExpr SourcedProgram

Equations

• StrataDDM.instToExprSourcedProgram = { toExpr := StrataDDM.instToExprSourcedProgram.toExpr, toTypeExpr := Lean.Expr.const `StrataDDM.SourcedProgram [] }

@[implicit_reducible]

instance StrataDDM.instHasInputContextCommandElabM : HasInputContext Lean.Elab.Command.CommandElabM

Equations

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

@[implicit_reducible]

instance StrataDDM.instHasInputContextCoreM : HasInputContext Lean.CoreM

Equations

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

def StrataDDM.addDefn (name : Lean.Name) (type value : Lean.Expr) (levelParams : List Lean.Name := []) (hints : Lean.ReducibilityHints := Lean.ReducibilityHints.abbrev) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) (all : List Lean.Name := [name]) : Lean.CoreM Unit

Add a definition to environment and compile it.

Equations

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

def StrataDDM.declareDialect (d : Dialect) : Lean.Elab.Command.CommandElabM Unit

Declare dialect and add to environment.

Equations

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

def StrataDDM.strataDialectCommand : Parser.Parser

Equations

• StrataDDM.strataDialectCommand = StrataDDM.ExternParser.mkParser `strataDialectCommand "#dialect" "#end"

def StrataDDM.strataDialectImpl : Lean.Elab.Command.CommandElab

Equations

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

def StrataDDM.strataProgram : Parser.Parser

Equations

• StrataDDM.strataProgram = StrataDDM.ExternParser.mkParser `strataProgram "#strata" "#end"

def StrataDDM.strataProgramImpl : Lean.Elab.Term.TermElab

Equations

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

def StrataDDM.loadDialectCommand : Lean.ParserDescr

Equations

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

def StrataDDM.getModuleRoot (path : System.FilePath) (modName : Lean.Name) : Except String System.FilePath

Derive the package source root from a module's file path and name by stripping one directory component per name part. For example, given /repo/Strata/Languages/Foo.lean and module name Strata.Languages.Foo, returns /repo.

Equations

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

def StrataDDM.loadDialectImpl : Lean.Elab.Command.CommandElab

Equations

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