967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |

967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$

967e5f3c25249c779575864692935627004d3f9eChristian MaederDescription : A parser for the SPASS Input Syntax

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007

967e5f3c25249c779575864692935627004d3f9eChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : Christian.Maeder@dfki.de

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional

967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability : portable

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederA parser for the SPASS Input Syntax taken from

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

967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule SoftFOL.DFGParser (parseSPASS) where

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport Text.ParserCombinators.Parsec

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport SoftFOL.Sign

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maederimport Common.AS_Annotation

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport qualified Data.Map as Map

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Data.List (isPrefixOf)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport Data.Char (isSpace)

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder-- begin helpers ----------------------------------------------------------

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski(<<) :: Parser a -> Parser b -> Parser a

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskia << b = a >>= \ r -> b >> return r

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederwordChar :: Parser Char

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederwordChar = alphaNum <|> oneOf "_"

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian MaederanyWord :: Parser String

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederanyWord = do

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder c <- wordChar

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder r <- many wordChar

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder whiteSpace

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder return $ c : r

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian MaederidentifierT :: Parser String

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederidentifierT = try $ anyWord >>=

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (\ s -> if isPrefixOf "end_of_list" s || isPrefixOf "list_of_" s

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder then unexpected $ show s else return s)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederarityT :: Parser Int

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederarityT = fmap read $ many1 digit <|> try (string "-1" << notFollowedBy digit)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercommentLine :: Parser ()

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedercommentLine = char '%' >> manyTill anyChar newline >> return ()

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederwhiteSpace :: Parser ()

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederwhiteSpace = skipMany $ (satisfy isSpace >> return ()) <|> commentLine

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersymbolT :: String -> Parser String

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersymbolT s = try (string s) << whiteSpace

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederkeywordT :: String -> Parser String

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederkeywordT s = try (string s << notFollowedBy wordChar) << whiteSpace

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdot :: Parser String

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederdot = symbolT "."

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maedercomma :: Parser String

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedercomma = symbolT ","

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercommaSep :: Parser a -> Parser [a]

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercommaSep p = sepBy1 p comma

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederparens :: Parser a -> Parser a

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederparens p = symbolT "(" >> p << symbolT ")"

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedersquares :: Parser a -> Parser a

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedersquares p = symbolT "[" >> p << symbolT "]"

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederparensDot :: Parser a -> Parser a

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederparensDot p = symbolT "(" >> p << symbolT ")."

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersquaresDot :: Parser a -> Parser a

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedersquaresDot p = symbolT "[" >> p << symbolT "]."

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedertext :: Parser [Char]

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedertext = fmap (reverse . dropWhile isSpace . reverse) $

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder symbolT "{*" >> (manyTill anyChar $ symbolT "*}")

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederlist_of :: [Char] -> Parser String

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederlist_of sort = symbolT $ "list_of_" ++ sort

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederlist_of_dot :: [Char] -> Parser String

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederlist_of_dot sort = list_of (sort ++ ".")

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederend_of_list :: Parser String

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederend_of_list = symbolT "end_of_list."

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTokensToData :: [(String, a)] -> Parser a

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTokensToData ls = choice (map tokenToData ls)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder where tokenToData (s,t) = keywordT s >> return t

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermaybeParser :: Parser a -> Parser (Maybe a)

