{- |
Module      :  ./SoftFOL/Print.hs
Description :  Pretty printing for SoftFOL problems in DFG.
Copyright   :  (c) Rene Wagner, C. Maeder, Uni Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

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

Pretty printing for SoftFOL signatures.
   Refer to <http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html>
   for the SPASS syntax documentation.
-}

module SoftFOL.Print (printFormula) where

import qualified Data.Map as Map
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id

import SoftFOL.Sign

instance Pretty SFSymbol where
  pretty :: SFSymbol -> Doc
pretty sy :: SFSymbol
sy = [Doc] -> Doc
cat [String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show (SPIdentifier -> String) -> SPIdentifier -> String
forall a b. (a -> b) -> a -> b
$ SFSymbol -> SPIdentifier
sym_ident SFSymbol
sy) , SFSymbType -> Doc
forall a. Pretty a => a -> Doc
pretty (SFSymbol -> SFSymbType
sym_type SFSymbol
sy)]

instance Pretty SFSymbType where
  pretty :: SFSymbType -> Doc
pretty st :: SFSymbType
st = case SFSymbType
st of
     SFOpType args :: [SPIdentifier]
args res :: SPIdentifier
res -> [Doc] -> Doc
sep [Doc
colon Doc -> Doc -> Doc
<+> [SPIdentifier] -> Doc
pr [SPIdentifier]
args, Doc
funArrow
       Doc -> Doc -> Doc
<+> String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
res)]
     SFPredType args :: [SPIdentifier]
args -> Doc
colon Doc -> Doc -> Doc
<+> [SPIdentifier] -> Doc
pr [SPIdentifier]
args
     SFSortType -> Doc
empty
     where pr :: [SPIdentifier] -> Doc
pr = [Doc] -> Doc
sep ([Doc] -> Doc)
-> ([SPIdentifier] -> [Doc]) -> [SPIdentifier] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
cross) ([Doc] -> [Doc])
-> ([SPIdentifier] -> [Doc]) -> [SPIdentifier] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPIdentifier -> Doc) -> [SPIdentifier] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (SPIdentifier -> String) -> SPIdentifier -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> String
forall a. Show a => a -> String
show)

{- |
  Helper function.
-}
endOfListS :: Doc
endOfListS :: Doc
endOfListS = String -> Doc
text "end_of_list."

{- |
  Creates a Doc from a SPASS Problem.
-}
instance Pretty SPProblem where
  pretty :: SPProblem -> Doc
pretty p :: SPProblem
p = String -> Doc
text "begin_problem" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ SPProblem -> String
identifier SPProblem
p) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    Doc -> Doc -> Doc
$++$ SPDescription -> Doc
forall a. Pretty a => a -> Doc
pretty (SPProblem -> SPDescription
description SPProblem
p)
    Doc -> Doc -> Doc
$++$ SPLogicalPart -> Doc
forall a. Pretty a => a -> Doc
pretty (SPProblem -> SPLogicalPart
logicalPart SPProblem
p)
    Doc -> Doc -> Doc
$++$ [SPSetting] -> Doc
printSettings (SPProblem -> [SPSetting]
settings SPProblem
p)
    Doc -> Doc -> Doc
$++$ String -> Doc
text "end_problem."

{- |
  Creates a Doc from a SPASS Logical Part.
-}
instance Pretty SPLogicalPart where
  pretty :: SPLogicalPart -> Doc
pretty lp :: SPLogicalPart
lp = Maybe SPSymbolList -> Doc
forall a. Pretty a => a -> Doc
pretty (SPLogicalPart -> Maybe SPSymbolList
symbolList SPLogicalPart
lp)
       Doc -> Doc -> Doc
$++$ (case SPLogicalPart -> Maybe [SPDeclaration]
declarationList SPLogicalPart
lp of
         Nothing -> Doc
empty
         Just l :: [SPDeclaration]
l -> String -> Doc
text "list_of_declarations."
           Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPDeclaration -> Doc) -> [SPDeclaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPDeclaration -> Doc
forall a. Pretty a => a -> Doc
pretty [SPDeclaration]
l)
           Doc -> Doc -> Doc
