------------------------------------------------------------------------
-- | Parser combinators with support for left recursion, following
-- Johnson\'s \"Memoization in Top-Down Parsing\".
--
-- This implementation is based on an implementation due to Atkey
-- (attached to an edlambda-members mailing list message from
-- 2011-02-15 titled \'Slides for \"Introduction to Parser
-- Combinators\"\').
--
-- Note that non-memoised left recursion is not guaranteed to work.
--
-- The code contains an important deviation from Johnson\'s paper: the
-- check for subsumed results is not included. This means that one can
-- get the same result multiple times when parsing using ambiguous
-- grammars. As an example, parsing the empty string using @S ∷= ε |
-- ε@ succeeds twice. This change also means that parsing fails to
-- terminate for some cyclic grammars that would otherwise be handled
-- successfully, such as @S ∷= S | ε@. However, the library is not
-- intended to handle infinitely ambiguous grammars. (It is unclear to
-- the author of this module whether the change leads to more
-- non-termination for grammars that are not cyclic.)


module Agda.Utils.Parser.MemoisedCPS
  ( ParserClass(..)
  , sat, token, tok, doc
  , DocP, bindP, choiceP, seqP, starP, atomP
  , Parser
  , ParserWithGrammar
  ) where

import Control.Applicative ( Alternative((<|>), empty, many, some) )
import Control.Monad (liftM2, (<=<))
import Control.Monad.State.Strict (State, evalState, runState, get, modify')

import Data.Array
import Data.Hashable
import qualified Data.HashMap.Strict as Map
import Data.HashMap.Strict (HashMap)


import qualified Data.IntMap.Strict as IntMap
import Data.IntMap.Strict (IntMap)
import qualified Data.List as List
import Data.Maybe

import Text.PrettyPrint.HughesPJ hiding (empty)
import qualified Text.PrettyPrint.HughesPJ as PP

import Agda.Utils.Pretty ( mparens )

import Agda.Utils.Impossible

-- | Positions.

type Pos = Int

-- | State monad used by the parser.

type M k r tok b = State (IntMap (HashMap k (Value k r tok b)))

-- | Continuations.

type Cont k r tok b a = Pos -> a -> M k r tok b [b]

-- | Memoised values.

data Value k r tok b = Value
  { forall k r tok b. Value k r tok b -> IntMap [r]
_results       :: !(IntMap [r])
  , forall k r tok b. Value k r tok b -> [Cont k r tok b r]
_continuations :: [Cont k r tok b r]
  }

-- | The parser type.
--
-- The parameters of the type @Parser k r tok a@ have the following
-- meanings:
--
-- [@k@] Type used for memoisation keys.
--
-- [@r@] The type of memoised values. (Yes, all memoised values have
-- to have the same type.)
--
-- [@tok@] The token type.
--
-- [@a@] The result type.

newtype Parser k r tok a =
  P { forall k r tok a.
Parser k r tok a
-> forall b.
   Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
unP :: forall b.
             Array Pos tok ->
             Pos ->
             Cont k r tok b a ->
             M k r tok b [b]
    }

instance Monad (Parser k r tok) where
  return :: forall a. a -> Parser k r tok a
return    = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  P forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p >>= :: forall a b.
Parser k r tok a -> (a -> Parser k r tok b) -> Parser k r tok b
>>= a -> Parser k r tok b
f = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b b
k ->
    forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p Array Pos tok
input Pos
i forall a b. (a -> b) -> a -> b
$ \Pos
j a
x -> forall k r tok a.
Parser k r tok a
-> forall b.
   Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
unP (a -> Parser k r tok b
f a
x) Array Pos tok
input Pos
j Cont k r tok b b
k

instance Functor (Parser k r tok) where
  fmap :: forall a b. (a -> b) -> Parser k r tok a -> Parser k r tok b
fmap a -> b
f (P forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p) = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b b
k ->
    forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p Array Pos tok
input Pos
i forall a b. (a -> b) -> a -> b
$ \Pos
i -> Cont k r tok b b
k Pos
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f

instance Applicative (Parser k r tok) where
  pure :: forall a. a -> Parser k r tok a
pure a
x        = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
_ Pos
i Cont k r tok b a
k -> Cont k r tok b a
k Pos
i a
x
  P forall b.
Array Pos tok -> Pos -> Cont k r tok b (a -> b) -> M k r tok b [b]
p1 <*> :: forall a b.
Parser k r tok (a -> b) -> Parser k r tok a -> Parser k r tok b
<*> P forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p2 = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b b
k ->
    forall b.
Array Pos tok -> Pos -> Cont k r tok b (a -> b) -> M k r tok b [b]
p1 Array Pos tok
input Pos
i forall a b. (a -> b) -> a -> b
$ \Pos
i a -> b
f ->
    forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p2 Array Pos tok
input Pos
i forall a b. (a -> b) -> a -> b
$ \Pos
i a
x ->
    Cont k r tok b b
k Pos
i (a -> b
f a
x)

instance Alternative (Parser k r tok) where
  empty :: forall a. Parser k r tok a
empty         = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
_ Pos
_ Cont k r tok b a
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
  P forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p1 <|> :: forall a. Parser k r tok a -> Parser k r tok a -> Parser k r tok a
<|> P forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p2 = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b a
k ->
    forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. [a] -> [a] -> [a]
(++) (forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p1 Array Pos tok
input Pos
i Cont k r tok b a
k) (forall b.
Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
p2 Array Pos tok
input Pos
i Cont k r tok b a
k)

class (Functor p, Applicative p, Alternative p, Monad p) =>
      ParserClass p k r tok | p -> k, p -> r, p -> tok where
  -- | Runs the parser.
  parse :: p a -> [tok] -> [a]

  -- | Tries to print the parser, or returns 'PP.empty', depending on
  -- the implementation. This function might not terminate.
  grammar :: Show k => p a -> Doc

  -- | Parses a token satisfying the given predicate. The computed
  -- value is returned.
  sat' :: (tok -> Maybe a) -> p a

  -- | Uses the given function to modify the printed representation
  -- (if any) of the given parser.
  annotate :: (DocP -> DocP) -> p a -> p a

  -- | Memoises the given parser.
  --
  -- Every memoised parser must be annotated with a /unique/ key.
  -- (Parametrised parsers must use distinct keys for distinct
  -- inputs.)
  memoise :: (Eq k, Hashable k, Show k) => k -> p r -> p r

  -- | Memoises the given parser, but only if printing, not if
  -- parsing.
  --
  -- Every memoised parser must be annotated with a /unique/ key.
  -- (Parametrised parsers must use distinct keys for distinct
  -- inputs.)
  memoiseIfPrinting :: (Eq k, Hashable k, Show k) => k -> p r -> p r

-- | Uses the given document as the printed representation of the
-- given parser. The document's precedence is taken to be 'atomP'.

doc :: ParserClass p k r tok => Doc -> p a -> p a
doc :: forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
Doc -> p a -> p a
doc Doc
d = forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
(DocP -> DocP) -> p a -> p a
annotate (\DocP
_ -> (Doc
d, Pos
atomP))

-- | Parses a token satisfying the given predicate.

sat :: ParserClass p k r tok => (tok -> Bool) -> p tok
sat :: forall (p :: * -> *) k r tok.
ParserClass p k r tok =>
(tok -> Bool) -> p tok
sat tok -> Bool
p = forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
(tok -> Maybe a) -> p a
sat' (\tok
t -> if tok -> Bool
p tok
t then forall a. a -> Maybe a
Just tok
t else forall a. Maybe a
Nothing)

-- | Parses a single token.

token :: ParserClass p k r tok => p tok
token :: forall (p :: * -> *) k r tok. ParserClass p k r tok => p tok
token = forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
Doc -> p a -> p a
doc Doc
"·" (forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
(tok -> Maybe a) -> p a
sat' forall a. a -> Maybe a
Just)

-- | Parses a given token.

tok :: (ParserClass p k r tok, Eq tok, Show tok) => tok -> p tok
tok :: forall (p :: * -> *) k r tok.
(ParserClass p k r tok, Eq tok, Show tok) =>
tok -> p tok
tok tok
t = forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
Doc -> p a -> p a
doc (String -> Doc
text (forall a. Show a => a -> String
show tok
t)) (forall (p :: * -> *) k r tok.
ParserClass p k r tok =>
(tok -> Bool) -> p tok
sat (tok
t forall a. Eq a => a -> a -> Bool
==))

instance ParserClass (Parser k r tok) k r tok where
  parse :: forall a. Parser k r tok a -> [tok] -> [a]
parse Parser k r tok a
p [tok]
toks =
    forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> a
evalState forall a. IntMap a
IntMap.empty forall a b. (a -> b) -> a -> b
$
    forall k r tok a.
Parser k r tok a
-> forall b.
   Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
unP Parser k r tok a
p (forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (Pos
0, Pos
n forall a. Num a => a -> a -> a
- Pos
1) [tok]
toks) Pos
0 forall a b. (a -> b) -> a -> b
$ \Pos
j a
x ->
      if Pos
j forall a. Eq a => a -> a -> Bool
== Pos
n then forall (m :: * -> *) a. Monad m => a -> m a
return [a
x] else forall (m :: * -> *) a. Monad m => a -> m a
return []
    where n :: Pos
n = forall i a. Num i => [a] -> i
List.genericLength [tok]
toks

  grammar :: forall a. Show k => Parser k r tok a -> Doc
grammar Parser k r tok a
_ = Doc
PP.empty

  sat' :: forall a. (tok -> Maybe a) -> Parser k r tok a
sat' tok -> Maybe a
p = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b a
k ->
    if forall a. Ix a => (a, a) -> a -> Bool
inRange (forall i e. Array i e -> (i, i)
bounds Array Pos tok
input) Pos
i then
      case tok -> Maybe a
p (Array Pos tok
input forall i e. Ix i => Array i e -> i -> e
! Pos
i) of
        Maybe a
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just a
x  -> (Cont k r tok b a
k forall a b. (a -> b) -> a -> b
$! (Pos
i forall a. Num a => a -> a -> a
+ Pos
1)) forall a b. (a -> b) -> a -> b
$! a
x
    else
      forall (m :: * -> *) a. Monad m => a -> m a
return []

  annotate :: forall a. (DocP -> DocP) -> Parser k r tok a -> Parser k r tok a
annotate DocP -> DocP
_ Parser k r tok a
p = Parser k r tok a
p

  memoiseIfPrinting :: (Eq k, Hashable k, Show k) =>
k -> Parser k r tok r -> Parser k r tok r
memoiseIfPrinting k
_ Parser k r tok r
p = Parser k r tok r
p

  memoise :: (Eq k, Hashable k, Show k) =>
k -> Parser k r tok r -> Parser k r tok r
memoise k
key Parser k r tok r
p = forall k r tok a.
(forall b.
 Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b])
