{-# LANGUAGE CPP, NoMonomorphismRestriction, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}
module Data.Logic.ATP.Parser where

-- Parsing expressions and statements
-- https://wiki.haskell.org/Parsing_expressions_and_statements

import Control.Monad.Identity
import Data.Char (isSpace)
import Data.List (nub)
import Data.String (fromString)
import Language.Haskell.TH.Quote (QuasiQuoter(..))
import Text.Parsec
import Text.Parsec.Error
import Text.Parsec.Expr
import Text.Parsec.Token
import Text.Parsec.Language
import Text.PrettyPrint.HughesPJClass (Pretty(pPrint), text)

import Data.Logic.ATP.Apply
import Data.Logic.ATP.Equate
import Data.Logic.ATP.Formulas
import Data.Logic.ATP.Lit
import Data.Logic.ATP.Prop
import Data.Logic.ATP.Quantified
import Data.Logic.ATP.Skolem
import Data.Logic.ATP.Term

instance Pretty ParseError where
    pPrint :: ParseError -> Doc
pPrint = String -> Doc
text (String -> Doc) -> (ParseError -> String) -> ParseError -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> String
forall a. Show a => a -> String
show

instance Pretty Message where
    pPrint :: Message -> Doc
pPrint (SysUnExpect String
s) = String -> Doc
text (String
"SysUnExpect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s)
    pPrint (UnExpect String
s) = String -> Doc
text (String
"UnExpect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s)
    pPrint (Expect String
s) = String -> Doc
text (String
"Expect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s)
    pPrint (Message String
s) = String -> Doc
text (String
"Message " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s)

-- | QuasiQuote for a first order formula.  Loading this symbol into the interpreter
-- and setting -XQuasiQuotes lets you type expressions like [fof| ∃ x. p(x) |]
fof :: QuasiQuoter
fof :: QuasiQuoter
fof = QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = \String
str -> [| (either (error . show) id . parseFOL) str :: Formula |]
    , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"fof does not implement quoteType"
    , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"fof does not implement quotePat"
    , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"fof does not implement quoteDec"
    }

-- | QuasiQuote for a propositional formula.  Exactly like fof, but no quantifiers.
pf :: QuasiQuoter
pf :: QuasiQuoter
pf = QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = \String
str -> [| (either (error . show) id . parsePL) str :: PFormula EqAtom |]
    , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"pf does not implement quoteType"
    , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"pf does not implement quotePat"
    , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"pf does not implement quoteDec"
    }

-- | QuasiQuote for a propositional formula.  Exactly like fof, but no quantifiers.
lit :: QuasiQuoter
lit :: QuasiQuoter
lit = QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = \String
str -> [| (either (error . show) id . parseLit) str :: LFormula EqAtom |]
    , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"pf does not implement quoteType"
    , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"pf does not implement quotePat"
    , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"pf does not implement quoteDec"
    }

-- | QuasiQuote for a propositional formula.  Exactly like fof, but no quantifiers.
term :: QuasiQuoter
term :: QuasiQuoter
term = QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = \String
str -> [| (either (error . show) id . parseFOLTerm) str :: FTerm |]
    , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"term does not implement quoteType"
    , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"term does not implement quotePat"
    , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"term does not implement quoteDec"
    }

#if 0
instance Read PrologRule where
   readsPrec _n str = [(parseProlog str,"")]

instance Read Formula where
   readsPrec _n str = [(parseFOL str,"")]

instance Read (PFormula EqAtom) where
   readsPrec _n str = [(parsePL str,"")]

