{- |

Module : $Header$

Description : A parser for the SPASS Input Syntax

Copyright : (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

A parser for the SPASS Input Syntax taken from

<http://spass.mpi-sb.mpg.de/download/binaries/spass-input-syntax15.pdf >.

-}

module SoftFOL.DFGParser (parseSPASS) where

import Text.ParserCombinators.Parsec

import SoftFOL.Sign

import Common.AS_Annotation

import qualified Data.Map as Map

import Data.List (isPrefixOf)

import Data.Char (isSpace)

-- begin helpers ----------------------------------------------------------

reservedNames :: [String]

reservedNames =

[ "forall", "exists", "equal", "true", "false", "or", "and", "not"

, "implies", "implied", "equiv", "end_of_list" ]

(<<) :: Parser a -> Parser b -> Parser a

a << b = a >>= \ r -> b >> return r

wordChar :: Parser Char

wordChar = alphaNum <|> oneOf "_'"

-- covers naturals too

anyWord :: Parser String

anyWord = do

c <- alphaNum

r <- many wordChar

whiteSpace

return $ c : r

identifierT :: Parser String

identifierT = try $ anyWord >>=

(\ s -> if elem s reservedNames || isPrefixOf "list_of_" s

then unexpected $ show s else return s)

natural :: Parser Integer

natural = fmap read $ many1 digit

commentLine :: Parser ()

commentLine = char '%' >> manyTill anyChar newline >> return ()

whiteSpace :: Parser ()

whiteSpace = skipMany $ (satisfy isSpace >> return ()) <|> commentLine

symbolT :: String -> Parser String

symbolT s = try (string s) << whiteSpace

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 = sepBy p comma

oParen :: Parser String

oParen = symbolT "("

cParen :: Parser String

cParen = symbolT ")"

parens :: Parser a -> Parser a

parens p = oParen >> p << cParen

squares :: Parser a -> Parser a

squares p = symbolT "[" >> p << symbolT "]"

parensDot :: Parser a -> Parser a

parensDot p = parens p << dot

squaresDot :: Parser a -> Parser a

squaresDot p = squares p << dot

text :: Parser [Char]

text = fmap (reverse . dropWhile isSpace . reverse) $

symbolT "{*" >> (manyTill anyChar $ symbolT "*}")

list_of :: [Char] -> Parser String

list_of sort = symbolT $ "list_of_" ++ sort

list_of_dot :: [Char] -> Parser String

list_of_dot sort = list_of (sort ++ ".")

end_of_list :: Parser String

end_of_list = symbolT "end_of_list."

mapTokensToData :: [(String, a)] -> Parser a

mapTokensToData ls = choice (map tokenToData ls)

where tokenToData (s,t) = keywordT s >> return t

maybeParser :: Parser a -> Parser (Maybe a)

maybeParser = option Nothing . fmap Just

-- end helpers ----------------------------------------------------------

-- ** SPASS Problem

{- |

This is the main function of the module

-}

{-

begin_problem(Unknown).list_of_descriptions.name({* Test *}).author({* me *}).status(satisfiable).description({* nothing CNF generated by FLOTTER V 2.8 *}).end_of_list.list_of_symbols.predicates[(a, 0), (b, 0)].end_of_list.list_of_clauses(axioms, cnf).clause(or(not(a),b),1).clause(or(not(b),not(a)),2).end_of_list.list_of_clauses(conjectures, cnf).end_of_list.list_of_settings(SPASS).{*set_ClauseFormulaRelation((1,axiom0),(2,axiom1)).*}end_of_list.end_problem.

-}

parseSPASS :: Parser SPProblem

parseSPASS = whiteSpace >> problem

problem :: Parser SPProblem

problem = do

symbolT "begin_problem"

i <- parensDot identifierT

dl <- description_list

lp <- logical_part

s <- setting_list

symbolT "end_problem."

eof

return SPProblem

{ identifier = i

, description = dl

, logicalPart = lp

, settings = s}

-- ** SPASS Desciptions

{- | 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. -}

description_list :: Parser SPDescription

description_list = do

list_of_dot "descriptions"

keywordT "name"

n <- parensDot text

keywordT "author"

a <- parensDot text

v <- maybeParser (keywordT "version" >> parensDot text)

l <- maybeParser (keywordT "logic" >> parensDot text)

s <- keywordT "status" >> parensDot (mapTokensToData

[ ("satisfiable", SPStateSatisfiable)

, ("unsatisfiable", SPStateUnsatisfiable)

, ("unknown", SPStateUnknown)])

keywordT "description"

de <- parensDot text

da <- maybeParser (keywordT "date" >> parensDot text)

end_of_list

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.

-}

