0 | module Text.TOML.Lexer
  1 |
  2 | import Data.Time.Time
  3 | import Data.List1
  4 | import Data.SnocList
  5 | import Text.Parse.Manual
  6 | import Text.Time.Lexer
  7 | import Text.TOML.Types
  8 |
  9 | %default total
 10 |
 11 | -- facilitates pattern matching on and creating of symbol
 12 | -- tokens such as "[". We don't want to export this, as it tends
 13 | -- to interfer with regular `String` literals.
 14 | %inline
 15 | fromString : String -> TomlToken
 16 | fromString = TSym
 17 |
 18 | --------------------------------------------------------------------------------
 19 | --          Keys
 20 | --------------------------------------------------------------------------------
 21 |
 22 | isKeyChar : Char -> Bool
 23 | isKeyChar '-' = True
 24 | isKeyChar '_' = True
 25 | isKeyChar c   = isAlphaNum c
 26 |
 27 | key : SnocList Char -> AutoTok e String
 28 | key sc (x::xs) =
 29 |   if isKeyChar x then key (sc :< x) xs else Succ (cast sc) (x::xs)
 30 | key sc []        = Succ (cast sc) []
 31 |
 32 | --------------------------------------------------------------------------------
 33 | --          String literals
 34 | --------------------------------------------------------------------------------
 35 |
 36 | MaxChar,LowerInvalid,UpperInvalid : Nat
 37 | MaxChar      = 0x10FFFF
 38 | LowerInvalid = 0xD800
 39 | UpperInvalid = 0xDFFF
 40 |
 41 | -- try to read a sequence of hexadecimal digits
 42 | tryHex : Nat -> List Char -> Maybe Char
 43 | tryHex k []        =
 44 |   if k <= MaxChar && (k < LowerInvalid || k > UpperInvalid) then Just $ cast k
 45 |   else Nothing
 46 | tryHex k (x :: xs) = case isHexDigit x of
 47 |   True  => tryHex (k*16 + hexDigit x) xs
 48 |   False => Nothing
 49 |
 50 | commentControl : Char -> Bool
 51 | commentControl '\127' = True
 52 | commentControl x      = x <= '\8' || (x >= '\10' && x <= '\31')
 53 |
 54 | tomlControl : Char -> Bool
 55 | tomlControl '\n' = True
 56 | tomlControl '\f' = True
 57 | tomlControl '\b' = True
 58 | tomlControl '\r' = True
 59 | tomlControl '\t' = True
 60 | tomlControl x    = commentControl x
 61 |
 62 | -- reads and unescapes a plain string
 63 | str : SnocList Char -> AutoTok e String
 64 | str sc ('\\' :: c  :: xs) = case c of
 65 |   '"'  => str (sc :< '"') xs
 66 |   'n'  => str (sc :< '\n') xs
 67 |   'f'  => str (sc :< '\f') xs
 68 |   'b'  => str (sc :< '\b') xs
 69 |   'r'  => str (sc :< '\r') xs
 70 |   't'  => str (sc :< '\t') xs
 71 |   '\\' => str (sc :< '\\') xs
 72 |   'u'  => case xs of
 73 |     w::x::y::z::t' => case tryHex 0 [w,x,y,z] of
 74 |       Just c => str (sc :< c) t'
 75 |       Nothing => invalidEscape p t'
 76 |     _    => invalidEscape p xs
 77 |   'U'  => case xs of
 78 |     s::t::u::v::w::x::y::z::t' => case tryHex 0 [s,t,u,v,w,x,y,z] of
 79 |       Just c => str (sc :< c) t'
 80 |       Nothing => invalidEscape p t'
 81 |     _    => invalidEscape p xs
 82 |   _    => invalidEscape p (c::xs)
 83 | str sc ('"'  :: xs) = Succ (cast sc) xs
 84 | str sc (c    :: xs) =
 85 |   if tomlControl c then range (InvalidControl c) p xs
 86 |   else str (sc :< c) xs
 87 | str sc []           = eoiAt p
 88 |
 89 | validTrim : List Char -> Bool
 90 | validTrim ('\t' :: xs)     = validTrim xs
 91 | validTrim (' ' :: xs)      = validTrim xs
 92 | validTrim ('\n' :: xs)     = True
 93 | validTrim ('\r'::'\n'::xs) = True
 94 | validTrim _ = False
 95 |
 96 | -- reads and unescapes a multi-line string
 97 | strML : (trim : Bool) -> SnocList Char -> AutoTok e String
 98 | strML trim sc ('\\' :: c  :: xs) = case c of
 99 |   '"'  => strML False (sc :< '"') xs
