PrintTPTP.hs revision f04e8f3ff56405901be968fd4c6e9769239f1a9b
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Pretty printing for SPASS signatures in TPTP syntax.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Rene Wagner, Rainer Grabbe, Uni Bremen 2005-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : rainer25@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : unknown
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederPretty printing for SoftFOL signatures in TPTP syntax.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder Refer to <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder for the TPTP syntax documentation.
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder-- | This type class allows pretty printing in TPTP syntax of instantiated data
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederclass PrintTPTP a where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder printTPTP :: a -> Doc
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Helper function. Generates a separating comment line.
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederseparator :: String
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederseparator = '%' : replicate 75 '-'
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Helper function. Generates a comma separated list of SoftFOL Terms as a Doc.
3dde4051c307b609159a097f08a05108fdd036efJonathan von SchroederprintCommaSeparated :: [SPTerm] -> Doc
3dde4051c307b609159a097f08a05108fdd036efJonathan von SchroederprintCommaSeparated = hcat . punctuate comma . map printTPTP
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maederinstance PrintTPTP Sign where
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder printTPTP = printTPTP . signToSPLogicalPart
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder Creates a Doc from a SoftFOL Problem.
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederinstance PrintTPTP SPProblem where
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder printTPTP p = text separator
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $+$ text "% Problem" <+> colon <+> text (identifier p)
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder $+$ printTPTP (description p)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder $+$ vcat (map printTPTP $ settings p)
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder $+$ text separator
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance $+$ printTPTP (logicalPart p)
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder Creates a Doc from a SoftFOL Logical Part.
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maederinstance PrintTPTP SPLogicalPart where
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich printTPTP lp =
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder let validDeclarations = filter (\ decl -> case decl of
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder SPSubsortDecl{} -> True
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder SPTermDecl{} -> True
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder SPSimpleTermDecl _ -> True
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder _ -> False) $ declarationList lp
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder in vcat (map (\ (decl, i) ->
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder text "fof" <>
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder parens (text ("declaration" ++ show i) <> comma <>
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder printTPTP SPOriginAxioms <> comma
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder $+$ parens (printTPTP decl)) <> dot)
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder $ zip validDeclarations [(0::Int)..])
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder $+$ vcat (map printTPTP $ formulaLists lp)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Creates a Doc from a SoftFOL Declaration.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder A subsort declaration will be rewritten as a special SPQuantTerm.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance PrintTPTP SPDeclaration where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder printTPTP decl = case decl of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder SPSubsortDecl{sortSymA= sortA, sortSymB= sortB}
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -> let subsortVar = spTerms $ genVarList sortA [sortB]
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder printTPTP SPQuantTerm{
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder quantSym=SPForall,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder variableList=subsortVar,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder qFormula=SPComplexTerm{
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder symbol=SPImplies,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder arguments=[SPComplexTerm{
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder symbol=SPCustomSymbol sortA,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder arguments=subsortVar},
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder SPComplexTerm{
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder symbol=SPCustomSymbol sortB,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder arguments=subsortVar}]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder SPTermDecl{termDeclTermList= tlist, termDeclTerm= tt}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> printTPTP SPQuantTerm{
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder quantSym=SPForall,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder variableList=tlist,
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder SPSimpleTermDecl stsym -> printTPTP stsym
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder pd@(SPPredDecl {}) -> maybe empty printTPTP $ predDecl2Term pd
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Creates a Doc from a SoftFOL Formula List.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance PrintTPTP SPFormulaList where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder printTPTP l = vcat $ map (printFormula $ originType l) $ formulae l
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Creates a Doc from a SoftFOL Origin Type.
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederinstance PrintTPTP SPOriginType where
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder printTPTP t = text $ case t of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder SPOriginAxioms -> "axiom"
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder SPOriginConjectures -> "conjecture"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Creates a Doc from a SoftFOL Formula. Needed since SPFormula is just a
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder 'type SPFormula = Named SPTerm' and thus instanciating PrintTPTP is not
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian MaederprintFormula :: SPOriginType -> SPFormula -> Doc
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder-- printFormula ot f = printFormulaText ot (senName f) (sentence f)
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian MaederprintFormula ot f =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder text "fof" <> parens (text (senName f) <> comma <> printTPTP ot <> comma
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $+$ parens (printTPTP $ sentence f)) <> dot
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Creates a Doc from a SoftFOL Term.
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maederinstance PrintTPTP SPTerm where
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder printTPTP t = case t of
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder SPQuantTerm{quantSym= qsym, variableList= tlist, qFormula= tt}
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -> printTPTP qsym
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder <+> brackets (printCommaSeparated $ getVariables tlist)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -- either all variables are simple terms
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder <+> if (filter isSimpleTerm tlist == tlist) then printTPTP tt
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder -- or there are none simple terms
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder else assert (null $ filter isSimpleTerm tlist)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- construct premiss for implication out of variableList (Forall)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- construct conjunction out of variableList (Exists)
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder printTermList (cond qsym) [SPComplexTerm{
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder symbol=SPAnd,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder arguments=tlist}, tt]
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder SPSimpleTerm stsym -> printTPTP stsym
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder SPComplexTerm{symbol= ctsym, arguments= args}
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder -> if null args
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder then printTPTP ctsym
14c56dc499da4bbeaeebeb558ceb755150ae341cChristian Maeder else printTermList ctsym args
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder isSimpleTerm tm = case tm of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder SPSimpleTerm _ -> True
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder -- check that every list entry is simple term
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder getSimpleVars = foldr (\v vl -> assert (isSimpleTerm v) $ v:vl) []
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder getVariables tl = if null $ filter isSimpleTerm tl
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder then foldr (\co col -> (getSimpleVars $
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder arguments co)++col)
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder else getSimpleVars tl
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder cond qsy = case qsy of
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder SPForall -> SPImplies
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers SPExists -> SPAnd
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder _ -> error "SoftFOL.PrintTPTP: unknown quantifier symbol"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Creates a Doc from a list of SoftFOL Terms connected by a SoftFOL Symbol.
c208973c890b8f993297720fd0247bc7481d4304Christian MaederprintTermList :: SPSymbol -> [SPTerm] -> Doc
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederprintTermList symb terms = case symb of
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder SPEqual -> assert (length terms == 2) $ associate SPEqual
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder SPTrue -> assert (length terms == 0) $ associate SPTrue
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers SPFalse -> assert (length terms == 0) $ associate SPFalse
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- variable number of terms for or/and
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder SPOr -> assert (length terms >= 0) $ associate SPOr
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder SPAnd -> assert (length terms >= 0) $ associate SPAnd
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- only one term can be negated
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder SPNot -> assert (length terms == 1) $ applicate SPNot
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder SPImplies -> assert (length terms == 2) $ associate SPImplies
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder SPImplied -> assert (length terms == 2) $ associate SPImplied
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder SPEquiv -> assert (length terms == 2) $ associate SPEquiv
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder SPCustomSymbol cst -> applicate $ SPCustomSymbol cst
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder associate sb = case terms of
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder [x] -> printTPTP x
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder _ -> parens $ vcat $ punctuate (space <> printTPTP sb)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder $ map printTPTP terms
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder applicate sb =
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder if null terms then printTPTP sb
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder else printTPTP sb <> parens (printCommaSeparated terms)
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder Creates a Doc from a SoftFOL Quantifier Symbol.
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maederinstance PrintTPTP SPQuantSym where
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder printTPTP qs = text $ case qs of
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder SPForall -> "!"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder SPExists -> "?"
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder SPCustomQuantSym cst -> cst
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Creates a Doc from a SoftFOL Symbol.
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederinstance PrintTPTP SPSymbol where
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder printTPTP s = text $ case s of
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder SPEqual -> "="
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder SPTrue -> "$true"
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder SPFalse -> "$false"
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder SPImplies -> "=>"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder SPImplied -> "<="
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder SPEquiv -> "<=>"
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder SPCustomSymbol cst -> cst
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder Creates a Doc from a SoftFOL description.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinstance PrintTPTP SPDescription where
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder printTPTP d = spCommentText "Name " (name d)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $+$ spCommentText "Author " (author d)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $+$ maybe empty (spCommentText "Version") (version d)
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder $+$ maybe empty (spCommentText "Logic ") (logic d)
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder $+$ text "% Status " <+> colon <+> printTPTP (status d)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder $+$ spCommentText "Desc " (desc d)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $+$ maybe empty (spCommentText "Date ") (date d)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Helper function. Creates a formatted comment output for a description field.
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder On left side will be displayed the field's name, on right side its content.
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederspCommentText :: String -> String -> Doc
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian MaederspCommentText fieldName fieldDesc =
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder hsep [text "%", text fieldName, colon, text fieldDesc]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Creates a Doc from an 'SPLogState'.
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederinstance PrintTPTP SPLogState where
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder printTPTP s = text $ case s of
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly SPStateSatisfiable -> "satisfiable"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder SPStateUnsatisfiable -> "unsatisfiable"
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke SPStateUnknown -> "unknown"
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maederinstance PrintTPTP SPSetting where
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder printTPTP (SPFlag sw v) =
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu if (null sw) then
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroeder hsep [text "% Option ", colon, text v]
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder hsep [text "% Option ", colon, text sw, comma, text v]
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder error "SPClauseRelation pretty printing not yet implemented"