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

@[instance_reducible]

instance StrataDDM.instInhabitedSourcedProgram : Inhabited SourcedProgram

Equations

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

def StrataDDM.SourcedProgram.toString (p : SourcedProgram) : String

Equations

• p.toString = toString p.program

@[instance_reducible]

instance StrataDDM.SourcedProgram.instToString : ToString SourcedProgram

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

Equations

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

@[instance_reducible]

instance StrataDDM.SourcedProgram.instCoeProgram : Coe SourcedProgram Program

Allow SourcedProgram to be used wherever a Program is expected; the source/positions are dropped.

Equations

• StrataDDM.SourcedProgram.instCoeProgram = { 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