
   0 | module Text.TOML.Lexer
   1 | 
   2 | import Data.Buffer
   3 | import Data.ByteString
   4 | import Data.List
   5 | import Data.Maybe
   6 | import Text.TOML.Types
   7 | import Text.ILex.RExp
   8 | import Text.ILex.Util
   9 | 
  10 | %default total
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | -- General Character Classes
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | export %inline
  17 | underscore : Bits8
  18 | underscore = 95
  19 | 
  20 | ||| wschar =  %x20  ; Space
  21 | ||| wschar =/ %x09  ; Horizontal tab
  22 | export
  23 | wschar : RExp True
  24 | wschar = ' ' || '\t'
  25 | 
  26 | ||| newline =  %x0A     ; LF
  27 | ||| newline =/ %x0D.0A  ; CRLF
  28 | export
  29 | newline : RExp True
  30 | newline = '\n' <|> "\r\n"
  31 | 
  32 | ||| non-ascii = %x80-D7FF / %xE000-10FFFF
  33 | export
  34 | nonAscii : RExp True
  35 | nonAscii = range32 0x80 0xD7FF || range32 0xE000 0x10FFFF
  36 | 
  37 | ||| comment-start-symbol = %x23 ; #
  38 | ||| comment = comment-start-symbol *non-eol
  39 | ||| non-eol = %x09 / %x20-7E / non-ascii
  40 | export
  41 | comment : RExp True
  42 | comment = '#' >> star ('\t' || range32 0x20 0x7E || nonAscii)
  43 | 
  44 | --------------------------------------------------------------------------------
  45 | -- Strings and Keys
  46 | --------------------------------------------------------------------------------
  47 | 
  48 | ||| unquoted-key = 1*( ALPHA / DIGIT / %x2D / %x5F ) ; A-Z / a-z / 0-9 / - / _
  49 | export
  50 | unquotedKey : RExp True
  51 | unquotedKey = plus (alphaNum || '-' || '_')
  52 | 
  53 | ||| literal-char = %x09 / %x20-26 / %x28-7E / non-ascii
  54 | export
  55 | literalChars : RExp True
  56 | literalChars = plus $ '\t' || range32 0x20 0x26 || range32 0x28 0x7e || nonAscii
  57 | 
  58 | ||| basic-unescaped = wschar / %x21 / %x23-5B / %x5D-7E / non-ascii
  59 | export
  60 | basicUnescaped : RExp True
  61 | basicUnescaped =
  62 |   wschar || '!' || range32 0x23 0x5b || range32 0x5d 0x7e || nonAscii
  63 | 
  64 | ||| mlb-escaped-nl = escape ws newline *( wschar / newline )
  65 | export
  66 | mlbEscapedNL : RExp True
  67 | mlbEscapedNL =
  68 |   '\\' >> star wschar >> newline >> star (wschar <|> newline)
  69 | 
  70 | --------------------------------------------------------------------------------
  71 | -- Numbers
  72 | --------------------------------------------------------------------------------
  73 | 
  74 | mp : RExp False
  75 | mp = opt $ oneof ['-', '+']
  76 | 
  77 | ||| dec-int = [ minus / plus ] unsigned-dec-int
  78 | ||| unsigned-dec-int = DIGIT / digit1-9 1*( DIGIT / underscore DIGIT )
  79 | export
  80 | decInt : RExp True
  81 | decInt = mp >> ('0' <|> (posdigit >> star (opt '_' >> digit)))
  82 | 
  83 | ||| bin-int = bin-prefix digit0-1 *( digit0-1 / underscore digit0-1 )
  84 | export
  85 | binInt : RExp True
  86 | binInt = "0b" >> bindigit >> star (opt '_' >> bindigit)
  87 | 
  88 | ||| oct-int = oct-prefix digit0-7 *( digit0-7 / underscore digit0-7 )
  89 | export
  90 | octInt : RExp True
  91 | octInt = "0o" >> octdigit >> star (opt '_' >> octdigit)
  92 | 
  93 | ||| hex-int = hex-prefix HEXDIG *( HEXDIG / underscore HEXDIG )
  94 | export
  95 | hexInt : RExp True
  96 | hexInt = "0x" >> hexdigit >> star (opt '_' >> hexdigit)
  97 | 
  98 | export
  99 | readDecInt : ByteString -> Integer
 100 | readDecInt    (BS 0 _)      = 0
 101 | readDecInt bs@(BS (S k) bv) =
 102 |   case bv `at` 0 of
 103 |     43 => decimalSep underscore (BS k $ tail bv) -- '+xyz'
 104 |     45 => negate $ decimalSep underscore (BS k $ tail bv) -- '-xyz'
 105 |     _  => decimalSep underscore bs -- 'xyz'
 106 | 
 107 | export
 108 | nan : RExp True
 109 | nan = mp >> "nan"
 110 | 
 111 | export
 112 | posInf : RExp True
 113 | posInf = opt '+' >> "inf"
 114 | 
 115 | ||| float = float-int-part ( exp / frac [ exp ] )
 116 | ||| float-int-part = dec-int
 117 | ||| frac = decimal-point zero-prefixable-int
 118 | ||| decimal-point = %x2E               ; .
 119 | ||| zero-prefixable-int = DIGIT *( DIGIT / underscore DIGIT )
 120 | ||| exp = "e" float-exp-part
 121 | ||| float-exp-part = [ minus / plus ] zero-prefixable-int
 122 | export
 123 | float : RExp True
 124 | float = decInt >> (exp <|> (frac >> opt exp))
 125 |   where
 126 |     frac, exp, zeroPrefixableInt : RExp True
 127 |     frac              = '.' >> zeroPrefixableInt
 128 |     exp               = ('e' <|> 'E') >> mp >> zeroPrefixableInt
 129 |     zeroPrefixableInt = digit >> star (opt '_' >> digit)
 130 | 
 131 | export
 132 | readFloat : ByteString -> TomlFloat
 133 | readFloat bs =
 134 |   Float $ case unpack $ toString bs of
 135 |     '+' :: t => go [<] t
 136 |     t        => go [<] t
 137 |   where
 138 |     go : SnocList Char -> List Char -> Double
 139 |     go sc []        = cast $ pack (sc <>> [])
 140 |     go sc ('_'::cs) = go sc cs
 141 |     go sc ('E'::cs) = go (sc:<'e') cs
 142 |     go sc (c::cs)   = go (sc:<c) cs
 143 | 
 144 | --------------------------------------------------------------------------------
 145 | -- Date and Time
 146 | --------------------------------------------------------------------------------
 147 | 
 148 | %inline
 149 | readInt : (Integer -> Maybe a) -> a -> ByteString -> a
 150 | readInt f v = fromMaybe v . f . decimal
 151 | 
 152 | ||| full-date      = date-fullyear "-" date-month "-" date-mday
 153 | ||| local-date     = full-date
 154 | ||| date-fullyear  = 4DIGIT
 155 | ||| date-month     = 2DIGIT  ; 01-12
 156 | ||| date-mday      = 2DIGIT  ; 01-28, 01-29, 01-30, 01-31 based on month/year
 157 | export
 158 | fullDate : RExp True
 159 | fullDate = repeat 4 digit >> '-' >> month_day
 160 |   where
 161 |     d29,d30,d31,month_day : RExp True
 162 |     d29 = ('0' >> posdigit) <|> (oneof ['1','2'] >> digit)
 163 |     d30 = d29 <|> "30"
 164 |     d31 = d30 <|> "31"
 165 | 
 166 |     month_day =
 167 |           (("01"<|>"03"<|>"05"<|>"07"<|>"08"<|>"10"<|>"12") >> '-' >> d31)
 168 |       <|> (("04"<|>"06"<|>"09"<|>"11") >> '-' >> d30)
 169 |       <|> ("02-" >> d29)
 170 | 
 171 | export
 172 | readLocalDate : ByteString -> LocalDate
 173 | readLocalDate bs =
 174 |  let y      := readInt refineYear 0 (take 4 bs)
 175 |      m      := readInt intToMonth JAN (take 2 $ drop 5 bs)
 176 |   in case refineDay {m} (decimal $ take 2 $ drop 8 bs) of
 177 |        Just d  => MkDate y m d
 178 |        Nothing => MkDate y JAN 1
 179 | 
 180 | -- time-hour      = 2DIGIT  ; 00-23
 181 | timeHour : RExp True
 182 | timeHour    = (oneof ['0','1'] >> digit) <|> ('2' >> range '0' '3')
 183 | 
 184 | -- time-minute      = 2DIGIT  ; 00-59
 185 | timeMinute : RExp True
 186 | timeMinute  = range '0' '5' >> digit
 187 | 
 188 | ||| local-time   = partial-time
 189 | ||| partial-time = time-hour ":" time-minute [ ":" time-second [ time-secfrac ] ]
 190 | ||| time-secfrac = "." 1*DIGIT
 191 | export
 192 | localTime : RExp True
 193 | localTime = timeHour >> ':' >> timeMinute >> ':' >> sec >> opt frac
 194 |   where
 195 |     sec,frac : RExp True
 196 |     sec  = timeMinute <|> "60"
 197 |     frac = '.' >> plus digit
 198 | 
 199 | export
 200 | readLocalTime : ByteString -> LocalTime
 201 | readLocalTime bs =
 202 |   let h := readInt refineHour   0 (take 2 bs)
 203 |       m := readInt refineMinute 0 (take 2 $ drop 3 bs)
 204 |       s := readInt refineSecond 0 (take 2 $ drop 6 bs)
 205 |    in case drop 8 bs of
 206 |         BS 0 _           => LT h m s Nothing
 207 |         bs@(BS (S k) bv) => case bv `at` 0 of
 208 |           46 => -- 0.0
 209 |            let bs' := padRight 6 byte_0 $ takeWhile isDigit (BS k $ tail bv)
 210 |             in LT h m s $ Just $ readInt refineMicroSecond 0 bs'
 211 |           _  => LT h m s Nothing
 212 | 
 213 | ||| local-date-time = full-date time-delim partial-time
 214 | ||| time-delim     = "T" / %x20 ; T, t, or space
 215 | export
 216 | localDateTime : RExp True
 217 | localDateTime = fullDate >> oneof ['T','t',' '] >> localTime
 218 | 
 219 | export
 220 | readLocalDateTime : ByteString -> LocalDateTime
 221 | readLocalDateTime bs =
 222 |  let fd := readLocalDate bs
 223 |   in LDT fd (readLocalTime $ drop 11 bs)
 224 | 
 225 | ||| offset-date-time = full-date time-delim full-time
 226 | ||| full-time = partial-time time-offset
 227 | ||| time-offset    = "Z" / time-numoffset
 228 | ||| time-numoffset = ( "+" / "-" ) time-hour ":" time-minute
 229 | export
 230 | offsetDateTime : RExp True
 231 | offsetDateTime =
 232 |  let timeNumoffset := oneof ['+','-'] >> timeHour >> ':' >> timeMinute
 233 |   in localDateTime >> ('Z' <|> 'z' <|> timeNumoffset)
 234 | 
 235 | export
 236 | readOffsetDateTime : ByteString -> OffsetDateTime
 237 | readOffsetDateTime bs =
 238 |  let LDT d t := readLocalDateTime bs
 239 |   in ODT d (OT t offset)
 240 | 
 241 |   where
 242 |     offset : Offset
 243 |     offset =
 244 |      let bs2@(BS (S _) bv) := takeEnd 6 bs | _ => Z
 245 |       in case last bv of
 246 |            90  => Z -- 'Z'
 247 |            122 => Z -- 'z'
 248 |            _   =>
 249 |             let h := readInt refineHour 0 (take 2 $ drop 1 bs2)
 250 |                 m := readInt refineMinute 0 (take 2 $ drop 4 bs2)
 251 |                 x := if at bv 0 == 43 then Plus else Minus
 252 |              in O x h m
 253 |