{-# OPTIONS_GHC -Wunused-imports #-}
{-# 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 Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import qualified Agda.Utils.Parser.MemoisedCPS as Parser
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
$c== :: MemoKey -> MemoKey -> Bool
== :: MemoKey -> MemoKey -> Bool
$c/= :: MemoKey -> MemoKey -> Bool
/= :: 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
$cshowsPrec :: Int -> MemoKey -> ShowS
showsPrec :: Int -> MemoKey -> ShowS
$cshow :: MemoKey -> String
show :: MemoKey -> String
$cshowList :: [MemoKey] -> ShowS
showList :: [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
$cfrom :: forall x. MemoKey -> Rep MemoKey x
from :: forall x. MemoKey -> Rep MemoKey x
$cto :: forall x. Rep MemoKey x -> MemoKey
to :: forall x. Rep MemoKey x -> MemoKey
Generic)
type PrecedenceKey = Either PrecedenceLevel PrecedenceLevel
instance Hashable MemoKey
type Parser tok a =
#ifdef DEBUG_PARSING
Parser.ParserWithGrammar
#else
Parser.Parser
#endif
MemoKey tok (MaybePlaceholder tok) a
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 a.
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
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 a.
(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'
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
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
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
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
grammar :: Parser tok a -> Doc
grammar :: forall tok a. Parser tok a -> Doc
grammar = Parser MemoKey tok (MaybePlaceholder tok) a -> Doc
forall a.
Show MemoKey =>
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