$+$ Doc
endOfListS)
       Doc -> Doc -> Doc
$++$ [Doc] -> Doc
vcat ((SPFormulaList -> Doc) -> [SPFormulaList] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPFormulaList -> Doc
forall a. Pretty a => a -> Doc
pretty ([SPFormulaList] -> [Doc]) -> [SPFormulaList] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPLogicalPart -> [SPFormulaList]
formulaLists SPLogicalPart
lp)
       Doc -> Doc -> Doc
$++$ [Doc] -> Doc
vcat ((SPClauseList -> Doc) -> [SPClauseList] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPClauseList -> Doc
forall a. Pretty a => a -> Doc
pretty ([SPClauseList] -> [Doc]) -> [SPClauseList] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPLogicalPart -> [SPClauseList]
clauseLists SPLogicalPart
lp)
       Doc -> Doc -> Doc
$++$ [Doc] -> Doc
vcat ((SPProofList -> Doc) -> [SPProofList] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPProofList -> Doc
forall a. Pretty a => a -> Doc
pretty ([SPProofList] -> [Doc]) -> [SPProofList] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPLogicalPart -> [SPProofList]
proofLists SPLogicalPart
lp)

{- |
  Creates a Doc from a SPASS Symbol List.
-}
instance Pretty SPSymbolList where
  pretty :: SPSymbolList -> Doc
pretty sl :: SPSymbolList
sl = String -> Doc
text "list_of_symbols."
    Doc -> Doc -> Doc
$+$ String -> [SPSignSym] -> Doc
forall a. Pretty a => String -> [a] -> Doc
printSignSymList "functions" (SPSymbolList -> [SPSignSym]
functions SPSymbolList
sl)
    Doc -> Doc -> Doc
$+$ String -> [SPSignSym] -> Doc
forall a. Pretty a => String -> [a] -> Doc
printSignSymList "predicates" (SPSymbolList -> [SPSignSym]
predicates SPSymbolList
sl)
    Doc -> Doc -> Doc
$+$ (if [SPSignSym] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SPSignSym] -> Bool) -> [SPSignSym] -> Bool
forall a b. (a -> b) -> a -> b
$ SPSymbolList -> [SPSignSym]
sorts SPSymbolList
sl then Doc
empty else
         String -> Doc
text "sorts" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets ([SPSignSym] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas ([SPSignSym] -> Doc) -> [SPSignSym] -> Doc
forall a b. (a -> b) -> a -> b
$ SPSymbolList -> [SPSignSym]
sorts SPSymbolList
sl) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot)
    Doc -> Doc -> Doc
$+$ Doc
endOfListS
    where
      printSignSymList :: String -> [a] -> Doc
printSignSymList lname :: String
lname list :: [a]
list = if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
list then Doc
empty else
        [Doc] -> Doc
cat [ String -> Doc
text String
lname
            , Doc -> Doc
brackets ([Doc] -> Doc
fsep ([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
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
list) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot]

{- |
  Helper function. Creates a Doc from a Signature Symbol.
-}
instance Pretty SPSignSym where
  pretty :: SPSignSym -> Doc
pretty ssym :: SPSignSym
ssym = case SPSignSym
ssym of
      SPSimpleSignSym s :: SPIdentifier
s -> String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
s)
      _ -> Doc -> Doc
parens (String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show (SPIdentifier -> String) -> SPIdentifier -> String
forall a b. (a -> b) -> a -> b
$ SPSignSym -> SPIdentifier
sym SPSignSym
ssym) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty (SPSignSym -> Int
arity SPSignSym
ssym))

{- |
  Creates a Doc from a SPASS Declaration
-}
instance Pretty SPDeclaration where
  pretty :: SPDeclaration -> Doc
