DFGParser.hs revision 7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f
{- |
Module : ./SoftFOL/DFGParser.hs
Description : A parser for the SPASS Input Syntax
Copyright : (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
A parser for the SPASS Input Syntax taken from
-}
module SoftFOL.DFGParser (parseSPASS) where
import SoftFOL.Sign
import Common.AS_Annotation
import Common.Id
import Common.Lexer hiding (parens)
import Common.Parsec
import Control.Monad
import Data.Char (isSpace)
import Data.Maybe
import qualified Data.Map as Map
-- * lexical matter
wordChar :: Parser Char
wordChar = alphaNum <|> oneOf "_"
anyWord :: Parser String
anyWord = do
c <- wordChar
r <- many wordChar
whiteSpace
return $ c : r
reservedList :: [String]
reservedList = ["end_of_list", "sort", "subsort", "predicate"]
identifierS :: Parser String
identifierS = try $ anyWord >>=
(\ s -> if elem s reservedList then unexpected $ show s else return s)
identifierT :: Parser Token
identifierT = liftM2 (\ p s -> Token s (Range [p])) getPos identifierS
arityT :: Parser Int
arityT = fmap read $ many1 digit <|> try (string "-1" << notFollowedBy digit)
commentLine :: Parser ()
commentLine = forget $ char '%' >> manyTill anyChar newline
whiteSpace :: Parser ()
whiteSpace = skipMany $ forget (satisfy isSpace) <|> commentLine
symbolT :: String -> Parser String
symbolT = (<< whiteSpace) . tryString
keywordT :: String -> Parser String
keywordT s = try (string s << notFollowedBy wordChar) << whiteSpace
dot :: Parser String
dot = symbolT "."
comma :: Parser String
comma = symbolT ","
commaSep :: Parser a -> Parser [a]
commaSep p = sepBy1 p comma
parens :: Parser a -> Parser a
parens p = symbolT "(" >> p << symbolT ")"
squares :: Parser a -> Parser a
squares p = symbolT "[" >> p << symbolT "]"
parensDot :: Parser a -> Parser a
parensDot p = symbolT "(" >> p << symbolT ")."
squaresDot :: Parser a -> Parser a
squaresDot p = symbolT "[" >> p << symbolT "]."
text :: Parser String
text = fmap (reverse . dropWhile isSpace . reverse) $
symbolT "{*" >> manyTill anyChar (symbolT "*}")
listOf :: String -> Parser String
listOf = symbolT . ("list_of_" ++)
listOfDot :: String -> Parser String
listOfDot = listOf . (++ ".")
endOfList :: Parser String
endOfList = symbolT "end_of_list."
mapTokensToData :: [(String, a)] -> Parser a
mapTokensToData ls = choice (map tokenToData ls)
where tokenToData (s, t) = keywordT s >> return t
{- * SPASS Problem
This is the main function of the module
-}
parseSPASS :: Parser SPProblem
parseSPASS = whiteSpace >> problem
problem :: Parser SPProblem
problem = do
symbolT "begin_problem"
i <- parensDot identifierS
dl <- descriptionList
lp <- logicalPartP
s <- settingList
symbolT "end_problem."
many anyChar
eof
return SPProblem
{ identifier = i
, description = dl
, logicalPart = lp
, settings = s}
-- ** SPASS Descriptions
{- | A description is mandatory for a SPASS problem. It has to specify
at least a 'name', the name of the 'author', the 'status' (see also
'SPLogState' below), and a (verbose) description. -}
descriptionList :: Parser SPDescription
descriptionList = do
listOfDot "descriptions"
keywordT "name"
n <- parensDot text
keywordT "author"
a <- parensDot text
v <- optionMaybe (keywordT "version" >> parensDot text)
l <- optionMaybe (keywordT "logic" >> parensDot text)
s <- keywordT "status" >> parensDot (mapTokensToData
[ ("satisfiable", SPStateSatisfiable)
, ("unsatisfiable", SPStateUnsatisfiable)
, ("unknown", SPStateUnknown)])
keywordT "description"
de <- parensDot text
da <- optionMaybe (keywordT "date" >> parensDot text)
endOfList
return SPDescription
{ name = n
, author = a
, version = v
, logic = l
, status = s
, desc = de
, date = da }
-- ** SPASS Logical Parts
{- |
A SPASS logical part consists of a symbol list, a declaration list, and a
set of formula lists. Support for clause lists and proof lists hasn't
been implemented yet.
-}
logicalPartP :: Parser SPLogicalPart
logicalPartP = do
sl <- optionMaybe symbolListP
dl <- optionMaybe declarationListP
fs <- many formulaList
cl <- many clauseList
pl <- many proofList
return SPLogicalPart
{ symbolList = sl
, declarationList = dl
, formulaLists = fs
, clauseLists = cl
, proofLists = pl }
-- *** Symbol List
{- |
SPASS Symbol List
-}
symbolListP :: Parser SPSymbolList
symbolListP = do
listOfDot "symbols"
fs <- optionL (signSymFor "functions")
ps <- optionL (signSymFor "predicates")
ss <- optionL sortSymFor
endOfList
return emptySymbolList
{ functions = fs
, predicates = ps
, sorts = ss }
signSymFor :: String -> Parser [SPSignSym]
signSymFor kind = keywordT kind >> squaresDot
(commaSep $ parens signSym <|> fmap SPSimpleSignSym identifierT)
sortSymFor :: Parser [SPSignSym]
sortSymFor = keywordT "sorts" >> squaresDot
(commaSep $ fmap SPSimpleSignSym identifierT)
signSym :: Parser SPSignSym
signSym = do
s <- identifierT
comma
a <- arityT
return SPSignSym {sym = s, arity = a}
functList :: Parser [SPIdentifier]
functList = squaresDot $ commaSep identifierT
-- *** Formula List
{- |
SPASS Formula List
-}
formulaList :: Parser SPFormulaList
formulaList = do
listOf "formulae"
ot <- parensDot $ mapTokensToData
[ ("axioms", SPOriginAxioms)
, ("conjectures", SPOriginConjectures)]
fs <- many $ formula $ case ot of
SPOriginAxioms -> True
_ -> False
endOfList
return SPFormulaList { originType = ot, formulae = fs }
clauseList :: Parser SPClauseList
clauseList = do
listOf "clauses"
(ot, ct) <- parensDot $ do
ot <- mapTokensToData
[ ("axioms", SPOriginAxioms)
, ("conjectures", SPOriginConjectures)]
comma
ct <- mapTokensToData [("cnf", SPCNF), ("dnf", SPDNF)]
return (ot, ct)
fs <- many $ clause ct $ case ot of
SPOriginAxioms -> True
_ -> False
endOfList
return SPClauseList
{ coriginType = ot
, clauseType = ct
, clauses = fs }
clause :: SPClauseType -> Bool -> Parser SPClause
clause ct bool = keywordT "clause" >> parensDot (do
sen <- clauseFork ct
cname <- optionL (comma >> identifierS)
return (makeNamed cname sen) { isAxiom = bool })
clauseFork :: SPClauseType -> Parser NSPClause
clauseFork ct = do
termWsList1@(TWL ls b) <- termWsList
do symbolT "||"
termWsList2 <- termWsList
symbolT "->"
termWsList3 <- termWsList
return (BriefClause termWsList1 termWsList2 termWsList3)
<|> case ls of
[t] | not b -> toNSPClause ct t
_ -> unexpected "clause term"
toNSPClause :: Monad m => SPClauseType -> SPTerm -> m NSPClause
toNSPClause ct t = case t of
SPQuantTerm q vl l | q == SPForall && ct == SPCNF
|| q == SPExists && ct == SPDNF -> do
b <- toClauseBody ct l
return $ QuanClause vl b
_ -> do
b <- toClauseBody ct t
return $ SimpleClause b
termWsList :: Parser TermWsList
termWsList = do
twl <- many term
p <- optionMaybe (symbolT "+")
return $ TWL twl $ isJust p
formula :: Bool -> Parser (Named SoftFOL.Sign.SPTerm)
formula bool = keywordT "formula" >> parensDot (do
sen <- term
fname <- optionL (comma >> identifierS)
return (makeNamed fname sen) { isAxiom = bool })
declarationListP :: Parser [SPDeclaration]
declarationListP = do
listOfDot "declarations"
decl <- many declaration
endOfList
return decl
declaration :: Parser SPDeclaration
declaration = do
keywordT "sort"
sortName <- identifierT
maybeFreely <- option False (keywordT "freely" >> return True)
keywordT "generated by"
funList <- functList
return SPGenDecl
{ sortSym = sortName
, freelyGenerated = maybeFreely
, funcList = funList }
<|> do
keywordT "subsort"
(s1, s2) <- parensDot $ do
s1 <- identifierT
comma
s2 <- identifierT
return (s1, s2)
return SPSubsortDecl { sortSymA = s1, sortSymB = s2 }
<|> do
keywordT "predicate"
(pn, sl) <- parensDot $ do
pn <- identifierT
comma
sl <- commaSep identifierT
return (pn, sl)
return SPPredDecl { predSym = pn, sortSyms = sl }
<|> do
t <- term
dot
return $ case t of
SPQuantTerm SPForall tlist tb ->
SPTermDecl { termDeclTermList = tlist, termDeclTerm = tb }
_ -> SPSimpleTermDecl t
-- | SPASS Proof List
proofList :: Parser SPProofList
proofList = do
listOf "proof"
pa <- optionMaybe $ parensDot $ do
pt <- optionMaybe getproofType
assList <- option Map.empty (comma >> assocList)
return (pt, assList)
steps <- many proofStep
endOfList
return $ case pa of
Nothing -> SPProofList
{ proofType = Nothing
, plAssocList = Map.empty
, step = steps}
Just (pt, mal) -> SPProofList
{ proofType = pt
, plAssocList = mal
, step = steps}
getproofType :: Parser SPIdentifier
getproofType = identifierT
assocList :: Parser SPAssocList
assocList = fmap Map.fromList $ squares $ commaSep
$ pair getKey $ symbolT ":" >> getValue
getKey :: Parser SPKey
getKey = fmap PKeyTerm term
getValue :: Parser SPValue
getValue = fmap PValTerm term
proofStep :: Parser SPProofStep
proofStep = do
keywordT "step"
(ref, res, rule, pl, mal) <- parensDot takeStep
return SPProofStep
{ reference = ref
, result = res
, ruleAppl = rule
, parentList = pl
, stepAssocList = mal}
where takeStep = do
ref <- getReference
comma
res <- getResult
comma
rule <- getRuleAppl
comma
pl <- getParentList
mal <- option Map.empty (comma >> assocList)
return (ref, res, rule, pl, mal)
getReference = fmap PRefTerm term
getResult = fmap PResTerm term
getRuleAppl = do
t <- term
let r = PRuleTerm t
return $ case t of
SPComplexTerm (SPCustomSymbol ide) [] -> case lookup (tokStr ide)
$ map ( \ z -> (show z, z))
[GeR, SpL,
SpR, EqF,
Rew, Obv,
EmS, SoR,
EqR, Mpm,
SPm, OPm,
SHy, OHy,
URR, Fac,
Spt, Inp,
Con, RRE,
SSi, ClR,
UnC, Ter] of
Just u -> PRuleUser u
Nothing -> r
_ -> r
getParentList = squares $ commaSep getParent
getParent = fmap PParTerm term
-- SPASS Settings.
settingList :: Parser [SPSetting]
settingList = many setting
setting :: Parser SPSetting
setting = do
listOfDot "general_settings"
entriesList <- many settingEntry
endOfList
return SPGeneralSettings {entries = entriesList}
<|> do
listOf "settings"
slabel <- parensDot getLabel
symbolT "{*"
t <- many clauseFormulaRelation
symbolT "*}"
endOfList
return SPSettings {settingName = slabel, settingBody = t}
settingEntry :: Parser SPHypothesis
settingEntry = do
keywordT "hypothesis"
slabels <- squaresDot (commaSep identifierT)
return (SPHypothesis slabels)
getLabel :: Parser SPSettingLabel
getLabel = mapTokensToData $ map ( \ z -> (showSettingLabel z, z))
[KIV, LEM, OTTER, PROTEIN, SATURATE, ThreeTAP, SETHEO, SPASS]
-- SPASS Clause-Formula Relation
clauseFormulaRelation :: Parser SPSettingBody
clauseFormulaRelation = do
keywordT "set_ClauseFormulaRelation"
cfr <- parensDot $ flip sepBy comma $ parens $ do
i1 <- identifierS
comma
i2 <- identifierS
return $ SPCRBIND i1 i2
return (SPClauseRelation cfr)
<|> do
t' <- identifierS
al <- parensDot (commaSep identifierS)
return (SPFlag t' al)
-- *** Terms
{- |
A SPASS Term.
-}
term :: Parser SPTerm
term = do
i <- identifierT
let iStr = tokStr i
case lookup iStr [("true", SPTrue), ("false", SPFalse)] of
Just s -> return $ simpTerm s
Nothing -> do
let s = spSym i
option (simpTerm s) $ do
(ts, as@(a : _)) <- parens $ do
ts <- optionL (squares (commaSep term) << comma)
as <- if null ts then commaSep term
else fmap (: []) term
return (ts, as)
if null ts then if elem iStr [ "forall", "exists", "true", "false"]
then unexpected $ show iStr else return $ compTerm
(fromMaybe s (lookup iStr $ map ( \ z -> (showSPSymbol z, z))
[ SPEqual
, SPOr
, SPAnd
, SPNot
, SPImplies
, SPImplied
, SPEquiv])) as
else return SPQuantTerm
{ quantSym = fromMaybe (SPCustomQuantSym i) $ lookup iStr
[("forall", SPForall), ("exists", SPExists)]
, variableList = ts, qFormula = a }
toClauseBody :: Monad m => SPClauseType -> SPTerm -> m NSPClauseBody
toClauseBody b t = case t of
SPComplexTerm n ts | b == SPCNF && n == SPOr || b == SPDNF && n == SPAnd ->
do ls <- mapM toLiteral ts
return $ NSPClauseBody b ls
_ -> fail $ "expected " ++ show b ++ "-application"