Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Internal.Utils.Parser

Contents

The Parser type
Running a parser
Parser constructors
Parser combinators

Description

Provides a lightweight, general-purpose parser type and some related combinators.

The API is deliberately nearly a subset of the parsec API. One big difference is the behavior of the Alternative instace; our instance always backtracks, so there is no need for a try function.

Synopsis

data Parser a
parse :: Parser a -> String -> Maybe a
charIf :: (Char -> Bool) -> Parser Char
char :: Char -> Parser Char
anyChar :: Parser Char
oneOf :: [Char] -> Parser Char
string :: String -> Parser String
spaces :: Parser String
between :: Parser b -> Parser c -> Parser a -> Parser a
sepBy :: Parser a -> Parser b -> Parser [a]
sepBy1 :: Parser a -> Parser b -> Parser [a]
chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a
chainr1 :: Parser a -> Parser (a -> a -> a) -> Parser a
notFollowedBy :: Parser a -> Parser ()
eof :: Parser ()

The Parser type

data Parser a Source #

The Parser type is a simple state monad with state type String and inner monad Maybe.

Instances

Instances details

Monad Parser Source #
Instance details Defined in AutoProof.Internal.Utils.Parser.Types Methods (>>=) :: Parser a -> (a -> Parser b) -> Parser b # (>>) :: Parser a -> Parser b -> Parser b # return :: a -> Parser a #
Functor Parser Source #
Instance details Defined in AutoProof.Internal.Utils.Parser.Types Methods fmap :: (a -> b) -> Parser a -> Parser b # (<$) :: a -> Parser b -> Parser a #
Applicative Parser Source #
Instance details Defined in AutoProof.Internal.Utils.Parser.Types Methods pure :: a -> Parser a # (<>) :: Parser (a -> b) -> Parser a -> Parser b # liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c # (>) :: Parser a -> Parser b -> Parser b # (<*) :: Parser a -> Parser b -> Parser a #
Alternative Parser Source #
Instance details Defined in AutoProof.Internal.Utils.Parser.Types Methods empty :: Parser a # (<\|>) :: Parser a -> Parser a -> Parser a # some :: Parser a -> Parser [a] # many :: Parser a -> Parser [a] #

Running a parser

parse :: Parser a -> String -> Maybe a Source #

Run a parser on a string, discarding any unparsed suffix

Parser constructors

charIf :: (Char -> Bool) -> Parser Char Source #

Parse a single character if it satisfies a predicate

Examples

Expand

>>> runParser (charIf isDigit) "123"
Just ("23",'1')

>>> runParser (charIf isDigit) "abc"
Nothing

char :: Char -> Parser Char Source #

Parse a specific character.

Examples

Expand

>>> runParser (char 'a') "abc"
Just ("bc",'a')

>>> runParser (char 'a') "def"
Nothing

anyChar :: Parser Char Source #

Parse any character.

Examples

Expand

>>> runParser anyChar "abc"
Just ("bc",'a')

>>> runParser anyChar ""
Nothing

oneOf :: [Char] -> Parser Char Source #

Parse one out of a list of characters.

Examples

Expand

>>> runParser (oneOf ['a', 'b']) "bar"
Just ("ar",'b')

>>> runParser (oneOf ['a', 'b']) "foo"
Nothing

string :: String -> Parser String Source #

Parse a specific string.

Examples

Expand

>>> runParser (string "foo") "foobar"
Just ("bar","foo")

>>> runParser (string "foo") "fobar"
Nothing

spaces :: Parser String Source #

Parse zero or more spaces.

Examples

Expand

>>> runParser spaces "   123"
Just ("123","   ")

>>> runParser spaces "123"
Just ("123","")

>>> runParser spaces ""
Just ("","")

Parser combinators

between :: Parser b -> Parser c -> Parser a -> Parser a Source #

(between open close p) runs open, then p, then close, returning the value parsed by p.

sepBy :: Parser a -> Parser b -> Parser [a] Source #

(sepBy p sep) runs zero or more occurrences of p, separated by sep, returning the list of values parsed by p.

sepBy1 :: Parser a -> Parser b -> Parser [a] Source #

(sepBy1 p sep) runs one or more occurrences of p, separated by sep, returning the list of values parsed by p.

chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a Source #

(chainl1 p op) runs one or more occurrences of p, separated by op, returning the value obtained by a left-associative application of the functions parsed by op to the values parsed by p.

chainr1 :: Parser a -> Parser (a -> a -> a) -> Parser a Source #

(chainr1 p op) runs one or more occurrences of p, separated by op, returning the value obtained by a right-associative application of the functions parsed by op to the values parsed by p.

notFollowedBy :: Parser a -> Parser () Source #

(notFollowedBy p) succeeds if and only if p fails.

eof :: Parser () Source #

(eof) (end-of-file) only succeeds at the end of input.