Print.hs revision 135bcb7f65991146c103e5e7599adbc49fe7359d
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Pretty printing for SoftFOL problems in DFG.
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Rene Wagner, Uni Bremen 2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : luecke@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : unknown
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiPretty printing for SoftFOL signatures.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Refer to <http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder for the SPASS syntax documentation.
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederinstance Pretty Sign where
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder pretty = pretty . signToSPLogicalPart
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Helper function. Generates a '.' as a Doc.
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederendOfListS :: String
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederendOfListS = "end_of_list."
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Creates a Doc from a SPASS Problem.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Pretty SPProblem where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pretty p = text "begin_problem" <> parens (text (identifier p)) <> dot
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ pretty (description p)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $+$ pretty (logicalPart p)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ printSettings (settings p)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich $+$ text "end_problem."
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Creates a Doc from a SPASS Logical Part.
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichinstance Pretty SPLogicalPart where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty (symbolList lp)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $+$ (case declarationList lp of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> empty
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just l -> text "list_of_declarations."
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ vcat (map pretty l)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ text endOfListS)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder $+$ vcat (map pretty $ formulaLists lp)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Creates a Doc from a SPASS Symbol List.
26d11a256b1433604a3dbc69913b520fff7586acChristian Maederinstance Pretty SPSymbolList where
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder pretty sl = text "list_of_symbols."
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder $+$ printSignSymList "functions" (functions sl)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder $+$ printSignSymList "predicates" (predicates sl)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder $+$ printSignSymList "sorts" (sorts sl)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder $+$ printSignSymList "operators" (operators sl)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder $+$ printSignSymList "quantifiers" (quantifiers sl)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ text endOfListS
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder printSignSymList lname list = case list of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> text lname <>
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder brackets (vcat $ punctuate comma $ map pretty list) <> dot
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Helper function. Creates a Doc from a Signature Symbol.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance Pretty SPSignSym where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pretty ssym = case ssym of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder SPSimpleSignSym s -> text s
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> parens (text (sym ssym) <> comma <> pretty (arity ssym))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Creates a Doc from a SPASS Declaration
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Pretty SPDeclaration where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty d = case d of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder SPSubsortDecl {sortSymA= a, sortSymB= b} ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder text "subsort" <> parens (text a <> comma <> text b) <> dot
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPTermDecl {termDeclTermList= l, termDeclTerm= t} ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty (SPQuantTerm {quantSym= SPForall, variableList= l, qFormula= t})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPSimpleTermDecl t ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pretty t <> dot
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder SPPredDecl {predSym= p, sortSyms= slist} ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty (SPComplexTerm {symbol= (SPCustomSymbol "predicate"), arguments=
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder (map (\x-> SPSimpleTerm (SPCustomSymbol x)) (p:slist))}) <> dot
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder SPGenDecl {sortSym= s, freelyGenerated= freelygen, funcList= l} ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder text "sort" <+> text s <+> (if freelygen then text "freely" else empty)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> text "generated by"
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder <+> brackets (hcat $ punctuate comma $ map text l) <> dot
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Creates a Doc from a SPASS Formula List
26d11a256b1433604a3dbc69913b520fff7586acChristian Maederinstance Pretty SPFormulaList where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty l = text "list_of_formulae" <> parens (pretty (originType l)) <> dot
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ vcat (map (\ x -> printFormula x <> dot) $ formulae l)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $+$ text endOfListS
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Creates a Doc from a SPASS Origin Type
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty SPOriginType where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty t = text $ case t of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder SPOriginAxioms -> "axioms"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder SPOriginConjectures -> "conjectures"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Creates a Doc from a SPASS Formula. Needed since SPFormula is just a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder 'type SPFormula = Named SPTerm' and thus instanciating Pretty is not
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintFormula :: SPFormula-> Doc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintFormula f =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder text "formula" <> parens (pretty (sentence f) <> comma <> text (senAttr f))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Creates a Doc from a SPASS Term.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty SPTerm where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty t = case t of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder SPQuantTerm{quantSym= qsym, variableList= tlist, qFormula= tt} ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty qsym <>
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder parens (brackets (printTermList tlist) <> comma <> pretty tt)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski SPSimpleTerm stsym -> pretty stsym
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder SPComplexTerm{symbol= ctsym, arguments= args} ->
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pretty ctsym <>
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski if null args then empty else parens (printTermList args)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printTermList = hcat . punctuate comma . map pretty
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Creates a Doc from a SPASS Quantifier Symbol.
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederinstance Pretty SPQuantSym where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pretty qs = text $ case qs of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SPForall -> "forall"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SPExists -> "exists"
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder SPCustomQuantSym cst -> cst
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Creates a Doc from a SPASS Symbol.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- printSymbol :: SPSymbol-> Doc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Pretty SPSymbol where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty s = text $ case s of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPEqual -> "equal"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPTrue -> "true"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPFalse -> "false"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPAnd -> "and"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SPNot -> "not"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder SPImplies -> "implies"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder SPImplied -> "implied"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPEquiv -> "equiv"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPDiv -> "div"
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder SPComp -> "comp"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPSum -> "sum"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPConv -> "conv"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPCustomSymbol cst -> cst
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Creates a Doc from a SPASS description.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty SPDescription where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let sptext str v = text str <> parens (textBraces $ text v) <> dot
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mtext str = maybe empty $ sptext str
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in text "list_of_descriptions."
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $+$ sptext "name" (name d)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $+$ sptext "author" (author d)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $+$ mtext "version" (version d)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $+$ mtext "logic" (logic d)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $+$ text "status" <> parens (pretty $ status d) <> dot
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $+$ sptext "description" (desc d)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $+$ mtext "date" (date d)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $+$ text endOfListS
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder surrounds a doc with "{* *}" as required for some of the
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski description fields and the settings.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedertextBraces :: Doc -> Doc
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedertextBraces d = text "{* " <> d <> text " *}"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Creates a Doc from an 'SPLogState'.
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Pretty SPLogState where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pretty s = text $ case s of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder SPStateSatisfiable -> "satisfiable"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SPStateUnsatisfiable -> "unsatisfiable"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SPStateUnknown -> "unknown"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederprintSettings :: [SPSetting] -> Doc
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederprintSettings [] = empty
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian MaederprintSettings l = case l of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder text "list_of_settings(SPASS)." $+$
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder textBraces (hcat (map (pretty) l)) $+$
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder text endOfListS
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Pretty SPSetting where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pretty (SPGeneralSettings e) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder hcat (map (\es -> case es of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SPHypothesis labels ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder text "hypothesis" <>
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder brackets (sepByCommas (map (pretty) labels)) <> dot)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pretty (SPSettings _ body) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder hcat (map pretty body)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance Pretty SPSettingBody where
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pretty (SPFlag sw v) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder text sw <> parens (sepByCommas (map (pretty) v)) <> dot
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pretty (SPClauseRelation cfrList) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder text "set_clauseFormulaRelation" <> parens (sepByCommas (map (pretty) cfrList)) <> dot
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Pretty SPCRBIND where
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pretty (SPCRBIND cSPR fSPR) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder text cSPR <> comma <> text fSPR