Text.Molfile.SData

Reexports

import public Data.Nat
import public Data.String
import public Data.Refined
import public Data.Refined.Integer
import public Data.Refined.String

Definitions

IsHeaderChar : Char -> Bool

Totality: total
Visibility: public export

0 IsHeader : String -> Type

Totality: total
Visibility: public export

record SDHeader : Type

  Header of a SDF data entry. This is put in angles (`<>`) in an SD file.

Totality: total
Visibility: public export
Constructor:

SDH : (value : String) -> {auto 0 _ : IsHeader value} -> SDHeader

Projections:

0 .prf : ({rec:0} : SDHeader) -> IsHeader (value {rec:0})
.value : SDHeader -> String

Hints:

Eq SDHeader
Interpolation SDHeader
Ord SDHeader
Show SDHeader

.value : SDHeader -> String

Totality: total
Visibility: public export

value : SDHeader -> String

Totality: total
Visibility: public export

0 .prf : ({rec:0} : SDHeader) -> IsHeader (value {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : SDHeader) -> IsHeader (value {rec:0})

Totality: total
Visibility: public export

readHeader : ByteString -> SDHeader

Totality: total
Visibility: export

encodeHeader : String -> Maybe SDHeader

  Encodes a value header by replacing spaces with underscores and
  dropping some other invalid characters such as angles.

Totality: total
Visibility: export

0 IsValue : String -> Type

Totality: total
Visibility: public export

record SDValue : Type

  Value of an SDF data entry. This follows after the header (see
  `SDHeader`) and may span across several lines, each of which must not
  be longer than 200 characters.

Totality: total
Visibility: public export
Constructor:

SDV : (value : String) -> {auto 0 _ : IsValue value} -> SDValue

Projections:

0 .prf : ({rec:0} : SDValue) -> IsValue (value {rec:0})
.value : SDValue -> String

Hints:

Eq SDValue
Interpolation SDValue
Ord SDValue
Show SDValue

.value : SDValue -> String

Totality: total
Visibility: public export

value : SDValue -> String

Totality: total
Visibility: public export

0 .prf : ({rec:0} : SDValue) -> IsValue (value {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : SDValue) -> IsValue (value {rec:0})

Totality: total
Visibility: public export

record StructureData : Type

  A data entry in an SD file consisting of the data header and value.

Totality: total
Visibility: public export
Constructor:

SD : SDHeader -> SDValue -> StructureData

Projections:

.header : StructureData -> SDHeader
.value : StructureData -> SDValue

Hints:

Eq StructureData
Show StructureData

.header : StructureData -> SDHeader

Totality: total
Visibility: public export

header : StructureData -> SDHeader

Totality: total
Visibility: public export

.value : StructureData -> SDValue

Totality: total
Visibility: public export

value : StructureData -> SDValue

Totality: total
Visibility: public export

encodeStructureData : String -> String -> Maybe StructureData

  Tries to convert a name-value pair to a piece of
  SD-data.
  
  While the values is refined as it is, we try to encode the
  header in such a way that it does not contain any invalid
  characters.

Totality: total
Visibility: export