pretty d :: SPDeclaration
d = case SPDeclaration
d of
    SPSubsortDecl {sortSymA :: SPDeclaration -> SPIdentifier
sortSymA = SPIdentifier
a, sortSymB :: SPDeclaration -> SPIdentifier
sortSymB = SPIdentifier
b} ->
      String -> Doc
text "subsort" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
a) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
b))
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    SPTermDecl {termDeclTermList :: SPDeclaration -> [SPTerm]
termDeclTermList = [SPTerm]
l, termDeclTerm :: SPDeclaration -> SPTerm
termDeclTerm = SPTerm
t} ->
      SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm {quantSym :: SPQuantSym
quantSym = SPQuantSym
SPForall, variableList :: [SPTerm]
variableList = [SPTerm]
l, qFormula :: SPTerm
qFormula = SPTerm
t}
        Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    SPSimpleTermDecl t :: SPTerm
t -> SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    SPPredDecl {predSym :: SPDeclaration -> SPIdentifier
predSym = SPIdentifier
p, sortSyms :: SPDeclaration -> [SPIdentifier]
sortSyms = [SPIdentifier]
slist} ->
      SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty (SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPSymbol
forall a b. (a -> b) -> a -> b
$ String -> SPIdentifier
mkSimpleId "predicate") ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ (SPIdentifier -> SPTerm) -> [SPIdentifier] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map
                  (SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm)
-> (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> SPSymbol
spSym) ([SPIdentifier] -> [SPTerm]) -> [SPIdentifier] -> [SPTerm]
forall a b. (a -> b) -> a -> b
$ SPIdentifier
p SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
forall a. a -> [a] -> [a]
: [SPIdentifier]
slist) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    SPGenDecl {sortSym :: SPDeclaration -> SPIdentifier
sortSym = SPIdentifier
s, freelyGenerated :: SPDeclaration -> Bool
freelyGenerated = Bool
freelygen, funcList :: SPDeclaration -> [SPIdentifier]
funcList = [SPIdentifier]
l} ->
      String -> Doc
text "sort" Doc -> Doc -> Doc
<+> String -> Doc
text (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
s)
        Doc -> Doc -> Doc
<+> (if Bool
freelygen then String -> Doc
text "freely" else Doc
empty)
        Doc -> Doc -> Doc
<+> String -> Doc
text "generated by"
        Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Doc] -> Doc
fsep ([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
$ (SPIdentifier -> Doc) -> [SPIdentifier] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (SPIdentifier -> String) -> SPIdentifier -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> String
forall a. Show a => a -> String
show) [SPIdentifier]
l) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot

{- |
  Creates a Doc from a SPASS Formula List
-}
instance Pretty SPFormulaList where
  pretty :: SPFormulaList -> Doc
pretty l :: SPFormulaList
l = String -> Doc
text "list_of_formulae" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (SPOriginType -> Doc
forall a. Pretty a => a -> Doc
pretty (SPFormulaList -> SPOriginType
originType SPFormulaList
l)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPFormula -> Doc) -> [SPFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPFormula -> Doc
printFormula ([SPFormula] -> [Doc]) -> [SPFormula] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPFormulaList -> [SPFormula]
formulae SPFormulaList
l)
    Doc -> Doc -> Doc
$+$ Doc
endOfListS

instance Pretty SPClauseList where
  pretty :: SPClauseList -> Doc
pretty l :: SPClauseList
l = String -> Doc
text "list_of_clauses" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (SPOriginType -> Doc
forall a. Pretty a => a -> Doc
pretty (SPClauseList -> SPOriginType
coriginType SPClauseList
l)
           Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> SPClauseType -> Doc
forall a. Pretty a => a -> Doc
pretty (SPClauseList -> SPClauseType
clauseType SPClauseList
l)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPClause -> Doc) -> [SPClause] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPClause -> Doc
printClause ([SPClause] -> [Doc]) -> [SPClause] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPClauseList -> [SPClause]
clauses SPClauseList
l)
    Doc -> Doc -> Doc