parseProlog :: forall s. Stream s Identity Char => s -> PrologRule
parseProlog str = either (error . show) id $ parse prologparser "" str
#endif
parseFOL :: Stream String Identity Char => String -> Either ParseError Formula
parseFOL :: Stream String Identity Char => String -> Either ParseError Formula
parseFOL String
str = Parsec String () Formula
-> String -> String -> Either ParseError Formula
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () Formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
folparser String
"" ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
str)
parsePL :: Stream String Identity Char => String -> Either ParseError (PFormula EqAtom)
parsePL :: Stream String Identity Char =>
String -> Either ParseError (PFormula EqAtom)
parsePL String
str = Parsec String () (PFormula EqAtom)
-> String -> String -> Either ParseError (PFormula EqAtom)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (PFormula EqAtom)
forall formula s u (m :: * -> *).
(JustPropositional formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
propparser String
"" ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
str)
parseLit :: Stream String Identity Char => String -> Either ParseError (LFormula EqAtom)
parseLit :: Stream String Identity Char =>
String -> Either ParseError (LFormula EqAtom)
parseLit String
str = Parsec String () (LFormula EqAtom)
-> String -> String -> Either ParseError (LFormula EqAtom)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (LFormula EqAtom)
forall formula s u (m :: * -> *).
(JustLiteral formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
litparser String
"" ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
str)
parseFOLTerm :: Stream String Identity Char => String -> Either ParseError FTerm
parseFOLTerm :: Stream String Identity Char =>
String -> Either ParseError (Term FName V)
parseFOLTerm String
str = Parsec String () (Term FName V)
-> String -> String -> Either ParseError (Term FName V)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (Term FName V)
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm String
"" ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
str)

def :: forall s u m. Stream s m Char => GenLanguageDef s u m
def :: forall s u (m :: * -> *). Stream s m Char => GenLanguageDef s u m
def = LanguageDef Any
forall st. LanguageDef st
emptyDef{ identStart = letter
              , identLetter = alphaNum <|> oneOf "'"
              , opStart = oneOf (nub (map head allOps))
              , opLetter = oneOf (nub (concat (map tail allOps)))
              , reservedOpNames = allOps
              , reservedNames = allIds
              }

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 ()
TokenParser{ parens :: forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens = forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens
           , angles :: forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
angles = forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_angles
--           , brackets = m_brackets
           , symbol :: forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m String
symbol = String -> ParsecT t t1 t2 String
m_symbol
           , integer :: forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m Integer
integer = ParsecT t t1 t2 Integer
m_integer
           , identifier :: forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier = ParsecT t t1 t2 String
m_identifier
           , reservedOp :: forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp = String -> ParsecT t t1 t2 ()
m_reservedOp
           , reserved :: forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved = String -> ParsecT t t1 t2 ()
m_reserved
--           , semiSep1 = m_semiSep1
           , whiteSpace :: forall s u (m :: * -> *). GenTokenParser s u m -> ParsecT s u m ()
whiteSpace = ParsecT t t1 t2 ()
m_whiteSpace } = GenLanguageDef t t1 t2 -> GenTokenParser t t1 t2
forall s (m :: * -> *) u.
Stream s m Char =>
GenLanguageDef s u m -> GenTokenParser s u m
makeTokenParser GenLanguageDef t t1 t2
forall s u (m :: * -> *). Stream s m Char => GenLanguageDef s u m
def

#if 0
prologparser :: forall s u m. Stream s m Char => ParsecT s u m PrologRule
prologparser = try (do
   left <- folparser
   m_symbol ":-"
   right <- sepBy folparser (m_symbol ",")
   return (Prolog right left))
   <|> (do
   left <- folparser
   return (Prolog [] left))
   <?> "prolog expression"
#endif

