Copyright | (C) 2017-18 Jakub Daniel |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Jakub Daniel <jakub.daniel@protonmail.com> |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
- type Context = Map String DynamicSort
- type Parser = ReaderT Context (StateT Context Parser)
- class Parseable f g where
- parse :: forall f s. (Parseable f f, SingI s) => Text -> Maybe (IFix f s)
- parseWith :: forall f s. (Parseable f f, SingI s) => Context -> Text -> Maybe (IFix f s)
- char :: Char -> Parser Char
- choice :: [Parser a] -> Parser a
- decimal :: Parser Int
- digit :: Parser Char
- letter :: Parser Char
- many1 :: Parser a -> Parser [a]
- sepBy1 :: Parser a -> Parser s -> Parser [a]
- signed :: Parser Int -> Parser Int
- space :: Parser Char
- string :: Text -> Parser Text
- identifier :: Parser String
- (<?>) :: Parser a -> String -> Parser a
- assertSort :: String -> DynamicSort -> Parser ()
- assumeSort :: String -> Parser DynamicSort
Documentation
type Parser = ReaderT Context (StateT Context Parser) Source #
Context-sensitive parser that remembers sorts of variables
class Parseable f g where Source #
Expressions that can be parsed
parser :: Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort ArrayF f => Parseable ((Sort -> *) -> Sort -> *) ArrayF f Source # | |
(:<:) Sort ArithmeticF f => Parseable ((Sort -> *) -> Sort -> *) ArithmeticF f Source # | |
(:<:) Sort NegationF f => Parseable ((Sort -> *) -> Sort -> *) NegationF f Source # | |
(:<:) Sort DisjunctionF f => Parseable ((Sort -> *) -> Sort -> *) DisjunctionF f Source # | |
(:<:) Sort ConjunctionF f => Parseable ((Sort -> *) -> Sort -> *) ConjunctionF f Source # | |
(:<:) Sort (EqualityF Sort) f => Parseable ((k -> *) -> Sort -> *) (EqualityF k) f Source # | |
((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f Source # | |
((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f Source # | |
(:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f Source # | |
(Parseable (k1 -> k -> *) f h, Parseable (k1 -> k -> *) g h) => Parseable (k1 -> k -> *) ((:+:) k k1 f g) h Source # | |
parse :: forall f s. (Parseable f f, SingI s) => Text -> Maybe (IFix f s) Source #
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) Source #
Like parse
but allows adding initial assumption about sorts of some variables.
sepBy1 :: Parser a -> Parser s -> Parser [a] Source #
Matches one or more times, separated by specified separator.
identifier :: Parser String Source #
Matches identifier that starts with [a-zA-Z'_#] and is followed by [a-zA-Z'_
#0-9].
assertSort :: String -> DynamicSort -> Parser () Source #
Asserts what sort is assigned to a variable in current context.
assumeSort :: String -> Parser DynamicSort Source #
Variable assumes sort based on current context.