logical_part :: Parser SPLogicalPart

logical_part = do

sl <- maybeParser symbol_list

dl <- maybeParser declaration_list

fs <- many formula_list

cl <- many clause_list

pl <- many proof_list

return SPLogicalPart

{ symbolList = sl

, declarationList = dl

, formulaLists = fs

, clauseLists = cl

, proofLists = pl }

-- *** Symbol List

{- |

SPASS Symbol List

-}

symbol_list :: Parser SPSymbolList

symbol_list = do

list_of_dot "symbols"

fs <- option [] (signSymFor "functions")

ps <- option [] (signSymFor "predicates")

ss <- option [] (signSymFor "sorts")

end_of_list

return SPSymbolList

{ functions = fs

, predicates = ps

, sorts = ss

, operators = [] -- not supported in dfg-syntax version 1.5

, quantifiers = [] } -- not supported in dfg-syntax version 1.5

{-

"list_of_symbols.functions[(f,2), (a,0), (b,0), (c,0)].predicates[(F,2)].end_of_list."

-}

signSymFor :: String -> Parser [SPSignSym]

signSymFor kind = keywordT kind >> squaresDot

(commaSep $ parens signSym <|> fmap SPSimpleSignSym identifierT)

signSym :: Parser SPSignSym

signSym = do

s <- identifierT

a <- maybeParser (comma >> natural)

return $ case a of

Just a' -> SPSignSym {sym = s, arity = fromInteger a'}

Nothing -> SPSimpleSignSym s

func_list :: Parser [SPIdentifier]

func_list = squaresDot $ commaSep identifierT

-- *** Formula List

{- |

SPASS Formula List

-}

formula_list :: Parser SPFormulaList

formula_list = do

list_of "formulae"

ot <- parens $ mapTokensToData

[ ("axioms", SPOriginAxioms)

, ("conjectures", SPOriginConjectures)]

dot

fs <- many (formula (case ot of {SPOriginAxioms -> True; _ -> False}))

end_of_list

return SPFormulaList { originType = ot, formulae = fs }

{-

"list_of_formulae(axioms).formula(all([a,b],R(a,b)),bla).end_of_list."

-}

clause_list :: Parser SPClauseList

clause_list = do

list_of "clauses"

oParen

ot <- mapTokensToData

[ ("axioms", SPOriginAxioms)

, ("conjectures", SPOriginConjectures)]

comma

ct <- mapTokensToData [("cnf", SPCNF), ("dnf", SPDNF)]

cParen

dot

fs <- many $ clause ct $ case ot of

SPOriginAxioms -> True

_ -> False

end_of_list

return SPClauseList

{ coriginType = ot

, clauseType = ct

, clauses = fs }

{-

"list_of_clauses(axioms, cnf). clause(or(not(a),b),1). clause(or(not(b),not(a)),2). end_of_list."

-}

clause :: SPClauseType -> Bool -> Parser SPClause

clause ct bool = keywordT "clause" >> parensDot (do

sen <- clauseFork ct

cname <- (option "" (comma >> identifierT))

return (makeNamed cname sen) { isAxiom = bool })

-- propagated from 'origin_type' of 'list_of_formulae'

clauseFork :: SPClauseType -> Parser NSPClause

clauseFork ct = try briefClause <|> case ct of

SPCNF -> cnfClause

SPDNF -> dnfClause

cnfClause :: Parser NSPClause

cnfClause = (keywordT "forall" >> parens (do

tl <- term_list

comma

ct <- cnfLiteral

return (QuanClause tl ct)))

<|> fmap SimpleClause cnfLiteral

dnfClause :: Parser NSPClause

dnfClause = (keywordT "exists" >> parens (do

tl <- term_list

comma

dt <- dnfLiteral

return (QuanClause tl dt)))

<|> fmap SimpleClause dnfLiteral

briefClause :: Parser NSPClause

briefClause = do

termWsList1 <- term_ws_list

symbolT "||"

termWsList2 <- term_ws_list

symbolT "->"

termWsList3 <- term_ws_list

return (BriefClause termWsList1 termWsList2 termWsList3)

term_ws_list :: Parser TermWsList

