def StrataDDM.infoSourceRange (info : Lean.SourceInfo) : Option SourceRange

Equations

• StrataDDM.infoSourceRange (Lean.SourceInfo.original leading pos trailing endPos) = some { start := pos, stop := endPos }
• StrataDDM.infoSourceRange (Lean.SourceInfo.synthetic pos endPos canonical) = some { start := pos, stop := endPos }
• StrataDDM.infoSourceRange Lean.SourceInfo.none = none

@[irreducible]

def StrataDDM.sourceLocPos (stx : Lean.Syntax) : Option String.Pos.Raw

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.sourceLocPos (Lean.Syntax.atom info val) = Option.map (fun (x : StrataDDM.SourceRange) => x.start) (StrataDDM.infoSourceRange info)
• StrataDDM.sourceLocPos (Lean.Syntax.ident info rawVal val preresolved) = Option.map (fun (x : StrataDDM.SourceRange) => x.start) (StrataDDM.infoSourceRange info)
• StrataDDM.sourceLocPos Lean.Syntax.missing = none

@[irreducible]

def StrataDDM.sourceLocEnd (stx : Lean.Syntax) : Option String.Pos.Raw

End position of a syntax tree, skipping trailing zero-width children.

For a node with no range of its own, the end is that of its last child that covers source text, found by scanning right-to-left and skipping zero-width children. A trailing element with no concrete syntax — an absent trailing optional, or an empty-template op (op else0 () => ;) — parses to a zero-width node past the real content (on the preceding token's consumed trailing whitespace), so it must be skipped, not taken as the end. The common case is an O(1) own-info check: these nodes carry their own zero-width range (stamped by the parser). A rangeless nested op is the exception — it needs a descent to tell whether its subtree is zero-width (see lastSpanningEnd's none case).

The skip lives here, in the descending function, so a parent reaching a nested child's end gets the corrected position at every level, e.g. if … else new C → else → new → its absent trailing type-args. mkSourceRange? is then just ⟨sourceLocPos, sourceLocEnd⟩. The i == 0 case keeps the first child's end even if empty, so a wholly-empty node still yields a position. The skip is one-sided — sourceLocPos needs no leading skip (see its comment).

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.sourceLocEnd (Lean.Syntax.atom info val) = Option.map (fun (x : StrataDDM.SourceRange) => x.stop) (StrataDDM.infoSourceRange info)
• StrataDDM.sourceLocEnd (Lean.Syntax.ident info rawVal val preresolved) = Option.map (fun (x : StrataDDM.SourceRange) => x.stop) (StrataDDM.infoSourceRange info)
• StrataDDM.sourceLocEnd Lean.Syntax.missing = none

def StrataDDM.mkSourceRange? (stx : Lean.Syntax) : Option SourceRange

Source range of a syntax tree: its start position paired with its end.

Both bounds come from sourceLocPos / sourceLocEnd, so the trailing zero-width skip that sourceLocEnd performs is honored here for free — this is just the two positional queries combined.

Equations

• StrataDDM.mkSourceRange? stx = match StrataDDM.sourceLocPos stx, StrataDDM.sourceLocEnd stx with | some start, some stop => some { start := start, stop := stop } | x, x_1 => none

def StrataDDM.Elab.«termMd{_,}» : Lean.ParserDescr

Equations

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

class StrataDDM.Elab.ElabClass (m : Type → Type) extends Monad m : Type 1

• map {α β : Type} : (α → β) → m α → m β
• mapConst {α β : Type} : α → m β → m α
• pure {α : Type} : α → m α
• seq {α β : Type} : m (α → β) → (Unit → m α) → m β
• seqLeft {α β : Type} : m α → (Unit → m β) → m α
• seqRight {α β : Type} : m α → (Unit → m β) → m β
• bind {α β : Type} : m α → (α → m β) → m β
• getInputContext : m Parser.InputContext
• getDialects : m DialectMap
• getOpenDialects : m (Std.HashSet DialectName)
• getGlobalContext : m GlobalContext
• getErrorCount : m Nat
• logErrorMessage : Lean.Message → m Unit

def StrataDDM.Elab.runChecked {m : Type → Type} {α : Type} [ElabClass m] (action : m α) : m (α × Bool)

Runs action and returns result along with Bool that is true if action ran without producing errors.

Equations

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

def StrataDDM.Elab.mkErrorMessage (inputCtx : Parser.InputContext) (loc : SourceRange) (msg : String) (isSilent : Bool := false) : Lean.Message

Equations

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

