summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs')
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs100
1 files changed, 100 insertions, 0 deletions
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs
new file mode 100644
index 0000000..2c0dfc6
--- /dev/null
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs
@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+-- | The parser monad used by the operator parser
+------------------------------------------------------------------------
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Agda.Syntax.Concrete.Operators.Parser.Monad
+ ( MemoKey(..)
+ , Parser
+ , parse
+ , token
+ , sat
+ , tok
+ , annotate
+ , 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 (Either Integer Integer)
+ | PostLeftsK (Either Integer Integer)
+ | PreRightsK (Either Integer Integer)
+ | TopK
+ | AppK
+ | NonfixK
+ deriving (Eq, Show, Generic)
+
+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 = Parser.parse
+
+-- | Parses a single token.
+
+token :: Parser tok (MaybePlaceholder tok)
+token = Parser.token
+
+-- | Parses a token satisfying the given predicate.
+
+sat :: (MaybePlaceholder tok -> Bool) ->
+ Parser tok (MaybePlaceholder tok)
+sat = Parser.sat
+
+-- | Parses a given token.
+
+tok :: (Eq tok, Show tok) =>
+ MaybePlaceholder tok -> Parser tok (MaybePlaceholder tok)
+tok = Parser.tok
+
+-- | Uses the given function to modify the printed representation (if
+-- any) of the given parser.
+
+annotate :: (Doc -> Doc) -> Parser tok a -> Parser tok a
+annotate = Parser.annotate
+
+-- | 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 = 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 = 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 = Parser.grammar