term_ws_list = do

twl <- term_list_without_comma

p <- maybeParser (symbolT "+")

return (TWL twl (maybe False (const True) p))

formula :: Bool -> Parser (Named SoftFOL.Sign.SPTerm)

formula bool = keywordT "formula" >> parensDot (do

sen <- term

fname <- option "" (comma >> identifierT)

return (makeNamed fname sen) { isAxiom = bool })

-- propagated from 'origin_type' of 'list_of_formulae'

{-

list_of_declarations.subsort(even,nat).even(zero).forall([nat(x)],nat(s(x))).forall([nat(x),nat(y)],nat(plus(x,y))).forall([even(x),even(y)],even(plus(x,y))).forall([even(x)],even(s(s(x)))).forall([nat(y)],even(plus(y,y))).end_of_list.

-}

declaration_list :: Parser [SPDeclaration]

declaration_list = do

list_of_dot "declarations"

decl <- many declaration

end_of_list

return decl

declaration :: Parser SPDeclaration

declaration = do

keywordT "sort"

sortName <- identifierT

maybeFreely <- option False (keywordT "freely" >> return True)

keywordT "generated"

keywordT "by"

funList <- func_list

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 }

<|> fmap SPSimpleTermDecl (term << dot)

<|> do

keywordT "forall"

(tlist, t) <- parensDot $ do

tlist <- term_list

comma

t <- term

return (tlist, t)

return SPTermDecl { termDeclTermList = tlist, termDeclTerm = t }

<|> do

keywordT "predicate"

(pn, sl) <- parensDot $ do

pn <- identifierT

comma

sl <- commaSep $ identifierT

return (pn, sl)

return SPPredDecl { predSym = pn, sortSyms = sl }

-- SPASS Proof List

{-

list_of_proof(SPASS).step(10,forall([V,U,W],or(equal(U,V),equal(V,skf1(W)),P(W,U))),SpR,[3,1]).step(36,forall([V,U],or(equal(U,V),equal(V,skf1(skf1(U))))),GeR,[10,2]).step(43,forall([V,U],or(equal(U,V),P(skf1(U),V))),SpR,[36,1]).step(58,forall([V,U],or(not(P(U,skf1(V))),equal(V,U))),SpL,[36,2]).step(86,forall([V,U],or(equal(U,skf1(V)),equal(V,skf1(U)))),GeR,[43,58]).step(87,forall([U],or(not(equal(U,U)),equal(skf1(U),U))),EqF,[86,86]).step(124,forall([U],or(equal(skf1(U),U))),Obv,[87]).step(129,forall([U],or(P(U,U))),Rew,[124,1]).step(130,forall([U],or(not(P(U,U)))),Rew,[124,2]).step(213,or(false),ClR,[129,130]).end_of_list.

-}

proof_list :: Parser SPProofList

proof_list = do

list_of "proof"

pa <- maybeParser $ parens $ do

pt <- maybeParser getproofType

assocList <- maybeParser (comma >> assoc_list)

return (pt, assocList)

dot

steps <- many proof_step

end_of_list

return $ case pa of

Nothing -> SPProofList

{ proofType = Nothing

, plAssocList = Nothing

, step = steps}

Just (pt, mal) -> SPProofList

{ proofType = pt

, plAssocList = mal

, step = steps}

getproofType :: Parser SPIdentifier

getproofType = identifierT

assoc_list :: Parser SPAssocList

assoc_list = fmap Map.fromList $ squares ( commaSep $ takeTroop )

where takeTroop = do

key <- getKey

symbolT ":"

val <- getValue

return (key, val)

getKey :: Parser SPKey

getKey = fmap PKeyTerm term <|> fmap PKeyId identifierT

getValue :: Parser SPValue

getValue =

fmap PValTerm term <|> fmap PValId identifierT <|> fmap PValUser natural

proof_step :: Parser SPProofStep

proof_step = 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 <- maybeParser (comma >> assoc_list)

return (ref, res, rule, pl, mal)

getReference = fmap PRefTerm term <|> fmap PRefId identifierT

<|> fmap PRefUser natural

getResult = fmap PResTerm term <|> fmap PResUser cnfClause

getRuleAppl = fmap PRuleTerm term <|> fmap PRuleId identifierT