def StrataDDM.Elab.logError {m : Type → Type} [ElabClass m] (loc : SourceRange) (msg : String) (isSilent : Bool := false) : m Unit

Equations

• StrataDDM.Elab.logError loc msg isSilent = do let inputCtx ← StrataDDM.Elab.ElabClass.getInputContext StrataDDM.Elab.logErrorMessage (StrataDDM.Elab.mkErrorMessage inputCtx loc msg isSilent)

def StrataDDM.Elab.logErrorMF {m : Type → Type} [ElabClass m] (loc : SourceRange) (msg : StrataFormat) (isSilent : Bool := false) (globalContext? : Option GlobalContext := none) : m Unit

Equations

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

structure StrataDDM.Elab.DeclContext : Type

• inputContext : Parser.InputContext
• stopPos : String.Pos.Raw
• loader : LoadedDialects
• missingImport : Bool

  Flag indicating imports are missing (silences some errors).

• typecheck : Bool

  When false, type inference and unification are skipped during elaboration.

def StrataDDM.Elab.DeclContext.empty : DeclContext

Equations

• StrataDDM.Elab.DeclContext.empty = { inputContext := default, stopPos := 0, loader := StrataDDM.Elab.LoadedDialects.empty, missingImport := false }

class StrataDDM.Elab.NamedValue (α : Type) : Type

Represents an entity with some form of unique string name.

• name : α → String

@[reducible, inline]

abbrev StrataDDM.Elab.ValueWithName (α : Type) [NamedValue α] (name : String) : Type

Equations

