32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer{- |

7a8401ce858002b67e8f4198fde45a1562696ccbChristian MaederModule : $Header$

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian MaederDescription : A parser for the SPASS Input Syntax

37eedb575dd3dc0ab25809693aa2d318f9084c56Christian MaederCopyright : (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian MaederMaintainer : Christian.Maeder@dfki.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian MaederPortability : portable

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian MaederA parser for the SPASS Input Syntax taken from

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

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder-}

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyermodule SoftFOL.DFGParser (parseSPASS) where

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport SoftFOL.Sign

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyerimport Text.ParserCombinators.Parsec

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport Common.AS_Annotation

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport Common.Id

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport Common.Lexer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport Common.Parsec

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyerimport Control.Monad

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyerimport Data.Char (isSpace)

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport Data.Maybe

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerimport qualified Data.Map as Map

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer-- * lexical matter

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyerwordChar :: Parser Char

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyerwordChar = alphaNum <|> oneOf "_"

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyeranyWord :: Parser String

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederanyWord = do

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer c <- wordChar

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer r <- many wordChar

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer whiteSpace

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer return $ c : r

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerreservedList :: [String]

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerreservedList = ["end_of_list", "sort", "subsort", "predicate"]

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyeridentifierS :: Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyeridentifierS = try $ anyWord >>=

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer (\ s -> if elem s reservedList then unexpected $ show s else return s)

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyeridentifierT :: Parser Token

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyeridentifierT = liftM2 (\ p s -> Token s (Range [p])) getPos identifierS

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerarityT :: Parser Int

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerarityT = fmap read $ many1 digit <|> try (string "-1" << notFollowedBy digit)

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyercommentLine :: Parser ()

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyercommentLine = forget $ char '%' >> manyTill anyChar newline

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerwhiteSpace :: Parser ()

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerwhiteSpace = skipMany $ forget (satisfy isSpace) <|> commentLine

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyersymbolT :: String -> Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyersymbolT = (<< whiteSpace) . tryString

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerkeywordT :: String -> Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerkeywordT s = try (string s << notFollowedBy wordChar) << whiteSpace

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyerdot :: Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyerdot = symbolT "."

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyercomma :: Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyercomma = symbolT ","

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyercommaSep :: Parser a -> Parser [a]

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyercommaSep p = sepBy1 p comma

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyerparens :: Parser a -> Parser a

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyerparens p = symbolT "(" >> p << symbolT ")"

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyersquares :: Parser a -> Parser a

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyersquares p = symbolT "[" >> p << symbolT "]"

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerparensDot :: Parser a -> Parser a

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerparensDot p = symbolT "(" >> p << symbolT ")."

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyersquaresDot :: Parser a -> Parser a

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyersquaresDot p = symbolT "[" >> p << symbolT "]."

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyertext :: Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyertext = fmap (reverse . dropWhile isSpace . reverse) $

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer symbolT "{*" >> manyTill anyChar (symbolT "*}")

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerlistOf :: String -> Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerlistOf = symbolT . ("list_of_" ++)

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerlistOfDot :: String -> Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerlistOfDot = listOf . (++ ".")

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerendOfList :: Parser String

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerendOfList = symbolT "end_of_list."

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyermapTokensToData :: [(String, a)] -> Parser a

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyermapTokensToData ls = choice (map tokenToData ls)

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

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer{- * SPASS Problem

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerThis is the main function of the module

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer-}

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerparseSPASS :: Parser SPProblem

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo WiedemeyerparseSPASS = whiteSpace >> problem

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerproblem :: Parser SPProblem

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyerproblem = do

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer symbolT "begin_problem"

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer i <- parensDot identifierS

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer dl <- descriptionList

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer lp <- logicalPartP

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer s <- settingList

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer symbolT "end_problem."

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer many anyChar

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer eof

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer return SPProblem

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer { identifier = i

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , description = dl

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , logicalPart = lp

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , settings = s}

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer-- ** SPASS Descriptions

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer{- | A description is mandatory for a SPASS problem. It has to specify

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer at least a 'name', the name of the 'author', the 'status' (see also

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer 'SPLogState' below), and a (verbose) description. -}

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyerdescriptionList :: Parser SPDescription

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyerdescriptionList = do

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer listOfDot "descriptions"

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer keywordT "name"

c7f4a6ff1152bff4eb0025eb70cfb2d96b55d4d8Thiemo Wiedemeyer n <- parensDot text

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer keywordT "author"

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer a <- parensDot text

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer v <- optionMaybe (keywordT "version" >> parensDot text)

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer l <- optionMaybe (keywordT "logic" >> parensDot text)

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer s <- keywordT "status" >> parensDot (mapTokensToData

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer [ ("satisfiable", SPStateSatisfiable)

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , ("unsatisfiable", SPStateUnsatisfiable)

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , ("unknown", SPStateUnknown)])

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer keywordT "description"

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer de <- parensDot text

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer da <- optionMaybe (keywordT "date" >> parensDot text)

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer endOfList

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer return SPDescription

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer { name = n

57bb31a6834641607fff7fc457b5a3e19238a132Christian Maeder , author = a

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , version = v

2083e66e910c2144cf800f31910993064c5f16beThiemo Wiedemeyer , logic = l

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , status = s

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , desc = de

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , date = da }

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer-- ** SPASS Logical Parts

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer{- |

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer A SPASS logical part consists of a symbol list, a declaration list, and a

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer set of formula lists. Support for clause lists and proof lists hasn't

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer been implemented yet.

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer-}

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyerlogicalPartP :: Parser SPLogicalPart

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyerlogicalPartP = do

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer sl <- optionMaybe symbolListP

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer dl <- optionMaybe declarationListP

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer fs <- many formulaList

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer cl <- many clauseList

dbd5da92be2bc4a8afcaa21980a5f59831037171Thiemo Wiedemeyer pl <- many proofList

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer return SPLogicalPart

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer { symbolList = sl

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , declarationList = dl

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , formulaLists = fs

9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer , clauseLists = cl

dbd5da92be2bc4a8afcaa21980a5f59831037171Thiemo Wiedemeyer , proofLists = pl }

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer-- *** Symbol List

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer{- |

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer SPASS Symbol List

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer-}

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersymbolListP :: Parser SPSymbolList

57bb31a6834641607fff7fc457b5a3e19238a132Christian MaedersymbolListP = do

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer listOfDot "symbols"

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer fs <- optionL (signSymFor "functions")

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer ps <- optionL (signSymFor "predicates")

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer ss <- optionL sortSymFor

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer endOfList

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer return emptySymbolList

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer { functions = fs

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , predicates = ps

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , sorts = ss }

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersignSymFor :: String -> Parser [SPSignSym]

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersignSymFor kind = keywordT kind >> squaresDot

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

57bb31a6834641607fff7fc457b5a3e19238a132Christian Maeder

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersortSymFor :: Parser [SPSignSym]

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersortSymFor = keywordT "sorts" >> squaresDot

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer (commaSep $ fmap SPSimpleSignSym identifierT)

d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersignSym :: Parser SPSignSym

d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersignSym = do

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder s <- identifierT

2083e66e910c2144cf800f31910993064c5f16beThiemo Wiedemeyer comma

2083e66e910c2144cf800f31910993064c5f16beThiemo Wiedemeyer a <- arityT

2083e66e910c2144cf800f31910993064c5f16beThiemo Wiedemeyer return SPSignSym {sym = s, arity = a}

2083e66e910c2144cf800f31910993064c5f16beThiemo Wiedemeyer

2083e66e910c2144cf800f31910993064c5f16beThiemo WiedemeyerfunctList :: Parser [SPIdentifier]

2083e66e910c2144cf800f31910993064c5f16beThiemo WiedemeyerfunctList = squaresDot $ commaSep identifierT

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer-- *** Formula List

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer{- |

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer SPASS Formula List

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer-}

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo WiedemeyerformulaList :: Parser SPFormulaList

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo WiedemeyerformulaList = do

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer listOf "formulae"

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer ot <- parensDot $ mapTokensToData

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer [ ("axioms", SPOriginAxioms)

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer , ("conjectures", SPOriginConjectures)]

6e2c6baa4352577819386beb3a21d7c247eab52cThiemo Wiedemeyer fs <- many $ formula $ case ot of

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder SPOriginAxioms -> True

2c3b3333159c7eeef90480500729409bf3388550Klaus Luettich _ -> False

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder 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"