$+$ Doc
endOfListS

instance Pretty SPProofList where
  pretty :: SPProofList -> Doc
pretty l :: SPProofList
l = String -> Doc
text "list_of_proof" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (SPIdentifier -> Doc) -> Maybe SPIdentifier -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty
    (Doc -> Doc
parens (Doc -> Doc) -> (SPIdentifier -> Doc) -> SPIdentifier -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPAssocList -> Doc
printAssocList (SPProofList -> SPAssocList
plAssocList SPProofList
l)) (Doc -> Doc) -> (SPIdentifier -> Doc) -> SPIdentifier -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> Doc
forall a. Pretty a => a -> Doc
pretty) (SPProofList -> Maybe SPIdentifier
proofType SPProofList
l)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPProofStep -> Doc) -> [SPProofStep] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPProofStep -> Doc
printStep ([SPProofStep] -> [Doc]) -> [SPProofStep] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPProofList -> [SPProofStep]
step SPProofList
l)
    Doc -> Doc -> Doc
$+$ Doc
endOfListS

printAssocList :: SPAssocList -> Doc
printAssocList :: SPAssocList -> Doc
printAssocList m :: SPAssocList
m = if SPAssocList -> Bool
forall k a. Map k a -> Bool
Map.null SPAssocList
m then Doc
empty else Doc
comma Doc -> Doc -> Doc
<+>
    Doc -> Doc
