@[reducible, inline]

abbrev StrataDDM.Elab.DialectParsers : Type

Map from dialect names to all the declaration parsers brought into scope for that dialect.

Equations

• StrataDDM.Elab.DialectParsers = Std.HashMap StrataDDM.DialectName (Array StrataDDM.Parser.DeclParser)

def StrataDDM.Elab.DialectParsers.addDialect! (pm : DialectParsers) (pctx : Parser.ParsingContext) (dialect : Dialect) : DialectParsers

Equations

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

structure StrataDDM.Elab.LoadedDialects : Type

Information about dialects.

• dialects : DialectMap
  • Map from dialect names to the dialect definition.
• dialectParsers : DialectParsers

  Parsers for dialects in map.

• syntaxElabMap : SyntaxElabMap

  / Map for elaborating operations and functions.

def StrataDDM.Elab.instInhabitedLoadedDialects.default : LoadedDialects

Equations

• StrataDDM.Elab.instInhabitedLoadedDialects.default = { dialects := default, dialectParsers := default, syntaxElabMap := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedLoadedDialects : Inhabited LoadedDialects

Equations

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

@[reducible]

def StrataDDM.Elab.initParsers : Parser.ParsingContext

Equations

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

def StrataDDM.Elab.DialectParsers.ofDialects (ds : Array Dialect) : Except String DialectParsers

Equations

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

def StrataDDM.Elab.SyntaxElabMap.ofDialects (ds : Array Dialect) : Except String SyntaxElabMap

Equations

• StrataDDM.Elab.SyntaxElabMap.ofDialects ds = Array.foldlM (fun (x1 : StrataDDM.Elab.SyntaxElabMap) (x2 : StrataDDM.Dialect) => x1.addDialect x2) ∅ ds

def StrataDDM.Elab.LoadedDialects.empty : LoadedDialects

Equations

• StrataDDM.Elab.LoadedDialects.empty = { dialects := ∅, dialectParsers := ∅, syntaxElabMap := ∅ }

def StrataDDM.Elab.LoadedDialects.addDialect! (loader : LoadedDialects) (d : Dialect) : LoadedDialects

Equations

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

def StrataDDM.Elab.LoadedDialects.ofDialects! (ds : Array Dialect) : LoadedDialects

Equations

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

@[reducible, inline]

abbrev StrataDDM.Elab.LoadDialectCallback : Type

Equations

• StrataDDM.Elab.LoadDialectCallback = (StrataDDM.DialectName → BaseIO (Except String StrataDDM.Dialect))

inductive StrataDDM.DialectFileMap.Encoding : Type

• ion : Encoding
• text : Encoding

structure StrataDDM.DialectFileMap : Type

The dialect file mapping maintains a mapping from dialect names to the file to read for loading this dialect.

It is used to identify where to find dialects that have not yet been loaded into LoadedDialects. It also holds a mutable reference to the LoadedDialects that is updated as dialects are loaded.

This structure is not safe for concurrent use by multiple threads, as concurrent dialect loading could produce conflicting updates to the shared LoadedDialects reference.

• map : Std.HashMap DialectName (IO.FS.SystemTime × Encoding × System.FilePath)
• loaded : IO.Ref Elab.LoadedDialects

  Mutable reference to loaded dialects.

def StrataDDM.DialectFileMap.new (preloaded : Elab.LoadedDialects) : BaseIO DialectFileMap

Equations

• StrataDDM.DialectFileMap.new preloaded = do let ref ← IO.mkRef preloaded pure { loaded := ref }

def StrataDDM.DialectFileMap.getLoaded (fm : DialectFileMap) : BaseIO Elab.LoadedDialects

Equations

• fm.getLoaded = ST.Ref.get fm.loaded

def StrataDDM.DialectFileMap.modifyLoaded (fm : DialectFileMap) (f : Elab.LoadedDialects → Elab.LoadedDialects) : BaseIO Unit

Equations

• fm.modifyLoaded f = ST.Ref.modify fm.loaded f

def StrataDDM.DialectFileMap.strata_dialect_ext : String

Equations

• StrataDDM.DialectFileMap.strata_dialect_ext = ".dialect.st"

def StrataDDM.DialectFileMap.strata_ion_dialect_ext : String

Equations

• StrataDDM.DialectFileMap.strata_ion_dialect_ext = ".dialect.st.ion"

def StrataDDM.DialectFileMap.matchExt (path ext : String) : Option String

Equations

• StrataDDM.DialectFileMap.matchExt path ext = if path.endsWith ext = true then some (path.dropEnd ext.length).toString else none

def StrataDDM.DialectFileMap.addEntry (m : DialectFileMap) (stem : DialectName) (enc : Encoding) (path : System.FilePath) : BaseIO DialectFileMap

Equations

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

def StrataDDM.DialectFileMap.add (m : DialectFileMap) (dir : System.FilePath) : EIO String DialectFileMap

Equations

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

def StrataDDM.DialectFileMap.ofDirs (dirs : Array System.FilePath) (init : DialectFileMap) : EIO String DialectFileMap

Equations

• StrataDDM.DialectFileMap.ofDirs dirs init = Array.foldlM (fun (m : StrataDDM.DialectFileMap) (dir : System.FilePath) => m.add dir) init dirs

def StrataDDM.DialectFileMap.findPath (m : DialectFileMap) (name : DialectName) : Option System.FilePath

Equations

• m.findPath name = match m.map[name]? with | none => none | some (fst, fst_1, path) => pure path