atp-haskell-1.14.3: Translation from Ocaml to Haskell of John Harrison's ATP code
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Logic.ATP.Parser

Synopsis

Documentation

fof :: QuasiQuoter Source #

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 Source #

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

lit :: QuasiQuoter Source #

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

term :: QuasiQuoter Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Orphan instances