def StrataDDM.SepFormat.toIonName : SepFormat → String

Equations

• StrataDDM.SepFormat.none.toIonName = "seq"
• StrataDDM.SepFormat.comma.toIonName = "commaSepList"
• StrataDDM.SepFormat.space.toIonName = "spaceSepList"
• StrataDDM.SepFormat.spacePrefix.toIonName = "spacePrefixedList"
• StrataDDM.SepFormat.newline.toIonName = "newlineSepList"
• StrataDDM.SepFormat.semicolonNewline.toIonName = "semicolonSepList"

def StrataDDM.SepFormat.fromIonName? : String → Option SepFormat

Equations

• StrataDDM.SepFormat.fromIonName? "seq" = some StrataDDM.SepFormat.none
• StrataDDM.SepFormat.fromIonName? "commaSepList" = some StrataDDM.SepFormat.comma
• StrataDDM.SepFormat.fromIonName? "spaceSepList" = some StrataDDM.SepFormat.space
• StrataDDM.SepFormat.fromIonName? "spacePrefixedList" = some StrataDDM.SepFormat.spacePrefix
• StrataDDM.SepFormat.fromIonName? "newlineSepList" = some StrataDDM.SepFormat.newline
• StrataDDM.SepFormat.fromIonName? "semicolonSepList" = some StrataDDM.SepFormat.semicolonNewline
• StrataDDM.SepFormat.fromIonName? x✝ = none

theorem StrataDDM.SepFormat.fromIonName_toIonName_roundtrip (sep : SepFormat) : fromIonName? sep.toIonName = some sep

theorem StrataDDM.SepFormat.fromIonName_none_of_invalid (s : String) (h : ∀ (sep : SepFormat), sep.toIonName ≠ s) : fromIonName? s = Option.none

Invalid Ion separator names return none.

structure StrataDDM.FromIonContext : Type

• symbols : Ion.SymbolTable

def StrataDDM.FromIonM (α : Type) : Type

Equations

• StrataDDM.FromIonM = ReaderT StrataDDM.FromIonContext (Except String)

@[implicit_reducible]

instance StrataDDM.instMonadFromIonM : Monad FromIonM

Equations

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

class StrataDDM.FromIon (α : Type) : Type

• fromIon : Ion.Ion Ion.SymbolId → FromIonM α

def StrataDDM.FromIon.deserialize {α : Type} [FromIon α] (bs : ByteArray) : Except String α

Equations

• StrataDDM.FromIon.deserialize bs = StrataDDM.FromIonM.deserializeValue✝ bs StrataDDM.fromIon

structure StrataDDM.Ion.Fragment : Type

This contains information from a partially parsed Ion File.

• symbols : Ion.SymbolTable
• values : Array (Ion.Ion Ion.SymbolId)
• offset : Nat

inductive StrataDDM.Ion.Header : Type

• dialect : DialectName → Header
• program : DialectName → Header

def StrataDDM.Ion.Header.parse (bytes : ByteArray) : Except String (Header × Fragment)

Equations

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

def StrataDDM.Dialect.fromIonFragment (dialect : DialectName) (f : Ion.Fragment) : Except String Dialect

Equations

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

def StrataDDM.Dialect.toIon : Dialect → ByteArray

Equations

• x✝.toIon = match StrataDDM.Dialect.toIonValues✝ x✝ with | (tbl, v) => Ion.serialize #[tbl.localSymbolTableValue, v]

structure StrataDDM.StrataFile : Type

• filePath : String
• program : Program

@[implicit_reducible]

instance StrataDDM.instInhabitedStrataFile : Inhabited StrataFile

Equations

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

def StrataDDM.instInhabitedStrataFile.default : StrataFile

Equations

• StrataDDM.instInhabitedStrataFile.default = { filePath := default, program := default }

def StrataDDM.Program.toIon : Program → ByteArray

Equations

• x✝.toIon = match StrataDDM.Program.toIonValues✝ x✝ with | (tbl, v) => Ion.serialize #[tbl.localSymbolTableValue, v]

def StrataDDM.Program.fromIonFragmentCommands (f : Ion.Fragment) : Except String (Array Operation)

Equations

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

def StrataDDM.Program.fromIonFragment (f : Ion.Fragment) (dialects : DialectMap) (dialect : DialectName) : Except String Program

Equations

• StrataDDM.Program.fromIonFragment f dialects dialect = do let commands ← StrataDDM.Program.fromIonFragmentCommands f pure (StrataDDM.Program.create dialects dialect commands)

def StrataDDM.Program.fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Program

Decodes bytes in the Ion format into a single Strata program.

Equations

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

def StrataDDM.Program.filesFromIon (dialects : DialectMap) (bytes : ByteArray) : Except String (List StrataFile)

Equations

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