
   0 | -- SPDX-FileCopyrightText: 2021 The toml-idr developers
   1 | --
   2 | -- SPDX-License-Identifier: MPL-2.0
   3 | 
   4 | module Language.TOML.Tokens
   5 | 
   6 | import Text.Bounded
   7 | import Text.Token
   8 | 
   9 | %default total
  10 | 
  11 | public export
  12 | strTrue : String
  13 | strTrue = "true"
  14 | 
  15 | public export
  16 | strFalse : String
  17 | strFalse = "false"
  18 | 
  19 | public export
  20 | data Bracket = Open | Close
  21 | 
  22 | export
  23 | Show Bracket where
  24 |     show Open = "open"
  25 |     show Close = "close"
  26 | 
  27 | public export
  28 | Eq Bracket where
  29 |     (==) Open Open = True
  30 |     (==) Close Close = True
  31 |     (==) _ _ = False
  32 | 
  33 | public export
  34 | data Punctuation
  35 |     = Comma
  36 |     | Dot
  37 |     | Equal
  38 |     | NewLine
  39 |     | Square Bracket
  40 |     | Curly Bracket
  41 | 
  42 | export
  43 | Show Punctuation where
  44 |     show Comma = ","
  45 |     show Dot = "."
  46 |     show Equal = "="
  47 |     show NewLine = "\\n"
  48 |     show (Square Open) = "["
  49 |     show (Square Close) = "]"
  50 |     show (Curly Open) = "("
  51 |     show (Curly Close) = ")"
  52 | 
  53 | public export
  54 | Eq Punctuation where
  55 |     (==) Comma Comma = True
  56 |     (==) Dot Dot = True
  57 |     (==) Equal Equal = True
  58 |     (==) NewLine NewLine = True
  59 |     (==) (Square x) (Square y) = x == y
  60 |     (==) (Curly x) (Curly y) = x == y
  61 |     (==) _ _ = False
  62 | 
  63 | ||| What sort of string this is
  64 | ||| Names are taken from the [toml spec](https://toml.io/en/v1.0.0#string)
  65 | public export
  66 | data StringType : Type where
  67 |     ||| Double quoted, single-line string
  68 |     ||| Supports escaping
  69 |     ||| "hello \n world"
  70 |     Basic : StringType
  71 |     ||| Single quoted, singe-line string
  72 |     ||| Does not support escaping
  73 |     ||| 'hello \n world'
  74 |     Literal : StringType
  75 |     -- TODO: the following
  76 |     ||| Double quoted, multi-line string
  77 |     ||| Supports escaping and line folding
  78 |     BasicMultiline : StringType
  79 |     ||| Single quoted, multi-line string
  80 |     ||| Does not support escaping or line folding
  81 |     LiteralMultiline : StringType
  82 | 
  83 | export
  84 | Show StringType where
  85 |     show Basic = "Basic"
  86 |     show Literal = "Literal"
  87 |     show BasicMultiline = "BasicMultiline"
  88 |     show LiteralMultiline = "LiteralMultiline"
  89 | 
  90 | export
  91 | Eq StringType where
  92 |     Basic == Basic = True
  93 |     Literal == Literal = True
  94 |     BasicMultiline == BasicMultiline = True
  95 |     LiteralMultiline == LiteralMultiline = True
  96 |     _ == _ = False
  97 | 
  98 | 
  99 | public export
 100 | data TOMLTokenKind
 101 |     = TTBoolean
 102 |     | TTInt
 103 |     | TTFloat
 104 |     | TTString StringType
 105 |     | TTPunct Punctuation
 106 |     | TTBare
 107 |     | TTIgnored
 108 | 
 109 | public export
 110 | TOMLToken : Type
 111 | TOMLToken = Token TOMLTokenKind
 112 | 
 113 | export
 114 | Show TOMLTokenKind where
 115 |     show TTBoolean = "boolean"
 116 |     show TTInt = "integer"
 117 |     show TTFloat = "float"
 118 |     show (TTString type) = "\{show type} string"
 119 |     show (TTPunct x) = show x
 120 |     show TTBare = "key"
 121 |     show TTIgnored = "comment"
 122 | 
 123 | public export
 124 | Eq TOMLTokenKind where
 125 |     (==) TTBoolean TTBoolean = True
 126 |     (==) TTInt TTInt = True
 127 |     (==) TTFloat TTFloat = True
 128 |     (==) (TTString x) (TTString y) = x == y
 129 |     (==) (TTPunct x) (TTPunct y) = x == y
 130 |     (==) TTBare TTBare = True
 131 |     (==) TTIgnored TTIgnored = True
 132 |     (==) _ _ = False
 133 | 
 134 | charToInt : Char -> Integer
 135 | charToInt c =
 136 |     if '0' <= c && c <= '9'
 137 |         then cast $ ord c - ord '0'
 138 |         else cast $ ord (toLower c) - ord 'a'
 139 | 
 140 | parameters (sign, base : Integer)
 141 |     private
 142 |     parseIntLoop :
 143 |         List Char ->
 144 |         (acc : Integer) ->
 145 |         Integer
 146 |     parseIntLoop [] acc = acc
 147 |     parseIntLoop ('_'::rest) acc = parseIntLoop rest acc
 148 |     parseIntLoop (c::rest) acc =
 149 |         parseIntLoop rest (acc * base + charToInt c * sign)
 150 | 
 151 | private
 152 | parseWithSign : List Char -> (sign : Integer) -> Integer
 153 | parseWithSign [] sign = 0
 154 | parseWithSign ('0'::'b'::rest) sign = parseIntLoop sign 2 rest 0
 155 | parseWithSign ('0'::'o'::rest) sign = parseIntLoop sign 8 rest 0
 156 | parseWithSign ('0'::'x'::rest) sign = parseIntLoop sign 16 rest 0
 157 | parseWithSign rest sign = parseIntLoop sign 10 rest 0
 158 | 
 159 | private
 160 | parseInt : List Char -> Integer
 161 | parseInt [] = 0
 162 | parseInt ('+'::rest) = parseWithSign rest 1
 163 | parseInt ('-'::rest) = parseWithSign rest (-1)
 164 | parseInt rest = parseWithSign rest 1
 165 | 
 166 | nan : Double
 167 | nan = sqrt (-1)
 168 | 
 169 | inf : Double
 170 | inf = 1.0 / 0.0
 171 | 
 172 | namespace Float
 173 |     parameters (sign : Double)
 174 |         ||| parse the exponent part of a double
 175 |         ||| not including the e
 176 |         parseExponent :
 177 |             (number : Double) ->
 178 |             (acc : Integer) ->
 179 |             List Char ->
 180 |             Double
 181 |         parseExponent number acc [] = sign * number * pow 10 (cast acc)
 182 |         parseExponent number acc ('_'::rest) = parseExponent number acc rest
 183 |         parseExponent number acc (x::rest) = parseExponent number (10 * acc + charToInt x) rest
 184 | 
 185 |         ||| parse the decimal part of a double
 186 |         ||| not including the .
 187 |         ||| up to and including the e
 188 |         parseDecimal :
 189 |             (whole : Integer) ->
 190 |             (acc : Double) ->
 191 |             (exponent : Double) ->
 192 |             List Char ->
 193 |             Double
 194 |         parseDecimal whole acc exponent [] = sign * (cast whole + acc)
 195 |         parseDecimal whole acc exponent ('e'::rest) = parseExponent (cast whole + acc) 0 rest
 196 |         parseDecimal whole acc exponent ('E'::rest) = parseExponent (cast whole + acc) 0 rest
 197 |         parseDecimal whole acc exponent ('_'::rest) = parseDecimal whole acc exponent rest
 198 |         parseDecimal whole acc exponent (x::rest) =
 199 |             parseDecimal
 200 |                 whole
 201 |                 (acc + cast (charToInt x) * exponent)
 202 |                 (exponent * 0.1)
 203 |                 rest
 204 | 
 205 |         ||| parse the part of the double before the `.`
 206 |         parseWhole : (acc : Integer) -> List Char -> Double
 207 |         parseWhole acc [] = 0.0
 208 |         parseWhole acc ('.'::rest) = parseDecimal acc 0.0 0.1 rest
 209 |         parseWhole acc ('e'::rest) = parseExponent (cast acc) 0 rest
 210 |         parseWhole acc ('E'::rest) = parseExponent (cast acc) 0 rest
 211 |         parseWhole acc ('_'::rest) = parseWhole acc rest
 212 |         parseWhole acc (x::rest) = parseWhole (10 * acc + charToInt x) rest
 213 | 
 214 |     parseSign : List Char -> Double
 215 |     parseSign ('+'::rest) = parseWhole 1.0 0 rest
 216 |     parseSign ('-'::rest) = parseWhole (-1.0) 0 rest
 217 |     parseSign rest = parseWhole 1.0 0 rest
 218 | 
 219 |     export
 220 |     parseFloat : String -> Double
 221 |     parseFloat "nan" = nan
 222 |     parseFloat "+nan" = nan
 223 |     parseFloat "-nan" = -nan
 224 |     parseFloat "inf" = inf
 225 |     parseFloat "+inf" = inf
 226 |     parseFloat "-inf" = -inf
 227 |     parseFloat x = parseSign (unpack x)
 228 | 
 229 | private
 230 | unescapeBasic : List Char -> Either String (List Char)
 231 | unescapeBasic ('"'::rest) = loop rest
 232 |     where
 233 |         -- hex digit to int
 234 |         hexToInt : Char -> Either String Int
 235 |         hexToInt c =
 236 |             if isHexDigit c
 237 |                 then Right $
 238 |                     if '0' <= c && c <= '9'
 239 |                         then ord c - ord '0'
 240 |                         else ord (toLower c) - ord 'a'
 241 |                 else Left "invalid hex character: '\{cast {to=String} c}'"
 242 | 
 243 |         unicodeEscape : List Char -> (acc : Int) -> Either String Char
 244 |         unicodeEscape [] acc = pure $ chr acc
 245 |         unicodeEscape (c::cs) acc = do
 246 |             x <- hexToInt c
 247 |             unicodeEscape cs (acc * 16 + x)
 248 | 
 249 |         loop : List Char -> Either String (List Char)
 250 |         loop [] = Left "unexpected end of input"
 251 |         loop ('"'::_) = Right []
 252 |         loop ('\\'::'b'::rest) = ('\b' ::) <$> loop rest
 253 |         loop ('\\'::'t'::rest) = ('\t' ::) <$> loop rest
 254 |         loop ('\\'::'n'::rest) = ('\n' ::) <$> loop rest
 255 |         loop ('\\'::'f'::rest) = ('\f' ::) <$> loop rest
 256 |         loop ('\\'::'r'::rest) = ('\r' ::) <$> loop rest
 257 |         loop ('\\'::'"'::rest) = ('"' ::) <$> loop rest
 258 |         loop ('\\'::'\\'::rest) = ('\\' ::) <$> loop rest
 259 |         loop ('\\'::'u'::u0::u1::u2::u3::rest) = do
 260 |             c <- unicodeEscape [u0, u1, u2, u3] 0
 261 |             (c ::) <$> loop rest
 262 |         loop ('\\'::'U'::u0::u1::u2::u3::u4::u5::u6::u7::rest) = do
 263 |             c <- unicodeEscape [u0, u1, u2, u3, u4, u5, u6, u7] 0
 264 |             (c ::) <$> loop rest
 265 |         loop ('\\'::_) = Left "invalid escape code"
 266 |         loop (x::rest) = (x ::) <$> loop rest
 267 | unescapeBasic _ = Left "expected quote"
 268 | 
 269 | public export
 270 | TokenKind TOMLTokenKind where
 271 |     TokType TTBoolean = Bool
 272 |     TokType TTInt = Integer
 273 |     TokType TTFloat = Double
 274 |     -- a string accepted by the lexer isn't necessarily
 275 |     -- a valid toml string
 276 |     TokType (TTString _) = Either String String
 277 |     TokType (TTPunct _) = ()
 278 |     TokType TTBare = String
 279 |     TokType TTIgnored = ()
 280 | 
 281 |     tokValue TTBoolean s = s == strTrue
 282 |     tokValue TTInt s = parseInt (unpack s)
 283 |     tokValue TTFloat s = parseFloat s
 284 | 
 285 |     tokValue (TTString Basic) s = map pack $ unescapeBasic (unpack s)
 286 |     tokValue (TTString Literal) s = Left "unimplemted string type: literal"
 287 |     tokValue (TTString BasicMultiline) s = Left "unimplemted string type: basic multiline"
 288 |     tokValue (TTString LiteralMultiline) s = Left "unimplemted string type: literal multiline"
 289 | 
 290 |     tokValue (TTPunct _) _ = ()
 291 |     tokValue TTBare s = s
 292 |     tokValue TTIgnored _ = ()
 293 | 
 294 | export
 295 | getString : Token TOMLTokenKind -> Maybe (Either String String)
 296 | getString tok@(Tok ((TTString _)) text) = Just (value tok)
 297 | getString _ = Nothing
 298 | 
 299 | export
 300 | getKeyString : Token TOMLTokenKind -> Maybe (Either String String)
 301 | getKeyString tok@(Tok ((TTString Basic)) text) = Just (value tok)
 302 | getKeyString tok@(Tok ((TTString Literal)) text) = Just (value tok)
 303 | getKeyString _ = Nothing
 304 | 
 305 | export
 306 | ignored : WithBounds TOMLToken -> Bool
 307 | ignored (MkBounded (Tok TTIgnored _) _ _) = True
 308 | ignored _ = False