litparser :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
litparser :: forall formula s u (m :: * -> *).
(JustLiteral formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
litparser = ParsecT s u m formula -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsLiteral formula, Stream s m Char) =>
ParsecT s u m formula -> ParsecT s u m formula
litexprparser ParsecT s u m formula
forall formula s u (m :: * -> *).
(JustLiteral formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
litterm
propparser :: forall formula s u m. (JustPropositional 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
propparser = ParsecT s u m formula -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsPropositional formula, Stream s m Char) =>
ParsecT s u m formula -> ParsecT s u m formula
propexprparser ParsecT s u m formula
forall formula s u (m :: * -> *).
(JustPropositional formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
propterm
folparser :: forall formula s u m. (IsQuantified 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
folparser = ParsecT s u m formula -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsPropositional formula, Stream s m Char) =>
ParsecT s u m formula -> ParsecT s u m formula
propexprparser ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
folterm

litexprparser :: forall formula s u m. (IsLiteral formula, Stream s m Char) => ParsecT s u m formula -> 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
litexprparser ParsecT s u m formula
trm = OperatorTable s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s (m :: * -> *) t u a.
Stream s m t =>
OperatorTable s u m a -> ParsecT s u m a -> ParsecT s u m a
buildExpressionParser OperatorTable s u m formula
forall {s} {m :: * -> *} {a} {u}.
(Stream s m Char, IsLiteral a) =>
[[Operator s u m a]]
table ParsecT s u m formula
trm ParsecT s u m formula -> String -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"lit"
 where
  table :: [[Operator s u m a]]
table = [ [ParsecT s u m (a -> a) -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Prefix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"~" ParsecT s u m ()
-> ParsecT s u m (a -> a) -> ParsecT s u m (a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a) -> ParsecT s u m (a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a
forall formula. IsLiteral formula => formula -> formula
(.~.))]
          ]

propexprparser :: forall formula s u m. (IsPropositional 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
propexprparser ParsecT s u m formula
trm = OperatorTable s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s (m :: * -> *) t u a.
Stream s m t =>
OperatorTable s u m a -> ParsecT s u m a -> ParsecT s u m a
buildExpressionParser OperatorTable s u m formula
forall {s} {m :: * -> *} {a} {u}.
(Stream s m Char, IsPropositional a) =>
[[Operator s u m a]]
table ParsecT s u m formula
trm ParsecT s u m formula -> String -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"prop"
 where
  table :: [[Operator s u m a]]
table = [ (String -> Operator s u m a) -> [String] -> [Operator s u m a]
forall a b. (a -> b) -> [a] -> [b]
map (\String
op -> ParsecT s u m (a -> a) -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Prefix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op ParsecT s u m ()
-> ParsecT s u m (a -> a) -> ParsecT s u m (a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a) -> ParsecT s u m (a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a
forall formula. IsLiteral formula => formula -> formula
(.~.))) [String]
notOps
          , (String -> Operator s u m a) -> [String] -> [Operator s u m a]
forall a b. (a -> b) -> [a] -> [b]
map (\String
op -> ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.)) Assoc
AssocRight) [String]
andOps -- should these be assocLeft?
          , (String -> Operator s u m a) -> [String] -> [Operator s u m a]
forall a b. (a -> b) -> [a] -> [b]
map (\String
op -> ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.)) Assoc
AssocRight) [String]
orOps
          , (String -> Operator s u m a) -> [String] -> [Operator s u m a]
forall a b. (a -> b) -> [a] -> [b]
map (\String
op -> ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.)) Assoc
AssocRight) [String]
impOps
          , (String -> Operator s u m a) -> [String] -> [Operator s u m a]
forall a b. (a -> b) -> [a] -> [b]
map (\String
op -> ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.)) Assoc
AssocRight) [String]
iffOps
          ]

litterm :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => 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
litterm = ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m formula -> ParsecT s u m formula
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens ParsecT s u m formula
forall formula s u (m :: * -> *).
(JustLiteral formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
litparser)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate_infix
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueOps)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseOps)

propterm :: forall formula s u m. (JustPropositional 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
propterm = ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m formula -> ParsecT s u m formula
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens ParsecT s u m formula
forall formula s u (m :: * -> *).
(JustPropositional formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
propparser)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate_infix
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueOps)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseOps)

folterm :: forall formula s u m. (IsQuantified 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
folterm = ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m formula -> ParsecT s u m formula
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
folparser)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate_infix
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) =>
ParsecT s u m formula
folpredicate
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
existentialQuantifier
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
forallQuantifier
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
true) [String]
trueOps)
       ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
s ParsecT s u m () -> ParsecT s u m formula -> ParsecT s u m formula
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
forall formula. IsFormula formula => formula
false) [String]
falseOps)

