Strata DDM API

File I/O for reading and writing Strata programs in textual or Ion format.

DialectFileMap construction

def StrataDDM.mkDialectFileMap (dialects : Array Dialect := #[]) : IO DialectFileMap

Build a DialectFileMap preloaded with the given dialects (plus the built-in DDM dialects: init, header, and StrataDDL). Use this to construct a DialectFileMap opaquely without touching DDM internals.

Equations

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

def StrataDDM.DialectFileMap.addSearchPath (fm : DialectFileMap) (dir : System.FilePath) : EIO String DialectFileMap

Register a directory to search for dialect definition files (.dialect.st / .dialect.st.ion). Returns an updated DialectFileMap.

Equations

• fm.addSearchPath dir = fm.add dir

File I/O

inductive StrataDDM.DialectOrProgram : Type

A Dialect or Program, used to represent the results of reading from a Strata text or Ion file. Such a file can define either a dialect or a program.

• dialect (d : Dialect) : DialectOrProgram
• program (pgm : Program) : DialectOrProgram

def StrataDDM.readStrataText (fm : DialectFileMap) (path : System.FilePath) (bytes : ByteArray) : IO DialectOrProgram

Parse a Strata dialect or program in textual format, possibly loading other dialects as needed along the way. The DialectFileMap indicates where to find the definitions of other dialects. The FilePath indicates the name of the file to be parsed. And the ByteArray includes the contents of that file. TODO: should it take just a file name and read it directly?

Equations

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

def StrataDDM.readStrataIon (fm : DialectFileMap) (path : System.FilePath) (bytes : ByteArray) : IO DialectOrProgram

Parse a Strata dialect or program in Ion format, possibly loading other dialects as needed along the way. The DialectFileMap indicates where to find the definitions of other dialects. The FilePath indicates the name of the file to be parsed. And the ByteArray includes the contents of that file. TODO: should it take just a file name and read it directly?

Equations

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

def StrataDDM.readStrataFile (fm : DialectFileMap) (path : System.FilePath) : IO DialectOrProgram

Parse a Strata dialect or program in either textual or Ion format, possibly loading other dialects as needed along the way. The DialectFileMap indicates where to find the definitions of other dialects. The FilePath indicates the name of the file to be loaded.

Equations

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

def StrataDDM.readStrataProgramFile (fm : DialectFileMap) (path : System.FilePath) : IO Program

Read a Strata file (text or Ion) and require it to be a program. Fails if the file defines a dialect.

Equations

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

def StrataDDM.readStrataDialectFile (fm : DialectFileMap) (path : System.FilePath) : IO Dialect

Read a Strata file (text or Ion) and require it to be a dialect. Fails if the file defines a program.

Equations

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

def StrataDDM.writeStrataText : Program → ByteArray

Serialize a Strata program in textual format. Returns a byte array rather than writing directly to a file.

Equations

• StrataDDM.writeStrataText x✝ = x✝.toString.toByteArray

def StrataDDM.writeStrataIon : Program → ByteArray

Serialize a Strata program in Ion format. Returns a byte array rather than writing directly to a file.

Equations

• StrataDDM.writeStrataIon x✝ = x✝.toIon