Data.Expression.Parser

Documentation

type Context = Map String DynamicSort

Parsing context assigning sorts to known variables

type Parser = ReaderT Context (StateT Context Parser)

Context-sensitive parser that remembers sorts of variables

class Parseable f g where

Expressions that can be parsed

Minimal complete definition

parser

Methods

parser :: Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

Instances

(:<:) Sort ArrayF f => Parseable ((Sort -> *) -> Sort -> *) ArrayF f

Methods

parser :: Proxy ArrayF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort ArithmeticF f => Parseable ((Sort -> *) -> Sort -> *) ArithmeticF f

Methods

parser :: Proxy ArithmeticF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort NegationF f => Parseable ((Sort -> *) -> Sort -> *) NegationF f

Methods

parser :: Proxy NegationF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort DisjunctionF f => Parseable ((Sort -> *) -> Sort -> *) DisjunctionF f

Methods

parser :: Proxy DisjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort ConjunctionF f => Parseable ((Sort -> *) -> Sort -> *) ConjunctionF f

Methods

parser :: Proxy ConjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort (EqualityF Sort) f => Parseable ((k -> *) -> Sort -> *) (EqualityF k) f

Methods

parser :: Proxy (EqualityF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f

Methods

parser :: Proxy (ExistentialF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f

Methods

parser :: Proxy (UniversalF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f

Methods

parser :: Proxy (VarF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(Parseable (k1 -> k -> *) f h, Parseable (k1 -> k -> *) g h) => Parseable (k1 -> k -> *) ((:+:) k k1 f g) h

Methods

parser :: Proxy ((k :+: k1) f g) h -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

parse :: forall f s. (Parseable f f, SingI s) => Text -> Maybe (IFix f s)

Tries to parse the entire input text and produce an expression in desired language and with desired sort.

parseWith :: forall f s. (Parseable f f, SingI s) => Context -> Text -> Maybe (IFix f s)

Like parse but allows adding initial assumption about sorts of some variables.

char :: Char -> Parser Char

Matches a given character.

choice :: [Parser a] -> Parser a

Matches first of many choices.

decimal :: Parser Int

Matches a given decimal number.

digit :: Parser Char

Matches a given digit.

letter :: Parser Char

Matches any character.

many1 :: Parser a -> Parser [a]

Matches one or more times.

sepBy1 :: Parser a -> Parser s -> Parser [a]

Matches one or more times, separated by specified separator.

signed :: Parser Int -> Parser Int

Matches a signed number.

space :: Parser Char

Matches space.

string :: Text -> Parser Text

Matches a given string.

identifier :: Parser String

Matches identifier that starts with [a-zA-Z'_#] and is followed by [a-zA-Z'_#0-9].

(<?>) :: Parser a -> String -> Parser a

Labels parser.

assertSort :: String -> DynamicSort -> Parser ()

Asserts what sort is assigned to a variable in current context.

assumeSort :: String -> Parser DynamicSort

Variable assumes sort based on current context.