existentialQuantifier :: 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
existentialQuantifier = (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
s -> String -> (String -> formula -> formula) -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
String -> (String -> formula -> formula) -> ParsecT s u m formula
quantifierId String
s (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists (VarOf formula -> formula -> formula)
-> (String -> VarOf formula) -> String -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VarOf formula
forall a. IsString a => String -> a
fromString)) [String]
existsIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
s -> String -> (String -> formula -> formula) -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
String -> (String -> formula -> formula) -> ParsecT s u m formula
quantifierOp String
s (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists (VarOf formula -> formula -> formula)
-> (String -> VarOf formula) -> String -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VarOf formula
forall a. IsString a => String -> a
fromString)) [String]
existsOps)
forallQuantifier :: 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
forallQuantifier = (ParsecT s u m formula
 -> ParsecT s u m formula -> ParsecT s u m formula)
-> [ParsecT s u m formula] -> ParsecT s u m formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ParsecT s u m formula
-> ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
(<|>) ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
s -> String -> (String -> formula -> formula) -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
String -> (String -> formula -> formula) -> ParsecT s u m formula
quantifierId String
s (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all (VarOf formula -> formula -> formula)
-> (String -> VarOf formula) -> String -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VarOf formula
forall a. IsString a => String -> a
fromString)) [String]
forallIds [ParsecT s u m formula]
-> [ParsecT s u m formula] -> [ParsecT s u m formula]
forall a. [a] -> [a] -> [a]
++ (String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
s -> String -> (String -> formula -> formula) -> ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
String -> (String -> formula -> formula) -> ParsecT s u m formula
quantifierOp String
s (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all (VarOf formula -> formula -> formula)
-> (String -> VarOf formula) -> String -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VarOf formula
forall a. IsString a => String -> a
fromString)) [String]
forallOps)

quantifierId :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) =>
              String -> (String -> formula -> formula) -> 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
quantifierId String
name String -> formula -> formula
op = do
   String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
name
   [String]
is <- ParsecT s u m String -> ParsecT s u m [String]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier
   String
_ <- String -> ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 String
m_symbol String
"."
   formula
fm <- ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
folparser
   formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> formula -> formula) -> formula -> [String] -> formula
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> formula -> formula
op formula
fm [String]
is)

quantifierOp :: 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
quantifierOp String
name String -> formula -> formula
op = do
   String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
name
   [String]
is <- ParsecT s u m String -> ParsecT s u m [String]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier
   String
_ <- String -> ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 String
m_symbol String
"."
   formula
fm <- ParsecT s u m formula
forall formula s u (m :: * -> *).
(IsQuantified formula, HasEquate (AtomOf formula),
 Stream s m Char) =>
ParsecT s u m formula
folparser
   formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> formula -> formula) -> formula -> [String] -> formula
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> formula -> formula
op formula
fm [String]
is)

folpredicate_infix :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => 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_infix = [ParsecT s u m formula] -> ParsecT s u m formula
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> ParsecT s u m formula)
-> [String] -> [ParsecT s u m formula]
forall a b. (a -> b) -> [a] -> [b]
map (ParsecT s u m formula -> ParsecT s u m formula
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m formula -> ParsecT s u m formula)
-> (String -> ParsecT s u m formula)
-> String
-> ParsecT s u m formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ParsecT s u m formula
forall {b} {s} {m :: * -> *} {u}.
(Stream s m Char, IsFormula b, HasEquate (AtomOf b)) =>
String -> ParsecT s u m b
app) [String]
predicate_infix_symbols)
 where
  app :: String -> ParsecT s u m b
app String
op = do
   TermOf (AtomOf b)
x <- ParsecT s u m (TermOf (AtomOf b))
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm
   String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
op
   TermOf (AtomOf b)
y <- ParsecT s u m (TermOf (AtomOf b))
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm
   b -> ParsecT s u m b
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (if String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
op [String]
equateOps then TermOf (AtomOf b)
x TermOf (AtomOf b) -> TermOf (AtomOf b) -> b
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. TermOf (AtomOf b)
y else PredOf (AtomOf b) -> [TermOf (AtomOf b)] -> b
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (String -> PredOf (AtomOf b)
forall a. IsString a => String -> a
fromString String
op) [TermOf (AtomOf b)
x, TermOf (AtomOf b)
y])

folpredicate :: 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
folpredicate = do
   String
