DFGParser.hs revision 5366c0cd087ad4ce1aeeb0a6addf77d290714d28
8e34905974b7a442a55adac3b3fdb196c389e807takashiModule : $Header$
640b2adac05bb7f5e9fba064434c91852c3a72e6ndDescription : A parser for the SPASS Input Syntax
640b2adac05bb7f5e9fba064434c91852c3a72e6ndCopyright : (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007
640b2adac05bb7f5e9fba064434c91852c3a72e6ndLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
640b2adac05bb7f5e9fba064434c91852c3a72e6ndMaintainer : Christian.Maeder@dfki.de
6e89d4f6c259afc94f8806c74a33a8fe81392499sfStability : provisional
640b2adac05bb7f5e9fba064434c91852c3a72e6ndPortability : portable
8e34905974b7a442a55adac3b3fdb196c389e807takashiA parser for the SPASS Input Syntax taken from
640b2adac05bb7f5e9fba064434c91852c3a72e6nd<http://spass.mpi-sb.mpg.de/download/binaries/spass-input-syntax15.pdf >.
640b2adac05bb7f5e9fba064434c91852c3a72e6ndIn this version the non-terminals /settings, declaration_list, clause_list,/
640b2adac05bb7f5e9fba064434c91852c3a72e6ndand /proof_list/ are currentliy not supported.
8e34905974b7a442a55adac3b3fdb196c389e807takashiimport qualified Data.Map as Map
640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport Data.List (isPrefixOf)
640b2adac05bb7f5e9fba064434c91852c3a72e6nd-- begin helpers ----------------------------------------------------------
640b2adac05bb7f5e9fba064434c91852c3a72e6ndreservedNames :: [String]
640b2adac05bb7f5e9fba064434c91852c3a72e6ndreservedNames =
640b2adac05bb7f5e9fba064434c91852c3a72e6nd [ "forall", "exists", "equal", "true", "false", "or", "and", "not"
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive , "implies", "implied", "equiv", "end_of_list" ]
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive(<<) :: Parser a -> Parser b -> Parser a
ef685e00a47967e27d89709461728a229d762172nda << b = a >>= \ r -> b >> return r
ef685e00a47967e27d89709461728a229d762172nd-- covers naturals too
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveanyWord :: Parser String
6e89d4f6c259afc94f8806c74a33a8fe81392499sfanyWord = do
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive c <- alphaNum
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars r <- many $ alphaNum <|> oneOf "_'"
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars return $ c : r
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveidentifierT :: Parser String
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveidentifierT = try $ anyWord >>=
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive (\ s -> if elem s reservedNames || isPrefixOf "list_of_" s
b44815871de48215476ad1d4cc46d3f99da532a5erikabele then unexpected $ show s else return s)
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivenatural :: Parser Integer
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivenatural = fmap read $ many1 digit
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivewhiteSpace :: Parser ()
51853aa2ebfdf9903a094467e1d02099f143639daaronwhiteSpace = skipMany $ oneOf "\n\r\t\v\f \160"
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivesymbolT :: String -> Parser String
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivesymbolT s = try (string s) << whiteSpace
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivedot :: Parser String
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivedot = symbolT "."
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecomma :: Parser String
8e34905974b7a442a55adac3b3fdb196c389e807takashicomma = symbolT ","
ef685e00a47967e27d89709461728a229d762172ndcommaSep :: Parser a -> Parser [a]
ef685e00a47967e27d89709461728a229d762172ndcommaSep p = sepBy p comma
6e89d4f6c259afc94f8806c74a33a8fe81392499sfoParen :: Parser String
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsoParen = symbolT "("
4a7e911a2df39170655de6ea32debfcf7e376bfaslivecParen :: Parser String
4a7e911a2df39170655de6ea32debfcf7e376bfaslivecParen = symbolT ")"
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsparens :: Parser a -> Parser a
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsparens p = oParen >> p << cParen
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larssquares :: Parser a -> Parser a
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivesquares p = symbolT "[" >> p << symbolT "]"
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveparensDot :: Parser a -> Parser a
4a7e911a2df39170655de6ea32debfcf7e376bfasliveparensDot p = parens p << dot
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivesquaresDot :: Parser a -> Parser a
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivesquaresDot p = squares p << dot
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivetext :: Parser [Char]
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivetext = try (string "{*") >> (manyTill anyChar (try (string "*}")))
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive*SPASS.Parser> run text "{* mein Kommentar *}"
2b024ea7e2bf985dfcf2914361d9e8b373e87df0rbowen" mein Kommentar "
2b024ea7e2bf985dfcf2914361d9e8b373e87df0rbowenlist_of :: [Char] -> Parser String
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivelist_of sort = symbolT $ "list_of_" ++ sort
17ca00f92106c825382359ebf0a754f8df21e316rbowenlist_of_dot :: [Char] -> Parser String
17ca00f92106c825382359ebf0a754f8df21e316rbowenlist_of_dot sort = list_of (sort ++ ".")
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsend_of_list :: Parser String
6e89d4f6c259afc94f8806c74a33a8fe81392499sfend_of_list = symbolT "end_of_list."
2b024ea7e2bf985dfcf2914361d9e8b373e87df0rbowenoneOfTokens :: [String] -> Parser String
2b024ea7e2bf985dfcf2914361d9e8b373e87df0rbowenoneOfTokens ls = choice (map (try . symbolT) ls)
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars*SPASS.Parser> run (oneOfTokens ["ab","cd"]) "abcd"
17ca00f92106c825382359ebf0a754f8df21e316rbowenmapTokensToData :: [(String, a)] -> Parser a
17ca00f92106c825382359ebf0a754f8df21e316rbowenmapTokensToData ls = choice (map (try . tokenToData) ls)
17ca00f92106c825382359ebf0a754f8df21e316rbowen where tokenToData (s,t) = symbolT s >> return t
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivemaybeParser :: GenParser tok st a -> GenParser tok st (Maybe a)
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivemaybeParser = option Nothing . fmap Just
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- end helpers ----------------------------------------------------------
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- ** SPASS Problem
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive This is the main function of the module
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive 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.
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsparseSPASS :: Parser SPProblem
45220913988eb2543fff442282c4aaa6b20559a8rbowenparseSPASS = whiteSpace >> problem
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsproblem :: Parser SPProblem
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsproblem = do
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars symbolT "begin_problem"
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive i <- parensDot identifierT
b44815871de48215476ad1d4cc46d3f99da532a5erikabele dl <- description_list
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars lp <- logical_part
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive s <- setting_list
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive symbolT "end_problem."
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars return SPProblem
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars { identifier = i
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars , description = dl
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive , logicalPart = lp
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive , settings = s}
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- ** SPASS Desciptions
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive{- | A description is mandatory for a SPASS problem. It has to specify
95e8cab14596a61826fa52477dcaebc07bfbad00colm at least a 'name', the name of the 'author', the 'status' (see also
8e34905974b7a442a55adac3b3fdb196c389e807takashi 'SPLogState' below), and a (verbose) description. -}
95e8cab14596a61826fa52477dcaebc07bfbad00colmdescription_list :: Parser SPDescription
95e8cab14596a61826fa52477dcaebc07bfbad00colmdescription_list = do
95e8cab14596a61826fa52477dcaebc07bfbad00colm list_of_dot "descriptions"
95e8cab14596a61826fa52477dcaebc07bfbad00colm symbolT "name"
6e89d4f6c259afc94f8806c74a33a8fe81392499sf n <- parensDot text
95e8cab14596a61826fa52477dcaebc07bfbad00colm symbolT "author"
95e8cab14596a61826fa52477dcaebc07bfbad00colm a <- parensDot text
95e8cab14596a61826fa52477dcaebc07bfbad00colm v <- maybeParser (symbolT "version" >> parensDot text)
95e8cab14596a61826fa52477dcaebc07bfbad00colm l <- maybeParser (symbolT "logic" >> parensDot text)
95e8cab14596a61826fa52477dcaebc07bfbad00colm s <- symbolT "status" >> parensDot (mapTokensToData
95e8cab14596a61826fa52477dcaebc07bfbad00colm [ ("satisfiable", SPStateSatisfiable)
95e8cab14596a61826fa52477dcaebc07bfbad00colm , ("unsatisfiable", SPStateUnsatisfiable)
95e8cab14596a61826fa52477dcaebc07bfbad00colm , ("unknown", SPStateUnknown)])
95e8cab14596a61826fa52477dcaebc07bfbad00colm symbolT "description"
95e8cab14596a61826fa52477dcaebc07bfbad00colm de <- parensDot text
95e8cab14596a61826fa52477dcaebc07bfbad00colm da <- maybeParser (symbolT "date" >> parensDot text)
95e8cab14596a61826fa52477dcaebc07bfbad00colm end_of_list
95e8cab14596a61826fa52477dcaebc07bfbad00colm return SPDescription
95e8cab14596a61826fa52477dcaebc07bfbad00colm { name = n
95e8cab14596a61826fa52477dcaebc07bfbad00colm , author = a
95e8cab14596a61826fa52477dcaebc07bfbad00colm , version = v
95e8cab14596a61826fa52477dcaebc07bfbad00colm , logic = l
95e8cab14596a61826fa52477dcaebc07bfbad00colm , status = s
95e8cab14596a61826fa52477dcaebc07bfbad00colm , desc = de
95e8cab14596a61826fa52477dcaebc07bfbad00colm , date = da }
95e8cab14596a61826fa52477dcaebc07bfbad00colm-- ** SPASS Logical Parts
17efa6b5344b7574597eec03f02ef28103e19265nd A SPASS logical part consists of a symbol list, a declaration list, and a
17efa6b5344b7574597eec03f02ef28103e19265nd set of formula lists. Support for clause lists and proof lists hasn't
17efa6b5344b7574597eec03f02ef28103e19265nd been implemented yet.
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxlogical_part :: Parser SPLogicalPart
6e89d4f6c259afc94f8806c74a33a8fe81392499sflogical_part = do
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx sl <- maybeParser symbol_list
17efa6b5344b7574597eec03f02ef28103e19265nd dl <- maybeParser declaration_list
17efa6b5344b7574597eec03f02ef28103e19265nd fs <- many formula_list
17efa6b5344b7574597eec03f02ef28103e19265nd cl <- many clause_list
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx pl <- many proof_list
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx return SPLogicalPart
17efa6b5344b7574597eec03f02ef28103e19265nd { symbolList = sl
b44815871de48215476ad1d4cc46d3f99da532a5erikabele , declarationList = dl
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx , formulaLists = fs
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx , clauseLists = cl
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx , proofLists = pl }
17efa6b5344b7574597eec03f02ef28103e19265nd-- *** Symbol List
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx SPASS Symbol List
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxsymbol_list :: Parser SPSymbolList
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxsymbol_list = do
17efa6b5344b7574597eec03f02ef28103e19265nd list_of_dot "symbols"
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx fs <- option [] (signSymFor "functions")
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai ps <- option [] (signSymFor "predicates")
8e34905974b7a442a55adac3b3fdb196c389e807takashi ss <- option [] (signSymFor "sorts")
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai end_of_list
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai return SPSymbolList
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai { functions = fs
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai , predicates = ps
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai , sorts = ss
6e89d4f6c259afc94f8806c74a33a8fe81392499sf , operators = [] -- not supported in dfg-syntax version 1.5
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai , quantifiers = [] } -- not supported in dfg-syntax version 1.5
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai*SPASS.Parser> run symbol_list "list_of_symbols.functions[(f,2), (a,0), (b,0), (c,0)].predicates[(F,2)].end_of_list."
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaisignSymFor :: String -> Parser [SPSignSym]
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaisignSymFor kind = symbolT kind >> squaresDot
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai (commaSep $ parens signSym <|> fmap SPSimpleSignSym identifierT)
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaisignSym :: Parser SPSignSym
8e34905974b7a442a55adac3b3fdb196c389e807takashisignSym = do
8e34905974b7a442a55adac3b3fdb196c389e807takashi s <- identifierT
8e34905974b7a442a55adac3b3fdb196c389e807takashi a <- maybeParser (comma >> natural)
8e34905974b7a442a55adac3b3fdb196c389e807takashi return $ case a of
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai Just a' -> SPSignSym {sym = s, arity = fromInteger a'}
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai Nothing -> SPSimpleSignSym s
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaifunc_list :: Parser [SPIdentifier]
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaifunc_list = squaresDot $ commaSep identifierT
17efa6b5344b7574597eec03f02ef28103e19265nd-- *** Formula List
17efa6b5344b7574597eec03f02ef28103e19265nd SPASS Formula List
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickformula_list :: Parser SPFormulaList
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickformula_list = do
6e89d4f6c259afc94f8806c74a33a8fe81392499sf list_of "formulae"
17efa6b5344b7574597eec03f02ef28103e19265nd ot <- parens $ mapTokensToData
8e34905974b7a442a55adac3b3fdb196c389e807takashi [ ("axioms", SPOriginAxioms)
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , ("conjectures", SPOriginConjectures)]
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick fs <- many (formula (case ot of {SPOriginAxioms -> True; _ -> False}))
8e34905974b7a442a55adac3b3fdb196c389e807takashi end_of_list
17efa6b5344b7574597eec03f02ef28103e19265nd return SPFormulaList { originType = ot, formulae = fs }
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick*SPASS.Parser> run formula_list "list_of_formulae(axioms).formula(all([a,b],R(a,b)),bla).end_of_list."
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickclause_list :: Parser SPClauseList
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickclause_list = do
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick list_of "clauses"
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick ot <- mapTokensToData
17efa6b5344b7574597eec03f02ef28103e19265nd [ ("axioms", SPOriginAxioms)
8e34905974b7a442a55adac3b3fdb196c389e807takashi , ("conjectures", SPOriginConjectures)]
17efa6b5344b7574597eec03f02ef28103e19265nd ct <- mapTokensToData [("cnf", SPCNF), ("dnf", SPDNF)]
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive fs <- many $ clause ct $ case ot of
6e89d4f6c259afc94f8806c74a33a8fe81392499sf SPOriginAxioms -> True
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive end_of_list
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive return SPClauseList
17efa6b5344b7574597eec03f02ef28103e19265nd { coriginType = ot
b44815871de48215476ad1d4cc46d3f99da532a5erikabele , clauseType = ct
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive , clauses = fs }
17efa6b5344b7574597eec03f02ef28103e19265ndrun clause_list "list_of_clauses(axioms, cnf). clause(or(not(a),b),1). clause(or(not(b),not(a)),2). end_of_list."
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveclause :: SPClauseType -> Bool -> Parser SPClause
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveclause ct bool = symbolT "clause" >> parensDot (do
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive sen <- clauseFork ct
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive cname <- (option "" (comma >> identifierT))
17efa6b5344b7574597eec03f02ef28103e19265nd return (makeNamed cname sen) { isAxiom = bool })
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele -- propagated from 'origin_type' of 'list_of_formulae'
94abf1cc80072ea31506946ac6595631ca6d2c14rbowenclauseFork :: SPClauseType -> Parser NSPClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowenclauseFork ct = try briefClause <|> case ct of
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen SPCNF -> cnfClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen SPDNF -> dnfClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowencnfClause :: Parser NSPClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowencnfClause = (symbolT "forall" >> parens (do
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen tl <- term_list
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen ct <- cnfLiteral
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen return (QuanClause tl ct)))
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen <|> fmap SimpleClause cnfLiteral
94abf1cc80072ea31506946ac6595631ca6d2c14rbowendnfClause :: Parser NSPClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowendnfClause = (symbolT "exists" >> parens (do
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen tl <- term_list
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen dt <- dnfLiteral
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen return (QuanClause tl dt)))
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen <|> fmap SimpleClause dnfLiteral
94abf1cc80072ea31506946ac6595631ca6d2c14rbowenbriefClause :: Parser NSPClause
94abf1cc80072ea31506946ac6595631ca6d2c14rbowenbriefClause = do
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen termWsList1 <- term_ws_list
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen symbolT "||"
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen termWsList2 <- term_ws_list
94abf1cc80072ea31506946ac6595631ca6d2c14rbowen symbolT "->"
17efa6b5344b7574597eec03f02ef28103e19265nd termWsList3 <- term_ws_list
8e34905974b7a442a55adac3b3fdb196c389e807takashi return (BriefClause termWsList1 termWsList2 termWsList3)
17efa6b5344b7574597eec03f02ef28103e19265ndterm_ws_list :: Parser TermWsList
1f666f93c91dbb492dc7706573b369cd03b84265poirierterm_ws_list = do
ef685e00a47967e27d89709461728a229d762172nd twl <- term_list_without_comma
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele p <- maybeParser (symbolT "+")
6e89d4f6c259afc94f8806c74a33a8fe81392499sf return (TWL twl (maybe False (const True) p))
1f666f93c91dbb492dc7706573b369cd03b84265poirierformula :: Bool -> Parser (Named SoftFOL.Sign.SPTerm)
1f666f93c91dbb492dc7706573b369cd03b84265poirierformula bool = symbolT "formula" >> parensDot (do
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele fname <- option "" (comma >> identifierT)
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele return (makeNamed fname sen) { isAxiom = bool })
1f666f93c91dbb492dc7706573b369cd03b84265poirier -- propagated from 'origin_type' of 'list_of_formulae'
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelelist_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.
1f666f93c91dbb492dc7706573b369cd03b84265poirierdeclaration_list :: Parser [SPDeclaration]
1f666f93c91dbb492dc7706573b369cd03b84265poirierdeclaration_list = do
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele list_of_dot "declarations"
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele decl <- many declaration
81622596373177e079337e956f7a5800895443b3erikabeledeclaration :: Parser SPDeclaration
81622596373177e079337e956f7a5800895443b3erikabeledeclaration = do
8e34905974b7a442a55adac3b3fdb196c389e807takashi try $ symbolT "sort"
81622596373177e079337e956f7a5800895443b3erikabele sortName <- identifierT
ef685e00a47967e27d89709461728a229d762172nd maybeFreely <- option False (symbolT "freely" >> return True)
ef685e00a47967e27d89709461728a229d762172nd symbolT "generated by"
ef685e00a47967e27d89709461728a229d762172nd funList <- func_list
81622596373177e079337e956f7a5800895443b3erikabele return SPGenDecl
6e89d4f6c259afc94f8806c74a33a8fe81392499sf { sortSym = sortName
81622596373177e079337e956f7a5800895443b3erikabele , freelyGenerated = maybeFreely
81622596373177e079337e956f7a5800895443b3erikabele , funcList = funList }
81622596373177e079337e956f7a5800895443b3erikabele try $ symbolT "subsort"
81622596373177e079337e956f7a5800895443b3erikabele (s1, s2) <- parensDot $ do
81622596373177e079337e956f7a5800895443b3erikabele s1 <- identifierT
81622596373177e079337e956f7a5800895443b3erikabele s2 <- identifierT
81622596373177e079337e956f7a5800895443b3erikabele return (s1, s2)
81622596373177e079337e956f7a5800895443b3erikabele return SPSubsortDecl { sortSymA = s1, sortSymB = s2 }
81622596373177e079337e956f7a5800895443b3erikabele <|> fmap SPSimpleTermDecl (term << dot)
81622596373177e079337e956f7a5800895443b3erikabele symbolT "forall"
81622596373177e079337e956f7a5800895443b3erikabele (tlist, t) <- parensDot $ do
81622596373177e079337e956f7a5800895443b3erikabele tlist <- term_list
81622596373177e079337e956f7a5800895443b3erikabele return (tlist, t)
81622596373177e079337e956f7a5800895443b3erikabele return SPTermDecl { termDeclTermList = tlist, termDeclTerm = t }
ef685e00a47967e27d89709461728a229d762172nd symbolT "predicate"
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen (pn, sl) <- parensDot $ do
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen pn <- identifierT
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen sl <- commaSep $ identifierT
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen return (pn, sl)
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen return SPPredDecl { predSym = pn, sortSyms = sl }
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen-- SPASS Proof List
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen 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.
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowenproof_list :: Parser SPProofList
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowenproof_list = do
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen list_of "proof"
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen pa <- maybeParser $ parens $ do
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen pt <- maybeParser getproofType
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen assocList <- maybeParser (comma >> assoc_list)
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen return (pt, assocList)
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen steps <- many proof_step
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen end_of_list
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen return $ case pa of
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen Nothing -> SPProofList
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen { proofType = Nothing
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen , plAssocList = Nothing
e554dd2dae4ba2c32dbd05fc0d4e0a42ef4ba902rbowen , step = steps}
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele Just (pt, mal) -> SPProofList
8e34905974b7a442a55adac3b3fdb196c389e807takashi { proofType = pt
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele , plAssocList = mal
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele , step = steps}
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetproofType :: Parser SPIdentifier
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetproofType = identifierT
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabeleassoc_list :: Parser SPAssocList
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabeleassoc_list = fmap Map.fromList $ squares ( commaSep $ takeTroop )
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele where takeTroop = do
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele key <- getKey
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele val <- getValue
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele return (key, val)
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetKey :: Parser SPKey
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetKey = fmap PKeyTerm term <|> fmap PKeyId identifierT
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetValue :: Parser SPValue
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele fmap PValTerm term <|> fmap PValId identifierT <|> fmap PValUser natural
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabeleproof_step :: Parser SPProofStep
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabeleproof_step = do
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele symbolT "step"
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele (ref, res, rule, pl, mal) <- parensDot takeStep
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki return SPProofStep
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd { reference = ref
8e34905974b7a442a55adac3b3fdb196c389e807takashi , result = res
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd , ruleAppl = rule
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd , parentList = pl
8e34905974b7a442a55adac3b3fdb196c389e807takashi , stepAssocList = mal}
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd where takeStep = do
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ref <- getReference
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd res <- getResult
8e34905974b7a442a55adac3b3fdb196c389e807takashi rule <- getRuleAppl
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd pl <- getParentList
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd mal <- maybeParser (comma >> assoc_list)
8e34905974b7a442a55adac3b3fdb196c389e807takashi return (ref, res, rule, pl, mal)
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd getReference = fmap PRefTerm term <|> fmap PRefId identifierT
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd <|> fmap PRefUser natural
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd getResult = fmap PResTerm term <|> fmap PResUser cnfClause
8e34905974b7a442a55adac3b3fdb196c389e807takashi getRuleAppl = fmap PRuleTerm term <|> fmap PRuleId identifierT
8e34905974b7a442a55adac3b3fdb196c389e807takashi <|> fmap PRuleUser (mapTokensToData
8e34905974b7a442a55adac3b3fdb196c389e807takashi [("GeR", GeR),("SpL", SpL),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("SpR", SpR),("EqF", EqF),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("Rew", Rew),("Obv", Obv),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("EmS", EmS),("SoR", SoR),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("EqR", EqR),("Mpm", Mpm),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("SPm", SPm),("OPm", OPm),
f4166cb2bf5e48c1b0f18b0d1f6757fce82230a8nd ("SHy", SHy),("OHy", OHy),
17efa6b5344b7574597eec03f02ef28103e19265nd ("URR", URR),("Fac", Fac),
8e34905974b7a442a55adac3b3fdb196c389e807takashi ("Spt", Spt),("Inp", Inp),
17efa6b5344b7574597eec03f02ef28103e19265nd ("Con", Con),("RRE", RRE),
17efa6b5344b7574597eec03f02ef28103e19265nd ("SSi", SSi),("ClR", ClR),
17efa6b5344b7574597eec03f02ef28103e19265nd ("UnC", UnC),("Ter", Ter)])
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki getParentList = squares (commaSep $ getParent)
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki getParent = fmap PParTerm term <|> fmap PParId identifierT
6e89d4f6c259afc94f8806c74a33a8fe81392499sf <|> fmap PParUser natural
17efa6b5344b7574597eec03f02ef28103e19265nd-- SPASS Settings.
17efa6b5344b7574597eec03f02ef28103e19265ndsetting_list :: Parser [SPSetting]
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikisetting_list = many setting
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikisetting :: Parser SPSetting
17efa6b5344b7574597eec03f02ef28103e19265ndsetting = do
17efa6b5344b7574597eec03f02ef28103e19265nd list_of "general_settings"
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki entriesList <- many setting_entry
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki end_of_list
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki return SPGeneralSettings {entries = entriesList}
17efa6b5344b7574597eec03f02ef28103e19265nd list_of "settings"
17efa6b5344b7574597eec03f02ef28103e19265nd slabel <- parensDot getLabel
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki symbolT "{*"
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki t <- many clauseFormulaRelation
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki symbolT "*}"
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki end_of_list
17efa6b5344b7574597eec03f02ef28103e19265nd return SPSettings {settingName = slabel, settingBody = t}
e9e8e471353eaa5576e1e96530968d02f208e39fndsetting_entry :: Parser SPHypothesis
8e34905974b7a442a55adac3b3fdb196c389e807takashisetting_entry = do
e9e8e471353eaa5576e1e96530968d02f208e39fnd symbolT "hypothesis"
e9e8e471353eaa5576e1e96530968d02f208e39fnd slabels <- squaresDot (commaSep identifierT)
1e1be8a0871405df3c1ec4d6d33aab71996ad0c9nilgun return (SPHypothesis slabels)
e9e8e471353eaa5576e1e96530968d02f208e39fndgetLabel :: Parser SPSettingLabel
6e89d4f6c259afc94f8806c74a33a8fe81392499sfgetLabel = mapTokensToData
e9e8e471353eaa5576e1e96530968d02f208e39fnd [("KIV", KIV), ("LEM", LEM), ("OTTER", OTTER),
1e1be8a0871405df3c1ec4d6d33aab71996ad0c9nilgun ("PROTEIN", PROTEIN), ("SATURATE", SATURATE),
e9e8e471353eaa5576e1e96530968d02f208e39fnd ("3TAP", ThreeTAP), ("SETHEO", SETHEO),
e9e8e471353eaa5576e1e96530968d02f208e39fnd ("SPASS", SPASS)]
1e1be8a0871405df3c1ec4d6d33aab71996ad0c9nilgun-- SPASS Clause-Formula Relation
e9e8e471353eaa5576e1e96530968d02f208e39fndclauseFormulaRelation :: Parser SPSettingBody
e9e8e471353eaa5576e1e96530968d02f208e39fndclauseFormulaRelation = do
e9e8e471353eaa5576e1e96530968d02f208e39fnd try $ symbolT "set_ClauseFormulaRelation"
1e1be8a0871405df3c1ec4d6d33aab71996ad0c9nilgun cfr <- try (parensDot $ commaSep $ parens $ do
1e1be8a0871405df3c1ec4d6d33aab71996ad0c9nilgun i1 <- identifierT
e9e8e471353eaa5576e1e96530968d02f208e39fnd i2 <- identifierT
e9e8e471353eaa5576e1e96530968d02f208e39fnd return $ SPCRBIND i1 i2) <|> do
e9e8e471353eaa5576e1e96530968d02f208e39fnd try $ parensDot whiteSpace