
   0 | module Data.List.Suffix.Result0
   1 | 
   2 | import Derive.Prelude
   3 | import Data.Nat
   4 | import Data.List.Suffix
   5 | import Text.Bounds
   6 | import Text.FC
   7 | import Text.ParseError
   8 | 
   9 | %default total
  10 | %language ElabReflection
  11 | 
  12 | ||| Result of consuming and converting a (possibly strict) prefix
  13 | ||| of a list of tokens.
  14 | |||
  15 | ||| This comes with an erased proof about the number of tokens
  16 | ||| consumed. Consider using `Data.List.Suffix.Result` if you need
  17 | ||| to keep track of the number of tokens consumed at runtime.
  18 | |||
  19 | ||| Use this for manually writing high-performance parsers, which
  20 | ||| (in the case of strict results) are guaranteed to terminate.
  21 | ||| See module `Text.Parse.Manual` for
  22 | ||| utilities for consuming and converting prefixes
  23 | ||| of tokens, but for a nicer interface, consider using `Text.Parse.Core`
  24 | ||| (at the cost of a drop in performance).
  25 | |||
  26 | ||| @ strict : True if a strict prefix of the list of tokens has
  27 | |||            been consumed.
  28 | ||| @ t      : the type of token consumed.
  29 | ||| @ ts     : the original list of tokens
  30 | ||| @ e      : the error type in case of a failure
  31 | ||| @ a      : the result type
  32 | public export
  33 | data Result0 :
  34 |      (strict : Bool)
  35 |   -> (t : Type)
  36 |   -> List t
  37 |   -> (e,a : Type)
  38 |   -> Type where
  39 | 
  40 |   Succ0 :
  41 |        {0 b : Bool}
  42 |     -> {0 t,e,a : Type}
  43 |     -> {0 ts : List t}
  44 |     -> (val : a)
  45 |     -> (xs : List t)
  46 |     -> {auto 0 p : Suffix b xs ts}
  47 |     -> Result0 b t ts e a
  48 | 
  49 |   Fail0 :
  50 |        {0 b : Bool}
  51 |     -> {0 t,e,a : Type}
  52 |     -> {0 ts : List t}
  53 |     -> (err : e)
  54 |     -> Result0 b t ts e a
  55 | 
  56 | ||| Alias for `Succ`, which takes the proof as an
  57 | ||| explicit argument
  58 | public export %inline
  59 | succ : 
  60 |        {0 b : Bool}
  61 |     -> {0 t,e,a : Type}
  62 |     -> {0 ts : List t}
  63 |     -> (val : a)
  64 |     -> {xs : List t}
  65 |     -> (0 p : Suffix b xs ts)
  66 |     -> Result0 b t ts e a
  67 | succ val _ = Succ0 val xs
  68 | 
  69 | public export
  70 | Functor (Result0 b t ts e) where
  71 |   map f (Succ0 v xs) = Succ0 (f v) xs
  72 |   map _ (Fail0 err)  = Fail0 err
  73 | 
  74 | public export %inline
  75 | fromEither :
  76 |      {0 ts : List t}
  77 |   -> (xs : List t)
  78 |   -> {auto 0 p : Suffix b xs ts}
  79 |   -> Either e a
  80 |   -> Result0 b t ts e a
  81 | fromEither xs (Left x)  = Fail0 x
  82 | fromEither xs (Right x) = Succ0 x xs
  83 | 
  84 | --------------------------------------------------------------------------------
  85 | --          Conversions
  86 | --------------------------------------------------------------------------------
  87 | 
  88 | public export %inline
  89 | swapOr : {0 x,y : _} -> Result0 (x || y) t ts e a -> Result0 (y || x) t ts e a
  90 | swapOr = swapOr (\k => Result0 k t ts e a)
  91 | 
  92 | public export %inline
  93 | orSame : {0 x : _} -> Result0 (x || x) t ts e a -> Result0 x t ts e a
  94 | orSame = orSame (\k => Result0 k t ts e a)
  95 | 
  96 | public export %inline
  97 | orTrue : {0 x : _} -> Result0 (x || True) t ts e a -> Result0 True t ts e a
  98 | orTrue = orTrue (\k => Result0 k t ts e a)
  99 | 
 100 | public export %inline
 101 | orFalse : {0 x : _} -> Result0 (x || False) t ts e a -> Result0 x t ts e a
 102 | orFalse = orFalse (\k => Result0 k t ts e a)
 103 | 
 104 | public export %inline
 105 | swapAnd : {0 x,y : _} -> Result0 (x && y) t ts e a -> Result0 (y && x) t ts e a
 106 | swapAnd = swapAnd (\k => Result0 k t ts e a)
 107 | 
 108 | public export %inline
 109 | andSame : {0 x : _} -> Result0 (x && x) t ts e a -> Result0 x t ts e a
 110 | andSame = andSame (\k => Result0 k t ts e a)
 111 | 
 112 | public export %inline
 113 | andTrue : {0 x : _} -> Result0 (x && True) t ts e a -> Result0 x t ts e a
 114 | andTrue = andTrue (\k => Result0 k t ts e a)
 115 | 
 116 | public export %inline
 117 | andFalse : {0 x : _} -> Result0 (x && False) t ts e a -> Result0 False t ts e a
 118 | andFalse = andFalse (\k => Result0 k t ts e a)
 119 | 
 120 | public export %inline
 121 | weaken : {0 x : _} -> Result0 x t ts e a -> Result0 False t ts e a
 122 | weaken (Succ0 val xs @{p}) = Succ0 val xs @{weaken p}
 123 | weaken (Fail0 err)         = Fail0 err
 124 | 
 125 | public export %inline
 126 | weakens : {0 x : _} -> Result0 True t ts e a -> Result0 x t ts e a
 127 | weakens (Succ0 val xs @{p}) = Succ0 val xs @{weakens p}
 128 | weakens (Fail0 err)         = Fail0 err
 129 | 
 130 | public export %inline
 131 | and1 : {0 x : _} -> Result0 x t ts e a -> Result0 (x && y) t ts e a
 132 | and1 (Succ0 val xs @{p}) = Succ0 val xs @{and1 p}
 133 | and1 (Fail0 err)         = Fail0 err
 134 | 
 135 | public export %inline
 136 | and2 : {0 x : _} -> Result0 x t ts e a -> Result0 (y && x) t ts e a
 137 | and2 r = swapAnd $ and1 r
 138 | 
 139 | public export %inline
 140 | trans :
 141 |      Result0 b1 t xs e a
 142 |   -> (0 _ : Suffix b2 xs ys)
 143 |   -> Result0 (b1 || b2) t ys e a
 144 | trans (Succ0 val ts @{p}) q = Succ0 val ts @{trans p q}
 145 | trans (Fail0 err)         _ = Fail0 err
 146 | 
 147 | public export %inline
 148 | succT :
 149 |       Result0 b1 t xs e a
 150 |   -> {auto 0 p : Suffix True xs ys}
 151 |   -> Result0 True t ys e a
 152 | succT r = swapOr $ trans r p
 153 | 
 154 | public export %inline
 155 | succF :
 156 |       Result0 b1 t xs e a
 157 |   -> {auto 0 p : Suffix True xs ys}
 158 |   -> Result0 False t ys e a
 159 | succF r = weaken $ trans r p
 160 | 
 161 | --------------------------------------------------------------------------------
 162 | --          Combinators
 163 | -----------------------------------------------------------------------------
 164 | 
 165 | public export
 166 | (<|>) :
 167 |      Result0 b1 t ts e a
 168 |   -> Lazy (Result0 b2 t ts e a)
 169 |   -> Result0 (b1 && b2) t ts e a
 170 | Succ0 v xs @{p} <|> _  = Succ0 v xs @{and1 p}
 171 | Fail0 _         <|> r2 = and2 r2
 172 | 
 173 | --------------------------------------------------------------------------------
 174 | --          Running a Parser
 175 | -----------------------------------------------------------------------------
 176 | 
 177 | ||| Repeatedly consumes a strict prefix of a list of items
 178 | ||| until the whole list is consumed.
 179 | |||
 180 | ||| This is provably total, due to the strictness of the consuming
 181 | ||| function.
 182 | public export
 183 | run :
 184 |      {0 t,e,a : Type}
 185 |   -> ((ts : List t) -> Result0 True t ts e a)
 186 |   -> List t -> Either e (List a)
 187 | run f cs = go [<] cs suffixAcc
 188 | 
 189 |   where
 190 |     go : SnocList a
 191 |       -> (ts : List t)
 192 |       -> (0 acc : SuffixAcc ts)
 193 |       -> Either e (List a)
 194 |     go sx [] _      = Right $ sx <>> []
 195 |     go sx xs (SA r) = case f xs of
 196 |       Succ0 v xs2 => go (sx :< v) xs2 r
 197 |       Fail0 err   => Left err
 198 | 
 199 | ||| Repeatedly consumes a strict prefix of a list of characters
 200 | ||| until the whole list is consumed. Drops all white space
 201 | ||| it encounters (unsing `Prelude.isSpace` to determine, what is
 202 | ||| a whitespace character).
 203 | |||
 204 | ||| This is provably total, due to the strictness of the consuming
 205 | ||| function.
 206 | public export
 207 | runDropWhitespace :
 208 |      {0 e,a : Type}
 209 |   -> ((cs : List Char) -> Result0 True Char cs e a)
 210 |   -> List Char -> Either e (List a)
 211 | runDropWhitespace f cs = go [<] cs suffixAcc
 212 | 
 213 |   where
 214 |     go : SnocList a
 215 |       -> (cs : List Char)
 216 |       -> (0 acc : SuffixAcc cs)
 217 |       -> Either e (List a)
 218 |     go sx [] _           = Right $ sx <>> []
 219 |     go sx (x::xs) (SA r) = 
 220 |       if isSpace x then go sx xs r
 221 |       else case f (x::xs) of
 222 |         Succ0 v xs2 => go (sx :< v) xs2 r
 223 |         Fail0 err   => Left err
 224 | 
 225 | --------------------------------------------------------------------------------
 226 | --          Erased Consumers
 227 | -----------------------------------------------------------------------------
 228 | 
 229 | public export
 230 | data TokError : Type -> Type where
 231 |   EOI         : TokError t
 232 |   ExpectedEOI : t -> TokError t
 233 |   Unexpected  : t -> TokError t
 234 | 
 235 | export
 236 | Interpolation t => Interpolation (TokError t) where
 237 |   interpolate (Unexpected t)  = "Unexpected item: \{t}"
 238 |   interpolate EOI             = "End of input"
 239 |   interpolate (ExpectedEOI t) = "Expected end of input but found: \{t}"
 240 | 
 241 | %runElab derive "TokError" [Show,Eq]
 242 | 
 243 | ||| A tokenizing function, which will consume additional characters
 244 | ||| from the input string. This can only be used if already some
 245 | ||| have been consumed.
 246 | public export
 247 | 0 AutoTok0 : (t,e,a : Type) -> Type
 248 | AutoTok0 t e a =
 249 |      {orig     : List t}
 250 |   -> (xs       : List t)
 251 |   -> {auto 0 p : Suffix True xs orig}
 252 |   -> Result0 True t orig e a
 253 | 
 254 | ||| A tokenizing function that cannot fail.
 255 | public export
 256 | 0 SafeTok0 : (t,a : Type) -> Type
 257 | SafeTok0 t a =
 258 |      {0 e      : Type}
 259 |   -> {orig     : List t}
 260 |   -> (xs       : List t)
 261 |   -> {auto 0 p : Suffix True xs orig}
 262 |   -> Result0 True t orig e a
 263 | 
 264 | ||| A tokenizing function, which will consume additional items
 265 | ||| from the input.
 266 | public export
 267 | 0 OntoTok0 : (t,e,a : Type) -> Type
 268 | OntoTok0 t e a =
 269 |      {orig     : List t}
 270 |   -> (xs       : List t)
 271 |   -> {auto 0 p : Suffix False xs orig}
 272 |   -> Result0 True t orig e a
 273 | 
 274 | public export
 275 | head : OntoTok0 t (TokError t) t
 276 | head (x :: xs) = Succ0 x xs
 277 | head []        = Fail0 EOI
 278 | 
 279 | public export
 280 | eoi : AutoTok0 t (TokError t) ()
 281 | eoi []        = Succ0 () []
 282 | eoi (x :: _)  = Fail0 (ExpectedEOI x)
 283 | 
 284 | public export
 285 | takeOnto : SnocList t -> (n : Nat) -> AutoTok0 t (TokError t) (SnocList t)
 286 | takeOnto st 0     xs        = Succ0 st xs
 287 | takeOnto st (S k) (x :: xs) = takeOnto (st :< x) k xs
 288 | takeOnto st (S k) []        = Fail0 EOI
 289 | 
 290 | public export %inline
 291 | take : (n : Nat) -> AutoTok0 t (TokError t) (SnocList t)
 292 | take = takeOnto [<]
 293 | 
 294 | public export %inline
 295 | take1 : (n : Nat) -> (0 _ : IsSucc n) => OntoTok0 t (TokError t) (SnocList t)
 296 | take1 (S n) (x :: xs) = takeOnto [<x] n xs
 297 | take1 _     []        = Fail0 EOI
 298 | 
 299 | public export
 300 | takeWhileOnto : SnocList t -> (t -> Bool) -> SafeTok0 t (SnocList t)
 301 | takeWhileOnto st f (x :: xs) =
 302 |   if f x then takeWhileOnto (st :< x) f xs else Succ0 st (x::xs)
 303 | takeWhileOnto st f []        = Succ0 st []
 304 | 
 305 | public export %inline
 306 | takeWhile : (t -> Bool) -> SafeTok0 t (SnocList t)
 307 | takeWhile = takeWhileOnto [<]
 308 | 
 309 | public export %inline
 310 | takeWhile1 : (t -> Bool) -> OntoTok0 t (TokError t) (SnocList t)
 311 | takeWhile1 f (x :: xs) =
 312 |   if f x then takeWhileOnto [<x] f xs else Fail0 (Unexpected x)
 313 | takeWhile1 f [] = Fail0 EOI
 314 | 
 315 | public export %inline
 316 | takeUntil : (t -> Bool) -> SafeTok0 t (SnocList t)
 317 | takeUntil f = takeWhile (not . f)
 318 | 
 319 | public export %inline
 320 | takeUntil1 : (t -> Bool) -> OntoTok0 t (TokError t) (SnocList t)
 321 | takeUntil1 f = takeWhile1 (not . f)
 322 | 
 323 | public export
 324 | takeWhileJustOnto : SnocList s -> (t -> Maybe s) -> SafeTok0 t (SnocList s)
 325 | takeWhileJustOnto st f (x :: xs) = case f x of
 326 |   Just vs => takeWhileJustOnto (st :< vs) f xs
 327 |   Nothing => Succ0 st (x::xs)
 328 | takeWhileJustOnto st f []        = Succ0 st []
 329 | 
 330 | public export %inline
 331 | takeWhileJust : (t -> Maybe s) -> SafeTok0 t (SnocList s)
 332 | takeWhileJust = takeWhileJustOnto [<]
 333 | 
 334 | public export
 335 | takeWhileJust1 : (t -> Maybe s) -> OntoTok0 t (TokError t) (SnocList s)
 336 | takeWhileJust1 f (x :: xs) = case f x of
 337 |   Just vs => takeWhileJustOnto [<vs] f xs
 338 |   Nothing => Fail0 (Unexpected x)
 339 | takeWhileJust1 f []        = Fail0 EOI
 340 | 
 341 | public export %inline
 342 | accum : s -> (s -> t -> Maybe s) -> SafeTok0 t s
 343 | accum cur f (x::xs) = case f cur x of
 344 |   Just s2 => accum s2 f xs
 345 |   Nothing => Succ0 cur (x::xs)
 346 | accum cur f [] = Succ0 cur []
 347 | 
 348 | public export %inline
 349 | accum1 : s -> (s -> t -> Maybe s) -> OntoTok0 t (TokError t) s
 350 | accum1 cur f (x::xs) = case f cur x of
 351 |   Just s2 => accum s2 f xs
 352 |   Nothing => Fail0 (Unexpected x)
 353 | accum1 cur f [] = Fail0 EOI
 354 | 
 355 | public export
 356 | data AccumRes : (state,err : Type) -> Type where
 357 |   Done  : {0 state,err : _} -> AccumRes state err
 358 |   Cont  : {0 state,err : _} -> state -> AccumRes state err
 359 |   Error : {0 state,err : _} -> err -> AccumRes state err
 360 | 
 361 | public export %inline
 362 | accumErr : s -> (s -> x) -> (s -> t -> AccumRes s e) -> AutoTok0 t e x
 363 | accumErr cur f g (x::xs) = case g cur x of
 364 |   Done      => Succ0 (f cur) (x::xs)
 365 |   Cont s'   => accumErr s' f g xs
 366 |   Error err => Fail0 err
 367 | accumErr cur f g [] = Succ0 (f cur) []
 368 | 
 369 | --------------------------------------------------------------------------------
 370 | -- Parse Errors and Bounds
 371 | --------------------------------------------------------------------------------
 372 | 
 373 | public export %inline
 374 | FailParse (Result0 b t ts (Bounded $ InnerError y)) y where
 375 |   parseFail b err = Fail0 (B err b)
 376 | 
 377 | ||| General catch-all error generator when parsing within some kind
 378 | ||| of opening token: Will fail with an `Unclosed` error if at the
 379 | ||| end of input, or with an `Unknown` error wrapping the next token.
 380 | ||| Otherwise, will rethrow the current error.
 381 | |||
 382 | ||| @ b   : Bounds of the opening paren or token
 383 | ||| @ tok : Opening paren or token
 384 | ||| @ res : Current parsing result
 385 | public export
 386 | failInParen :
 387 |      {auto int : Interpolation t}
 388 |   -> (b : Bounds)
 389 |   -> (tok : t)
 390 |   -> Result0 b1 (Bounded t) ts (Bounded $ InnerError e) a
 391 |   -> Result0 b2 (Bounded t) ts (Bounded $ InnerError e) x
 392 | failInParen b tok (Fail0 (B EOI _))   = unclosed b tok
 393 | failInParen b tok (Fail0 err)         = Fail0 err
 394 | failInParen b tok (Succ0 _ [])        = unclosed b tok
 395 | failInParen b tok (Succ0 _ (x :: xs)) = unexpected x
 396 | 
 397 | ||| Catch-all error generator when no other rule applies.
 398 | public export
 399 | fail :
 400 |      {auto int : Interpolation t}
 401 |   -> List (Bounded t)
 402 |   -> Result0 b (Bounded t) ts (Bounded $ InnerError y) a
 403 | fail (x :: xs) = unexpected x
 404 | fail []        = eoi
 405 | 
 406 | public export
 407 | result :
 408 |      {auto int : Interpolation t}
 409 |   -> Origin
 410 |   -> String
 411 |   -> Result0 b (Bounded t) ts (Bounded $ InnerError e) a
 412 |   -> Either (ParseError e) a
 413 | result o s (Fail0 err)           = Left $ toParseError o s err
 414 | result _ s (Succ0 res [])        = Right res
 415 | result o s (Succ0 res (x :: xs)) = leftErr o s $ unexpected x
 416 |