
   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 | export %inline
 101 | Cast a e => Cast a (InnerError e) where
 102 |   cast = Custom . cast
 103 | 
 104 | ||| Convenience alias for `Bounded . InnerError`
 105 | public export
 106 | 0 BoundedErr : Type -> Type
 107 | BoundedErr = Bounded . InnerError
 108 | 
 109 | public export
 110 | Functor InnerError where
 111 |   map f (Custom err)        = Custom $ f err
 112 |   map f EOI                 = EOI
 113 |   map f (Expected xs x)     = Expected xs x
 114 |   map f (ExpectedChar x)    = ExpectedChar x
 115 |   map f ExpectedEOI         = ExpectedEOI
 116 |   map f (InvalidControl c1) = InvalidControl c1
 117 |   map f InvalidEscape       = InvalidEscape
 118 |   map f (OutOfBounds x)     = OutOfBounds x
 119 |   map f (Unclosed x)        = Unclosed x
 120 |   map f (Unknown x)         = Unknown x
 121 |   map f (InvalidByte x)     = InvalidByte x
 122 | 
 123 | uncontrol : Char -> String
 124 | uncontrol c = if isControl c then adj (unpack $ show c) else singleton c
 125 |   where
 126 |     adj : List Char -> String
 127 |     adj = pack . filter ('\'' /=)
 128 | 
 129 | quote : String -> String
 130 | quote s =
 131 |   case map uncontrol (unpack s) of
 132 |     [c] => "'\{c}'"
 133 |     cs  => "\"\{concat cs}\""
 134 | 
 135 | quotes : String -> List String -> String
 136 | quotes x []  = quote x
 137 | quotes x [y] = "\{quote x} or \{quote y}"
 138 | quotes x xs  = go x xs
 139 |   where
 140 |     go : String -> List String -> String
 141 |     go s []        = "or \{quote s}"
 142 |     go s (y :: ys) = "\{quote s}, " ++ go y ys
 143 | 
 144 | ||| Converts a value in the range `[0..15]` to a hexadecimal
 145 | ||| lower-case character.
 146 | |||
 147 | ||| For simplicity, this function assumes the range has been checked.
 148 | ||| Therefore, values `>= 15` will return `'f'`.
 149 | public export
 150 | hexChar : Bits8 -> Char
 151 | hexChar 0  = '0'
 152 | hexChar 1  = '1'
 153 | hexChar 2  = '2'
 154 | hexChar 3  = '3'
 155 | hexChar 4  = '4'
 156 | hexChar 5  = '5'
 157 | hexChar 6  = '6'
 158 | hexChar 7  = '7'
 159 | hexChar 8  = '8'
 160 | hexChar 9  = '9'
 161 | hexChar 10 = 'a'
 162 | hexChar 11 = 'b'
 163 | hexChar 12 = 'c'
 164 | hexChar 13 = 'd'
 165 | hexChar 14 = 'e'
 166 | hexChar _  = 'f'
 167 | 
 168 | ||| Pretty prints a byte as two hexadecimal digits.
 169 | |||
 170 | ||| Example: `toHex 110 === "6e"`.
 171 | export
 172 | toHex : Bits8 -> String
 173 | toHex x = pack [hexChar (shiftR x 4), hexChar (x .&. 15)]
 174 | 
 175 | export
 176 | Interpolation e => Interpolation (InnerError e) where
 177 |   interpolate EOI                  = "Unexpected end of input"
 178 |   interpolate (Expected [] x)      = "Unexpected \{quote x}"
 179 |   interpolate (Expected (s::ss) x) = "Expected \{quotes s ss}, but got \{quote x}"
 180 |   interpolate (ExpectedChar x)     = "Expected \{x}"
 181 |   interpolate ExpectedEOI          = "Expected end of input"
 182 |   interpolate (InvalidControl c)   = "Invalid control character: '\{uncontrol c}'"
 183 |   interpolate InvalidEscape        = "Invalid escape sequence"
 184 |   interpolate (OutOfBounds x)      = "Value out of bounds: \{x}"
 185 |   interpolate (Unclosed x)         = "Unclosed \{quote x}"
 186 |   interpolate (Unknown x)          = "Unknown or invalid token: \{x}"
 187 |   interpolate (Custom err)         = interpolate err
 188 |   interpolate (InvalidByte x)      = "Unexpected or invalid byte: 0x\{toHex x}"
 189 | 
 190 | --------------------------------------------------------------------------------
 191 | --          Interface
 192 | --------------------------------------------------------------------------------
 193 | 
 194 | public export
 195 | interface FailParse (0 m : Type -> Type) (0 e : Type) | m where
 196 |   parseFail : Bounds -> InnerError e -> m a
 197 | 
 198 | public export %inline
 199 | FailParse (Either $ Bounded $ InnerError e) e where
 200 |   parseFail b err = Left (B err b)
 201 | 
 202 | public export %inline
 203 | custom : FailParse m e => Bounds -> e -> m a
 204 | custom b = parseFail b . Custom
 205 | 
 206 | public export %inline
 207 | expected : Interpolation t => FailParse m e => Bounds -> t -> String -> m a
 208 | expected b v s = parseFail b $ Expected [interpolate v] s
 209 | 
 210 | public export %inline
 211 | unclosed : Interpolation t => FailParse m e => Bounds -> t -> m a
 212 | unclosed b = parseFail b . Unclosed . interpolate
 213 | 
 214 | public export %inline
 215 | unexpected : Interpolation t => FailParse m e => Bounded t -> m a
 216 | unexpected v = parseFail v.bounds (Expected [] . interpolate $ v.val)
 217 | 
 218 | public export %inline
 219 | eoi : FailParse m e => m a
 220 | eoi = parseFail NoBounds EOI
 221 | 
 222 | public export %inline
 223 | expectedEOI : FailParse m e => Bounds -> m a
 224 | expectedEOI b = parseFail b ExpectedEOI
 225 | 
 226 | --------------------------------------------------------------------------------
 227 | --          Identities
 228 | --------------------------------------------------------------------------------
 229 | 
 230 | public export
 231 | fromVoid : InnerError Void -> InnerError e
 232 | fromVoid EOI                = EOI
 233 | fromVoid (Expected xs x)    = Expected xs x
 234 | fromVoid (ExpectedChar x)   = ExpectedChar x
 235 | fromVoid ExpectedEOI        = ExpectedEOI
 236 | fromVoid (InvalidControl c) = InvalidControl c
 237 | fromVoid InvalidEscape      = InvalidEscape
 238 | fromVoid (OutOfBounds x)    = OutOfBounds x
 239 | fromVoid (Unclosed x)       = Unclosed x
 240 | fromVoid (Unknown x)        = Unknown x
 241 | fromVoid (InvalidByte b)    = InvalidByte b
 242 | 
 243 | --------------------------------------------------------------------------------
 244 | --          ParseError
 245 | --------------------------------------------------------------------------------
 246 | 
 247 | ||| Pairs a parsing error with a text's origin, the error's bound, and
 248 | ||| the text itself.
 249 | public export
 250 | record FCErr e where
 251 |   constructor PE
 252 |   ||| Origin of the byte sequence that was parsed.
 253 |   origin    : Origin
 254 | 
 255 |   ||| Absolute bounds where the error occurred.
 256 |   bounds    : Bounds
 257 | 
 258 |   ||| Bounds where the error occurred relative to the string stored
 259 |   ||| in `content`. See also the docs of `Text.ILex.FC.printFC` for an
 260 |   ||| explanation why the distinction between relative and absolute bounds
 261 |   ||| is necessary.
 262 |   relBounds : Bounds
 263 | 
 264 |   ||| Relevant part of the text that was parsed.
 265 |   content   : Maybe String
 266 | 
 267 |   ||| The actual error that occurred.
 268 |   error     : e
 269 | 
 270 | %runElab derive "FCErr" [Show,Eq]
 271 | 
 272 | public export
 273 | 0 ParseError : (e : Type) -> Type
 274 | ParseError e = FCErr (InnerError e)
 275 | 
 276 | ||| Converts a bounded error to a `ParseError` by pairing it with
 277 | ||| an origin and the parsed string.
 278 | export
 279 | toParseError : Origin -> String -> Bounded e -> FCErr e
 280 | toParseError o s (B err bs) = PE o bs bs (Just s) err
 281 | 
 282 | export
 283 | Interpolation e => Interpolation (FCErr e) where
 284 |   interpolate (PE origin bounds relbs cont err) =
 285 |     let fc := FC origin bounds
 286 |      in case cont of
 287 |           Just c  => unlines $ "\{err}" :: printFC fc relbs (lines c)
 288 |           Nothing => unlines ["\{err}", interpolate fc]
 289 | 
 290 | export %inline
 291 | leftErr : Origin -> String -> Either (Bounded e) a -> Either (FCErr e) a
 292 | leftErr o = mapFst . toParseError o
 293 |