module Data.Logic.ATP.Parser where
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 = text . show
instance Pretty Message where
pPrint (SysUnExpect s) = text ("SysUnExpect " ++ show s)
pPrint (UnExpect s) = text ("UnExpect " ++ show s)
pPrint (Expect s) = text ("Expect " ++ show s)
pPrint (Message s) = text ("Message " ++ show s)
fof :: QuasiQuoter
fof = QuasiQuoter
{ quoteExp = \str -> [| (either (error . show) id . parseFOL) str :: Formula |]
, quoteType = error "fof does not implement quoteType"
, quotePat = error "fof does not implement quotePat"
, quoteDec = error "fof does not implement quoteDec"
}
pf :: QuasiQuoter
pf = QuasiQuoter
{ quoteExp = \str -> [| (either (error . show) id . parsePL) str :: PFormula EqAtom |]
, quoteType = error "pf does not implement quoteType"
, quotePat = error "pf does not implement quotePat"
, quoteDec = error "pf does not implement quoteDec"
}
lit :: QuasiQuoter
lit = QuasiQuoter
{ quoteExp = \str -> [| (either (error . show) id . parseLit) str :: LFormula EqAtom |]
, quoteType = error "pf does not implement quoteType"
, quotePat = error "pf does not implement quotePat"
, quoteDec = error "pf does not implement quoteDec"
}
term :: QuasiQuoter
term = QuasiQuoter
{ quoteExp = \str -> [| (either (error . show) id . parseFOLTerm) str :: FTerm |]
, quoteType = error "term does not implement quoteType"
, quotePat = error "term does not implement quotePat"
, quoteDec = error "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 str = parse folparser "" (dropWhile isSpace str)
parsePL :: Stream String Identity Char => String -> Either ParseError (PFormula EqAtom)
parsePL str = parse propparser "" (dropWhile isSpace str)
parseLit :: Stream String Identity Char => String -> Either ParseError (LFormula EqAtom)
parseLit str = parse litparser "" (dropWhile isSpace str)
parseFOLTerm :: Stream String Identity Char => String -> Either ParseError FTerm
parseFOLTerm str = parse folsubterm "" (dropWhile isSpace str)
def :: forall s u m. Stream s m Char => GenLanguageDef s u m
def = 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 = m_parens
, angles = m_angles
, symbol = m_symbol
, integer = m_integer
, identifier = m_identifier
, reservedOp = m_reservedOp
, reserved = m_reserved
, whiteSpace = m_whiteSpace } = makeTokenParser 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 = litexprparser litterm
propparser :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
propparser = propexprparser propterm
folparser :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
folparser = propexprparser folterm
litexprparser :: forall formula s u m. (IsLiteral formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
litexprparser trm = buildExpressionParser table trm <?> "lit"
where
table = [ [Prefix (m_reservedOp "~" >> return (.~.))]
]
propexprparser :: forall formula s u m. (IsPropositional formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
propexprparser trm = buildExpressionParser table trm <?> "prop"
where
table = [ map (\op -> Prefix (m_reservedOp op >> return (.~.))) notOps
, map (\op -> Infix (m_reservedOp op >> return (.&.)) AssocRight) andOps
, map (\op -> Infix (m_reservedOp op >> return (.|.)) AssocRight) orOps
, map (\op -> Infix (m_reservedOp op >> return (.=>.)) AssocRight) impOps
, map (\op -> Infix (m_reservedOp op >> return (.<=>.)) AssocRight) iffOps
]
litterm :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
litterm = try (m_parens litparser)
<|> try folpredicate_infix
<|> folpredicate
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return true) trueIds ++ map (\s -> m_reservedOp s >> return true) trueOps)
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return false) falseIds ++ map (\s -> m_reservedOp s >> return false) falseOps)
propterm :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
propterm = try (m_parens propparser)
<|> try folpredicate_infix
<|> folpredicate
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return true) trueIds ++ map (\s -> m_reservedOp s >> return true) trueOps)
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return false) falseIds ++ map (\s -> m_reservedOp s >> return false) falseOps)
folterm :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
folterm = try (m_parens folparser)
<|> try folpredicate_infix
<|> folpredicate
<|> existentialQuantifier
<|> forallQuantifier
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return true) trueIds ++ map (\s -> m_reservedOp s >> return true) trueOps)
<|> foldr1 (<|>) (map (\s -> m_reserved s >> return false) falseIds ++ map (\s -> m_reservedOp s >> return false) falseOps)
existentialQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
existentialQuantifier = foldr1 (<|>) (map (\ s -> quantifierId s (exists . fromString)) existsIds ++ map (\ s -> quantifierOp s (exists . fromString)) existsOps)
forallQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
forallQuantifier = foldr1 (<|>) (map (\ s -> quantifierId s (for_all . fromString)) forallIds ++ map (\ s -> quantifierOp s (for_all . fromString)) 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 name op = do
m_reserved name
is <- many1 m_identifier
_ <- m_symbol "."
fm <- folparser
return (foldr op fm 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 name op = do
m_reservedOp name
is <- many1 m_identifier
_ <- m_symbol "."
fm <- folparser
return (foldr op fm is)
folpredicate_infix :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
folpredicate_infix = choice (map (try . app) predicate_infix_symbols)
where
app op = do
x <- folsubterm
m_reservedOp op
y <- folsubterm
return (if elem op equateOps then x .=. y else pApp (fromString op) [x, y])
folpredicate :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
folpredicate = do
p <- m_identifier <|> m_symbol "|--"
xs <- option [] (m_parens (sepBy1 folsubterm (m_symbol ",")))
return (pApp (fromString p) xs)
folfunction :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folfunction = do
fname <- m_identifier
xs <- m_parens (sepBy1 folsubterm (m_symbol ","))
return (fApp (fromString fname) xs)
folconstant_numeric :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
folconstant_numeric = do
i <- m_integer
return (fApp (fromString . show $ i) [])
folconstant_reserved :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => String -> ParsecT t t1 t2 term
folconstant_reserved str = do
m_reserved str
return (fApp (fromString str) [])
folconstant :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
folconstant = do
name <- m_angles m_identifier
return (fApp (fromString name) [])
folsubterm :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folsubterm = folfunction_infix <|> folsubterm_prefix
folsubterm_prefix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folsubterm_prefix =
m_parens folfunction_infix
<|> try folfunction
<|> choice (map folconstant_reserved constants)
<|> folconstant_numeric
<|> folconstant
<|> (fmap (vt . fromString) m_identifier)
folfunction_infix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
folfunction_infix = buildExpressionParser table folsubterm_prefix <?> "fof"
where
table = [ [Infix (m_reservedOp "::" >> return (\x y -> fApp (fromString "::") [x,y])) AssocRight]
, [Infix (m_reservedOp "*" >> return (\x y -> fApp (fromString "*") [x,y])) AssocLeft, Infix (m_reservedOp "/" >> return (\x y -> fApp (fromString "/") [x,y])) AssocLeft]
, [Infix (m_reservedOp "+" >> return (\x y -> fApp (fromString "+") [x,y])) AssocLeft, Infix (m_reservedOp "-" >> return (\x y -> fApp (fromString "-") [x,y])) AssocLeft]
]
allOps :: [String]
allOps = notOps ++ trueOps ++ falseOps ++ andOps ++ orOps ++ impOps ++ iffOps ++
forallOps ++ existsOps ++ equateOps ++ provesOps ++ entailsOps ++ predicate_infix_symbols
allIds :: [String]
allIds = trueIds ++ falseIds ++ existsIds ++ forallIds ++ constants
predicate_infix_symbols :: [String]
predicate_infix_symbols = equateOps ++ ["<",">","<=",">="]
constants :: [[Char]]
constants = ["nil"]
equateOps = ["=", ".=."]
provesOps = ["⊢", "|--"]
entailsOps = ["⊨", "|=="]
notOps :: [String]
notOps = ["¬", "~", ".~."]
trueOps, trueIds, falseOps, falseIds, provesOps, entailsOps, equateOps :: [String]
trueOps = ["⊤"]
trueIds = ["True", "true"]
falseOps = ["⊥"]
falseIds = ["False", "false"]
andOps, orOps, impOps, iffOps :: [String]
andOps = [".&.", "&", "∧", "⋀", "/\\", "·"]
orOps = ["|", "∨", "⋁", "+", ".|.", "\\/"]
impOps = ["==>", "⇒", "⟹", ".=>.", "→", "⊃"]
iffOps = ["<==>", "⇔", ".<=>.", "↔"]
forallIds, forallOps, existsIds, existsOps :: [String]
forallIds = ["forall", "for_all"]
forallOps= ["∀"]
existsIds = ["exists"]
existsOps = ["∃"]