-> Parser k r tok a
P forall a b. (a -> b) -> a -> b
$ \Array Pos tok
input Pos
i Cont k r tok b r
k -> do

    let alter :: Pos -> b -> (b -> b) -> IntMap b -> IntMap b
alter Pos
j b
zero b -> b
f IntMap b
m =
          forall a. (Maybe a -> Maybe a) -> Pos -> IntMap a -> IntMap a
IntMap.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe b
zero) Pos
j IntMap b
m

        lookupTable :: StateT
  (IntMap (HashMap k (Value k r tok b)))
  Identity
  (Maybe (Value k r tok b))
lookupTable   = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup k
key forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Pos -> IntMap a -> Maybe a
IntMap.lookup Pos
i) forall s (m :: * -> *). MonadState s m => m s
get
        insertTable :: Value k r tok b
-> StateT (IntMap (HashMap k (Value k r tok b))) Identity ()
insertTable Value k r tok b
v = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' forall a b. (a -> b) -> a -> b
$ forall {b}. Pos -> b -> (b -> b) -> IntMap b -> IntMap b
alter Pos
i forall k v. HashMap k v
Map.empty (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert k
key Value k r tok b
v)

    Maybe (Value k r tok b)
v <- StateT
  (IntMap (HashMap k (Value k r tok b)))
  Identity
  (Maybe (Value k r tok b))
