{- |
Module      :  ./SoftFOL/PrintTPTP.hs
Description :  Pretty printing for SPASS signatures in TPTP syntax.
Copyright   :  (c) Rene Wagner, Rainer Grabbe, Uni Bremen 2005-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  unknown

Pretty printing for SoftFOL signatures in TPTP syntax.
   Refer to <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
   for the TPTP syntax documentation.

-}

module SoftFOL.PrintTPTP where

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils

import SoftFOL.Sign
import SoftFOL.Conversions

import Data.Maybe

{- | This type class allows pretty printing in TPTP syntax of instantiated data
types -}
class PrintTPTP a where
    printTPTP :: a -> Doc

instance Pretty TPTP where
    pretty :: TPTP -> Doc
pretty (FormAnno _ _ _ t :: SPTerm
t _) = SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
t
    pretty _ = Doc
empty

{- |
  Helper function. Generates a separating comment line.
-}
separator :: String
separator :: String
separator = '%' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> Char -> String
forall a. Int -> a -> [a]
replicate 75 '-'

instance PrintTPTP Sign where
    printTPTP :: Sign -> Doc
printTPTP = SPLogicalPart -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPLogicalPart -> Doc) -> (Sign -> SPLogicalPart) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> SPLogicalPart
signToSPLogicalPart

{- |
  Creates a Doc from a SoftFOL Problem.
-}
instance PrintTPTP SPProblem where
    printTPTP :: SPProblem -> Doc
printTPTP p :: SPProblem
p = String -> Doc
text String
separator
      Doc -> Doc -> Doc
$+$ String -> Doc
text "% Problem" Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text (SPProblem -> String
identifier SPProblem
p)
      Doc -> Doc -> Doc
$+$ SPDescription -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPProblem -> SPDescription
description SPProblem
p)
      Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPSetting -> Doc) -> [SPSetting] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPSetting -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP ([SPSetting] -> [Doc]) -> [SPSetting] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPProblem -> [SPSetting]
settings SPProblem
p)
      Doc -> Doc -> Doc
$+$ String -> Doc
text String
separator
      Doc -> Doc -> Doc
$+$ SPLogicalPart -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPProblem -> SPLogicalPart
logicalPart SPProblem
p)

{- |
  Creates a Doc from a SoftFOL Logical Part.
-}
instance PrintTPTP SPLogicalPart where
    printTPTP :: SPLogicalPart -> Doc
printTPTP lp :: SPLogicalPart
lp =
      let decls :: Maybe [SPDeclaration]
decls = SPLogicalPart -> Maybe [SPDeclaration]
declarationList SPLogicalPart
lp
          validDeclarations :: [SPDeclaration]
validDeclarations = (SPDeclaration -> Bool) -> [SPDeclaration] -> [SPDeclaration]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ decl :: SPDeclaration
decl -> case SPDeclaration
decl of
              SPSubsortDecl {} -> Bool
True
              SPTermDecl {} -> Bool
True
              SPSimpleTermDecl _ -> Bool
True
              _ -> Bool
False)
                     ([SPDeclaration] -> [SPDeclaration])
-> [SPDeclaration] -> [SPDeclaration]
forall a b. (a -> b) -> a -> b
$ [SPDeclaration] -> Maybe [SPDeclaration] -> [SPDeclaration]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [SPDeclaration]
decls
          fs :: [SPFormulaList]
fs = SPLogicalPart -> [SPFormulaList]
formulaLists SPLogicalPart
lp
      in if [SPDeclaration] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPDeclaration]
validDeclarations Bool -> Bool -> Bool
&& [SPFormulaList] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPFormulaList]
fs then
            String -> Doc
text "fof" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens
              (String -> Doc
text "empty" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPOriginType -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPOriginType
SPOriginAxioms
               Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPSymbol -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPSymbol
SPTrue) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
         else [Doc] -> Doc
