0 | module Text.TOML.Types
  1 |
  2 | import public Data.Time.Time
  3 | import public Data.SortedMap
  4 | import Derive.Prelude
  5 | import Text.Bounds
  6 | import Text.ParseError
  7 |
  8 | %default total
  9 | %language ElabReflection
 10 |
 11 | --------------------------------------------------------------------------------
 12 | --          Floating Point Literals
 13 | --------------------------------------------------------------------------------
 14 |
 15 | public export
 16 | data TomlFloat : Type where
 17 |   NaN   : TomlFloat
 18 |   Infty : Maybe Sign -> TomlFloat
 19 |   Float : Double -> TomlFloat
 20 |
 21 | %runElab derive "TomlFloat" [Eq,Show]
 22 |
 23 | export
 24 | Interpolation TomlFloat where
 25 |   interpolate NaN = "nan"
 26 |   interpolate (Infty x) =
 27 |     let s = maybe "" interpolate x
 28 |      in "\{s}inf"
 29 |   interpolate (Float dbl) = show dbl
 30 |
 31 | --------------------------------------------------------------------------------
 32 | --          Table Type
 33 | --------------------------------------------------------------------------------
 34 |
 35 | public export
 36 | data TableType = None | Inline | Table
 37 |
 38 | %runElab derive "TableType" [Show,Eq,Ord]
 39 |
 40 | public export
 41 | data ArrayType = Static | OfTables
 42 |
 43 | %runElab derive "ArrayType" [Show,Eq,Ord]
 44 |
 45 | --------------------------------------------------------------------------------
 46 | --          TomlValue and Table
 47 | --------------------------------------------------------------------------------
 48 |
 49 | public export
 50 | 0 Key : Type
 51 | Key = List1 String
 52 |
 53 | ||| Data type for trees of TOML data.
 54 | public export
 55 | data TomlValue : Type where
 56 |   ||| A string literal
 57 |   TStr  : String -> TomlValue
 58 |
 59 |   ||| A boolean literal
 60 |   TBool : Bool -> TomlValue
 61 |
 62 |   ||| A date-time literal
 63 |   TTime : AnyTime -> TomlValue
 64 |
 65 |   ||| An integer
 66 |   TInt  : Integer -> TomlValue
 67 |
 68 |   ||| A floating point number
 69 |   TDbl  : TomlFloat  -> TomlValue
 70 |
 71 |   ||| An array of values
 72 |   TArr  : ArrayType -> SnocList TomlValue -> TomlValue
 73 |
 74 |   ||| A table of key-value pairs
 75 |   TTbl  : TableType -> SortedMap String TomlValue -> TomlValue
 76 |
 77 | %runElab derive "TomlValue" [Eq,Show]
 78 |
 79 | ||| Currently, a TOML table is a list of pairs. This might be later
 80 | ||| changed to some kind of dictionary.
 81 | public export
 82 | 0 TomlTable : Type
 83 | TomlTable = SortedMap String TomlValue
 84 |
 85 | --------------------------------------------------------------------------------
 86 | --          Tokens
 87 | --------------------------------------------------------------------------------
 88 |
 89 | public export
 90 | data KeyType = Plain | Quoted | Literal
 91 |
 92 | %runElab derive "KeyType" [Eq,Show]
 93 |
 94 | public export
 95 | record KeyToken where
 96 |   constructor KT
 97 |   key    : String
 98 |   tpe    : KeyType
 99 |   bounds : Bounds
100 |
101 | %runElab derive "KeyToken" [Eq,Show]
102 |
103 | export
104 | Interpolation KeyToken where
105 |   interpolate (KT k t _) = case t of
106 |     Plain   => k
107 |     Quoted  => show k
108 |     Literal => "'" ++ k ++ "'"
109 |
110 | ||| Type of TOML lexemes
111 | public export
112 | data TomlToken : Type where
113 |   ||| A path of dot-separated keys
114 |   TKey    : List1 KeyToken -> TomlToken
115 |
116 |   ||| A (literal) value
117 |   TVal    : TomlValue -> TomlToken
118 |
119 |   ||| A single or multi-character symbol like "[", "[[" or "."
120 |   TSym    : String -> TomlToken
121 |
122 |   ||| Whitespace containing at least one line break
123 |   NL      : TomlToken
124 |
125 |   ||| Whitespace without line breaks (tabs and spaces)
126 |   Space   : TomlToken
127 |
128 |   ||| A line comment
129 |   Comment : TomlToken
130 |
131 | %runElab derive "TomlToken" [Eq,Show]
132 |
133 | public export %inline
134 | key1 : KeyToken -> TomlToken
135 | key1 = TKey . singleton
136 |
137 | export
138 | interpolateKey : List KeyToken -> String
139 | interpolateKey = concat . intersperse "." . map interpolate
140 |
141 | export
142 | Interpolation TomlToken where
143 |   interpolate NL       = "<line break>"
144 |   interpolate Space    = "<space>"
145 |   interpolate Comment  = "<comment>"
146 |   interpolate (TKey s) = interpolateKey $ forget s
147 |   interpolate (TVal v) = case v of
148 |     TStr str => "string literal"
149 |     TBool x  => toLower $ show x
150 |     TInt i   => show i
151 |     TTime i  => interpolate i
152 |     TDbl dbl => interpolate dbl
153 |     TArr _ _ => "array"
154 |     TTbl _ x => "table"
155 |   interpolate (TSym c) = show c
156 |
157 | --------------------------------------------------------------------------------
158 | --          Errors
159 | --------------------------------------------------------------------------------
160 |
161 | public export
162 | data TomlParseError : Type where
163 |   ValueExists       : List KeyToken -> TomlParseError
164 |   InlineTableExists : List KeyToken -> TomlParseError
165 |   TableExists       : List KeyToken -> TomlParseError
166 |   StaticArray       : List KeyToken -> TomlParseError
167 |   ExpectedKey       : TomlParseError
168 |
169 | %runElab derive "TomlParseError" [Eq,Show]
170 |
171 | export
172 | Interpolation TomlParseError where
173 |   interpolate ExpectedKey = "Expected a key"
174 |   interpolate (ValueExists k) =
175 |     "Trying to overwrite existing value: \{interpolateKey k}"
176 |   interpolate (InlineTableExists k) =
177 |     "Trying to modify existing inline table: \{interpolateKey k}"
178 |   interpolate (TableExists k) =
179 |     "Trying to overwrite existing table: \{interpolateKey k}"
180 |   interpolate (StaticArray k) =
181 |     "Trying to modify a static array: \{interpolateKey k}"
182 |
183 | ||| Error type when lexing and parsing TOML files
184 | public export
185 | 0 TomlErr : Type
186 | TomlErr = InnerError TomlParseError
187 |