967e5f3c25249c779575864692935627004d3f9eChristian MaedermaybeParser = option Nothing . fmap Just

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maeder-- end helpers ----------------------------------------------------------

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder-- ** SPASS Problem

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder{- |

967e5f3c25249c779575864692935627004d3f9eChristian Maeder This is the main function of the module

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-}

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder{-

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder 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.

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederparseSPASS :: Parser SPProblem

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederparseSPASS = whiteSpace >> problem

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maederproblem :: Parser SPProblem

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederproblem = do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder symbolT "begin_problem"

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder i <- parensDot identifierT

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder dl <- description_list

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder lp <- logical_part

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder s <- setting_list

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder symbolT "end_problem."

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder eof

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder return SPProblem

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder { identifier = i

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , description = dl

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder , logicalPart = lp

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , settings = s}

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder-- ** SPASS Desciptions

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder{- | A description is mandatory for a SPASS problem. It has to specify

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder at least a 'name', the name of the 'author', the 'status' (see also

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder 'SPLogState' below), and a (verbose) description. -}

842eedc62639561781b6c33533d1949693ef6cc5Christian Maederdescription_list :: Parser SPDescription

842eedc62639561781b6c33533d1949693ef6cc5Christian Maederdescription_list = do

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder list_of_dot "descriptions"

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder keywordT "name"

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder n <- parensDot text

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder keywordT "author"

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder a <- parensDot text

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

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder s <- keywordT "status" >> parensDot (mapTokensToData

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder [ ("satisfiable", SPStateSatisfiable)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , ("unsatisfiable", SPStateUnsatisfiable)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , ("unknown", SPStateUnknown)])

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder keywordT "description"

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder de <- parensDot text

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

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder end_of_list

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return SPDescription

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { name = n

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder , author = a

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , version = v

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , logic = l

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , status = s

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , desc = de

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , date = da }

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- ** SPASS Logical Parts

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder{- |

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder A SPASS logical part consists of a symbol list, a declaration list, and a

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder set of formula lists. Support for clause lists and proof lists hasn't

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder been implemented yet.

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederlogical_part :: Parser SPLogicalPart

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederlogical_part = do

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder sl <- maybeParser symbol_list

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder dl <- maybeParser declaration_list

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder fs <- many formula_list

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder cl <- many clause_list

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder pl <- many proof_list

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return SPLogicalPart

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { symbolList = sl

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , declarationList = dl

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , formulaLists = fs

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , clauseLists = cl

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , proofLists = pl }

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- *** Symbol List

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder{- |

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder SPASS Symbol List

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedersymbol_list :: Parser SPSymbolList

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedersymbol_list = do

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder list_of_dot "symbols"

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fs <- option [] (signSymFor "functions")

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ps <- option [] (signSymFor "predicates")

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ss <- option [] sortSymFor

967e5f3c25249c779575864692935627004d3f9eChristian Maeder end_of_list

967e5f3c25249c779575864692935627004d3f9eChristian Maeder return emptySymbolList

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder { functions = fs

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , predicates = ps

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , sorts = ss }

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder{-

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

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersignSymFor :: String -> Parser [SPSignSym]

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersignSymFor kind = keywordT kind >> squaresDot

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

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersortSymFor :: Parser [SPSignSym]

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersortSymFor = keywordT "sorts" >> squaresDot

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (commaSep $ fmap SPSimpleSignSym identifierT)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersignSym :: Parser SPSignSym

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedersignSym = do

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder s <- identifierT

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder comma

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder a <- arityT

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder return SPSignSym {sym = s, arity = a}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederfunc_list :: Parser [SPIdentifier]

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederfunc_list = squaresDot $ commaSep identifierT

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- *** Formula List

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder{- |

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder SPASS Formula List

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-}

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederformula_list :: Parser SPFormulaList

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederformula_list = do

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder list_of "formulae"

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ot <- parensDot $ mapTokensToData

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder [ ("axioms", SPOriginAxioms)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , ("conjectures", SPOriginConjectures)]

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder end_of_list

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return SPFormulaList { originType = ot, formulae = fs }

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder{-

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

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder-}

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederclause_list :: Parser SPClauseList

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederclause_list = do

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder list_of "clauses"

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (ot, ct) <- parensDot $ do

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ot <- mapTokensToData

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder [ ("axioms", SPOriginAxioms)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , ("conjectures", SPOriginConjectures)]

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder comma

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

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder return (ot, ct)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fs <- many $ clause ct $ case ot of

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder SPOriginAxioms -> True

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder _ -> False

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder end_of_list

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder 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 True

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

<|> do

keywordT "predicate"

(pn, sl) <- parensDot $ do

pn <- identifierT

comma

sl <- commaSep $ identifierT

return (pn, sl)

return SPPredDecl { predSym = pn, sortSyms = sl }

<|> do

keywordT "forall"

(tlist, t) <- parensDot $ do

tlist <- term_list

comma

t <- term True

return (tlist, t)

return SPTermDecl { termDeclTermList = tlist, termDeclTerm = t }

<|> fmap SPSimpleTermDecl (term True << dot)

-- 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 $ parensDot $ do

pt <- maybeParser getproofType

assocList <- option Map.empty (comma >> assoc_list)

return (pt, assocList)

steps <- many proof_step

end_of_list

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

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 True)

getValue :: Parser SPValue

getValue = fmap PValTerm (term True)

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 <- option Map.empty (comma >> assoc_list)

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

getReference = fmap PRefTerm (term True)

getResult = fmap PResTerm (term True)

getRuleAppl =

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)])

<|> fmap PRuleTerm (term True)

getParentList = squares (commaSep $ getParent)

getParent = fmap PParTerm (term True)

-- 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 <- parensDot $ flip sepBy comma $ parens $ do

i1 <- identifierT

comma

i2 <- identifierT

return $ SPCRBIND i1 i2

return (SPClauseRelation cfr)

<|> do

t' <- identifierT

al <- parensDot (commaSep identifierT)

return (SPFlag t' al)

-- *** Terms

{- |

A SPASS Term.

-}

term :: Bool -> Parser SPTerm

term allowQuant = do

i <- identifierT

case lookup i [("true", SPTrue), ("false", SPFalse)] of

Just s -> return $ SPSimpleTerm s

Nothing -> do

let s = SPCustomSymbol i

option (SPSimpleTerm s) $ do

(ts, as@(a : _)) <- parens $ do

ts <- if allowQuant then

option [] (squares (commaSep $ term False) << comma)

else return []

as <- if null ts then commaSep $ term allowQuant

else fmap (: []) $ term True

return (ts, as)

if null ts then if elem i

[ "forall", "exists", "true", "false", "end_of_list"]

then unexpected $ show i else return SPComplexTerm

{ symbol = case lookup i

[ ("equal", SPEqual)

, ("or", SPOr)

, ("and", SPAnd)

, ("not", SPNot)

, ("implies", SPImplies)

, ("implied", SPImplied)

, ("equiv", SPEquiv)] of

Just ks -> ks

Nothing -> s

, arguments = as}

else return SPQuantTerm

{ quantSym = case lookup i

[("forall", SPForall), ("exists", SPExists)] of

Just q -> q

Nothing -> SPCustomQuantSym i

, variableList = ts, qFormula = a }

term_list :: Parser [SPTerm]

term_list = squares (commaSep $ term True)

term_list_without_comma :: Parser [SPTerm]

term_list_without_comma = many $ term True

literal :: Parser SPLiteral

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

<|> do

keywordT "not"

fmap NSPNotPLit $ parens $ term False

<|> fmap NSPPLit (term False)

cnfLiteral :: Parser NSPClauseBody

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

dnfLiteral :: Parser NSPClauseBody

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