Safe Haskell	None
Language	Haskell2010

Agda.Utils.Parser.MemoisedCPS

Description

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.)

Synopsis

class (Functor p, Applicative p, Alternative p, Monad p) => ParserClass (p :: Type -> Type) k r tok | p -> k, p -> r, p -> tok where
- parse :: p a -> [tok] -> [a]
- grammar :: Show k => p a -> Doc
- sat' :: (tok -> Maybe a) -> p a
- annotate :: (DocP -> DocP) -> p a -> p a
- memoise :: k -> p r -> p r
- memoiseIfPrinting :: k -> p r -> p r
sat :: ParserClass p k r tok => (tok -> Bool) -> p tok
token :: ParserClass p k r tok => p tok
tok :: (ParserClass p k r tok, Eq tok, Show tok) => tok -> p tok
doc :: ParserClass p k r tok => Doc -> p a -> p a
type DocP = (Doc, Int)
bindP :: Int
choiceP :: Int
seqP :: Int
starP :: Int
atomP :: Int
data Parser k r tok a
data ParserWithGrammar k r tok a

Documentation

class (Functor p, Applicative p, Alternative p, Monad p) => ParserClass (p :: Type -> Type) k r tok | p -> k, p -> r, p -> tok where Source #

Methods

parse :: p a -> [tok] -> [a] Source #

Runs the parser.

grammar :: Show k => p a -> Doc Source #

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

sat' :: (tok -> Maybe a) -> p a Source #

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

annotate :: (DocP -> DocP) -> p a -> p a Source #

Uses the given function to modify the printed representation (if any) of the given parser.

memoise :: k -> p r -> p r Source #

Memoises the given parser.

Every memoised parser must be annotated with a unique key. (Parametrised parsers must use distinct keys for distinct inputs.)

memoiseIfPrinting :: k -> p r -> p r Source #

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.)

Instances

Instances details

ParserClass (Parser k r tok) k r tok Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods parse :: Parser k r tok a -> [tok] -> [a] Source # grammar :: Show k => Parser k r tok a -> Doc Source # sat' :: (tok -> Maybe a) -> Parser k r tok a Source # annotate :: (DocP -> DocP) -> Parser k r tok a -> Parser k r tok a Source # memoise :: k -> Parser k r tok r -> Parser k r tok r Source # memoiseIfPrinting :: k -> Parser k r tok r -> Parser k r tok r Source #
ParserClass (ParserWithGrammar k r tok) k r tok Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods parse :: ParserWithGrammar k r tok a -> [tok] -> [a] Source # grammar :: Show k => ParserWithGrammar k r tok a -> Doc Source # sat' :: (tok -> Maybe a) -> ParserWithGrammar k r tok a Source # annotate :: (DocP -> DocP) -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a Source # memoise :: k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r Source # memoiseIfPrinting :: k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r Source #

sat :: ParserClass p k r tok => (tok -> Bool) -> p tok Source #

Parses a token satisfying the given predicate.

token :: ParserClass p k r tok => p tok Source #

Parses a single token.

tok :: (ParserClass p k r tok, Eq tok, Show tok) => tok -> p tok Source #

Parses a given token.

doc :: ParserClass p k r tok => Doc -> p a -> p a Source #

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

type DocP = (Doc, Int) Source #

Documents paired with precedence levels.

bindP :: Int Source #

Precedence of >>=.

choiceP :: Int Source #

Precedence of |.

seqP :: Int Source #

Precedence of *.

starP :: Int Source #

Precedence of ⋆ and +.

atomP :: Int Source #

Precedence of atoms.

data Parser k r tok a Source #

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.

Instances

Instances details

Alternative (Parser k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods empty :: Parser k r tok a (<\|>) :: Parser k r tok a -> Parser k r tok a -> Parser k r tok a some :: Parser k r tok a -> Parser k r tok [a] many :: Parser k r tok a -> Parser k r tok [a]
Applicative (Parser k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods pure :: a -> Parser k r tok a (<>) :: Parser k r tok (a -> b) -> Parser k r tok a -> Parser k r tok b # liftA2 :: (a -> b -> c) -> Parser k r tok a -> Parser k r tok b -> Parser k r tok c (>) :: Parser k r tok a -> Parser k r tok b -> Parser k r tok b (<*) :: Parser k r tok a -> Parser k r tok b -> Parser k r tok a
Functor (Parser k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods fmap :: (a -> b) -> Parser k r tok a -> Parser k r tok b (<$) :: a -> Parser k r tok b -> Parser k r tok a #
Monad (Parser k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods (>>=) :: Parser k r tok a -> (a -> Parser k r tok b) -> Parser k r tok b (>>) :: Parser k r tok a -> Parser k r tok b -> Parser k r tok b return :: a -> Parser k r tok a
ParserClass (Parser k r tok) k r tok Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods parse :: Parser k r tok a -> [tok] -> [a] Source # grammar :: Show k => Parser k r tok a -> Doc Source # sat' :: (tok -> Maybe a) -> Parser k r tok a Source # annotate :: (DocP -> DocP) -> Parser k r tok a -> Parser k r tok a Source # memoise :: k -> Parser k r tok r -> Parser k r tok r Source # memoiseIfPrinting :: k -> Parser k r tok r -> Parser k r tok r Source #

data ParserWithGrammar k r tok a Source #

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

Instances

Instances details

Alternative (ParserWithGrammar k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods empty :: ParserWithGrammar k r tok a (<\|>) :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a some :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok [a] many :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok [a]
Applicative (ParserWithGrammar k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods pure :: a -> ParserWithGrammar k r tok a (<>) :: ParserWithGrammar k r tok (a -> b) -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b # liftA2 :: (a -> b -> c) -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b -> ParserWithGrammar k r tok c (>) :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b -> ParserWithGrammar k r tok b (<*) :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b -> ParserWithGrammar k r tok a
Functor (ParserWithGrammar k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods fmap :: (a -> b) -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b (<$) :: a -> ParserWithGrammar k r tok b -> ParserWithGrammar k r tok a #
Monad (ParserWithGrammar k r tok) Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods (>>=) :: ParserWithGrammar k r tok a -> (a -> ParserWithGrammar k r tok b) -> ParserWithGrammar k r tok b (>>) :: ParserWithGrammar k r tok a -> ParserWithGrammar k r tok b -> ParserWithGrammar k r tok b return :: a -> ParserWithGrammar k r tok a
ParserClass (ParserWithGrammar k r tok) k r tok Source #
Instance details Defined in Agda.Utils.Parser.MemoisedCPS Methods parse :: ParserWithGrammar k r tok a -> [tok] -> [a] Source # grammar :: Show k => ParserWithGrammar k r tok a -> Doc Source # sat' :: (tok -> Maybe a) -> ParserWithGrammar k r tok a Source # annotate :: (DocP -> DocP) -> ParserWithGrammar k r tok a -> ParserWithGrammar k r tok a Source # memoise :: k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r Source # memoiseIfPrinting :: k -> ParserWithGrammar k r tok r -> ParserWithGrammar k r tok r Source #