
   0 | module Text.ParseError
   1 | 
   2 | import Data.Bits
   3 | import Derive.Prelude
   4 | import Text.Bounds
   5 | import Text.FC
   6 | 
   7 | %default total
   8 | %language ElabReflection
   9 | 
  10 | public export
  11 | data DigitType : Type where
  12 |   Bin : DigitType
  13 |   Oct : DigitType
  14 |   Dec : DigitType
  15 |   Hex : DigitType
  16 | 
  17 | %runElab derive "DigitType" [Show,Eq,Ord]
  18 | 
  19 | export
  20 | Interpolation DigitType where
  21 |   interpolate Bin = "a binary digit ('0' or '1')"
  22 |   interpolate Oct = "an octal digit ('0' to '7')"
  23 |   interpolate Dec = "a decimal digit ('0' to '9')"
  24 |   interpolate Hex = "a hexadecimal digit ('0' to '9' or 'a' to 'f')"
  25 | 
  26 | public export
  27 | data CharClass : Type where
  28 |   ||| A whitespace character
  29 |   Space : CharClass
  30 | 
  31 |   ||| A digit
  32 |   Digit : DigitType -> CharClass
  33 | 
  34 |   ||| An upper-case letter
  35 |   Upper : CharClass
  36 | 
  37 |   ||| A lower-case letter
  38 |   Lower : CharClass
  39 | 
  40 |   ||| An upper- or lower-case letter
  41 |   Alpha : CharClass
  42 | 
  43 |   ||| An upper- or lower-case letter or a decimal digit
  44 |   AlphaNum : CharClass
  45 | 
  46 | %runElab derive "CharClass" [Show,Eq,Ord]
  47 | 
  48 | export
  49 | Interpolation CharClass where
  50 |   interpolate Space     = "a space character"
  51 |   interpolate (Digit x) = interpolate x
  52 |   interpolate Upper     = "an upper-case letter"
  53 |   interpolate Lower     = "a lower-case letter"
  54 |   interpolate Alpha     = "a letter ('a' to 'z' or 'A' to 'Z')"
  55 |   interpolate AlphaNum  = "a letter or a digit"
  56 | 
  57 | --------------------------------------------------------------------------------
  58 | --          Parse Errors
  59 | --------------------------------------------------------------------------------
  60 | 
  61 | public export
  62 | data InnerError : (err : Type) -> Type where
  63 |   ||| A custom error for the current parsing topic
  64 |   Custom         : (err : e) -> InnerError e
  65 | 
  66 |   ||| Unexpected end of input
  67 |   EOI            : InnerError e
  68 | 
  69 |   ||| Expected one of the given tokens but got something else.
  70 |   Expected       : List String -> String -> InnerError e
  71 | 
  72 |   ||| Expected the given type of character
  73 |   ExpectedChar   : CharClass -> InnerError e
  74 | 
  75 |   ||| Got more input that we expected
  76 |   ExpectedEOI    : InnerError e
  77 | 
  78 |   ||| Got an invalid control character
  79 |   InvalidControl : Char -> InnerError e
  80 | 
  81 |   ||| Got an invalid character escape sequence
  82 |   InvalidEscape  : InnerError e
  83 | 
  84 |   ||| Got a (usually numeric) value that was out of bounds
  85 |   OutOfBounds    : String -> InnerError e
  86 | 
  87 |   ||| An unclosed opening token
  88 |   Unclosed       : String -> InnerError e
  89 | 
  90 |   ||| Got an unknown or invalid token
  91 |   Unknown        : String -> InnerError e
  92 | 
  93 |   ||| An unexpected non-ascii byte, either from an unexpected
  94 |   ||| mutli-byte codepoint or from altogether invalid unicode
  95 |   ||| input.
  96 |   InvalidByte    : Bits8 -> InnerError e
  97 | 
  98 | %runElab derive "InnerError" [Show,Eq]
  99 | 
 100 | ||| Convenience alias for `Bounded . InnerError`
 101 | public export
 102 | 0 BoundedErr : Type -> Type
 103 | BoundedErr = Bounded . InnerError
 104 | 
 105 | public export
 106 | Functor InnerError where
 107 |   map f (Custom err)        = Custom $ f err
 108 |   map f EOI                 = EOI
 109 |   map f (Expected xs x)     = Expected xs x
 110 |   map f (ExpectedChar x)    = ExpectedChar x
 111 |   map f ExpectedEOI         = ExpectedEOI
 112 |   map f (InvalidControl c1) = InvalidControl c1
 113 |   map f InvalidEscape       = InvalidEscape
 114 |   map f (OutOfBounds x)     = OutOfBounds x
 115 |   map f (Unclosed x)        = Unclosed x
 116 |   map f (Unknown x)         = Unknown x
 117 |   map f (InvalidByte x)     = InvalidByte x
 118 | 
 119 | uncontrol : Char -> String
 120 | uncontrol c = if isControl c then adj (unpack $ show c) else singleton c
 121 |   where
 122 |     adj : List Char -> String
 123 |     adj = pack . filter ('\'' /=)
 124 | 
 125 | quote : String -> String
 126 | quote s =
 127 |   case map uncontrol (unpack s) of
 128 |     [c] => "'\{c}'"
 129 |     cs  => "\"\{concat cs}\""
 130 | 
 131 | quotes : String -> List String -> String
 132 | quotes x []  = quote x
 133 | quotes x [y] = "\{quote x} or \{quote y}"
 134 | quotes x xs  = go x xs
 135 |   where
 136 |     go : String -> List String -> String
 137 |     go s []        = "or \{quote s}"
 138 |     go s (y :: ys) = "\{quote s}, " ++ go y ys
 139 | 
 140 | ||| Converts a value in the range `[0..15]` to a hexadecimal
 141 | ||| lower-case character.
 142 | |||
 143 | ||| For simplicity, this function assumes the range has been checked.
 144 | ||| Therefore, values `>= 15` will return `'f'`.
 145 | public export
 146 | hexChar : Bits8 -> Char
 147 | hexChar 0  = '0'
 148 | hexChar 1  = '1'
 149 | hexChar 2  = '2'
 150 | hexChar 3  = '3'
 151 | hexChar 4  = '4'
 152 | hexChar 5  = '5'
 153 | hexChar 6  = '6'
 154 | hexChar 7  = '7'
 155 | hexChar 8  = '8'
 156 | hexChar 9  = '9'
 157 | hexChar 10 = 'a'
 158 | hexChar 11 = 'b'
 159 | hexChar 12 = 'c'
 160 | hexChar 13 = 'd'
 161 | hexChar 14 = 'e'
 162 | hexChar _  = 'f'
 163 | 
 164 | ||| Pretty prints a byte as two hexadecimal digits.
 165 | |||
 166 | ||| Example: `toHex 110 === "6e"`.
 167 | export
 168 | toHex : Bits8 -> String
 169 | toHex x = pack [hexChar (shiftR x 4), hexChar (x .&. 15)]
 170 | 
 171 | export
 172 | Interpolation e => Interpolation (InnerError e) where
 173 |   interpolate EOI                  = "Unexpected end of input"
 174 |   interpolate (Expected [] x)      = "Unexpected \{quote x}"
 175 |   interpolate (Expected (s::ss) x) = "Expected \{quotes s ss}, but got \{quote x}"
 176 |   interpolate (ExpectedChar x)     = "Expected \{x}"
 177 |   interpolate ExpectedEOI          = "Expected end of input"
 178 |   interpolate (InvalidControl c)   = "Invalid control character: '\{uncontrol c}'"
 179 |   interpolate InvalidEscape        = "Invalid escape sequence"
 180 |   interpolate (OutOfBounds x)      = "Value out of bounds: \{x}"
 181 |   interpolate (Unclosed x)         = "Unclosed \{quote x}"
 182 |   interpolate (Unknown x)          = "Unknown or invalid token: \{x}"
 183 |   interpolate (Custom err)         = interpolate err
 184 |   interpolate (InvalidByte x)      = "Unexpected or invalid byte: 0x\{toHex x}"
 185 | 
 186 | --------------------------------------------------------------------------------
 187 | --          Interface
 188 | --------------------------------------------------------------------------------
 189 | 
 190 | public export
 191 | interface FailParse (0 m : Type -> Type) (0 e : Type) | m where
 192 |   parseFail : Bounds -> InnerError e -> m a
 193 | 
 194 | public export %inline
 195 | FailParse (Either $ Bounded $ InnerError e) e where
 196 |   parseFail b err = Left (B err b)
 197 | 
 198 | public export %inline
 199 | custom : FailParse m e => Bounds -> e -> m a
 200 | custom b = parseFail b . Custom
 201 | 
 202 | public export %inline
 203 | expected : Interpolation t => FailParse m e => Bounds -> t -> String -> m a
 204 | expected b v s = parseFail b $ Expected [interpolate v] s
 205 | 
 206 | public export %inline
 207 | unclosed : Interpolation t => FailParse m e => Bounds -> t -> m a
 208 | unclosed b = parseFail b . Unclosed . interpolate
 209 | 
 210 | public export %inline
 211 | unexpected : Interpolation t => FailParse m e => Bounded t -> m a
 212 | unexpected v = parseFail v.bounds (Expected [] . interpolate $ v.val)
 213 | 
 214 | public export %inline
 215 | eoi : FailParse m e => m a
 216 | eoi = parseFail NoBounds EOI
 217 | 
 218 | public export %inline
 219 | expectedEOI : FailParse m e => Bounds -> m a
 220 | expectedEOI b = parseFail b ExpectedEOI
 221 | 
 222 | --------------------------------------------------------------------------------
 223 | --          Identities
 224 | --------------------------------------------------------------------------------
 225 | 
 226 | public export
 227 | fromVoid : InnerError Void -> InnerError e
 228 | fromVoid EOI                = EOI
 229 | fromVoid (Expected xs x)    = Expected xs x
 230 | fromVoid (ExpectedChar x)   = ExpectedChar x
 231 | fromVoid ExpectedEOI        = ExpectedEOI
 232 | fromVoid (InvalidControl c) = InvalidControl c
 233 | fromVoid InvalidEscape      = InvalidEscape
 234 | fromVoid (OutOfBounds x)    = OutOfBounds x
 235 | fromVoid (Unclosed x)       = Unclosed x
 236 | fromVoid (Unknown x)        = Unknown x
 237 | fromVoid (InvalidByte b)    = InvalidByte b
 238 | 
 239 | --------------------------------------------------------------------------------
 240 | --          ParseError
 241 | --------------------------------------------------------------------------------
 242 | 
 243 | ||| Pairs a parsing error with a text's origin, the error's bound, and
 244 | ||| the text itself.
 245 | public export
 246 | record ParseError e where
 247 |   constructor PE
 248 |   ||| Origin of the byte sequence that was parsed.
 249 |   origin    : Origin
 250 | 
 251 |   ||| Absolute bounds where the error occurred.
 252 |   bounds    : Bounds
 253 | 
 254 |   ||| Bounds where the error occurred relative to the string stored
 255 |   ||| in `content`. See also the docs of `Text.ILex.FC.printFC` for an
 256 |   ||| explanation why the distinction between relative and absolute bounds
 257 |   ||| is necessary.
 258 |   relBounds : Bounds
 259 | 
 260 |   ||| Relevant part of the text that was parsed.
 261 |   content   : Maybe String
 262 | 
 263 |   ||| The actual error that occurred.
 264 |   error     : InnerError e
 265 | 
 266 | %runElab derive "ParseError" [Show,Eq]
 267 | 
 268 | ||| Converts a bounded error to a `ParseError` by pairing it with
 269 | ||| an origin and the parsed string.
 270 | export
 271 | toParseError : Origin -> String -> Bounded (InnerError e) -> ParseError e
 272 | toParseError o s (B err bs) = PE o bs bs (Just s) err
 273 | 
 274 | export
 275 | Interpolation e => Interpolation (ParseError e) where
 276 |   interpolate (PE origin bounds relbs cont err) =
 277 |     let fc := FC origin bounds
 278 |      in case cont of
 279 |           Just c  => unlines $ "Error: \{err}" :: printFC fc relbs (lines c)
 280 |           Nothing => unlines ["Error: \{err}", interpolate fc]
 281 | 
 282 | export %inline
 283 | leftErr :
 284 |      Origin
 285 |   -> String
 286 |   -> Either (Bounded (InnerError e)) a
 287 |   -> Either (ParseError e) a
 288 | leftErr o = mapFst . toParseError o
 289 |