0 | module Data.Swirl.Parsing
  1 |
  2 | import public Data.Swirl
  3 |
  4 | %default total
  5 |
  6 | --- Parsing ---
  7 |
  8 | -- TODO to add a documentation example, say, by a swirl of chars produce a swirl of strings separated by EOL
  9 |
 10 | public export
 11 | data WhetherConsumeLast a = ConsumeLast a | DoNotConsumeLast a
 12 |
 13 | export
 14 | (.val) : WhetherConsumeLast a -> a
 15 | (.val) $ ConsumeLast x      = x
 16 | (.val) $ DoNotConsumeLast x = x
 17 |
 18 | export
 19 | ifConsumes : WhetherConsumeLast a -> (cons, notCons : Lazy b) -> b
 20 | ifConsumes (ConsumeLast _     ) cons notCons = cons
 21 | ifConsumes (DoNotConsumeLast _) cons notCons = notCons
 22 |
 23 | public export
 24 | Functor WhetherConsumeLast where
 25 |   map f $ ConsumeLast x      = ConsumeLast $ f x
 26 |   map f $ DoNotConsumeLast x = DoNotConsumeLast $ f x
 27 |
 28 | --- Raw parser (will lots of stuff exposed in the type) ---
 29 |
 30 | public export
 31 | record RawParser m st e' r r' o o' where
 32 |   constructor RP
 33 |   initSeed  : st
 34 |   parseStep : o -> st -> Either st $ WhetherConsumeLast $ Swirl m e' () o'
 35 |   manageFin : st -> r -> Swirl m e' r' o'
 36 |
 37 | %name RawParser pr, ps
 38 |
 39 | export
 40 | Functor m => Functor (RawParser m st e' r r' o) where
 41 |   map f = {parseStep $= (map @{Compose} (mapSnd f) .:), manageFin $= (mapSnd f .:)}
 42 |
 43 | --- Parsing of swirls with the raw parser ---
 44 |
 45 | %inline
 46 | (.passFin) : RawParser m st e' r'' r' o o' -> RawParser m st e' r (st, r) o o'
 47 | (.passFin) = {manageFin := curry succeed}
 48 |
 49 | export
 50 | rawParseOnce : Functor m =>
 51 |                (0 _ : IfUnsolved r' ()) =>
 52 |                (0 _ : IfUnsolved o' Void) =>
 53 |                RawParser m st e'' r r' o o' ->
 54 |                Swirl m e r o -> Swirl m (Either e e'') (Either r' $ Swirl m e r o) o'
 55 | rawParseOnce pr = mapError (mapFst snd) . go pr pr.initSeed where
 56 |   go : forall st, e, e'', r, r', o, o'.
 57 |        RawParser m st e'' r r' o o' ->
 58 |        st ->
 59 |        Swirl m e r o ->
 60 |        Swirl m (Either (st, e) e'') (Either r' $ Swirl m e r o) o'
 61 |   go pr s $ Done x         = mapError Right $ mapFst Left $ pr.manageFin s x
 62 |   go pr s $ Fail e         = fail $ Left (s, e)
 63 |   go pr s sw'@(Yield x sw) = case pr.parseStep x s of
 64 |                                Left s'   => go pr s' sw
 65 |                                Right sub => mapFst (const $ Right $ ifConsumes sub sw sw') $ mapError Right sub.val
 66 |   go pr s $ Effect msw     = Effect $ msw <&> assert_total go pr s
 67 |   go pr s $ BindR sw g     = go pr.passFin s sw `bindR` \case
 68 |                                Left (s', ir) => go pr s' $ g ir
 69 |                                Right cont    => succeed $ Right $ cont `bindR` g
 70 |   go pr s $ BindE sw h     = BindE (mapFst (map Left) $ go pr.passFin s sw) (\case
 71 |                                  Left (s', ei) => mapFst (map Right) $ go pr.passFin s' $ h ei
 72 |                                  Right ep      => fail $ Right ep
 73 |                                ) `BindR` \case
 74 |                                  Left (s', r) => mapFst Left $ mapError Right $ pr.manageFin s' r
 75 |                                  Right cont   => succeed $ Right $ either (`BindE` h) id cont
 76 |   go pr s $ Ensure l x     = Ensure l (go pr.passFin s x) `BindR` \case
 77 |                                (rf, Left (s', r)) => mapError Right $ mapFst Left $ pr.manageFin s' (rf, r)
 78 |                                (rf, Right cont)   => succeed $ Right $ mapFst (rf,) cont
 79 |
 80 | export
 81 | rawParseAll : Functor m =>
 82 |               (0 _ : IfUnsolved r' ()) =>
 83 |               (0 _ : IfUnsolved o' Void) =>
 84 |               RawParser m st e' r r' o o' ->
 85 |               Swirl m e r o -> Swirl m (Either e e') r' o'
 86 | rawParseAll pr sw = (rawParseAll' sw >>= mapError Right . uncurry pr.manageFin) @{ByResult} where
 87 |   rawParseAll' : Swirl m e r o -> Swirl m (Either e e') (st, r) o'
 88 |   rawParseAll' sw = rawParseOnce pr.passFin sw `bindR` \case
 89 |                    Left x     => succeed x
 90 |                    Right cont => rawParseAll' $ assert_smaller sw cont
 91 |
 92 | -- TODO to add composable parsers. They should contain much lesser type parameters (say, `st`, `e'` and `r'` from `RawParser` shouldn't be exposed)
 93 | -- and be able to be composed, say, with `>>` and `>>=` combinators.
 94 | -- This can be done in several ways, at least:
 95 | --
 96 | -- - changing signatures of functions inside `RawParser`, say, replacing `st` to `Swirl m e' st Void` in the result of `parseStep`
 97 | --   to allow the rest to fail, and thus to continue parsing; or
 98 | --
 99 | -- - making `Parser` to contain binds as constructors and to have `parseOnce` taking `Parser` and performing sequential parsing with raw-subparsers
100 | --   in an "external" way comparing to a `RawParser`'s abilities.
101 |