vcat (((SPDeclaration, Int) -> Doc) -> [(SPDeclaration, Int)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (decl :: SPDeclaration
decl, i :: Int
i) ->
                    String -> Doc
text "fof" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
                    Doc -> Doc
parens (String -> Doc
text ("declaration" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
                    SPOriginType -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPOriginType
SPOriginAxioms Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
                    Doc -> Doc -> Doc
$+$ SPDeclaration -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPDeclaration
decl) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot)
                ([(SPDeclaration, Int)] -> [Doc])
-> [(SPDeclaration, Int)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [SPDeclaration] -> [Int] -> [(SPDeclaration, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SPDeclaration]
validDeclarations [(0 :: Int) ..])
         Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPFormulaList -> Doc) -> [SPFormulaList] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPFormulaList -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP [SPFormulaList]
fs)

{- |
 Creates a Doc from a SoftFOL Declaration.
 A subsort declaration will be rewritten as a special SPQuantTerm.
-}
instance PrintTPTP SPDeclaration where
    printTPTP :: SPDeclaration -> Doc
printTPTP decl :: SPDeclaration
decl = case SPDeclaration
decl of
      SPSubsortDecl {sortSymA :: SPDeclaration -> SPIdentifier
sortSymA = SPIdentifier
sortA, sortSymB :: SPDeclaration -> SPIdentifier
sortSymB = SPIdentifier
sortB}
        -> let subsortVar :: [SPTerm]
subsortVar = [SPIdentifier] -> [SPTerm]
spTerms ([SPIdentifier] -> [SPTerm]) -> [SPIdentifier] -> [SPTerm]
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList SPIdentifier
sortA [SPIdentifier
sortB]
           in SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm
             { quantSym :: SPQuantSym
quantSym = SPQuantSym
SPForall,
               variableList :: [SPTerm]
variableList = [SPTerm]
subsortVar,
               qFormula :: SPTerm
qFormula = SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPImplies
                 [ SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
sortA) [SPTerm]
subsortVar
                 , SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
sortB) [SPTerm]
subsortVar] }
      SPTermDecl {termDeclTermList :: SPDeclaration -> [SPTerm]
termDeclTermList = [SPTerm]
tlist, termDeclTerm :: SPDeclaration -> SPTerm
termDeclTerm = SPTerm
tt}
        -> SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm {
                       quantSym :: SPQuantSym
quantSym = SPQuantSym
SPForall,
                       variableList :: [SPTerm]
variableList = [SPTerm]
tlist,
                       qFormula :: SPTerm
qFormula = SPTerm
tt}
      SPSimpleTermDecl stsym :: SPTerm
stsym -> SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
stsym
      pd :: SPDeclaration
pd@(SPPredDecl {}) -> Doc -> (SPTerm -> Doc) -> Maybe SPTerm -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (Maybe SPTerm -> Doc) -> Maybe SPTerm -> Doc
forall a b. (a -> b) -> a -> b
$ SPDeclaration -> Maybe SPTerm
predDecl2Term SPDeclaration
pd
      _ -> Doc
empty

{- |
  Creates a Doc from a SoftFOL Formula List.
-}
instance PrintTPTP SPFormulaList where
    printTPTP :: SPFormulaList -> Doc
printTPTP l :: SPFormulaList
l = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SPFormula -> Doc) -> [SPFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SPOriginType -> SPFormula -> Doc
printFormula (SPOriginType -> SPFormula -> Doc)
-> SPOriginType -> SPFormula -> Doc
forall a b. (a -> b) -> a -> b
$ SPFormulaList -> SPOriginType
originType SPFormulaList
l) ([SPFormula] -> [Doc]) -> [SPFormula] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPFormulaList -> [SPFormula]
formulae SPFormulaList
l

{- |
  Creates a Doc from a SoftFOL Origin Type.
-}
instance PrintTPTP SPOriginType where
    printTPTP :: SPOriginType -> Doc
printTPTP t :: SPOriginType
t = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPOriginType
t of
        SPOriginAxioms -> "axiom"
        SPOriginConjectures -> "conjecture"

{- |
  Creates a Doc from a SoftFOL Formula. Needed since SPFormula is just a
  'type SPFormula = Named SPTerm' and thus instanciating PrintTPTP is not
  possible.
-}
printFormula :: SPOriginType -> SPFormula -> Doc
-- printFormula ot f = printFormulaText ot (senAttr f) (sentence f)
printFormula :: SPOriginType -> SPFormula -> Doc
printFormula ot :: SPOriginType
ot f :: SPFormula
f =
    String -> Doc
text "fof" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (String -> Doc
text (SPFormula -> String
forall s a. SenAttr s a -> a
senAttr SPFormula
f) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPOriginType -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPOriginType
ot Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
                          Doc -> Doc -> Doc
$+$ SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPFormula -> SPTerm
forall s a. SenAttr s a -> s
sentence SPFormula
f)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot

{- |
  Creates a Doc from a SoftFOL Term.
-}
instance PrintTPTP SPTerm where
    printTPTP :: SPTerm -> Doc
printTPTP t :: SPTerm
t = case SPTerm
t of
      SPQuantTerm {quantSym :: SPTerm -> SPQuantSym
quantSym = SPQuantSym
qsym, variableList :: SPTerm -> [SPTerm]
variableList = [SPTerm]
tlist, qFormula :: SPTerm -> SPTerm
qFormula = SPTerm
tt} -> let
        isComplexTerm :: SPTerm -> Bool
