Copyright | (c) 2017 2018 N Steenbergen |
---|---|
License | GPL-3 |
Maintainer | ns@slak.ws |
Stability | experimental |
Safe Haskell | Safe |
Language | Haskell2010 |
Attoparsec-based parser for various logical (sub)structures.
- class Parseable a where
- parse :: (Monad m, Parseable a) => Text -> m a
- formula :: Parser ext -> Parser (Formula ext)
- modality :: Parser Modality
- justification :: Parser Justification
- quantifier :: Parser Quantifier
- named :: Parser x -> Parser (String, x)
- marked :: Parser formula -> Parser (Marked formula)
- identifier :: Parser String
- boolean :: Parser Bool
- comments :: Parser ()
- data Operator a
- expression :: [[Operator a]] -> Parser a -> Parser a
- ambiguity :: [Parser a] -> Parser [a]
Parser typeclass
class Parseable a where Source #
A Parseable is something with an associated Attoparsec Parser
.
A parser for type a
.
parserEmbedded :: Parser a Source #
In some cases, the parser for a type must be embellished with some other symbols when it occurs as part of a parser of a different type, but not when it occurs on its own. This parser allows us to specify this alternative.
Parseable Justification Source # | |
Parseable Modality Source # | |
Parseable Quantifier Source # | |
Parseable Classical Source # | |
Parseable f => Parseable [f] Source # | |
Parseable e => Parseable (Ambiguous (Term e)) Source # | |
Parseable f => Parseable (Marked f) Source # | |
Parseable e => Parseable (Formula e) Source # | |
Formula parsers
formula :: Parser ext -> Parser (Formula ext) Source #
Builds a parser for formulas of classical propositional logic extended
with some type e
.
justification :: Parser Justification Source #
Parser for justification terms of justification logic.
quantifier :: Parser Quantifier Source #
Parser for quantifiers of first-order predicate logic.
Auxiliary parsers
named :: Parser x -> Parser (String, x) Source #
Make a parser for something that is named by prepending it with an identifier and a = sign.
identifier :: Parser String Source #
Parser that accepts and returns any string that starts with a letter.
Generic parser building
Operators wrap a parser for a function in additional information. Note that the function they wrap must take arguments of the same type.