brackets ([Doc] -> Doc
fsep ([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
$ ((SPKey, SPValue) -> Doc) -> [(SPKey, SPValue)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map
      ( \ (k :: SPKey
k, v :: SPValue
v) -> SPKey -> Doc
forall a. Pretty a => a -> Doc
pretty SPKey
k Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text ":" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPValue -> Doc
forall a. Pretty a => a -> Doc
pretty SPValue
v) ([(SPKey, SPValue)] -> [Doc]) -> [(SPKey, SPValue)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ SPAssocList -> [(SPKey, SPValue)]
forall k a. Map k a -> [(k, a)]
Map.toList SPAssocList
m)

instance Pretty SPKey where
    pretty :: SPKey -> Doc
pretty (PKeyTerm t :: SPTerm
t) = SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t

instance Pretty SPValue where
    pretty :: SPValue -> Doc
pretty (PValTerm t :: SPTerm
t) = SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t

{- |
  Creates a Doc from a SPASS Origin Type
-}
instance Pretty SPOriginType where
  pretty :: SPOriginType -> Doc
pretty t :: SPOriginType
t = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPOriginType
t of
    SPOriginAxioms -> "axioms"
    SPOriginConjectures -> "conjectures"

instance Pretty SPClauseType where
  pretty :: SPClauseType -> Doc
pretty t :: SPClauseType
t = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPClauseType
t of
    SPCNF -> "cnf"
    SPDNF -> "dnf"

{- |
  Creates a Doc from a SPASS Formula. Needed since SPFormula is just a
  'type SPFormula = Named SPTerm' and thus instantiating Pretty is not
  possible.
-}
printFormula :: SPFormula -> Doc
printFormula :: SPFormula -> Doc
printFormula f :: SPFormula
f = [Doc] -> Doc
cat [String -> Doc
text "formula", Doc -> Doc
parens ([Doc] -> Doc
sepByCommas
  ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty (SPFormula -> SPTerm
forall s a. SenAttr s a -> s
sentence SPFormula
f) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: SPFormula -> [Doc]
forall a. Named a -> [Doc]
printSenAttr SPFormula
f) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot]

printClause :: SPClause -> Doc
printClause :: SPClause -> Doc
printClause c :: SPClause
c = [Doc] -> Doc
cat [String -> Doc
text "clause", Doc -> Doc
parens ([Doc] -> Doc
sepByCommas
  ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ NSPClause -> Doc
forall a. Pretty a => a -> Doc
pretty (SPClause -> NSPClause
forall s a. SenAttr s a -> s
sentence SPClause
c) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: SPClause -> [Doc]
forall a. Named a -> [Doc]
printSenAttr SPClause
c) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot]

printSenAttr :: Named a -> [Doc]
printSenAttr :: Named a -> [Doc]
printSenAttr c :: Named a
c = case Named a -> String
forall s a. SenAttr s a -> a
senAttr Named a
c of
      "" -> []
      s :: String
s -> [String -> Doc
text String
s]

instance Pretty NSPClause where
    pretty :: NSPClause -> Doc
pretty t :: NSPClause
t = case NSPClause
t of
        QuanClause vs :: [SPTerm]
vs b :: NSPClauseBody
b -> SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty (SPTerm -> Doc) -> SPTerm -> Doc
forall a b. (a -> b) -> a -> b
$ SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm (case NSPClauseBody
b of
              NSPClauseBody SPCNF _ -> SPQuantSym
SPForall
              NSPClauseBody SPDNF _ -> SPQuantSym
SPExists) [SPTerm]
vs (NSPClauseBody -> SPTerm
clauseBodyToSPTerm NSPClauseBody
b)
        SimpleClause b :: NSPClauseBody
b -> SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty (SPTerm -> Doc) -> SPTerm -> Doc
forall a b. (a -> b) -> a -> b
$ NSPClauseBody -> SPTerm
clauseBodyToSPTerm NSPClauseBody
b
        BriefClause l1 :: TermWsList
l1 l2 :: TermWsList
l2 l3 :: TermWsList
l3 -> [Doc] -> Doc
fsep
            [TermWsList -> Doc
forall a. Pretty a => a -> Doc
pretty TermWsList
l1, String -> Doc
text "||", TermWsList -> Doc
forall a. Pretty a => a -> Doc
pretty TermWsList
l2, String -> Doc
text "->", TermWsList -> Doc
forall a. Pretty a => a -> Doc
pretty TermWsList
l3]

clauseBodyToSPTerm :: NSPClauseBody -> SPTerm
clauseBodyToSPTerm :: NSPClauseBody -> SPTerm
clauseBodyToSPTerm (NSPClauseBody ct :: SPClauseType
ct l :: [SPLiteral]
l) = SPSymbol -> [SPTerm] -> SPTerm
compTerm (case SPClauseType
ct of
    SPCNF -> SPSymbol
SPOr
    SPDNF -> SPSymbol
SPAnd) ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ (SPLiteral -> SPTerm) -> [SPLiteral] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map SPLiteral -> SPTerm
litToSPTerm [SPLiteral]
l

litToSPTerm :: SPLiteral -> SPTerm
litToSPTerm :: SPLiteral -> SPTerm
litToSPTerm (SPLiteral b :: Bool
b t :: SPSymbol
t) = let s :: SPTerm
s = SPSymbol -> SPTerm
simpTerm SPSymbol
t in
  if Bool
b then SPTerm
s else SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [SPTerm
s]

instance Pretty TermWsList where
    pretty :: TermWsList -> Doc
pretty (TWL l :: [SPTerm]
l b :: Bool
b) = [Doc] -> Doc
fsep ((SPTerm -> Doc) -> [SPTerm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty [SPTerm]
l) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> if Bool
b then String -> Doc
text "+" else Doc
empty

printStep :: SPProofStep -> Doc
printStep :: SPProofStep -> Doc
printStep (SPProofStep ref :: SPReference
ref res :: SPResult
res rul :: SPRuleAppl
rul parl :: [SPParent]
parl asl :: SPAssocList
asl) = String -> Doc
text "step" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens
      (SPReference -> Doc
forall a. Pretty a => a -> Doc
pretty SPReference
ref Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> SPResult -> Doc
forall a. Pretty a => a -> Doc
pretty SPResult
res Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> SPRuleAppl -> Doc
forall a. Pretty a => a -> Doc
pretty SPRuleAppl
rul Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
       Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([SPParent] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SPParent]
parl) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SPAssocList -> Doc
printAssocList SPAssocList
asl) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot

instance Pretty SPReference where
    pretty :: SPReference -> Doc
pretty (PRefTerm t :: SPTerm
t) = SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t

instance Pretty SPResult where
    pretty :: SPResult -> Doc
pretty (PResTerm t :: SPTerm
t) = SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t

instance Pretty SPRuleAppl where
    pretty :: SPRuleAppl -> Doc
pretty r :: SPRuleAppl
r = case SPRuleAppl
r of
        PRuleTerm t :: SPTerm
t -> SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t
        PRuleUser t :: SPUserRuleAppl
t -> SPUserRuleAppl -> Doc
forall a. Pretty a => a -> Doc
pretty SPUserRuleAppl
t

instance Pretty SPUserRuleAppl where
    pretty :: SPUserRuleAppl -> Doc
pretty r :: SPUserRuleAppl
r = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ SPUserRuleAppl -> String
forall a. Show a => a -> String
show SPUserRuleAppl
r

instance Pretty SPParent where
    pretty :: SPParent -> Doc
pretty (PParTerm t :: SPTerm
t) = SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
t

{- |
  Creates a Doc from a SPASS Term.
-}
instance Pretty SPTerm where
  pretty :: SPTerm -> Doc
pretty 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} -> [Doc] -> Doc
cat
      [ SPQuantSym -> Doc
forall a. Pretty a => a -> Doc
pretty SPQuantSym
qsym
      , Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets ([SPTerm] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SPTerm]
tlist) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> SPTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SPTerm
tt]
    SPComplexTerm {symbol :: SPTerm -> SPSymbol
symbol = SPSymbol
ctsym, arguments :: SPTerm -> [SPTerm]
arguments = [SPTerm]
args} -> [Doc] -> Doc
cat
      [ SPSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty SPSymbol
ctsym
      , if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args then Doc
empty else Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [SPTerm] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SPTerm]
args]

{- |
  Creates a Doc from a SPASS Quantifier Symbol.
-}
instance Pretty SPQuantSym where
  pretty :: SPQuantSym -> Doc
pretty qs :: SPQuantSym
qs = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case SPQuantSym
qs of
    SPForall -> "forall"
    SPExists -> "exists"
    SPCustomQuantSym cst :: SPIdentifier
cst -> SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst

{- |
  Creates a Doc from a SPASS Symbol.
printSymbol :: SPSymbol-> Doc -}
instance Pretty SPSymbol where
    pretty :: SPSymbol -> Doc
pretty = String -> Doc
text (String -> Doc) -> (SPSymbol -> String) -> SPSymbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPSymbol -> String
showSPSymbol

{- |
  Creates a Doc from a SPASS description.
-}
instance Pretty SPDescription where
  pretty :: SPDescription -> Doc
pretty d :: SPDescription
d =
    let sptext :: String -> String -> Doc
sptext str :: String
str v :: String
v = String -> Doc
text String
str Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc -> Doc
textBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
v) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
        mtext :: String -> Maybe String -> Doc