p <- ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier ParsecT s u m String
-> ParsecT s u m String -> ParsecT s u m String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 String
m_symbol String
"|--"
   [TermOf (AtomOf formula)]
xs <- [TermOf (AtomOf formula)]
-> ParsecT s u m [TermOf (AtomOf formula)]
-> ParsecT s u m [TermOf (AtomOf formula)]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (ParsecT s u m [TermOf (AtomOf formula)]
-> ParsecT s u m [TermOf (AtomOf formula)]
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens (ParsecT s u m (TermOf (AtomOf formula))
-> ParsecT s u m String -> ParsecT s u m [TermOf (AtomOf formula)]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT s u m (TermOf (AtomOf formula))
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm (String -> ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 String
m_symbol String
",")))
   formula -> ParsecT s u m formula
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PredOf (AtomOf formula) -> [TermOf (AtomOf formula)] -> formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (String -> PredOf (AtomOf formula)
forall a. IsString a => String -> a
fromString String
p) [TermOf (AtomOf formula)]
xs)

folfunction :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folfunction :: forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folfunction = do
   String
fname <- ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier
   [term]
xs <- ParsecT s u m [term] -> ParsecT s u m [term]
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens (ParsecT s u m term -> ParsecT s u m String -> ParsecT s u m [term]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm (String -> ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 String
m_symbol String
","))
   term -> ParsecT s u m term
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf term
forall a. IsString a => String -> a
fromString String
fname) [term]
xs)

folconstant_numeric :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
folconstant_numeric :: forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folconstant_numeric = do
   Integer
i <- ParsecT t t1 t2 Integer
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 Integer
m_integer
   term -> ParsecT t t1 t2 term
forall a. a -> ParsecT t t1 t2 a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf term
forall a. IsString a => String -> a
fromString (String -> FunOf term)
-> (Integer -> String) -> Integer -> FunOf term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show (Integer -> FunOf term) -> Integer -> FunOf term
forall a b. (a -> b) -> a -> b
$ Integer
i) [])

folconstant_reserved :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => String -> 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_reserved String
str = do
   String -> ParsecT t t1 t2 ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reserved String
str
   term -> ParsecT t t1 t2 term
forall a. a -> ParsecT t t1 t2 a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf term
forall a. IsString a => String -> a
fromString String
str) [])

folconstant :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
folconstant :: forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folconstant = do
   String
name <- ParsecT t t1 t2 String -> ParsecT t t1 t2 String
forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_angles ParsecT t t1 t2 String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier
   term -> ParsecT t t1 t2 term
forall a. a -> ParsecT t t1 t2 a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf term
forall a. IsString a => String -> a
fromString String
name) [])

folsubterm :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folsubterm :: forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm = ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folfunction_infix ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm_prefix

folsubterm_prefix :: 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
folsubterm_prefix =
   ParsecT s u m term -> ParsecT s u m term
forall a. ParsecT s u m a -> ParsecT s u m a
forall t t1 (t2 :: * -> *) a.
Stream t t2 Char =>
ParsecT t t1 t2 a -> ParsecT t t1 t2 a
m_parens ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folfunction_infix
   ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folfunction
   ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [ParsecT s u m term] -> ParsecT s u m term
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> ParsecT s u m term) -> [String] -> [ParsecT s u m term]
forall a b. (a -> b) -> [a] -> [b]
map String -> ParsecT s u m term
forall term t t1 (t2 :: * -> *).
(IsTerm term, Stream t t2 Char) =>
String -> ParsecT t t1 t2 term
folconstant_reserved [String]
constants)
   ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folconstant_numeric
   ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folconstant
   ParsecT s u m term -> ParsecT s u m term -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((String -> term) -> ParsecT s u m String -> ParsecT s u m term
forall a b. (a -> b) -> ParsecT s u m a -> ParsecT s u m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (TVarOf term -> term) -> (String -> TVarOf term) -> String -> term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TVarOf term
forall a. IsString a => String -> a
fromString) ParsecT s u m String
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
ParsecT t t1 t2 String
m_identifier)