lookupTable
    case Maybe (Value k r tok b)
v of
      Maybe (Value k r tok b)
Nothing -> do
        Value k r tok b
-> StateT (IntMap (HashMap k (Value k r tok b))) Identity ()
insertTable (forall k r tok b.
IntMap [r] -> [Cont k r tok b r] -> Value k r tok b
Value forall a. IntMap a
IntMap.empty [Cont k r tok b r
k])
        forall k r tok a.
Parser k r tok a
-> forall b.
   Array Pos tok -> Pos -> Cont k r tok b a -> M k r tok b [b]
unP Parser k r tok r
p Array Pos tok
input Pos
i forall a b. (a -> b) -> a -> b
$ \Pos
j r
r -> do
          ~(Just (Value IntMap [r]
rs [Cont k r tok b r]
ks)) <- StateT
  (IntMap (HashMap k (Value k r tok b)))
  Identity
  (Maybe (Value k r tok b))
lookupTable
          Value k r tok b
-> StateT (IntMap (HashMap k (Value k r tok b))) Identity ()
insertTable (forall k r tok b.
IntMap [r] -> [Cont k r tok b r] -> Value k r tok b
Value (forall {b}. Pos -> b -> (b -> b) -> IntMap b -> IntMap b
alter Pos
j [] (r
r forall a. a -> [a] -> [a]
:) IntMap [r]
rs) [Cont k r tok b r]
ks)
          forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Cont k r tok b r