mtext str :: String
str = Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty ((String -> Doc) -> Maybe String -> Doc)
-> (String -> Doc) -> Maybe String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String -> Doc
sptext String
str
    in String -> Doc
text "list_of_descriptions."
    Doc -> Doc -> Doc
$+$ String -> String -> Doc
sptext "name" (SPDescription -> String
name SPDescription
d)
    Doc -> Doc -> Doc
$+$ String -> String -> Doc
sptext "author" (SPDescription -> String
author SPDescription
d)
    Doc -> Doc -> Doc
$+$ String -> Maybe String -> Doc
mtext "version" (SPDescription -> Maybe String
version SPDescription
d)
    Doc -> Doc -> Doc
$+$ String -> Maybe String -> Doc
mtext "logic" (SPDescription -> Maybe String
logic SPDescription
d)
    Doc -> Doc -> Doc
$+$ String -> Doc
text "status" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (SPLogState -> Doc
forall a. Pretty a => a -> Doc
pretty (SPLogState -> Doc) -> SPLogState -> Doc
forall a b. (a -> b) -> a -> b
$ SPDescription -> SPLogState
status SPDescription
d) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
    Doc -> Doc -> Doc
$+$ String -> String -> Doc
sptext "description" (SPDescription -> String
desc SPDescription
d)
    Doc -> Doc -> Doc