folfunction_infix :: 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
folfunction_infix = OperatorTable s u m term
-> ParsecT s u m term -> ParsecT s u m term
forall s (m :: * -> *) t u a.
Stream s m t =>
OperatorTable s u m a -> ParsecT s u m a -> ParsecT s u m a
buildExpressionParser OperatorTable s u m term
forall {s} {m :: * -> *} {a} {u}.
(Stream s m Char, IsTerm a) =>
[[Operator s u m a]]
table ParsecT s u m term
forall term s u (m :: * -> *).
(IsTerm term, Stream s m Char) =>
ParsecT s u m term
folsubterm_prefix ParsecT s u m term -> String -> ParsecT s u m term
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"fof"
 where
  table :: [[Operator s u m a]]
table = [ [ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"::" ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (\a
x a
y -> FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf a
forall a. IsString a => String -> a
fromString String
"::") [a
x,a
y])) Assoc
AssocRight]
          , [ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"*" ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (\a
x a
y -> FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf a
forall a. IsString a => String -> a
fromString String
"*") [a
x,a
y])) Assoc
AssocLeft, ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"/" ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (\a
x a
y -> FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf a
forall a. IsString a => String -> a
fromString String
"/") [a
x,a
y])) Assoc
AssocLeft]
          , [ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"+" ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (\a
x a
y -> FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf a
forall a. IsString a => String -> a
fromString String
"+") [a
x,a
y])) Assoc
AssocLeft, ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> ParsecT s u m ()
forall t t1 (t2 :: * -> *).
Stream t t2 Char =>
String -> ParsecT t t1 t2 ()
m_reservedOp String
"-" ParsecT s u m ()
-> ParsecT s u m (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a b. ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a) -> ParsecT s u m (a -> a -> a)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (\a
x a
y -> FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> FunOf a
forall a. IsString a => String -> a
fromString String
"-") [a
x,a
y])) Assoc
AssocLeft]
          ]

allOps :: [String]
allOps :: [String]
allOps = [String]
notOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
trueOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
falseOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
andOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
orOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
impOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
iffOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
         [String]
forallOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
existsOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
equateOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
provesOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
entailsOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
predicate_infix_symbols

allIds :: [String]
allIds :: [String]
allIds = [String]
trueIds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
falseIds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
existsIds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
forallIds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
constants

predicate_infix_symbols :: [String]
predicate_infix_symbols :: [String]
predicate_infix_symbols = [String]
equateOps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"<",String
">",String
"<=",String
">="]

constants :: [[Char]]
constants :: [String]
constants = [String
"nil"]

equateOps :: [String]
equateOps = [String
"=", String
".=."]
provesOps :: [String]
provesOps = [String
"⊢", String
"|--"]
entailsOps :: [String]
entailsOps = [String
"⊨", String
"|=="]

notOps :: [String]
notOps :: [String]
notOps = [String
"¬", String
"~", String
".~."]

trueOps, trueIds, falseOps, falseIds, provesOps, entailsOps, equateOps :: [String]
trueOps :: [String]
trueOps = [String
"⊤"]
trueIds :: [String]
trueIds = [String
"True", String
"true"]
falseOps :: [String]
falseOps = [String
"⊥"]
falseIds :: [String]
falseIds = [String
"False", String
"false"]

andOps, orOps, impOps, iffOps :: [String]
andOps :: [String]
andOps = [String
".&.", String
"&", String
"∧", String
"⋀", String
"/\\", String
"·"]
orOps :: [String]
orOps = [String
"|", String
"∨", String
"⋁", String
"+", String
".|.", String
"\\/"]
impOps :: [String]
impOps = [String
"==>", String
"⇒", String
"⟹", String
".=>.", String
"→", String
"⊃"]
iffOps :: [String]
iffOps = [String
"<==>", String
"⇔", String
".<=>.", String
"↔"]

forallIds, forallOps, existsIds, existsOps :: [String]
forallIds :: [String]
forallIds = [String
"forall", String
"for_all"]
forallOps :: [String]
forallOps= [String
"∀"]
existsIds :: [String]
existsIds = [String
"exists"]
existsOps :: [String]
existsOps = [String
"∃"]