100 |   'n'  => strML False (sc :< '\n') xs
101 |   'f'  => strML False (sc :< '\f') xs
102 |   'b'  => strML False (sc :< '\b') xs
103 |   'r'  => strML False (sc :< '\r') xs
104 |   't'  => strML False (sc :< '\t') xs
105 |   '\\' => strML False (sc :< '\\') xs
106 |   'u'  => case xs of
107 |     w::x::y::z::t' => case tryHex 0 [w,x,y,z] of
108 |       Just c => strML False (sc :< c) t'
109 |       Nothing => invalidEscape p t'
110 |     _    => invalidEscape p xs
111 |   'U'  => case xs of
112 |     s::t::u::v::w::x::y::z::t' => case tryHex 0 [s,t,u,v,w,x,y,z] of
113 |       Just c => strML False (sc :< c) t'
114 |       Nothing => invalidEscape p t'
115 |     _    => invalidEscape p xs
116 |   _    => if validTrim (c::xs) then strML True sc xs
117 |           else invalidEscape p (c::xs)
118 | strML trim sc ('"'::'"'::'"'::'"'::'"'::xs) = Succ (cast $ sc :< '"' :< '"') xs
119 | strML trim sc ('"'::'"'::'"'::'"'::xs) = Succ (cast $ sc :< '"') xs
120 | strML trim sc ('"'::'"'::'"'::xs) = Succ (cast sc) xs
121 | strML trim sc ('\n'::cs) =
122 |   if trim then strML trim sc cs else strML trim (sc :< '\n') cs
123 | strML trim sc ('\t'::cs) =
124 |   if trim then strML trim sc cs else strML trim (sc :< '\t') cs
125 | strML trim sc ('\r'::'\n'::cs) =
126 |   if trim then strML trim sc cs else strML trim (sc :< '\r' :< '\n') cs
127 | strML trim sc (c            ::xs) =
128 |   if tomlControl c then range (InvalidControl c) p xs
129 |   else if isSpace c && trim then strML trim sc xs
130 |   else strML False (sc :< c) xs
131 | strML trim sc []           = eoiAt p
132 |
133 | -- reads a literal stirng
134 | literal : SnocList Char -> AutoTok e String
135 | literal sc ('\''::cs) = Succ (cast sc) cs
136 | literal sc (c :: cs)  =
137 |   if tomlControl c && c /= '\t' then range (InvalidControl c) p cs
138 |   else literal (sc :< c) cs
139 | literal sc [] = eoiAt p
140 |
141 | -- reads a literal multi-line stirng
142 | literalML : SnocList Char -> AutoTok e String
143 | literalML sc ('\''::'\''::'\''::'\''::'\''::cs) = Succ (cast $ sc :< '\'' :< '\'') cs
144 | literalML sc ('\''::'\''::'\''::'\''::cs) = Succ (cast $ sc :< '\'') cs
145 | literalML sc ('\''::'\''::'\''::cs) = Succ (cast sc) cs
146 | literalML sc ('\n'::cs) = literalML (sc :< '\n') cs
147 | literalML sc ('\r'::'\n'::cs) = literalML (sc :< '\r' :< '\n') cs
148 | literalML sc (c :: cs)  =
149 |   if tomlControl c && c /= '\t' then range (InvalidControl c) p cs
150 |   else literalML (sc :< c) cs
151 | literalML sc [] = eoiAt p
152 |
153 | -------------------------------------------------------------------------------
154 | --          Numeric literals
155 | -------------------------------------------------------------------------------
156 |
157 | -- converts an integer literal
158 | intLit : SnocList Char -> (res,pow : Nat) -> TomlToken
159 | intLit [<]       res _   = TVal (TInt $ cast res)
160 | intLit [<'-']    res _   = TVal (TInt . negate $ cast res)
161 | intLit (sx :< x) res pow = intLit sx (res + pow * digit x) (pow * 10)
162 |
163 | -- converts a floating point literal
164 | dblLit : SnocList Char -> TomlToken
165 | dblLit sc = 
166 |   if any (\c => '.' == c || 'e' == c) sc
167 |      then TVal . TDbl . Float . cast $ cast {to = String} sc
168 |      else intLit sc 0 1
169 |
170 | num',rest,dot,exp,digs,digs1 : SnocList Char -> AutoTok e TomlToken
171 |
172 | -- addditional exponent digits, possibly separated by underscores
173 | digs sc ('_'::x::xs) =
174 |   if isDigit x then digs (sc:<x) xs else unknownRange p xs
175 | digs sc (x::xs)      =
176 |   if isDigit x then digs (sc:<x) xs else Succ (dblLit sc) (x::xs)
177 | digs sc []           = Succ (dblLit sc) []
178 |
179 | -- mandatory exponent digits, possibly separated by underscores
180 | digs1 sc (x :: xs) = if isDigit x then digs (sc:<x) xs else unknown p
181 | digs1 sc []        = eoiAt p
182 |
183 | -- exponent: 'e' or 'E' followed by optional '+' or '-' and
184 | -- at least one decimal digit
185 | exp sc ('e'::'+'::xs) = digs1 (sc:<'e') xs
186 | exp sc ('E'::'+'::xs) = digs1 (sc:<'e') xs
187 | exp sc ('e'::'-'::xs) = digs1 (sc:<'e':<'-') xs
188 | exp sc ('E'::'-'::xs) = digs1 (sc:<'e':<'-') xs
189 | exp sc ('e'::xs)      = digs1 (sc:<'e') xs
190 | exp sc ('E'::xs)      = digs1 (sc:<'e') xs
191 | exp sc xs             = Succ (dblLit sc) xs
192 |
193 | -- digits after the decimal dot, possibly separated by '_'
194 | dot sc ('_'::x::xs) = if isDigit x then dot (sc:<x) xs else unknownRange p xs
195 | dot sc (x::xs)      = if isDigit x then dot (sc:<x) xs else exp sc (x::xs)
196 | dot sc []           = Succ (dblLit sc) []
197 |
198 | -- optional decimal and exponent part.
199 | rest sc ('.'::x::xs) = if isDigit x then dot (sc:<'.':< x) xs else unknown p
200 | rest sc ('.'::[])    = unknown p
201 | rest sc xs           = exp sc xs
202 |
203 | -- lexes an integer or floating point literal
204 | num' sc ('_'::x::xs) = if isDigit x then num' (sc:<x) xs else unknownRange p xs
205 | num' sc (x::xs)      = if isDigit x then num' (sc:<x) xs else rest sc (x::xs)
206 | num' sc []           = Succ (intLit sc 0 1) []
207 |
208 | num : Tok True e TomlToken
209 | num ('-'::'0'::t) = rest [<'-','0'] t
210 | num ('+'::'0'::t) = rest [<'0'] t
211 | num ('-'::d::t)   = if isDigit d then num' [<'-',d] t else unknownRange Same t
212 | num ('+'::d::t)   = if isDigit d then num' [<d] t else unknown Same
213 | num ('0'::t)      = rest [<'0'] t
214 | num (d::t)        = if isDigit d then num' [<d] t else unknown Same
215 | num []            = eoiAt Same
216 |
217 | --------------------------------------------------------------------------------
218 | --          Misc.
219 | --------------------------------------------------------------------------------
220 |
221 | comment : AutoTok e TomlToken
222 | comment []           = Succ Comment []
223 | comment ('\n' :: xs) = Succ Comment ('\n' :: xs)
224 | comment ('\r' :: xs) = Succ Comment ('\r' :: xs)
225 | comment ('\t' :: xs) = comment xs
226 | comment (x :: xs)            =
227 |   if commentControl x then range (InvalidControl x) p xs else comment xs
228 |
229 | validSpace : Char -> Bool
230 | validSpace ' '  = True
231 | validSpace '\n' = True
232 | validSpace '\t' = True
233 | validSpace _    = False
234 |
235 | space : AutoTok e TomlToken
236 | space ('\r'::'\n'::xs) = space xs
237 | space (x::xs)          = if validSpace x then space xs else Succ Space (x::xs)
238 | space []               = Succ Space []
239 |
240 | --------------------------------------------------------------------------------
241 | --          Single-step lexers
242 | --------------------------------------------------------------------------------
243 |
244 | isTime : List Char -> Bool
245 | isTime (_::_::':'::_)       = True
246 | isTime (_::_::_::_::'-'::_) = True
247 | isTime _                    = False
248 |
249 | isNum : List Char -> Bool
250 | isNum ('-'::_) = True
251 | isNum ('+'::_) = True
252 | isNum (d::_)   = isDigit d
253 | isNum []       = False
254 |
255 | -- general lexemes that can occur in key and value contexts
256 | other : Tok True e TomlToken
257 | other ('.'  :: xs) = Succ "." xs
258 | other (','  :: xs) = Succ "," xs
259 | other ('='  :: xs) = Succ "=" xs
260 | other ('[' :: xs)  = Succ "[" xs
261 | other (']' :: xs)  = Succ "]" xs
262 | other ('}' :: xs)  = Succ "}" xs
263 | other ('#' :: xs)  = comment xs
264 | other ('\r'::'\n'::xs) = space xs
265 | other (x   :: xs)  = if validSpace x then space xs else unknown Same
266 | other []           = eoiAt Same
267 |
268 | toKey :
269 |      Position
270 |   -> KeyType
271 |   -> LexRes True cs e String
272 |   -> LexRes True cs e TomlToken
273 | toKey x t (Succ v xs @{p}) = Succ (key1 $ KT v t $ BS x (move x p)) xs
274 | toKey _ _ (Fail x y z)     = Fail x y z
275 |
276 | -- lexes a key or sequence of dot-separated keys
277 | -- this includes double brackets for table arrays
278 | anyKey : Position -> Tok True e TomlToken
279 | anyKey pos ('"'  :: xs) = toKey pos Quoted $ str [<] xs
280 | anyKey pos ('\'' :: xs) = toKey pos Literal $ literal [<] xs
281 | anyKey pos ('['::'[':: xs) = Succ "[[" xs
282 | anyKey pos (']'::']':: xs) = Succ "]]" xs
283 | anyKey pos (x :: xs)    =
284 |   if isKeyChar x then toKey pos Plain (key [<x] xs) else other (x::xs)
285 | anyKey _   xs           = other xs
286 |
287 | -- lexes a value or related symbol
288 | val : Tok True e TomlToken
289 | val ('{' :: xs)                   = Succ "{" xs
290 | val ('"' :: '"' :: '"' :: xs)     = case xs of
291 |   '\n'::t         => TVal . TStr <$> strML False [<] t
292 |   '\r' :: '\n'::t => TVal . TStr <$> strML False [<] t
293 |   _               => TVal . TStr <$> strML False [<] xs
294 | val ('\'' :: '\'' :: '\'' :: xs)     = case xs of
295 |   '\n'::t         => TVal . TStr <$> literalML [<] t
296 |   '\r' :: '\n'::t => TVal . TStr <$> literalML [<] t
297 |   _               => TVal . TStr <$> literalML [<] xs
298 | val ('"' :: xs)                   = TVal . TStr <$> str [<] xs
299 | val ('\'' :: xs)                  = TVal . TStr <$> literal [<] xs
300 | val ('0'::'x':: xs)               = TVal . TInt . cast <$> hexSep xs
301 | val ('0'::'b':: xs)               = TVal . TInt . cast <$> binSep xs
302 | val ('0'::'o':: xs)               = TVal . TInt . cast <$> octSep xs
303 | val ('t'::'r'::'u'::'e'::xs)      = Succ (TVal $ TBool True) xs
304 | val ('f'::'a'::'l'::'s'::'e'::xs) = Succ (TVal $ TBool False) xs
305 | val ('n'::'a'::'n'::xs)           = Succ (TVal $ TDbl NaN) xs
306 | val ('+'::'n'::'a'::'n'::xs)      = Succ (TVal $ TDbl NaN) xs
307 | val ('-'::'n'::'a'::'n'::xs)      = Succ (TVal $ TDbl NaN) xs
308 | val ('i'::'n'::'f'::xs)           = Succ (TVal $ TDbl $ Infty Nothing) xs
309 | val ('+'::'i'::'n'::'f'::xs)      = Succ (TVal $ TDbl $ Infty $ Just Plus) xs
310 | val ('-'::'i'::'n'::'f'::xs)      = Succ (TVal $ TDbl $ Infty $ Just Minus) xs
311 | val cs =
312 |   (TVal . TTime <$> anyTime cs) <|> num cs <|> other cs
313 |
314 | --------------------------------------------------------------------------------
315 | --          State
316 | --------------------------------------------------------------------------------
317 |
318 | -- In TOML files, we are either in a position where a (sequence of)
319 | -- keys is expected, or in a position, where a value is expected.
320 | -- This tag keeps track of the two possible contexts.
321 | data Ctxt = Key | Value
322 |
323 | -- Current state of the lexer: Keeps track of whether we are at
324 | -- the toplevel, or in a nesting of arrays and/or literal tables.
325 | -- Depending on the current state, we run one of two possible
326 | -- lexers, the result of which affects the next state.
327 | data LexState : Ctxt -> Type where
328 |   TopLevel : {0 t : Ctxt} -> LexState t
329 |   InArray  : (outer : LexState Value) -> LexState Value
330 |   InTable  : {0 t : Ctxt} -> (outer : LexState Value) -> LexState t
331 |
332 | -- after encountering an equals sign (`'='`) we switch from
333 | -- `Key` to `Value` context.
334 | switch : LexState Key -> LexState Value
335 | switch TopLevel        = TopLevel
336 | switch (InTable outer) = InTable outer
337 |
338 | adjState : (t : Ctxt) -> TomlToken -> LexState t -> (t2 ** LexState t2)
339 | adjState Key  "="  outer           = (_ ** switch outer)
340 | adjState Value NL  TopLevel        = (Key ** TopLevel)
341 | adjState Value "]" (InArray outer) = (_ ** outer)
342 | adjState _     "}" (InTable outer) = (_ ** outer)
343 | adjState Value "[" outer           = (_ ** InArray outer)
344 | adjState Value "{" outer           = (Key ** InTable outer)
345 | adjState Value "," (InTable outer) = (Key ** InTable outer)
346 | adjState t     _   st              = (t ** st)
347 |
348 | -- decides on the lexer to run depending on the current
349 | -- context
350 | %inline
351 | anyTok : Position -> Ctxt -> Tok True e TomlToken
352 | anyTok pos Key   = anyKey pos
353 | anyTok _   Value = val
354 |
355 | -- We convert a `Space` token to a `NL` if the sequence of
356 | -- spaces contains a line break and we are not in an array
357 | -- literal (where arbitrary line breaks are allowed).
358 | adjSpace : LexState c -> (hasNL : Bool) -> TomlToken -> Maybe TomlToken
359 | adjSpace TopLevel    True Space   = Just NL
360 | adjSpace (InTable _) True Space   = Just NL
361 | adjSpace _           _    Space   = Nothing
362 | adjSpace _           _    Comment = Nothing
363 | adjSpace _           _    t       = Just t
364 |
365 | --------------------------------------------------------------------------------
366 | --          Post Processing
367 | --------------------------------------------------------------------------------
368 |
369 | -- to simplify the parser, we group paths of dot-separated key in
370 | -- a single pass when converting the `SnocList` of tokens to
371 | -- a list of tokens.
372 | groupKeys :
373 |      List (Bounded TomlToken)
374 |   -> Bounded (List1 KeyToken)
375 |   -> SnocList (Bounded TomlToken)
376 |   -> List (Bounded TomlToken)
377 |
378 | -- to simplify the parser, we remove non-relevant tokens in
379 | -- a single pass when converting the `SnocList` of tokens to
380 | -- a list of tokens.
381 | postProcess :
382 |      List (Bounded TomlToken)
383 |   -> SnocList (Bounded TomlToken)
384 |   -> List (Bounded TomlToken)
385 |
386 | groupKeys ts ks (sx :< B (TKey p) bk :< B "." bd) =
387 |   groupKeys ts (B (p <+> ks.val) (ks.bounds <+> bd <+> bk)) sx
388 | groupKeys ts ks sx = postProcess (map TKey ks :: ts) sx
389 |
390 | postProcess ts [<]       = ts
391 | postProcess ts (sx :< x) = case x.val of
392 |   TKey s  => groupKeys ts (x $> s) sx
393 |   Comment => postProcess ts sx
394 |   _       => postProcess (x::ts) sx
395 |
396 | --------------------------------------------------------------------------------
397 | --          Complete Lexer
398 | --------------------------------------------------------------------------------
399 |
400 | lex :
401 |      {t : Ctxt}
402 |   -> LexState t
403 |   -> Position
404 |   -> SnocList (Bounded TomlToken)
405 |   -> (cs : List Char)
406 |   -> (0 acc : SuffixAcc cs)
407 |   -> Either (Bounded TomlErr) (List $ Bounded TomlToken)
408 | lex st pos sx [] _      = Right $ postProcess [] sx
409 | lex st pos sx xs (SA r) = case anyTok pos t xs of
410 |   Succ val ys @{p} =>
411 |     let pos2        := endPos pos p
412 |         Just v      := adjSpace st (pos2.line > pos.line) val
413 |           | Nothing => lex st pos2 sx ys r
414 |         (t2 ** st2) := adjState t v st
415 |      in lex st2 pos2 (sx :< bounded v pos pos2) ys r
416 |   Fail start errEnd y => Left $ boundedErr pos start errEnd y
417 |
418 | export %inline
419 | lexToml : String -> Either (Bounded TomlErr) (List $ Bounded TomlToken)
420 | lexToml s = lex {t = Key} TopLevel begin [<] (unpack s) suffixAcc
421 |