k -> Cont k r tok b r
k Pos
j r
r) [Cont k r tok b r]
ks  -- See note [Reverse ks?].
      Just (Value IntMap [r]
rs [Cont k r tok b r]
ks) -> do
        Value k r tok b
-> StateT (IntMap (HashMap k (Value k r tok b))) Identity ()
insertTable (forall k r tok b.
IntMap [r] -> [Cont k r tok b r] -> Value k r tok b
Value IntMap [r]
rs (Cont k r tok b r
k forall a. a -> [a] -> [a]
: [Cont k r tok b r]
ks))
        forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Pos
i, [r]
rs) -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Cont k r tok b r
k Pos
i) [r]
rs) (forall a. IntMap a -> [(Pos, a)]
IntMap.toList IntMap [r]
rs)

-- [Reverse ks?]
--
-- If ks were reversed, then the code would be productive for some
-- infinitely ambiguous grammars, including S ∷= S | ε. However, in
-- some cases the results would not be fair (some valid results would
-- never be returned).

-- | An extended parser type, with some support for printing parsers.

data ParserWithGrammar k r tok a =
  PG (Bool -> Either (Parser k r tok a) (Docs k))
  -- ^ Invariant: If the boolean is 'True', then the result must be
  -- @'Left' something@, and if the boolean is 'False', then the
  -- result must be @'Right' something@.

-- | Documents paired with precedence levels.

type DocP = (Doc, Int)

-- | Precedence of @>>=@.

bindP :: Int
bindP :: Pos
bindP = Pos
10

-- | Precedence of @<|>@.

choiceP :: Int
choiceP :: Pos
choiceP = Pos
20

-- | Precedence of @<*>@.

seqP :: Int
seqP :: Pos
seqP = Pos
30

-- | Precedence of @⋆@ and @+@.

starP :: Int
starP :: Pos
starP = Pos
40

-- | Precedence of atoms.

atomP :: Int
atomP :: Pos
atomP = Pos
50

-- | The extended parser type computes one top-level document, plus
-- one document per encountered memoisation key.
--
-- 'Nothing' is used to mark that a given memoisation key has been
-- seen, but that no corresponding document has yet been stored.

type Docs k = State (HashMap k (Maybe DocP)) DocP

-- | A smart constructor.

pg :: Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg :: forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg Parser k r tok a
p Docs k
d = forall k r tok a.
(Bool -> Either (Parser k r tok a) (Docs k))
-> ParserWithGrammar k r tok a
PG forall a b. (a -> b) -> a -> b
$ \Bool
b -> if Bool
b then forall a b. a -> Either a b
Left Parser k r tok a
p else forall a b. b -> Either a b
Right Docs k
d

-- | Extracts the parser.

parser :: ParserWithGrammar k r tok a -> Parser k r tok a
parser :: forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser (PG Bool -> Either (Parser k r tok a) (Docs k)
p) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id forall a. HasCallStack => a
__IMPOSSIBLE__ (Bool -> Either (Parser k r tok a) (Docs k)
p Bool
True)

-- | Extracts the documents.