<|> fmap PRuleUser (mapTokensToData

[("GeR", GeR),("SpL", SpL),

("SpR", SpR),("EqF", EqF),

("Rew", Rew),("Obv", Obv),

("EmS", EmS),("SoR", SoR),

("EqR", EqR),("Mpm", Mpm),

("SPm", SPm),("OPm", OPm),

("SHy", SHy),("OHy", OHy),

("URR", URR),("Fac", Fac),

("Spt", Spt),("Inp", Inp),

("Con", Con),("RRE", RRE),

("SSi", SSi),("ClR", ClR),

("UnC", UnC),("Ter", Ter)])

getParentList = squares (commaSep $ getParent)

getParent = fmap PParTerm term <|> fmap PParId identifierT

<|> fmap PParUser natural

-- SPASS Settings.

setting_list :: Parser [SPSetting]

setting_list = many setting

setting :: Parser SPSetting

setting = do

list_of_dot "general_settings"

entriesList <- many setting_entry

end_of_list

return SPGeneralSettings {entries = entriesList}

<|> do

list_of "settings"

slabel <- parensDot getLabel

symbolT "{*"

t <- many clauseFormulaRelation

symbolT "*}"

end_of_list

return SPSettings {settingName = slabel, settingBody = t}

setting_entry :: Parser SPHypothesis

setting_entry = do

keywordT "hypothesis"

slabels <- squaresDot (commaSep identifierT)

return (SPHypothesis slabels)

getLabel :: Parser SPSettingLabel

getLabel = mapTokensToData

[("KIV", KIV), ("LEM", LEM), ("OTTER", OTTER),

("PROTEIN", PROTEIN), ("SATURATE", SATURATE),

("3TAP", ThreeTAP), ("SETHEO", SETHEO),

("SPASS", SPASS)]

-- SPASS Clause-Formula Relation

clauseFormulaRelation :: Parser SPSettingBody

clauseFormulaRelation = do

keywordT "set_ClauseFormulaRelation"

cfr <- try (parensDot $ commaSep $ parens $ do

i1 <- identifierT

comma

i2 <- identifierT

return $ SPCRBIND i1 i2) <|> do

try $ parensDot whiteSpace

return []

return (SPClauseRelation cfr)

<|> do

t' <- identifierT

al <- parensDot (commaSep identifierT)

return (SPFlag t' al)

-- *** Terms

{- |

A SPASS Term.

-}

quantification :: SPQuantSym -> Parser SPTerm

quantification s = do

(ts',t') <- parens $ do

ts <- squares (commaSep term)

-- todo: var binding should allow only simple terms

comma

t <- term

return (ts, t)

return SPQuantTerm {quantSym = s, variableList = ts', qFormula = t'}

application :: SPSymbol -> Parser SPTerm

application s = do

ts <- parens (commaSep term)

return SPComplexTerm {symbol = s, arguments = ts}

term :: Parser SPTerm

term =

fmap SPSimpleTerm (mapTokensToData [("true", SPTrue), ("false", SPFalse)])

<|> do

q <- mapTokensToData [("forall", SPForall), ("exists", SPExists)]

quantification q

<|> do

a <- mapTokensToData

[("equal", SPEqual), ("or", SPOr), ("and", SPAnd), ("not", SPNot),

("implies", SPImplies), ("implied", SPImplied), ("equiv", SPEquiv)]

application a

<|> do

i <- identifierT

let s = SPCustomSymbol i

option (SPSimpleTerm s) $ do

oParen

ts <- option [] (squares (commaSep term) << comma)

as@(a : _) <- if null ts then commaSep term else fmap (: []) term

cParen

return $ if null ts then SPComplexTerm {symbol = s, arguments = as}

else SPQuantTerm

{quantSym = SPCustomQuantSym i, variableList = ts, qFormula = a}

term_list :: Parser [SPTerm]

term_list = squares (commaSep $ term)

term_list_without_comma :: Parser [SPTerm]

term_list_without_comma = many term

literal :: Parser SPLiteral

literal = mapTokensToData [("true", NSPTrue), ("false", NSPFalse)]

<|> do

keywordT "not"

oParen

t <- term

cParen

return $ NSPNotPLit t

<|> fmap NSPPLit term

cnfLiteral :: Parser NSPClauseBody

cnfLiteral = fmap NSPCNF $ keywordT "or" >> parens (commaSep literal)

dnfLiteral :: Parser NSPClauseBody

dnfLiteral = fmap NSPDNF $ keywordT "and" >> parens (commaSep literal)