Data.Logic.ATP.Parser

Documentation

fof :: QuasiQuoter

QuasiQuote for a first order formula. Loading this symbol into the interpreter and setting -XQuasiQuotes lets you type expressions like [fof| ∃ x. p(x) |]

pf :: QuasiQuoter

QuasiQuote for a propositional formula. Exactly like fof, but no quantifiers.

lit :: QuasiQuoter

QuasiQuote for a propositional formula. Exactly like fof, but no quantifiers.

term :: QuasiQuoter

QuasiQuote for a propositional formula. Exactly like fof, but no quantifiers.

parseFOL :: Stream String Identity Char => String -> Either ParseError Formula

parsePL :: Stream String Identity Char => String -> Either ParseError (PFormula EqAtom)

parseLit :: Stream String Identity Char => String -> Either ParseError (LFormula EqAtom)

parseFOLTerm :: Stream String Identity Char => String -> Either ParseError FTerm

def :: forall s u m. Stream s m Char => GenLanguageDef s u m

m_parens :: forall t t1 t2. Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a

m_angles :: forall t t1 t2. Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a

m_symbol :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 String

m_integer :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 Integer

m_identifier :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 String

m_reservedOp :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 ()

m_reserved :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 ()

m_whiteSpace :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 ()

litparser :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

propparser :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

folparser :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

litexprparser :: forall formula s u m. (IsLiteral formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula

propexprparser :: forall formula s u m. (IsPropositional formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula

litterm :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

propterm :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

folterm :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

existentialQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

forallQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

quantifierId :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula

quantifierOp :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula

folpredicate_infix :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

folpredicate :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula

folfunction :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term

folconstant_numeric :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term

folconstant_reserved :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => String -> ParsecT t t1 t2 term

folconstant :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term

folsubterm :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term

folsubterm_prefix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term

folfunction_infix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term

allOps :: [String]

allIds :: [String]

predicate_infix_symbols :: [String]

constants :: [[Char]]

notOps :: [String]

trueOps :: [String]

trueIds :: [String]

falseOps :: [String]

falseIds :: [String]

provesOps :: [String]

entailsOps :: [String]

equateOps :: [String]

andOps :: [String]

orOps :: [String]

impOps :: [String]

iffOps :: [String]

forallIds :: [String]

forallOps :: [String]

existsIds :: [String]

existsOps :: [String]