docs :: ParserWithGrammar k r tok a -> Docs k
docs :: forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs (PG Bool -> Either (Parser k r tok a) (Docs k)
p) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. HasCallStack => a
__IMPOSSIBLE__ forall a. a -> a
id (Bool -> Either (Parser k r tok a) (Docs k)
p Bool
False)

instance Monad (ParserWithGrammar k r tok) where
  return :: forall a. a -> ParserWithGrammar k r tok a
return  = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  ParserWithGrammar k r tok a
p >>= :: forall a b.
ParserWithGrammar k r tok a
-> (a -> ParserWithGrammar k r tok b)
-> ParserWithGrammar k r tok b
>>= a -> ParserWithGrammar k r tok b
f =
    forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ParserWithGrammar k r tok b
f)
       ((\(Doc
d, Pos
p) -> (Bool -> Doc -> Doc
mparens (Pos
p forall a. Ord a => a -> a -> Bool
< Pos
bindP) Doc
d Doc -> Doc -> Doc
<+> Doc
">>= ?", Pos
bindP))
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p)

instance Functor (ParserWithGrammar k r tok) where
  fmap :: forall a b.
(a -> b)
-> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b
fmap a -> b
f ParserWithGrammar k r tok a
p = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p)) (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p)

instance Applicative (ParserWithGrammar k r tok) where
  pure :: forall a. a -> ParserWithGrammar k r tok a
pure a
x    = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x) (forall (m :: * -> *) a. Monad m => a -> m a
return (Doc
"ε", Pos
atomP))
  ParserWithGrammar k r tok (a -> b)
p1 <*> :: forall a b.
ParserWithGrammar k r tok (a -> b)
-> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b
<*> ParserWithGrammar k r tok a
p2 =
    forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok (a -> b)
p1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p2)
       (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\(Doc
d1, Pos
p1) (Doc
d2, Pos
p2) ->
                   ([Doc] -> Doc
sep [ Bool -> Doc -> Doc
mparens (Pos
p1 forall a. Ord a => a -> a -> Bool
< Pos
seqP) Doc
d1
                        , Bool -> Doc -> Doc
mparens (Pos
p2 forall a. Ord a => a -> a -> Bool
< Pos
seqP) Doc
d2
                        ], Pos
seqP))
               (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok (a -> b)
p1) (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p2))

-- | A helper function.

starDocs :: String -> ParserWithGrammar k r tok a -> Docs k
starDocs :: forall k r tok a. String -> ParserWithGrammar k r tok a -> Docs k
starDocs String
s ParserWithGrammar k r tok a
p =
  (\(Doc
d, Pos
p) -> (Bool -> Doc -> Doc
mparens (Pos
p forall a. Ord a => a -> a -> Bool
< Pos
starP) Doc
d Doc -> Doc -> Doc
<+> String -> Doc
text String
s, Pos
starP)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p

instance Alternative (ParserWithGrammar k r tok) where
  empty :: forall a. ParserWithGrammar k r tok a
empty     = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg forall (f :: * -> *) a. Alternative f => f a
empty (forall (m :: * -> *) a. Monad m => a -> m a
return (Doc
"∅", Pos
atomP))
  ParserWithGrammar k r tok a
p1 <|> :: forall a.
ParserWithGrammar k r tok a
-> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a
<|> ParserWithGrammar k r tok a
p2 =
    forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p2)
       (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\(Doc
d1, Pos
p1) (Doc
d2, Pos
p2) ->
                   ([Doc] -> Doc
sep [ Bool -> Doc -> Doc
mparens (Pos
p1 forall a. Ord a => a -> a -> Bool
< Pos
choiceP) Doc
d1
                        , Doc
"|"
                        , Bool -> Doc -> Doc
mparens (Pos
p2 forall a. Ord a => a -> a -> Bool
< Pos
choiceP) Doc
d2
                        ], Pos
choiceP))
               (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p1) (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p2))

  many :: forall a.
ParserWithGrammar k r tok a -> ParserWithGrammar k r tok [a]
many ParserWithGrammar k r tok a
p = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p)) (forall k r tok a. String -> ParserWithGrammar k r tok a -> Docs k
starDocs String
"⋆" ParserWithGrammar k r tok a
p)
  some :: forall a.