• StrataDDM.Elab.ValueWithName α name = { d : α // StrataDDM.Elab.NamedValue.name d = name }

structure StrataDDM.Elab.NamedValueMap (α : Type) [NamedValue α] : Type

Map metadata attribute names to any declarations with that name that are in the current scope.

• map : Std.DHashMap String fun (name : String) => Array (DialectName × ValueWithName α name)

def StrataDDM.Elab.instInhabitedNamedValueMap.default {a✝ : Type} {a✝¹ : NamedValue a✝} : NamedValueMap a✝

Equations

• StrataDDM.Elab.instInhabitedNamedValueMap.default = { map := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedNamedValueMap {a✝ : Type} {a✝¹ : NamedValue a✝} : Inhabited (NamedValueMap a✝)

Equations

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

structure StrataDDM.Elab.MetadataDeclMap : Type

Map metadata attribute names to any declarations with that name that are in the current scope.

• map : Std.DHashMap String fun (name : String) => Array (DialectName × { d : MetadataDecl // d.name = name })

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedMetadataDeclMap : Inhabited MetadataDeclMap

Equations

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

def StrataDDM.Elab.instInhabitedMetadataDeclMap.default : MetadataDeclMap

Equations

• StrataDDM.Elab.instInhabitedMetadataDeclMap.default = { map := default }

def StrataDDM.Elab.MetadataDeclMap.add (m : MetadataDeclMap) (dialect : DialectName) (decl : MetadataDecl) : MetadataDeclMap

Equations

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

def StrataDDM.Elab.MetadataDeclMap.addDialect (m : MetadataDeclMap) (dialect : Dialect) : MetadataDeclMap

Equations

• m.addDialect dialect = StrataDDM.Collection.fold (fun (x1 : StrataDDM.Elab.MetadataDeclMap) (x2 : StrataDDM.MetadataDecl) => x1.add dialect.name x2) m dialect.metadata

def StrataDDM.Elab.MetadataDeclMap.get (m : MetadataDeclMap) (name : String) : Array (DialectName × { d : MetadataDecl // d.name = name })

Equations

• m.get name = m.map.getD name #[]

inductive StrataDDM.Elab.TypeOrCatDecl : Type

• syncat (d : SynCatDecl) : TypeOrCatDecl
• type (d : TypeDecl) : TypeOrCatDecl

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedTypeOrCatDecl : Inhabited TypeOrCatDecl

Equations

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

def StrataDDM.Elab.instInhabitedTypeOrCatDecl.default : TypeOrCatDecl

Equations

• StrataDDM.Elab.instInhabitedTypeOrCatDecl.default = StrataDDM.Elab.TypeOrCatDecl.syncat default

def StrataDDM.Elab.TypeOrCatDecl.name : TypeOrCatDecl → String

Equations

• (StrataDDM.Elab.TypeOrCatDecl.syncat d).name = d.name
• (StrataDDM.Elab.TypeOrCatDecl.type d).name = d.name

def StrataDDM.Elab.TypeOrCatDecl.decl : TypeOrCatDecl → Decl

Equations

• (StrataDDM.Elab.TypeOrCatDecl.syncat d).decl = StrataDDM.Decl.syncat d
• (StrataDDM.Elab.TypeOrCatDecl.type d).decl = StrataDDM.Decl.type d

structure StrataDDM.Elab.TypeOrCatDeclMap : Type

Map metadata attribute names to any declarations with that name that are in the current scope.

• map : Std.DHashMap String fun (name : String) => Array (DialectName × { d : TypeOrCatDecl // d.name = name })

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedTypeOrCatDeclMap : Inhabited TypeOrCatDeclMap

Equations

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

def StrataDDM.Elab.instInhabitedTypeOrCatDeclMap.default : TypeOrCatDeclMap

Equations

• StrataDDM.Elab.instInhabitedTypeOrCatDeclMap.default = { map := default }

def StrataDDM.Elab.TypeOrCatDeclMap.add (m : TypeOrCatDeclMap) (dialect : DialectName) (decl : TypeOrCatDecl) : TypeOrCatDeclMap

Equations

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

def StrataDDM.Elab.TypeOrCatDeclMap.addSynCat (m : TypeOrCatDeclMap) (dialect : DialectName) (d : SynCatDecl) : TypeOrCatDeclMap

Equations

• m.addSynCat dialect d = m.add dialect (StrataDDM.Elab.TypeOrCatDecl.syncat d)

def StrataDDM.Elab.TypeOrCatDeclMap.addType (m : TypeOrCatDeclMap) (dialect : DialectName) (d : TypeDecl) : TypeOrCatDeclMap

Equations

• m.addType dialect d = m.add dialect (StrataDDM.Elab.TypeOrCatDecl.type d)

def StrataDDM.Elab.TypeOrCatDeclMap.addDialect (m : TypeOrCatDeclMap) (dialect : Dialect) : TypeOrCatDeclMap

Equations

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

def StrataDDM.Elab.TypeOrCatDeclMap.get (m : TypeOrCatDeclMap) (name : String) : Array (DialectName × { d : TypeOrCatDecl // d.name = name })

Equations

• m.get name = m.map.getD name #[]

structure StrataDDM.Elab.DeclState : Type

• fixedParsers : Parser.ParsingContext
• openDialects : Array DialectName
• openDialectSet : Std.HashSet DialectName
• typeOrCatDeclMap : TypeOrCatDeclMap

  Map for looking up types and categories by name.

• metadataDeclMap : MetadataDeclMap

  Map for looking up metadata by name.

• parserMap : PrattParsingTableMap
• tokenTable : Lean.Parser.TokenTable
• globalContext : GlobalContext
• pos : String.Pos.Raw
• errors : Array Lean.Message

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedDeclState : Inhabited DeclState

Equations

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

def StrataDDM.Elab.instInhabitedDeclState.default : DeclState

Equations

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

def StrataDDM.Elab.DeclState.addParserToCat! (s : DeclState) (dp : Parser.DeclParser) : DeclState

Equations

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

def StrataDDM.Elab.DeclState.addSynCat! (s : DeclState) (dialect : String) (decl : SynCatDecl) : DeclState

Equations

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

def StrataDDM.Elab.DeclState.openParserDialect! (s : DeclState) (loader : LoadedDialects) (dialect : Dialect) : DeclState

Opens the dialect definition dialect in the parser so it is visible to parser, but not part of environment. This is used for dialect definitions.

Equations

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

partial def StrataDDM.Elab.DeclState.ensureLoaded! (s : DeclState) (loaded : LoadedDialects) (dialect : DialectName) : DeclState

partial def StrataDDM.Elab.DeclState.addDialect! (s : DeclState) (loaded : LoadedDialects) (dialect : Dialect) : DeclState

Opens the dialect (not must not already be open)

def StrataDDM.Elab.DeclState.openLoadedDialect! (s : DeclState) (loaded : LoadedDialects) (dialect : Dialect) : DeclState

Opens the dialect (not must not already be open)

Equations

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

def StrataDDM.Elab.DeclState.ofDialects (ds : LoadedDialects) : DeclState

Equations

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

@[reducible]

def StrataDDM.Elab.DeclM (α : Type) : Type

Equations

• StrataDDM.Elab.DeclM = ReaderT StrataDDM.Elab.DeclContext (StateM StrataDDM.Elab.DeclState)

@[implicit_reducible]

instance StrataDDM.Elab.DeclM.instElabClass : ElabClass DeclM

Equations

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

def StrataDDM.Elab.addTypeOrCatDecl (dialect : DialectName) (tpcd : TypeOrCatDecl) : DeclM Unit

Equations

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