isComplexTerm tm :: SPTerm
tm = case SPTerm
tm of
            SPComplexTerm _ [] -> Bool
False
            _ -> Bool
True
        getVars :: SPTerm -> [SPTerm]
getVars tm :: SPTerm
tm = case SPTerm
tm of
            SPComplexTerm _ args :: [SPTerm]
args ->
              if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args then [SPTerm
tm] else (SPTerm -> [SPTerm]) -> [SPTerm] -> [SPTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPTerm]
getVars [SPTerm]
args
            _ -> []
        cl :: [SPTerm]
cl = (SPTerm -> Bool) -> [SPTerm] -> [SPTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter SPTerm -> Bool
isComplexTerm [SPTerm]
tlist
        conj :: SPTerm
conj = case SPQuantSym
qsym of
                 SPExists -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPAnd ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ [SPTerm]
cl [SPTerm] -> [SPTerm] -> [SPTerm]
forall a. [a] -> [a] -> [a]
++ [SPTerm
tt]
                 _ -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPImplies ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ (case [SPTerm]
cl of
                   [hd :: SPTerm
hd] -> SPTerm
hd
                   _ -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPAnd [SPTerm]
cl) SPTerm -> [SPTerm] -> [SPTerm]
forall a. a -> [a] -> [a]
: [SPTerm
tt]
        in SPQuantSym -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPQuantSym
qsym
           Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([SPTerm] -> Doc
printCommaSeparated ([SPTerm] -> Doc) -> [SPTerm] -> Doc
forall a b. (a -> b) -> a -> b
$ (SPTerm -> [SPTerm]) -> [SPTerm] -> [SPTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPTerm]
getVars [SPTerm]
tlist)
           Doc -> Doc -> Doc
<+> Doc
colon
           -- either all variables are simple terms
           Doc -> Doc -> Doc
<+> if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
cl then SPTerm -> Doc
parPrintTPTP SPTerm
tt
               -- or there are none simple terms
               else
          {- construct premiss for implication out of variableList (Forall)
          construct conjunction out of variableList (Exists) -}
               Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
conj
      SPComplexTerm {symbol :: SPTerm -> SPSymbol
symbol = SPSymbol
ctsym, arguments :: SPTerm -> [SPTerm]
arguments = [SPTerm]
args}
        -> SPSymbol -> [SPTerm] -> Doc
printTermList SPSymbol
ctsym [SPTerm]
args

{- |
  Creates a Doc from a list of SoftFOL Terms connected by a SoftFOL Symbol.
-}
printTermList :: SPSymbol -> [SPTerm] -> Doc
printTermList :: SPSymbol -> [SPTerm] -> Doc
printTermList symb :: SPSymbol
symb terms :: [SPTerm]
terms = let
  sbd :: Doc
sbd = SPSymbol -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPSymbol
symb
  d :: Doc
d = if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
terms then Doc
sbd else Doc
sbd Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([SPTerm] -> Doc
printCommaSeparated [SPTerm]
terms)
  in case SPSymbol
symb of
  SPNot -> case [SPTerm]
terms of
        [t :: SPTerm
t] -> Doc
sbd Doc -> Doc -> Doc
<+> SPTerm -> Doc
parPrintTPTP SPTerm
t
        _ -> Doc
d
  _ -> if SPSymbol -> [SPSymbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SPSymbol
symb ([SPSymbol] -> Bool) -> [SPSymbol] -> Bool
forall a b. (a -> b) -> a -> b
$ SPSymbol
SPEqual SPSymbol -> [SPSymbol] -> [SPSymbol]
forall a. a -> [a] -> [a]
: [SPSymbol]
binLogOps then
     [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
prepPunctuate (Doc
sbd Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (SPTerm -> Doc) -> [SPTerm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Doc
parPrintTPTP [SPTerm]
terms
     else Doc
d

{- |
  Helper function. Generates a comma separated list of SoftFOL Terms as a Doc.
-}
printCommaSeparated :: [SPTerm] -> Doc
printCommaSeparated :: [SPTerm] -> Doc
printCommaSeparated = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([SPTerm] -> [Doc]) -> [SPTerm] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPTerm -> Doc) -> [SPTerm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP

parPrintTPTP :: SPTerm -> Doc
parPrintTPTP :: SPTerm -> Doc
parPrintTPTP t :: SPTerm
t = (if SPTerm -> Bool
isUnitary SPTerm
t then Doc -> Doc
forall a. a -> a
id else Doc -> Doc
parens) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
t

isUnitary :: SPTerm -> Bool
isUnitary :: SPTerm -> Bool
isUnitary t :: SPTerm
t = case SPTerm
t of
    SPComplexTerm {symbol :: SPTerm -> SPSymbol
symbol = SPSymbol
ctsym, arguments :: SPTerm -> [SPTerm]
arguments = _ : _ : _} ->
       SPSymbol -> [SPSymbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem SPSymbol
ctsym [SPSymbol]
binLogOps
    _ -> Bool
True

binLogOps :: [SPSymbol]
binLogOps :: [SPSymbol]
binLogOps = [SPSymbol
SPOr, SPSymbol
SPAnd, SPSymbol
SPImplies, SPSymbol
SPImplied, SPSymbol
SPEquiv]

{- |
  Creates a Doc from a SoftFOL Quantifier Symbol.
-}
instance PrintTPTP SPQuantSym where
    printTPTP :: SPQuantSym -> Doc
printTPTP qs :: SPQuantSym
qs = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPQuantSym
qs of
        SPForall -> "!"
        SPExists -> "?"
        SPCustomQuantSym cst :: SPIdentifier
cst -> SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst

{- |
  Creates a Doc from a SoftFOL Symbol.
-}
instance PrintTPTP SPSymbol where
    printTPTP :: SPSymbol -> Doc
printTPTP s :: SPSymbol
s = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPSymbol
s of
        SPEqual -> "="
        SPTrue -> "$true"
        SPFalse -> "$false"
        SPOr -> "|"
        SPAnd -> "&"
        SPNot -> "~"
        SPImplies -> "=>"
        SPImplied -> "<="
        SPEquiv -> "<=>"
        SPCustomSymbol cst :: SPIdentifier
cst -> SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst
        _ -> SPSymbol -> String
showSPSymbol SPSymbol
s

{- |
  Creates a Doc from a SoftFOL description.
-}
instance PrintTPTP SPDescription where
    printTPTP :: SPDescription -> Doc
printTPTP d :: SPDescription
d = String -> String -> Doc
spCommentText "Name   " (SPDescription -> String
name SPDescription
d)
      Doc -> Doc -> Doc
$+$ String -> String -> Doc
spCommentText "Author " (SPDescription -> String
author SPDescription
d)
      Doc -> Doc -> Doc
$+$ Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (String -> String -> Doc
spCommentText "Version") (SPDescription -> Maybe String
version SPDescription
d)
      Doc -> Doc -> Doc
$+$ Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (String -> String -> Doc
spCommentText "Logic  ") (SPDescription -> Maybe String
logic SPDescription
d)
      Doc -> Doc -> Doc
$+$ String -> Doc
text "% Status " Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> SPLogState -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPDescription -> SPLogState
status SPDescription
d)
      Doc -> Doc -> Doc
$+$ String -> String -> Doc
spCommentText "Desc   " (SPDescription -> String
desc SPDescription
d)
      Doc -> Doc -> Doc
$+$ Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (String -> String -> Doc
spCommentText "Date   ") (SPDescription -> Maybe String
date SPDescription
d)

{- |
  Helper function. Creates a formatted comment output for a description field.
  On left side will be displayed the field's name, on right side its content.
-}
spCommentText :: String -> String -> Doc
spCommentText :: String -> String -> Doc
spCommentText fieldName :: String
fieldName fieldDesc :: String
fieldDesc =
    [Doc] -> Doc
hsep [String -> Doc
text "%", String -> Doc
text String
fieldName, Doc
colon, String -> Doc
text String
fieldDesc]

{- |
  Creates a Doc from an 'SPLogState'.
-}
instance PrintTPTP SPLogState where
    printTPTP :: SPLogState -> Doc
printTPTP s :: SPLogState
s = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPLogState
s of
      SPStateSatisfiable -> "satisfiable"
      SPStateUnsatisfiable -> "unsatisfiable"
      SPStateUnknown -> "unknown"

instance PrintTPTP SPSetting where
    printTPTP :: SPSetting -> Doc
printTPTP s :: SPSetting
s = String -> String -> Doc
spCommentText "Option " "" Doc -> Doc -> Doc
<+> case SPSetting
s of
      SPGeneralSettings e :: [SPHypothesis]
e -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [SPHypothesis] -> String
forall a. Show a => a -> String
show [SPHypothesis]
e
      SPSettings _ settingText :: [SPSettingBody]
settingText -> [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SPSettingBody -> Doc) -> [SPSettingBody] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPSettingBody -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP [SPSettingBody]
settingText

instance PrintTPTP SPSettingBody where
    printTPTP :: SPSettingBody -> Doc
printTPTP s :: SPSettingBody
s = case SPSettingBody
s of
      SPFlag sw :: String
sw v :: [String]
v -> [Doc] -> Doc
hcat
        [String -> Doc
text String
sw, if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
v then Doc
empty else
                      Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
v]
      _ -> Doc
empty