Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

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

Documentation

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

Monad (Parser k r tok) Source 
Functor (Parser k r tok) Source 
Applicative (Parser k r tok) Source 
Alternative (Parser k r tok) Source 

parse :: Parser k r tok a -> [tok] -> [a] Source

Runs the parser.

token :: Parser k r tok tok Source

Parses a single token.

tok :: Eq tok => tok -> Parser k r tok tok Source

Parses a given token.

sat :: (tok -> Bool) -> Parser k r tok tok Source

Parses a token satisfying the given predicate.

chainl1 Source

Arguments

:: Parser k r tok a

Parser for a thing.

-> Parser k r tok (a -> a -> a)

Parser for a separator.

-> Parser k r tok a 

Parses one or more things, separated by separators.

Combines the results in a left-associative way.

chainr1 Source

Arguments

:: Parser k r tok a

Parser for a thing.

-> Parser k r tok (a -> a -> a)

Parser for a separator.

-> Parser k r tok a 

Parses one or more things, separated by separators.

Combines the results in a right-associative way.

memoise :: (Eq k, Hashable k) => k -> Parser k r tok r -> Parser k r tok 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.)