ParserWithGrammar k r tok a -> ParserWithGrammar k r tok [a]
some ParserWithGrammar k r tok a
p = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p)) (forall k r tok a. String -> ParserWithGrammar k r tok a -> Docs k
starDocs String
"+" ParserWithGrammar k r tok a
p)

-- | Pretty-prints a memoisation key.

prettyKey :: Show k => k -> DocP
prettyKey :: forall k. Show k => k -> DocP
prettyKey k
key = (String -> Doc
text (String
"<" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show k
key forall a. [a] -> [a] -> [a]
++ String
">"), Pos
atomP)

-- | A helper function.

memoiseDocs ::
  (Eq k, Hashable k, Show k) =>
  k -> ParserWithGrammar k r tok r -> Docs k
memoiseDocs :: forall k r tok.
(Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> Docs k
memoiseDocs k
key ParserWithGrammar k r tok r
p = do
  Maybe (Maybe DocP)
r <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup k
key forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  case Maybe (Maybe DocP)
r of
    Just Maybe DocP
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (Maybe DocP)
Nothing -> do
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert k
key forall a. Maybe a
Nothing)
      DocP
d <- forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok r
p
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert k
key (forall a. a -> Maybe a
Just DocP
d))
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall k. Show k => k -> DocP
prettyKey k
key)

instance ParserClass (ParserWithGrammar k r tok) k r tok where
  parse :: forall a. ParserWithGrammar k r tok a -> [tok] -> [a]
parse ParserWithGrammar k r tok a
p                 = forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
p a -> [tok] -> [a]
parse (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p)
  sat' :: forall a. (tok -> Maybe a) -> ParserWithGrammar k r tok a
sat' tok -> Maybe a
p                  = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (p :: * -> *) k r tok a.
ParserClass p k r tok =>
(tok -> Maybe a) -> p a
sat' tok -> Maybe a
p) (forall (m :: * -> *) a. Monad m => a -> m a
return (Doc
"<sat ?>", Pos
atomP))
  annotate :: forall a.
(DocP -> DocP)
-> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a
annotate DocP -> DocP
f ParserWithGrammar k r tok a
p            = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok a
p) (DocP -> DocP
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p)
  memoise :: (Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r
memoise k
key ParserWithGrammar k r tok r
p           = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall (p :: * -> *) k r tok.
(ParserClass p k r tok, Eq k, Hashable k, Show k) =>
k -> p r -> p r
memoise k
key (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok r
p))
                               (forall k r tok.
(Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> Docs k
memoiseDocs k
key ParserWithGrammar k r tok r
p)
  memoiseIfPrinting :: (Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r
memoiseIfPrinting k
key ParserWithGrammar k r tok r
p = forall k r tok a.
Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg (forall k r tok a. ParserWithGrammar k r tok a -> Parser k r tok a
parser ParserWithGrammar k r tok r
p) (forall k r tok.
(Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> Docs k
memoiseDocs k
key ParserWithGrammar k r tok r
p)

  grammar :: forall a. Show k => ParserWithGrammar k r tok a -> Doc
grammar ParserWithGrammar k r tok a
p =
    Doc
d
      Doc -> Doc -> Doc
$+$
    Pos -> Doc -> Doc
nest Pos
2 (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Doc -> Doc -> Doc
($+$) forall a b. (a -> b) -> a -> b
$
      Doc
"where" forall a. a -> [a] -> [a]
:
      forall a b. (a -> b) -> [a] -> [b]
map (\(k
k, Maybe DocP
d) -> forall a b. (a, b) -> a
fst (forall k. Show k => k -> DocP
prettyKey k
k) Doc -> Doc -> Doc
<+> Doc
"∷=" Doc -> Doc -> Doc
<+>
                        forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a, b) -> a
fst Maybe DocP
d)
          (forall k v. HashMap k v -> [(k, v)]
Map.toList HashMap k (Maybe DocP)
ds))
    where
    ((Doc
d, Pos
_), HashMap k (Maybe DocP)
ds) = forall s a. State s a -> s -> (a, s)
runState (forall k r tok a. ParserWithGrammar k r tok a -> Docs k
docs ParserWithGrammar k r tok a
p) forall k v. HashMap k v
Map.empty