Idris2Doc : Text.TOML.Types

Text.TOML.Types

(source)
Reexports
import public Data.Time.Time
import public Data.SortedMap
Definitions
data TomlFloat : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NaN : TomlFloat
  
Infty : Maybe Sign -> TomlFloat
  
Float : Double -> TomlFloat

  Hints:
  
Eq TomlFloat
  
Interpolation TomlFloat
  
Show TomlFloat
data TableType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
None : TableType
  
Inline : TableType
  
Table : TableType

  Hints:
  
Eq TableType
  
Ord TableType
  
Show TableType
data ArrayType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Static : ArrayType
  
OfTables : ArrayType

  Hints:
  
Eq ArrayType
  
Ord ArrayType
  
Show ArrayType
0 Key : Type
  Totality: total
  Visibility: public export
data TomlValue : Type
  Data type for trees of TOML data.

  Totality: total
  Visibility: public export
  Constructors:
  
TStr : String -> TomlValue
  A string literal
  
TBool : Bool -> TomlValue
  A boolean literal
  
TTime : AnyTime -> TomlValue
  A date-time literal
  
TInt : Integer -> TomlValue
  An integer
  
TDbl : TomlFloat -> TomlValue
  A floating point number
  
TArr : ArrayType -> SnocList TomlValue -> TomlValue
  An array of values
  
TTbl : TableType -> SortedMap String TomlValue -> TomlValue
  A table of key-value pairs

  Hints:
  
Eq TomlValue
  
Show TomlValue
0 TomlTable : Type
  Currently, a TOML table is a list of pairs. This might be later
  changed to some kind of dictionary.

  Totality: total
  Visibility: public export
data KeyType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Plain : KeyType
  
Quoted : KeyType
  
Literal : KeyType

  Hints:
  
Eq KeyType
  
Show KeyType
record KeyToken : Type
  Totality: total
  Visibility: public export
  Constructor: 
KT : String -> KeyType -> Bounds -> KeyToken

  Projections:
  
.bounds : KeyToken -> Bounds
  
.key : KeyToken -> String
  
.tpe : KeyToken -> KeyType

  Hints:
  
Eq KeyToken
  
Interpolation KeyToken
  
Show KeyToken
.key : KeyToken -> String
  Totality: total
  Visibility: public export
key : KeyToken -> String
  Totality: total
  Visibility: public export
.tpe : KeyToken -> KeyType
  Totality: total
  Visibility: public export
tpe : KeyToken -> KeyType
  Totality: total
  Visibility: public export
.bounds : KeyToken -> Bounds
  Totality: total
  Visibility: public export
bounds : KeyToken -> Bounds
  Totality: total
  Visibility: public export
data TomlToken : Type
  Type of TOML lexemes

  Totality: total
  Visibility: public export
  Constructors:
  
TKey : List1 KeyToken -> TomlToken
  A path of dot-separated keys
  
TVal : TomlValue -> TomlToken
  A (literal) value
  
TSym : String -> TomlToken
  A single or multi-character symbol like "[", "[[" or "."
  
NL : TomlToken
  Whitespace containing at least one line break
  
Space : TomlToken
  Whitespace without line breaks (tabs and spaces)
  
Comment : TomlToken
  A line comment

  Hints:
  
Eq TomlToken
  
Interpolation TomlToken
  
Show TomlToken
key1 : KeyToken -> TomlToken
  Totality: total
  Visibility: public export
interpolateKey : List KeyToken -> String
  Totality: total
  Visibility: export
data TomlParseError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ValueExists : List KeyToken -> TomlParseError
  
InlineTableExists : List KeyToken -> TomlParseError
  
TableExists : List KeyToken -> TomlParseError
  
StaticArray : List KeyToken -> TomlParseError
  
ExpectedKey : TomlParseError

  Hints:
  
Eq TomlParseError
  
Interpolation TomlParseError
  
Show TomlParseError
0 TomlErr : Type
  Error type when lexing and parsing TOML files

  Totality: total
  Visibility: public export