    ------------------------------------------------------------------------
    -- | The parser monad used by the operator parser
    ------------------------------------------------------------------------

    {-# LANGUAGE CPP #-}

    module Agda.Syntax.Concrete.Operators.Parser.Monad
      ( MemoKey(..), PrecedenceKey
      , Parser
      , parse
      , sat'
      , sat
      , doc
      , memoise
      , memoiseIfPrinting
      , grammar
      ) where

    import Data.Hashable
    import GHC.Generics (Generic)
    import Text.PrettyPrint.HughesPJ

    import Agda.Syntax.Common
    import qualified Agda.Utils.Parser.MemoisedCPS as Parser

    -- | Memoisation keys.

    data MemoKey = NodeK      PrecedenceKey
                 | PostLeftsK PrecedenceKey
                 | PreRightsK PrecedenceKey
                 | TopK
                 | AppK
                 | NonfixK
      deriving (MemoKey -> MemoKey -> Bool
    (MemoKey -> MemoKey -> Bool)
    -> (MemoKey -> MemoKey -> Bool) -> Eq MemoKey
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: MemoKey -> MemoKey -> Bool
    $c/= :: MemoKey -> MemoKey -> Bool
    == :: MemoKey -> MemoKey -> Bool
    $c== :: MemoKey -> MemoKey -> Bool
    Eq, Int -> MemoKey -> ShowS
    [MemoKey] -> ShowS
    MemoKey -> String
    (Int -> MemoKey -> ShowS)
    -> (MemoKey -> String) -> ([MemoKey] -> ShowS) -> Show MemoKey
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [MemoKey] -> ShowS
    $cshowList :: [MemoKey] -> ShowS
    show :: MemoKey -> String
    $cshow :: MemoKey -> String
    showsPrec :: Int -> MemoKey -> ShowS
    $cshowsPrec :: Int -> MemoKey -> ShowS
    Show, (forall x. MemoKey -> Rep MemoKey x)
    -> (forall x. Rep MemoKey x -> MemoKey) -> Generic MemoKey
    forall x. Rep MemoKey x -> MemoKey
    forall x. MemoKey -> Rep MemoKey x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep MemoKey x -> MemoKey
    $cfrom :: forall x. MemoKey -> Rep MemoKey x
    Generic)

    type PrecedenceKey = Either PrecedenceLevel PrecedenceLevel

    instance Hashable MemoKey

    -- | The parser monad.

    type Parser tok a =
    #ifdef DEBUG
      Parser.ParserWithGrammar
    #else
      Parser.Parser
    #endif
        MemoKey tok (MaybePlaceholder tok) a

    -- | Runs the parser.

    parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
    parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
    parse = Parser MemoKey tok (MaybePlaceholder tok) a
    -> [MaybePlaceholder tok] -> [a]
    forall (p :: * -> *) k r tok a.
    ParserClass p k r tok =>
    p a -> [tok] -> [a]
    Parser.parse

    -- | Parses a token satisfying the given predicate. The computed value
    -- is returned.

    sat' :: (MaybePlaceholder tok -> Maybe a) -> Parser tok a
    sat' :: forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
    sat' = (MaybePlaceholder tok -> Maybe a)
    -> Parser MemoKey tok (MaybePlaceholder tok) a
    forall (p :: * -> *) k r tok a.
    ParserClass p k r tok =>
    (tok -> Maybe a) -> p a
    Parser.sat'

    -- | Parses a token satisfying the given predicate.

    sat :: (MaybePlaceholder tok -> Bool) ->
           Parser tok (MaybePlaceholder tok)
    sat :: forall tok.
    (MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)
    sat = (MaybePlaceholder tok -> Bool)
    -> Parser MemoKey tok (MaybePlaceholder tok) (MaybePlaceholder tok)
    forall (p :: * -> *) k r tok.
    ParserClass p k r tok =>
    (tok -> Bool) -> p tok
    Parser.sat

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

    doc :: Doc -> Parser tok a -> Parser tok a
    doc :: forall tok a. Doc -> Parser tok a -> Parser tok a
    doc = Doc
    -> Parser MemoKey tok (MaybePlaceholder tok) a
    -> Parser MemoKey tok (MaybePlaceholder tok) a
    forall (p :: * -> *) k r tok a.
    ParserClass p k r tok =>
    Doc -> p a -> p a
    Parser.doc

    -- | Memoises the given parser.
    --
    -- Every memoised parser must be annotated with a /unique/ key.
    -- (Parametrised parsers must use distinct keys for distinct inputs.)

    memoise :: MemoKey -> Parser tok tok -> Parser tok tok
    memoise :: forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise = MemoKey
    -> Parser MemoKey tok (MaybePlaceholder tok) tok
    -> Parser MemoKey tok (MaybePlaceholder tok) tok
    forall (p :: * -> *) k r tok.
    (ParserClass p k r tok, Eq k, Hashable k, Show k) =>
    k -> p r -> p r
    Parser.memoise

    -- | 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 :: MemoKey -> Parser tok tok -> Parser tok tok
    memoiseIfPrinting :: forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoiseIfPrinting = MemoKey
    -> Parser MemoKey tok (MaybePlaceholder tok) tok
    -> Parser MemoKey tok (MaybePlaceholder tok) tok
    forall (p :: * -> *) k r tok.
    (ParserClass p k r tok, Eq k, Hashable k, Show k) =>
    k -> p r -> p r
    Parser.memoiseIfPrinting

    -- | Tries to print the parser, or returns 'empty', depending on the
    -- implementation. This function might not terminate.

    grammar :: Parser tok a -> Doc
    grammar :: forall tok a. Parser tok a -> Doc
    grammar = Parser MemoKey tok (MaybePlaceholder tok) a -> Doc
    forall (p :: * -> *) k r tok a.
    (ParserClass p k r tok, Show k) =>
    p a -> Doc
    Parser.grammar