$+$ String -> Maybe String -> Doc
mtext "date" (SPDescription -> Maybe String
date SPDescription
d)
    Doc -> Doc -> Doc
$+$ Doc
endOfListS

{- |
  surrounds  a doc with "{*  *}" as required for some of the
  description fields and the settings.
-}
textBraces :: Doc -> Doc
textBraces :: Doc -> Doc
textBraces d :: Doc
d = String -> Doc
text "{* " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text " *}"

{- |
  Creates a Doc from an 'SPLogState'.
-}
instance Pretty SPLogState where
  pretty :: SPLogState -> Doc
pretty 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"

printSettings :: [SPSetting] -> Doc
printSettings :: [SPSetting] -> Doc
printSettings = [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([SPSetting] -> [Doc]) -> [SPSetting] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPSetting -> Doc) -> [SPSetting] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPSetting -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty SPSetting where
    pretty :: SPSetting -> Doc
pretty (SPGeneralSettings es :: [SPHypothesis]
es) =
        String -> Doc
text "list_of_general_settings."
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((SPHypothesis -> Doc) -> [SPHypothesis] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SPHypothesis -> Doc
forall a. Pretty a => a -> Doc
pretty [SPHypothesis]
es)
        Doc -> Doc -> Doc
$+$ Doc
endOfListS
    pretty (SPSettings label :: SPSettingLabel
label body :: [SPSettingBody]
body) =
        String -> Doc
text "list_of_settings" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (SPSettingLabel -> Doc
forall a. Pretty a => a -> Doc
pretty SPSettingLabel
label) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
        Doc -> Doc -> Doc
$+$ Doc -> Doc
textBraces ([Doc] -> Doc
vcat ([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. Pretty a => a -> Doc
pretty [SPSettingBody]
body)
        Doc -> Doc -> Doc
$+$ Doc
endOfListS

instance Pretty SPSettingLabel where
    pretty :: SPSettingLabel -> Doc
pretty = String -> Doc
text (String -> Doc)
-> (SPSettingLabel -> String) -> SPSettingLabel -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPSettingLabel -> String
showSettingLabel

instance Pretty SPHypothesis where
    pretty :: SPHypothesis -> Doc
pretty (SPHypothesis ls :: [SPIdentifier]
ls) =
        String -> Doc
text "hypothesis" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets ([SPIdentifier] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SPIdentifier]
ls) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot

instance Pretty SPSettingBody where
    pretty :: SPSettingBody -> Doc
pretty (SPFlag sw :: String
sw v :: [String]
v) = [Doc] -> Doc
cat [String -> Doc
text String
sw, Doc -> Doc
parens ([String] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [String]
v) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot]
    pretty (SPClauseRelation cfrList :: [SPCRBIND]
cfrList) = [Doc] -> Doc
cat
      [ String -> Doc
text "set_ClauseFormulaRelation"
      , Doc -> Doc
parens ([SPCRBIND] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SPCRBIND]
cfrList) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot]

instance Pretty SPCRBIND where
    pretty :: SPCRBIND -> Doc
pretty (SPCRBIND cSPR :: String
cSPR fSPR :: String
fSPR) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
cSPR Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> String -> Doc
text String
fSPR