
   0 | module Text.Parse.Core
   1 | 
   2 | import Data.Bool
   3 | import Data.List
   4 | import Data.List1
   5 | import Data.List.Suffix
   6 | import Derive.Prelude
   7 | import Text.ParseError
   8 | import Text.FC
   9 | import Text.Bounds
  10 | import Text.Lex.Core
  11 | import Text.Lex.Tokenizer
  12 | 
  13 | %language ElabReflection
  14 | %default total
  15 | 
  16 | --------------------------------------------------------------------------------
  17 | --          Parsing Results
  18 | --------------------------------------------------------------------------------
  19 | 
  20 | ||| Result of running a parser.
  21 | public export
  22 | data Res :
  23 |      (strict : Bool)
  24 |   -> (t  : Type)
  25 |   -> (ts : List $ Bounded t)
  26 |   -> (state,e,a : Type)
  27 |   -> Type where
  28 | 
  29 |   Fail  :
  30 |        {0 b : Bool}
  31 |     -> {0 state,t,e,a : Type}
  32 |     -> {0 ts : List $ Bounded t}
  33 |     -> (consumed : Bool)
  34 |     -> (err      : List1 $ Bounded $ InnerError e)
  35 |     -> Res b t ts state e a
  36 | 
  37 |   Succ :
  38 |        {0 b : Bool}
  39 |     -> {0 state,t,e,a : Type}
  40 |     -> {0 ts : List $ Bounded t}
  41 |     -> state
  42 |     -> (res  : Bounded a)
  43 |     -> (toks : List $ Bounded t)
  44 |     -> (prf  : Suffix b toks ts)
  45 |     -> Res b t ts state e a
  46 | 
  47 | public export %inline
  48 | FailParse (Res b t ts state e) e where
  49 |   parseFail b e = Fail False (B e b ::: [])
  50 | 
  51 | public export
  52 | merge : Bounded z -> Res b t ts s e a -> Res b t ts s e a
  53 | merge x (Succ y res toks prf) = Succ y (x *> res) toks prf
  54 | merge x v                     = v
  55 | 
  56 | export
  57 | succ : Res b t ts s e a -> (p : Suffix True ts ts') -> Res b1 t ts' s e a
  58 | succ (Fail c err)          p = Fail c err
  59 | succ (Succ x res toks prf) p = Succ x res toks (weakens $ orTrue $ trans prf p)
  60 | 
  61 | --------------------------------------------------------------------------------
  62 | --          Grammar
  63 | --------------------------------------------------------------------------------
  64 | 
  65 | public export %tcinline
  66 | 0 inf : Bool -> Type -> Type
  67 | inf False y = y
  68 | inf True  y = Inf y
  69 | 
  70 | public export
  71 | data Grammar :
  72 |      (strict : Bool)
  73 |   -> (state,t,e,a : Type)
  74 |   -> Type where
  75 | 
  76 |   Lift :
  77 |        {0 state,t,e,a : Type}
  78 |     -> (state -> (ts : List $ Bounded t) -> Res b t ts state e a)
  79 |     -> Grammar b state t e a
  80 | 
  81 |   AppEat :
  82 |        {0 state,t,e,a : Type}
  83 |     -> Grammar True state t e (a -> b)
  84 |     -> Inf (Grammar b2 state t e a)
  85 |     -> Grammar True state t e b
  86 | 
  87 |   App :
  88 |        {0 state,t,e,a : Type}
  89 |     -> Grammar b1 state t e (a -> b)
  90 |     -> Grammar b2 state t e a
  91 |     -> Grammar (b1 || b2) state t e b
  92 | 
  93 |   BindEat :
  94 |       {0 state,t,e,a : Type}
  95 |    -> Grammar True state t e a
  96 |    -> Inf (a -> Grammar b2 state t e b)
  97 |    -> Grammar True state t e b
  98 | 
  99 |   (>>=) :
 100 |       {0 state,t,e,a : Type}
 101 |    -> Grammar b1 state t e a
 102 |    -> (a -> Grammar b2 state t e b)
 103 |    -> Grammar (b1 || b2) state t e b
 104 | 
 105 |   ThenEat :
 106 |       {0 state,t,e,a : Type}
 107 |    -> Grammar True state t e a
 108 |    -> Inf (Grammar b2 state t e b)
 109 |    -> Grammar True state t e b
 110 | 
 111 |   (>>) :
 112 |       {0 state,t,e,a : Type}
 113 |    -> Grammar b1 state t e a
 114 |    -> Grammar b2 state t e b
 115 |    -> Grammar (b1 || b2) state t e b
 116 | 
 117 |   Alt :
 118 |       {0 state,t,e,a : Type}
 119 |    -> Grammar b1 state t e a
 120 |    -> Lazy (Grammar b2 state t e a)
 121 |    -> Grammar (b1 && b2) state t e a
 122 | 
 123 |   Bounds :
 124 |       {0 state,t,e,a : Type}
 125 |    -> Grammar b state t e a
 126 |    -> Grammar b state t e (Bounded a)
 127 | 
 128 |   Try :
 129 |       {0 state,t,e,a : Type}
 130 |    -> Grammar b state t e a
 131 |    -> Grammar b state t e a
 132 | 
 133 | --------------------------------------------------------------------------------
 134 | --          Error Handling
 135 | --------------------------------------------------------------------------------
 136 | 
 137 | public export %inline
 138 | FailParse (Grammar b state t e) e where
 139 |   parseFail b err = Lift $ \_,_ => parseFail b err
 140 | 
 141 | -------------------------------------------------------------------------------
 142 | --         Core Parsers
 143 | -------------------------------------------------------------------------------
 144 | 
 145 | public export %inline
 146 | (<|>) :
 147 |      {0 b1,b2 : Bool}
 148 |   -> {0 state,t,e,a : Type}
 149 |   -> Grammar b1 state t e a
 150 |   -> Lazy (Grammar b2 state t e a)
 151 |   -> Grammar (b1 && b2) state t e a
 152 | (<|>) = Alt
 153 | 
 154 | public export %inline
 155 | pure : {0 state,t,e,a : Type} -> (res : a) -> Grammar False state t e a
 156 | pure res = Lift $ \s,ts => Succ s (pure res) ts Same
 157 | 
 158 | public export
 159 | Functor (Grammar b s t e) where
 160 |   map f g = rewrite sym (orFalseNeutral b) in g >>= pure . f
 161 | 
 162 | public export %tcinline
 163 | (<*>) :
 164 |      {0 state,t,e,a : Type}
 165 |   -> {b1 : Bool}
 166 |   -> Grammar b1 state t e (a -> b)
 167 |   -> inf b1 (Grammar b2 state t e a)
 168 |   -> Grammar (b1 || b2) state t e b
 169 | (<*>) {b1 = True}  = AppEat
 170 | (<*>) {b1 = False} = App
 171 | 
 172 | public export %inline
 173 | (*>) :
 174 |      {0 b1,b2 : Bool}
 175 |   -> {0 state,t,e,a : Type}
 176 |   -> Grammar b1 state t e a
 177 |   -> Grammar b2 state t e b
 178 |   -> Grammar (b1 || b2) state t e b
 179 | (*>) x y = x >>= \_ => y
 180 | 
 181 | public export %inline
 182 | (<*) :
 183 |      {0 b1,b2 : Bool}
 184 |   -> {0 state,t,e,a : Type}
 185 |   -> Grammar b1 state t e a
 186 |   -> Grammar b2 state t e b
 187 |   -> Grammar (b1 || b2) state t e a
 188 | (<*) x y = x >>= (y $>)
 189 | 
 190 | ||| Check whether the next token satisfies a predicate
 191 | public export
 192 | nextIs : Lazy e -> (t -> Bool) -> Grammar False s t e t
 193 | nextIs err f = Lift $ \s,cs => case cs of
 194 |   h :: t =>
 195 |     if f h.val then Succ s h (h::t) Same else custom h.bounds err
 196 |   []     => eoi
 197 | 
 198 | ||| Look at the next token in the input
 199 | public export
 200 | peek : Grammar False s t e t
 201 | peek = Lift $ \s,cs => case cs of
 202 |   h :: t => Succ s h (h::t) Same
 203 |   []     => eoi
 204 | 
 205 | ||| Look at the next token in the input
 206 | public export
 207 | readHead : (t -> Either (InnerError e) a) -> Grammar True s t e a
 208 | readHead f = Lift $ \s,cs => case cs of
 209 |   h :: t => case f h.val of
 210 |     Right v  => Succ s (B v h.bounds) t %search
 211 |     Left err => parseFail h.bounds err
 212 |   []     => eoi
 213 | 
 214 | ||| Look at the next token in the input
 215 | public export %inline
 216 | terminal : Interpolation t => (t -> Maybe a) -> Grammar True s t e a
 217 | terminal f = readHead $ \h => case f h of
 218 |   Just a  => Right a
 219 |   Nothing => Left (Expected [] "\{h}")
 220 | 
 221 | ||| Look at the next token in the input
 222 | public export
 223 | is : Interpolation t => Eq t => t -> Grammar True s t e ()
 224 | is x = readHead $ \h => if x == h then Right () else Left (Expected ["\{x}"] "\{h}")
 225 | 
 226 | ||| Optionally parse a thing, with a default value if the grammar doesn't
 227 | ||| match. May match the empty input.
 228 | export
 229 | option :
 230 |      {0 state,t,e,a : Type}
 231 |   -> (def : a)
 232 |   -> Grammar b state t e a
 233 |   -> Grammar False state t e a
 234 | option def g = rewrite sym (andFalseFalse b) in g <|> pure def
 235 | 
 236 | ||| Optionally parse a thing, with a default value if the grammar doesn't
 237 | ||| match. May match the empty input.
 238 | export
 239 | optional :
 240 |      {0 state,t,e,a : Type}
 241 |   -> Grammar b state t e a
 242 |   -> Grammar False state t e (Maybe a)
 243 | optional = option Nothing . map Just
 244 | 
 245 | public export
 246 | some : Grammar True s t e a -> Grammar True s t e (List1 a)
 247 | 
 248 | public export
 249 | many : Grammar True s t e a -> Grammar False s t e (List a)
 250 | 
 251 | some g = [| g ::: many g |]
 252 | 
 253 | many g = map forget (some g) <|> pure []
 254 | 
 255 | ||| Parse one or more instances of `p` until `end` succeeds, returning the
 256 | ||| list of values from `p`. Guaranteed to consume input.
 257 | export
 258 | someTill : 
 259 |      (end : Grammar b s t e x)
 260 |   -> (p : Grammar True s t e a )
 261 |   -> Grammar True s t e (List1 a)
 262 | 
 263 | ||| Parse zero or more instances of `p` until `end` succeeds, returning the
 264 | ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
 265 | export
 266 | manyTill : 
 267 |      (end : Grammar b s t e x)
 268 |   -> (p : Grammar True s t e a )
 269 |   -> Grammar b s t e (List a)
 270 | 
 271 | someTill end p = [| p ::: manyTill end p |]
 272 | 
 273 | manyTill end p =
 274 |   rewrite sym (andTrueNeutral b) in (end $> []) <|> (forget <$> someTill end p)
 275 | 
 276 | ||| Parse one or more instance of `skip` until `p` is encountered,
 277 | ||| returning its value.
 278 | export
 279 | afterSome :
 280 |      (skip : Grammar True s t e x)
 281 |   -> (p : Grammar b s t e a )
 282 |   -> Grammar True s t e a
 283 | 
 284 | ||| Parse zero or more instance of `skip` until `p` is encountered,
 285 | ||| returning its value.
 286 | export
 287 | afterMany :
 288 |      (skip : Grammar True s t e x)
 289 |   -> (p : Grammar b s t e a )
 290 |   -> Grammar b s t e a
 291 | 
 292 | afterSome skip p = [| (\_,x => x) skip (afterMany skip p) |]
 293 | 
 294 | afterMany skip p = rewrite sym (andTrueNeutral b) in p <|> afterSome skip p
 295 | 
 296 | ||| Parse one or more things, each separated by another thing.
 297 | export
 298 | sepBy1 :
 299 |      {b : Bool}
 300 |   -> (sep : Grammar True s t e s)
 301 |   -> (p : Grammar b s t e a)
 302 |   ->  Grammar b s t e (List1 a)
 303 | sepBy1 {b = True}  sep p = [| p ::: many (sep *> p) |]
 304 | sepBy1 {b = False} sep p = [| p ::: many (sep *> p) |]
 305 | 
 306 | ||| Parse zero or more things, each separated by another thing. May
 307 | ||| match the empty input.
 308 | export
 309 | sepBy :
 310 |      {b : Bool}
 311 |   -> (sep : Grammar True s t e s)
 312 |   -> (p : Grammar b s t e a)
 313 |   ->  Grammar False s t e (List a)
 314 | sepBy sep p = option [] $ forget <$> sepBy1 sep p
 315 | 
 316 | ||| Parse one or more instances of `p` separated by and optionally terminated by
 317 | ||| `sep`.
 318 | export
 319 | sepEndBy1 :
 320 |      {b : Bool}
 321 |   -> (sep : Grammar True s t e s)
 322 |   -> (p : Grammar b s t e a)
 323 |   ->  Grammar b s t e (List1 a)
 324 | sepEndBy1 sep p = rewrite sym (orFalseNeutral b) in sepBy1 sep p <* optional sep
 325 | 
 326 | ||| Parse zero or more instances of `p`, separated by and optionally terminated
 327 | ||| by `sep`. Will not match a separator by itself.
 328 | export
 329 | sepEndBy :
 330 |      {b : Bool}
 331 |   -> (sep : Grammar True s t e s)
 332 |   -> (p : Grammar b s t e a)
 333 |   ->  Grammar False s t e (List a)
 334 | sepEndBy sep p = option [] $ forget <$> sepEndBy1 sep p
 335 | 
 336 | ||| Parse one or more instances of `p`, separated and terminated by `sep`.
 337 | export
 338 | endBy1 :
 339 |      (sep : Grammar True s t e s)
 340 |   -> (p : Grammar b s t e a)
 341 |   ->  Grammar True s t e (List1 a)
 342 | endBy1 sep p = some $ rewrite sym (orTrueTrue b) in p <* sep
 343 | 
 344 | export
 345 | endBy :
 346 |      (sep : Grammar True s t e s)
 347 |   -> (p : Grammar b s t e a)
 348 |   ->  Grammar False s t e (List a)
 349 | endBy sep p = option [] $ forget <$> endBy1 sep p
 350 | 
 351 | ||| Parse an instance of `p` that is between `left` and `right`.
 352 | export %inline
 353 | between :
 354 |      (left : Grammar True s t e l)
 355 |   -> (right : Grammar True s t e r)
 356 |   -> (p : Grammar b s t e a)
 357 |   -> Grammar True s t e a
 358 | between left right contents = left *> contents <* right
 359 | 
 360 | prs :
 361 |      {0 state,t,e,a : Type}
 362 |   -> Grammar b state t e a
 363 |   -> state
 364 |   -> (consumed : Bool)
 365 |   -> (ts : List $ Bounded t)
 366 |   -> (0 sa : SuffixAcc ts)
 367 |   -> Res b t ts state e a
 368 | prs (Lift f) s1 c1 ts1 _ = case f s1 ts1 of
 369 |   Fail c2 err         => Fail (c1 || c2) err
 370 |   Succ x res toks prf => Succ x res toks prf
 371 | 
 372 | prs (App x y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 373 |   Succ s2 rf ts1 Same => case prs y s2 c1 ts1 sa of
 374 |     Fail c2 err       => Fail c2 err
 375 |     Succ s3 ra ts3 p3 => Succ s3 (rf <*> ra) ts3 p3
 376 |   Succ s2 rf ts2 (Uncons p2) => case prs y s2 True ts2 rec of
 377 |     Fail c2 err       => Fail c2 err
 378 |     Succ s3 ra ts3 p3 => Succ s3 (rf <*> ra) ts3 (swapOr $ trans p3 (Uncons p2))
 379 |   Fail c2 err => Fail c2 err
 380 | 
 381 | prs (AppEat x y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 382 |   Succ s2 rf ts2 p2 => case prs y s2 True ts2 rec of
 383 |     Fail c2 err       => Fail c2 err
 384 |     Succ s3 ra ts3 p3 => Succ s3 (rf <*> ra) ts3 (swapOr $ trans p3 p2)
 385 |   Fail c2 err => Fail c2 err
 386 | 
 387 | prs (BindEat x y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 388 |   Succ s2 res ts2 p => merge res $ succ (prs (y res.val) s2 True ts2 rec) p
 389 |   Fail c2 err       => Fail c2 err
 390 | 
 391 | prs (x >>= y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 392 |   Succ s2 res ts2 (Uncons p) =>
 393 |     merge res $ succ (prs (y res.val) s2 True ts2 rec) (Uncons p)
 394 |   Succ s2 res ts2 Same       => merge res $ prs (y res.val) s2 c1 ts2 sa
 395 |   Fail c2 err                => Fail c2 err
 396 | 
 397 | prs (ThenEat x y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 398 |   Succ s2 res ts2 p => merge res $ succ (prs y s2 True ts2 rec) p
 399 |   Fail c2 err       => Fail c2 err
 400 | 
 401 | prs (x >> y) s1 c1 ts1 sa@(SA rec) = case prs x s1 c1 ts1 sa of
 402 |   Succ s2 res ts2 (Uncons p) =>
 403 |     merge res $ succ (prs y s2 True ts2 rec) (Uncons p)
 404 |   Succ s2 res ts2 Same       => merge res $ prs y s2 c1 ts2 sa
 405 |   Fail c2 err                => Fail c2 err
 406 | 
 407 | prs (Alt x y) s1 c1 ts1 sa = case prs x s1 False ts1 sa of
 408 |   Succ s2 res ts2 p => Succ s2 res ts2 (and1 p)
 409 |   Fail True err     => Fail True err
 410 |   Fail {b = b1} False err  => case prs y s1 False ts1 sa of
 411 |     Succ s2 res ts2 p => Succ s2 res ts2 (and2 p)
 412 |     Fail True err2    => Fail True err2
 413 |     Fail False err2   => Fail c1 $ err ++ err2
 414 | 
 415 | prs (Bounds x) s1 c1 ts1 sa = case prs x s1 c1 ts1 sa of
 416 |   Succ s2 res ts2 p => Succ s2 (B res res.bounds) ts2 p
 417 |   Fail c2 err       => Fail c2 err
 418 | 
 419 | prs (Try x) s1 c1 ts1 sa = case prs x s1 c1 ts1 sa of
 420 |   Fail _ err => Fail False err
 421 |   res        => res
 422 | 
 423 | export
 424 | parse :
 425 |      {0 state,t,e,a : Type}
 426 |   -> Grammar b state t e a
 427 |   -> state
 428 |   -> (ts : List $ Bounded t)
 429 |   -> Either (List1 $ Bounded $ InnerError e) (state, a, List $ Bounded t)
 430 | parse g s ts = case prs g s False ts suffixAcc of
 431 |   Fail _ errs         => Left errs
 432 |   Succ x res toks prf => Right (x, res.val, toks)
 433 | 
 434 | --------------------------------------------------------------------------------
 435 | --          Combining Lexers and Parsers
 436 | --------------------------------------------------------------------------------
 437 | 
 438 | filterOnto :
 439 |      List (Bounded t)
 440 |   -> (t -> Bool)
 441 |   -> SnocList (Bounded t)
 442 |   -> List (Bounded t)
 443 | filterOnto xs f (sx :< x) =
 444 |   if f x.val then filterOnto (x :: xs) f sx else filterOnto xs f sx
 445 | filterOnto xs f [<]       = xs
 446 | 
 447 | ||| Given a tokenizer and an input string, return a list of recognised tokens.
 448 | |||
 449 | ||| This fails with an error if not the whole input is consumed.
 450 | export
 451 | lexFull :
 452 |      {auto int : Interpolation t}
 453 |   -> Origin
 454 |   -> Tokenizer e t
 455 |   -> (keep : t -> Bool)
 456 |   -> (s : String)
 457 |   -> Either (Bounded $ InnerError e) (List $ Bounded t)
 458 | lexFull orig tm keep s = case lex tm s of
 459 |   TR pos toks Nothing    _ _ => Right $ filterOnto [] keep toks
 460 |   TR _ _      (Just err) _ _ => Left err
 461 | 
 462 | export
 463 | lexAndParse :
 464 |      {0 state,t,e,a : Type}
 465 |   -> {auto int : Interpolation t}
 466 |   -> Origin
 467 |   -> Tokenizer e t
 468 |   -> (keep : t -> Bool)
 469 |   -> Grammar b state t e a
 470 |   -> state
 471 |   -> String
 472 |   -> Either (List1 (FileContext, InnerError e)) (state, a)
 473 | lexAndParse orig tm keep gr s str =
 474 |   let Right ts := lexFull orig tm keep str
 475 |         | Left err => Left $ singleton (fromBounded orig err)
 476 |    in case parse gr s ts of
 477 |         Left x         => Left $ fromBounded orig <$> x
 478 |         Right (s2,a,_) => Right (s2,a)
 479 |