{- |
Module      :  ./THF/PrintTHF.hs
Description :  A printer for the TPTP-THF Syntax
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  portable

A printer for the TPTP-THF Input Syntax v5.1.0.2 taken from
<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
-}

module THF.PrintTHF where

import THF.As

import Data.Char

import Common.Doc
import Common.DocUtils
import Common.Id (Token)

{- -----------------------------------------------------------------------------
Pretty Instances for the THF and THF0 Syntax.
Most methods match those of As.hs
----------------------------------------------------------------------------- -}

printTPTPTHF :: [TPTP_THF] -> Doc
printTPTPTHF :: [TPTP_THF] -> Doc
printTPTPTHF [] = Doc
empty
printTPTPTHF (t :: TPTP_THF
t : rt :: [TPTP_THF]
rt) = case TPTP_THF
t of
    TPTP_THF_Annotated_Formula {} -> TPTP_THF -> Doc
forall a. Pretty a => a -> Doc
pretty TPTP_THF
t Doc -> Doc -> Doc
$++$ [TPTP_THF] -> Doc
printTPTPTHF [TPTP_THF]
rt
    _ -> TPTP_THF -> Doc
forall a. Pretty a => a -> Doc
pretty TPTP_THF
t Doc -> Doc -> Doc
$+$ [TPTP_THF] -> Doc
printTPTPTHF [TPTP_THF]
rt

instance Pretty TPTP_THF where
    pretty :: TPTP_THF -> Doc
pretty t :: TPTP_THF
t = case TPTP_THF
t of
        TPTP_THF_Annotated_Formula n :: Name
n fr :: FormulaRole
fr f :: THFFormula
f a :: Annotations
a ->
            String -> Doc
text "thf" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
                Doc -> Doc -> Doc
<+> FormulaRole -> Doc
forall a. Pretty a => a -> Doc
pretty FormulaRole
fr Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
                Doc -> Doc -> Doc
<+> THFFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFFormula
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
forall a. Pretty a => a -> Doc
pretty Annotations
a)
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
        TPTP_Include i :: Include
i -> Include -> Doc
forall a. Pretty a => a -> Doc
pretty Include
i
        TPTP_Comment c :: Comment
c -> Comment -> Doc
forall a. Pretty a => a -> Doc
pretty Comment
c
        TPTP_Defined_Comment dc :: DefinedComment
dc -> DefinedComment -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedComment
dc
        TPTP_System_Comment sc :: SystemComment
sc -> SystemComment -> Doc
forall a. Pretty a => a -> Doc
pretty SystemComment
sc
        TPTP_Header h :: [Comment]
h -> [Comment] -> Doc
prettyHeader [Comment]
h

prettyHeader :: [Comment] -> Doc
prettyHeader :: [Comment] -> Doc
prettyHeader = (Comment -> Doc -> Doc) -> Doc -> [Comment] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($+$) (Doc -> Doc -> Doc) -> (Comment -> Doc) -> Comment -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Comment -> Doc
forall a. Pretty a => a -> Doc
pretty) Doc
empty

instance Pretty Comment where
    pretty :: Comment -> Doc
pretty c :: Comment
c = case Comment
c of
        Comment_Line s :: Token
s -> String -> Doc
text "%" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (String -> Doc
text (String -> Doc) -> (Token -> String) -> Token -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
forall a. Show a => a -> String
show) Token
s
        Comment_Block sl :: Token
sl -> String -> Doc
text "/*"
                Doc -> Doc -> Doc
$+$ [String] -> Doc
prettyCommentBlock (String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
sl)
                Doc -> Doc -> Doc
$+$ String -> Doc
text "*/"

instance Pretty DefinedComment where
    pretty :: DefinedComment -> Doc
pretty dc :: DefinedComment
dc = case DefinedComment
dc of
        Defined_Comment_Line s :: Token
s -> String -> Doc
text "%$" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (String -> Doc
text (String -> Doc) -> (Token -> String) -> Token -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
forall a. Show a => a -> String
show) Token
s
        Defined_Comment_Block sl :: Token
sl -> String -> Doc
text "/*$"
                Doc -> Doc -> Doc
$+$ [String] -> Doc
prettyCommentBlock (String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
sl)
                Doc -> Doc -> Doc
$+$ String -> Doc
text "*/"

instance Pretty SystemComment where
    pretty :: SystemComment -> Doc
pretty sc :: SystemComment
sc = case SystemComment
sc of
        System_Comment_Line s :: Token
s -> String -> Doc
text "%$$" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (String -> Doc
text (String -> Doc) -> (Token -> String) -> Token -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
forall a. Show a => a -> String
show) Token
s
        System_Comment_Block sl :: Token
sl -> String -> Doc
text "/*$$"
                Doc -> Doc -> Doc
$+$ [String] -> Doc
prettyCommentBlock (String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
sl)
                Doc -> Doc -> Doc
$+$ String -> Doc
text "*/"

prettyCommentBlock :: [String] -> Doc
prettyCommentBlock :: [String] -> Doc
prettyCommentBlock = (String -> Doc -> Doc) -> Doc -> [String] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($+$) (Doc -> Doc -> Doc) -> (String -> Doc) -> String -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text) Doc
empty

instance Pretty Include where
    pretty :: Include -> Doc
pretty (I_Include fn :: Token
fn nl :: Maybe NameList
nl) = String -> Doc
text "include" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Token -> Doc
prettySingleQuoted Token
fn
        Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (NameList -> Doc) -> Maybe NameList -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\ c :: NameList
c -> Doc
comma Doc -> Doc -> Doc
<+> NameList -> Doc
prettyNameList NameList
c) Maybe NameList
nl) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."

instance Pretty Annotations where
    pretty :: Annotations -> Doc
pretty a :: Annotations
a = case Annotations
a of
        Annotations s :: Source
s o :: OptionalInfo
o -> Doc
comma Doc -> Doc -> Doc
<+> Source -> Doc
forall a. Pretty a => a -> Doc
pretty Source
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OptionalInfo -> Doc
prettyOptionalInfo OptionalInfo
o
        Null -> Doc
empty

instance Pretty FormulaRole where
    pretty :: FormulaRole -> Doc
pretty fr :: FormulaRole
fr = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FormulaRole -> String
forall a. Show a => a -> String
show FormulaRole
fr)

instance Pretty THFFormula where
    pretty :: THFFormula -> Doc
pretty f :: THFFormula
f = case THFFormula
f of
        TF_THF_Logic_Formula lf :: THFLogicFormula
lf -> THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf
        TF_THF_Sequent s :: THFSequent
s -> THFSequent -> Doc
forall a. Pretty a => a -> Doc
pretty THFSequent
s
        T0F_THF_Typed_Const tc :: THFTypedConst
tc -> THFTypedConst -> Doc
forall a. Pretty a => a -> Doc
pretty THFTypedConst
tc

instance Pretty THFLogicFormula where
    pretty :: THFLogicFormula -> Doc
pretty lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
        TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> THFBinaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryFormula
bf
        TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf
        TLF_THF_Type_Formula tf :: THFTypeFormula
tf -> THFTypeFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFTypeFormula
tf
        TLF_THF_Sub_Type st :: THFSubType
st -> THFSubType -> Doc
forall a. Pretty a => a -> Doc
pretty THFSubType
st

instance Pretty THFBinaryFormula where
    pretty :: THFBinaryFormula -> Doc
pretty bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
        TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> THFBinaryTuple -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryTuple
bt
        TBF_THF_Binary_Type bt :: THFBinaryType
bt -> THFBinaryType -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryType
bt
        TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 pc :: THFPairConnective
pc uf2 :: THFUnitaryFormula
uf2 ->
            THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf1 Doc -> Doc -> Doc
<+> THFPairConnective -> Doc
forall a. Pretty a => a -> Doc
pretty THFPairConnective
pc Doc -> Doc -> Doc
<+> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf2

instance Pretty THFBinaryTuple where
    pretty :: THFBinaryTuple -> Doc
pretty bt :: THFBinaryTuple
bt = case THFBinaryTuple
bt of
        TBT_THF_Or_Formula ufl :: [THFUnitaryFormula]
ufl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryFormula -> Doc) -> [THFUnitaryFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryFormula]
ufl) Doc
orSign
        TBT_THF_And_Formula ufl :: [THFUnitaryFormula]
ufl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryFormula -> Doc) -> [THFUnitaryFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryFormula]
ufl) Doc
andSign
        TBT_THF_Apply_Formula ufl :: [THFUnitaryFormula]
ufl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryFormula -> Doc) -> [THFUnitaryFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryFormula]
ufl) Doc
applySign

instance Pretty THFUnitaryFormula where
    pretty :: THFUnitaryFormula -> Doc
pretty tuf :: THFUnitaryFormula
tuf = case THFUnitaryFormula
tuf of
        TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> THFQuantifiedFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFQuantifiedFormula
qf
        TUF_THF_Unary_Formula uc :: THFUnaryConnective
uc lf :: THFLogicFormula
lf -> THFUnaryConnective -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnaryConnective
uc Doc -> Doc -> Doc
<+> Doc -> Doc
parens (THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf)
        TUF_THF_Atom a :: THFAtom
a -> THFAtom -> Doc
forall a. Pretty a => a -> Doc
pretty THFAtom
a
        TUF_THF_Tuple t :: [THFLogicFormula]
t -> [THFLogicFormula] -> Doc
prettyTuple [THFLogicFormula]
t
        TUF_THF_Conditional lf1 :: THFLogicFormula
lf1 lf2 :: THFLogicFormula
lf2 lf3 :: THFLogicFormula
lf3 ->
            String -> Doc
text "$itef" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf1
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf2
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf3)
        TUF_THF_Logic_Formula_Par l :: THFLogicFormula
l -> Doc -> Doc
parens (THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
l)
        T0UF_THF_Abstraction vl :: THFVariableList
vl uf :: THFUnitaryFormula
uf -> String -> Doc
text "^" Doc -> Doc -> Doc
<+>
            Doc -> Doc
brackets (THFVariableList -> Doc
prettyVariableList THFVariableList
vl) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf

instance Pretty THFQuantifiedFormula where
    pretty :: THFQuantifiedFormula -> Doc
pretty qf :: THFQuantifiedFormula
qf = case THFQuantifiedFormula
qf of
        TQF_THF_Quantified_Formula tq :: THFQuantifier
tq vl :: THFVariableList
vl uf :: THFUnitaryFormula
uf -> THFQuantifier -> Doc
forall a. Pretty a => a -> Doc
pretty THFQuantifier
tq Doc -> Doc -> Doc
<+>
            Doc -> Doc
brackets (THFVariableList -> Doc
prettyVariableList THFVariableList
vl) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf
        T0QF_THF_Quantified_Var q :: Quantifier
q vl :: THFVariableList
vl uf :: THFUnitaryFormula
uf -> Quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty Quantifier
q Doc -> Doc -> Doc
<+>
            Doc -> Doc
brackets (THFVariableList -> Doc
prettyVariableList THFVariableList
vl) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf
        T0QF_THF_Quantified_Novar tq :: THFQuantifier
tq uf :: THFUnitaryFormula
uf ->
            THFQuantifier -> Doc
forall a. Pretty a => a -> Doc
pretty THFQuantifier
tq Doc -> Doc -> Doc
<+> Doc -> Doc
parens (THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf)

prettyVariableList :: THFVariableList -> Doc
prettyVariableList :: THFVariableList -> Doc
prettyVariableList vl :: THFVariableList
vl = [Doc] -> Doc
sepByCommas ((THFVariable -> Doc) -> THFVariableList -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFVariable -> Doc
forall a. Pretty a => a -> Doc
pretty THFVariableList
vl)

instance Pretty THFVariable where
    pretty :: THFVariable -> Doc
pretty v :: THFVariable
v = case THFVariable
v of
        TV_THF_Typed_Variable va :: Token
va tlt :: THFTopLevelType
tlt -> Token -> Doc
prettyUpperWord Token
va
            Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> THFTopLevelType -> Doc
forall a. Pretty a => a -> Doc
pretty THFTopLevelType
tlt
        TV_Variable var :: Token
var -> Token -> Doc
prettyUpperWord Token
var

instance Pretty THFTypedConst where
    pretty :: THFTypedConst -> Doc
pretty ttc :: THFTypedConst
ttc = case THFTypedConst
ttc of
        T0TC_Typed_Const c :: Constant
c tlt :: THFTopLevelType
tlt -> Constant -> Doc
prettyConstant Constant
c Doc -> Doc -> Doc
<+> String -> Doc
text ":"
            Doc -> Doc -> Doc
<+> THFTopLevelType -> Doc
forall a. Pretty a => a -> Doc
pretty THFTopLevelType
tlt
        T0TC_THF_TypedConst_Par tc :: THFTypedConst
tc -> Doc -> Doc
parens (THFTypedConst -> Doc
forall a. Pretty a => a -> Doc
pretty THFTypedConst
tc)

instance Pretty THFTypeFormula where
    pretty :: THFTypeFormula -> Doc
pretty ttf :: THFTypeFormula
ttf = case THFTypeFormula
ttf of
        TTF_THF_Type_Formula tf :: THFTypeableFormula
tf tlt :: THFTopLevelType
tlt -> THFTypeableFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFTypeableFormula
tf Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> THFTopLevelType -> Doc
forall a. Pretty a => a -> Doc
pretty THFTopLevelType
tlt
        TTF_THF_Typed_Const c :: Constant
c tlt :: THFTopLevelType
tlt -> Constant -> Doc
prettyConstant Constant
c Doc -> Doc -> Doc
<+> String -> Doc
text ":"
            Doc -> Doc -> Doc
<+> THFTopLevelType -> Doc
forall a. Pretty a => a -> Doc
pretty THFTopLevelType
tlt

instance Pretty THFTypeableFormula where
    pretty :: THFTypeableFormula -> Doc
pretty tbf :: THFTypeableFormula
tbf = case THFTypeableFormula
tbf of
        TTyF_THF_Atom a :: THFAtom
a -> THFAtom -> Doc
forall a. Pretty a => a -> Doc
pretty THFAtom
a
        TTyF_THF_Tuple t :: [THFLogicFormula]
t -> [THFLogicFormula] -> Doc
prettyTuple [THFLogicFormula]
t
        TTyF_THF_Logic_Formula lf :: THFLogicFormula
lf -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf

instance Pretty THFSubType where
    pretty :: THFSubType -> Doc
pretty (TST_THF_Sub_Type c1 :: Constant
c1 c2 :: Constant
c2) =
        Constant -> Doc
prettyConstant Constant
c1 Doc -> Doc -> Doc
<+> String -> Doc
text "<<" Doc -> Doc -> Doc
<+> Constant -> Doc
prettyConstant Constant
c2

instance Pretty THFTopLevelType where
    pretty :: THFTopLevelType -> Doc
pretty tlt :: THFTopLevelType
tlt = case THFTopLevelType
tlt of
        TTLT_THF_Logic_Formula lf :: THFLogicFormula
lf -> THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFLogicFormula
lf
        T0TLT_Constant c :: Constant
c -> Constant -> Doc
prettyConstant Constant
c
        T0TLT_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v
        T0TLT_Defined_Type dt :: DefinedType
dt -> DefinedType -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedType
dt
        T0TLT_System_Type st :: Token
st -> Token -> Doc
prettyAtomicSystemWord Token
st
        T0TLT_THF_Binary_Type bt :: THFBinaryType
bt -> THFBinaryType -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryType
bt

instance Pretty THFUnitaryType where
    pretty :: THFUnitaryType -> Doc
pretty ut :: THFUnitaryType
ut = case THFUnitaryType
ut of
        TUT_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> THFUnitaryFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnitaryFormula
uf
        T0UT_Constant c :: Constant
c -> Constant -> Doc
prettyConstant Constant
c
        T0UT_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v
        T0UT_Defined_Type dt :: DefinedType
dt -> DefinedType -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedType
dt
        T0UT_System_Type st :: Token
st -> Token -> Doc
prettyAtomicSystemWord Token
st
        T0UT_THF_Binary_Type_Par bt :: THFBinaryType
bt -> Doc -> Doc
parens (THFBinaryType -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryType
bt)

instance Pretty THFBinaryType where
    pretty :: THFBinaryType -> Doc
pretty tbt :: THFBinaryType
tbt = case THFBinaryType
tbt of
        TBT_THF_Mapping_Type utl :: [THFUnitaryType]
utl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryType -> Doc) -> [THFUnitaryType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryType -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryType]
utl) Doc
arrowSign
        TBT_THF_Xprod_Type utl :: [THFUnitaryType]
utl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryType -> Doc) -> [THFUnitaryType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryType -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryType]
utl) Doc
starSign
        TBT_THF_Union_Type utl :: [THFUnitaryType]
utl -> [Doc] -> Doc -> Doc
sepBy ((THFUnitaryType -> Doc) -> [THFUnitaryType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryType -> Doc
forall a. Pretty a => a -> Doc
pretty [THFUnitaryType]
utl) Doc
plusSign
        T0BT_THF_Binary_Type_Par bt :: THFBinaryType
bt -> Doc -> Doc
parens (THFBinaryType -> Doc
forall a. Pretty a => a -> Doc
pretty THFBinaryType
bt)

instance Pretty THFAtom where
    pretty :: THFAtom -> Doc
pretty a :: THFAtom
a = case THFAtom
a of
        TA_Term t :: Term
t -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t
        TA_THF_Conn_Term ct :: THFConnTerm
ct -> THFConnTerm -> Doc
forall a. Pretty a => a -> Doc
pretty THFConnTerm
ct
        TA_Defined_Type dt :: DefinedType
dt -> DefinedType -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedType
dt
        TA_Defined_Plain_Formula dp :: DefinedPlainFormula
dp -> DefinedPlainFormula -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedPlainFormula
dp
        TA_System_Type st :: Token
st -> Token -> Doc
prettyAtomicSystemWord Token
st
        TA_System_Atomic_Formula st :: SystemTerm
st -> SystemTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SystemTerm
st
        T0A_Constant c :: Constant
c -> Constant -> Doc
prettyConstant Constant
c
        T0A_Defined_Constant dc :: Token
dc -> Token -> Doc
prettyAtomicDefinedWord Token
dc
        T0A_System_Constant sc :: Token
sc -> Token -> Doc
prettyAtomicSystemWord Token
sc
        T0A_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v

prettyTuple :: THFTuple -> Doc
prettyTuple :: [THFLogicFormula] -> Doc
prettyTuple ufl :: [THFLogicFormula]
ufl = Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas ((THFLogicFormula -> Doc) -> [THFLogicFormula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THFLogicFormula -> Doc
forall a. Pretty a => a -> Doc
pretty [THFLogicFormula]
ufl)

instance Pretty THFSequent where
    pretty :: THFSequent -> Doc
pretty (TS_THF_Sequent_Par s :: THFSequent
s) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THFSequent -> Doc
forall a. Pretty a => a -> Doc
pretty THFSequent
s
    pretty (TS_THF_Sequent t1 :: [THFLogicFormula]
t1 t2 :: [THFLogicFormula]
t2) =
        [THFLogicFormula] -> Doc
prettyTuple [THFLogicFormula]
t1 Doc -> Doc -> Doc
<+> String -> Doc
text "-->" Doc -> Doc -> Doc
<+> [THFLogicFormula] -> Doc
prettyTuple [THFLogicFormula]
t2

instance Pretty THFConnTerm where
    pretty :: THFConnTerm -> Doc
pretty ct :: THFConnTerm
ct = case THFConnTerm
ct of
        TCT_THF_Pair_Connective pc :: THFPairConnective
pc -> THFPairConnective -> Doc
forall a. Pretty a => a -> Doc
pretty THFPairConnective
pc
        TCT_Assoc_Connective ac :: AssocConnective
ac -> AssocConnective -> Doc
forall a. Pretty a => a -> Doc
pretty AssocConnective
ac
        TCT_THF_Unary_Connective uc :: THFUnaryConnective
uc -> THFUnaryConnective -> Doc
forall a. Pretty a => a -> Doc
pretty THFUnaryConnective
uc
        T0CT_THF_Quantifier q :: THFQuantifier
q -> THFQuantifier -> Doc
forall a. Pretty a => a -> Doc
pretty THFQuantifier
q

instance Pretty THFQuantifier where
    pretty :: THFQuantifier -> Doc
pretty q :: THFQuantifier
q = case THFQuantifier
q of
        TQ_ForAll -> String -> Doc
text "!"
        TQ_Exists -> String -> Doc
text "?"
        TQ_Lambda_Binder -> String -> Doc
text "^"
        TQ_Dependent_Product -> String -> Doc
text "!>"
        TQ_Dependent_Sum -> String -> Doc
text "?*"
        TQ_Indefinite_Description -> String -> Doc
text "@+"
        TQ_Definite_Description -> String -> Doc
text "@-"
        T0Q_PiForAll -> String -> Doc
text "!!"
        T0Q_SigmaExists -> String -> Doc
text "??"

instance Pretty Quantifier where
    pretty :: Quantifier -> Doc
pretty q :: Quantifier
q = case Quantifier
q of
        T0Q_ForAll -> String -> Doc
text "!"
        T0Q_Exists -> String -> Doc
text "?"

instance Pretty THFPairConnective where
    pretty :: THFPairConnective -> Doc
pretty pc :: THFPairConnective
pc = case THFPairConnective
pc of
        Infix_Equality -> String -> Doc
text "="
        Infix_Inequality -> String -> Doc
text "!="
        Equivalent -> String -> Doc
text "<=>"
        Implication -> String -> Doc
text "=>"
        IF -> String -> Doc
text "<="
        XOR -> String -> Doc
text "<~>"
        NOR -> String -> Doc
text "~|"
        NAND -> String -> Doc
text "~&"

instance Pretty THFUnaryConnective where
    pretty :: THFUnaryConnective -> Doc
pretty uc :: THFUnaryConnective
uc = case THFUnaryConnective
uc of
        Negation -> String -> Doc
text "~"
        PiForAll -> String -> Doc
text "!!"
        SigmaExists -> String -> Doc
text "??"

instance Pretty AssocConnective where
    pretty :: AssocConnective -> Doc
pretty AND = String -> Doc
text "&"
    pretty OR = String -> Doc
text "|"

instance Pretty DefinedType where
    pretty :: DefinedType -> Doc
pretty DT_oType = String -> Doc
text "$o"
    pretty dt :: DefinedType
dt = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ '$' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String -> String
forall a. Int -> [a] -> [a]
drop 3 (DefinedType -> String
forall a. Show a => a -> String
show DefinedType
dt)

instance Pretty DefinedPlainFormula where
    pretty :: DefinedPlainFormula -> Doc
pretty dpf :: DefinedPlainFormula
dpf = case DefinedPlainFormula
dpf of
        DPF_Defined_Prop dp :: DefinedProp
dp -> DefinedProp -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedProp
dp
        DPF_Defined_Formula dp :: DefinedPred
dp a :: Arguments
a -> DefinedPred -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedPred
dp Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Arguments -> Doc
prettyArguments Arguments
a)

instance Pretty DefinedProp where
    pretty :: DefinedProp -> Doc
pretty DP_True = String -> Doc
text "$true"
    pretty DP_False = String -> Doc
text "$false"

instance Pretty DefinedPred where
    pretty :: DefinedPred -> Doc
pretty dp :: DefinedPred
dp = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ '$' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (DefinedPred -> String
forall a. Show a => a -> String
show DefinedPred
dp)

instance Pretty Term where
    pretty :: Term -> Doc
pretty t :: Term
t = case Term
t of
        T_Function_Term ft :: FunctionTerm
ft -> FunctionTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FunctionTerm
ft
        T_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v

instance Pretty FunctionTerm where
    pretty :: FunctionTerm -> Doc
pretty ft :: FunctionTerm
ft = case FunctionTerm
ft of
        FT_Plain_Term pt :: PlainTerm
pt -> PlainTerm -> Doc
forall a. Pretty a => a -> Doc
pretty PlainTerm
pt
        FT_Defined_Term dt :: DefinedTerm
dt -> DefinedTerm -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedTerm
dt
        FT_System_Term st :: SystemTerm
st -> SystemTerm -> Doc
forall a. Pretty a => a -> Doc
pretty SystemTerm
st

instance Pretty PlainTerm where
    pretty :: PlainTerm -> Doc
pretty pt :: PlainTerm
pt = case PlainTerm
pt of
        PT_Constant c :: Constant
c -> Constant -> Doc
prettyConstant Constant
c
        PT_Plain_Term f :: Constant
f a :: Arguments
a -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Arguments -> Doc
prettyArguments Arguments
a)

prettyConstant :: Constant -> Doc
prettyConstant :: Constant -> Doc
prettyConstant = Constant -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty DefinedTerm where
    pretty :: DefinedTerm -> Doc
pretty dt :: DefinedTerm
dt = case DefinedTerm
dt of
        DT_Defined_Atom da :: DefinedAtom
da -> DefinedAtom -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedAtom
da
        DT_Defined_Atomic_Term dpt :: DefinedPlainTerm
dpt -> DefinedPlainTerm -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedPlainTerm
dpt

instance Pretty DefinedAtom where
    pretty :: DefinedAtom -> Doc
pretty da :: DefinedAtom
da = case DefinedAtom
da of
        DA_Number n :: Number
n -> Number -> Doc
forall a. Pretty a => a -> Doc
pretty Number
n
        DA_Distinct_Object dio :: Token
dio -> Token -> Doc
prettyDistinctObject Token
dio

instance Pretty DefinedPlainTerm where
    pretty :: DefinedPlainTerm -> Doc
pretty dpt :: DefinedPlainTerm
dpt = case DefinedPlainTerm
dpt of
        DPT_Defined_Constant df :: DefinedFunctor
df -> DefinedFunctor -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedFunctor
df
        DPT_Defined_Function df :: DefinedFunctor
df a :: Arguments
a -> DefinedFunctor -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedFunctor
df Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Arguments -> Doc
prettyArguments Arguments
a)

instance Pretty DefinedFunctor where
    pretty :: DefinedFunctor -> Doc
pretty df :: DefinedFunctor
df = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ '$' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (DefinedFunctor -> String
forall a. Show a => a -> String
show DefinedFunctor
df)

instance Pretty SystemTerm where
    pretty :: SystemTerm -> Doc
pretty st :: SystemTerm
st = case SystemTerm
st of
        ST_System_Constant sf :: Token
sf -> Token -> Doc
prettyAtomicSystemWord Token
sf
        ST_System_Term sf :: Token
sf a :: Arguments
a -> Token -> Doc
prettyAtomicSystemWord Token
sf
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Arguments -> Doc
prettyArguments Arguments
a)

prettyArguments :: Arguments -> Doc
prettyArguments :: Arguments -> Doc
prettyArguments = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> (Arguments -> [Doc]) -> Arguments -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Doc) -> Arguments -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty PrincipalSymbol where
    pretty :: PrincipalSymbol -> Doc
pretty ps :: PrincipalSymbol
ps = case PrincipalSymbol
ps of
        PS_Functor f :: Constant
f -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
f
        PS_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v

instance Pretty Source where
    pretty :: Source -> Doc
pretty s :: Source
s = case Source
s of
        S_Dag_Source ds :: DagSource
ds -> DagSource -> Doc
forall a. Pretty a => a -> Doc
pretty DagSource
ds
        S_Internal_Source it :: IntroType
it oi :: OptionalInfo
oi -> String -> Doc
text "introduced" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (
            IntroType -> Doc
forall a. Pretty a => a -> Doc
pretty IntroType
it Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OptionalInfo -> Doc
prettyOptionalInfo OptionalInfo
oi)
        S_External_Source es :: ExternalSource
es -> ExternalSource -> Doc
forall a. Pretty a => a -> Doc
pretty ExternalSource
es
        S_Sources ss :: [Source]
ss -> [Doc] -> Doc
sepByCommas ((Source -> Doc) -> [Source] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Source -> Doc
forall a. Pretty a => a -> Doc
pretty [Source]
ss)
        S_Unknown -> String -> Doc
text "unknown"

instance Pretty DagSource where
    pretty :: DagSource -> Doc
pretty ds :: DagSource
ds = case DagSource
ds of
        DS_Name n :: Name
n -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n
        DS_Inference_Record aw :: Constant
aw ui :: UsefulInfo
ui pl :: [ParentInfo]
pl -> String -> Doc
text "inference"
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> UsefulInfo -> Doc
prettyUsefulInfo UsefulInfo
ui
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Doc] -> Doc
sepByCommas ((ParentInfo -> Doc) -> [ParentInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ParentInfo -> Doc
forall a. Pretty a => a -> Doc
pretty [ParentInfo]
pl)))

instance Pretty ParentInfo where
    pretty :: ParentInfo -> Doc
pretty (PI_Parent_Info s :: Source
s mgl :: Maybe GeneralList
mgl) =
        let gl :: Doc
gl = Doc -> (GeneralList -> Doc) -> Maybe GeneralList -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\ c :: GeneralList
c -> String -> Doc
text ":" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> GeneralList -> Doc
prettyGeneralList GeneralList
c) Maybe GeneralList
mgl
        in Source -> Doc
forall a. Pretty a => a -> Doc
pretty Source
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
gl

instance Pretty IntroType where
    pretty :: IntroType -> Doc
pretty it :: IntroType
it = String -> Doc
text (Int -> String -> String
forall a. Int -> [a] -> [a]
drop 3 (IntroType -> String
forall a. Show a => a -> String
show IntroType
it))

instance Pretty ExternalSource where
    pretty :: ExternalSource -> Doc
pretty es :: ExternalSource
es = case ExternalSource
es of
        ES_File_Source fs :: FileSource
fs -> FileSource -> Doc
forall a. Pretty a => a -> Doc
pretty FileSource
fs
        ES_Theory tn :: TheoryName
tn oi :: OptionalInfo
oi -> String -> Doc
text "theory" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (
            TheoryName -> Doc
forall a. Pretty a => a -> Doc
pretty TheoryName
tn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OptionalInfo -> Doc
prettyOptionalInfo OptionalInfo
oi)
        ES_Creator_Source aw :: Constant
aw oi :: OptionalInfo
oi -> String -> Doc
text "creator" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (
            Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OptionalInfo -> Doc
prettyOptionalInfo OptionalInfo
oi)

instance Pretty FileSource where
    pretty :: FileSource -> Doc
pretty (FS_File fn :: Token
fn mn :: Maybe Name
mn) =
        let n :: Doc
n = Doc -> (Name -> Doc) -> Maybe Name -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\ c :: Name
c -> Doc
comma Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
c) Maybe Name
mn
        in String -> Doc
text "file" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Token -> Doc
prettySingleQuoted Token
fn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
n)

instance Pretty TheoryName where
    pretty :: TheoryName -> Doc
pretty tn :: TheoryName
tn = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (TheoryName -> String
forall a. Show a => a -> String
show TheoryName
tn)

prettyOptionalInfo :: OptionalInfo -> Doc
prettyOptionalInfo :: OptionalInfo -> Doc
prettyOptionalInfo = Doc -> (UsefulInfo -> Doc) -> OptionalInfo -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\ ui :: UsefulInfo
ui -> Doc
comma Doc -> Doc -> Doc
<+> UsefulInfo -> Doc
prettyUsefulInfo UsefulInfo
ui)

prettyUsefulInfo :: UsefulInfo -> Doc
prettyUsefulInfo :: UsefulInfo -> Doc
prettyUsefulInfo = Doc -> Doc
brackets (Doc -> Doc) -> (UsefulInfo -> Doc) -> UsefulInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> (UsefulInfo -> [Doc]) -> UsefulInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InfoItem -> Doc) -> UsefulInfo -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map InfoItem -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty InfoItem where
    pretty :: InfoItem -> Doc
pretty ii :: InfoItem
ii = case InfoItem
ii of
        II_Formula_Item fi :: FormulaItem
fi -> FormulaItem -> Doc
forall a. Pretty a => a -> Doc
pretty FormulaItem
fi
        II_Inference_Item infi :: InferenceItem
infi -> InferenceItem -> Doc
forall a. Pretty a => a -> Doc
pretty InferenceItem
infi
        II_General_Function gf :: GeneralFunction
gf -> GeneralFunction -> Doc
forall a. Pretty a => a -> Doc
pretty GeneralFunction
gf

instance Pretty FormulaItem where
    pretty :: FormulaItem -> Doc
pretty fi :: FormulaItem
fi = case FormulaItem
fi of
        FI_Description_Item aw :: Constant
aw -> String -> Doc
text "description" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw)
        FI_Iquote_Item aw :: Constant
aw -> String -> Doc
text "iquote" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw)

instance Pretty InferenceItem where
    pretty :: InferenceItem -> Doc
pretty ii :: InferenceItem
ii = case InferenceItem
ii of
        II_Inference_Status is :: InferenceStatus
is -> InferenceStatus -> Doc
forall a. Pretty a => a -> Doc
pretty InferenceStatus
is
        II_Assumptions_Record nl :: NameList
nl -> String -> Doc
text "assumptions"
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc -> Doc
brackets (NameList -> Doc
prettyNameList NameList
nl))
        II_New_Symbol_Record aw :: Constant
aw psl :: [PrincipalSymbol]
psl -> String -> Doc
text "new_symbols" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Doc] -> Doc
sepByCommas ((PrincipalSymbol -> Doc) -> [PrincipalSymbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrincipalSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty [PrincipalSymbol]
psl)))
        II_Refutation fs :: FileSource
fs -> String -> Doc
text "refutation" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (FileSource -> Doc
forall a. Pretty a => a -> Doc
pretty FileSource
fs)

instance Pretty InferenceStatus where
    pretty :: InferenceStatus -> Doc
pretty is :: InferenceStatus
is = case InferenceStatus
is of
        IS_Status s :: StatusValue
s -> String -> Doc
text "status" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (StatusValue -> Doc
forall a. Pretty a => a -> Doc
pretty StatusValue
s)
        IS_Inference_Info aw1 :: Constant
aw1 aw2 :: Constant
aw2 gl :: GeneralList
gl -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw2
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> GeneralList -> Doc
prettyGeneralList GeneralList
gl)

instance Pretty StatusValue where
    pretty :: StatusValue -> Doc
pretty sv :: StatusValue
sv = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (StatusValue -> String
forall a. Show a => a -> String
show StatusValue
sv)

prettyNameList :: NameList -> Doc
prettyNameList :: NameList -> Doc
prettyNameList = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> (NameList -> [Doc]) -> NameList -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Doc) -> NameList -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty GeneralTerm where
    pretty :: GeneralTerm -> Doc
pretty gt :: GeneralTerm
gt = case GeneralTerm
gt of
        GT_General_Data gd :: GeneralData
gd -> GeneralData -> Doc
forall a. Pretty a => a -> Doc
pretty GeneralData
gd
        GT_General_Data_Term gd :: GeneralData
gd gt1 :: GeneralTerm
gt1 -> GeneralData -> Doc
forall a. Pretty a => a -> Doc
pretty GeneralData
gd Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> GeneralTerm -> Doc
forall a. Pretty a => a -> Doc
pretty GeneralTerm
gt1
        GT_General_List gl :: GeneralList
gl -> GeneralList -> Doc
prettyGeneralList GeneralList
gl

instance Pretty GeneralData where
    pretty :: GeneralData -> Doc
pretty gd :: GeneralData
gd = case GeneralData
gd of
        GD_Atomic_Word aw :: Constant
aw -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw
        GD_General_Function gf :: GeneralFunction
gf -> GeneralFunction -> Doc
forall a. Pretty a => a -> Doc
pretty GeneralFunction
gf
        GD_Variable v :: Token
v -> Token -> Doc
prettyUpperWord Token
v
        GD_Number n :: Number
n -> Number -> Doc
forall a. Pretty a => a -> Doc
pretty Number
n
        GD_Distinct_Object dio :: Token
dio -> Token -> Doc
prettyDistinctObject Token
dio
        GD_Formula_Data fd :: FormulaData
fd -> FormulaData -> Doc
forall a. Pretty a => a -> Doc
pretty FormulaData
fd
        GD_Bind v :: Token
v fd :: FormulaData
fd -> String -> Doc
text "bind" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (
            Token -> Doc
prettyUpperWord Token
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> FormulaData -> Doc
forall a. Pretty a => a -> Doc
pretty FormulaData
fd)

instance Pretty GeneralFunction where
    pretty :: GeneralFunction -> Doc
pretty (GF_General_Function aw :: Constant
aw gts :: GeneralList
gts) =
        Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
aw Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (GeneralList -> Doc
prettyGeneralTerms GeneralList
gts)

instance Pretty FormulaData where
    pretty :: FormulaData -> Doc
pretty (THF_Formula thff :: THFFormula
thff) = String -> Doc
text "$thf" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (THFFormula -> Doc
forall a. Pretty a => a -> Doc
pretty THFFormula
thff)

prettyGeneralList :: GeneralList -> Doc
prettyGeneralList :: GeneralList -> Doc
prettyGeneralList = Doc -> Doc
brackets (Doc -> Doc) -> (GeneralList -> Doc) -> GeneralList -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GeneralList -> Doc
prettyGeneralTerms

prettyGeneralTerms :: GeneralTerms -> Doc
prettyGeneralTerms :: GeneralList -> Doc
prettyGeneralTerms = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> (GeneralList -> [Doc]) -> GeneralList -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GeneralTerm -> Doc) -> GeneralList -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map GeneralTerm -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty Name where
    pretty :: Name -> Doc
pretty n :: Name
n = case Name
n of
        N_Atomic_Word a :: Constant
a -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
a
        N_Integer s :: Token
s -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
s
        T0N_Unsigned_Integer s :: Token
s -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
s

instance Pretty AtomicWord where
    pretty :: Constant -> Doc
pretty a :: Constant
a = case Constant
a of
        A_Single_Quoted s :: Token
s -> Token -> Doc
prettySingleQuoted Token
s
        A_Lower_Word l :: Token
l -> Token -> Doc
prettyLowerWord Token
l

prettyAtomicSystemWord :: Token -> Doc
prettyAtomicSystemWord :: Token -> Doc
prettyAtomicSystemWord asw :: Token
asw = String -> Doc
text ("$$" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
asw)

prettyAtomicDefinedWord :: Token -> Doc
prettyAtomicDefinedWord :: Token -> Doc
prettyAtomicDefinedWord adw :: Token
adw = String -> Doc
text ('$' Char -> String -> String
forall a. a -> [a] -> [a]
: Token -> String
forall a. Show a => a -> String
show Token
adw)

instance Pretty Number where
    pretty :: Number -> Doc
pretty n :: Number
n = case Number
n of
        Num_Integer i :: Token
i -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
i
        Num_Rational ra :: Token
ra -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
ra
        Num_Real re :: Token
re -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
re

prettySingleQuoted :: Token -> Doc
prettySingleQuoted :: Token -> Doc
prettySingleQuoted s :: Token
s = String -> Doc
text "\'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (String -> Doc
text (String -> Doc) -> (Token -> String) -> Token -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
forall a. Show a => a -> String
show) Token
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "\'"

prettyDistinctObject :: Token -> Doc
prettyDistinctObject :: Token -> Doc
prettyDistinctObject s :: Token
s = String -> Doc
text "\"" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (String -> Doc
text (String -> Doc) -> (Token -> String) -> Token -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
forall a. Show a => a -> String
show) Token
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "\""

prettyLowerWord :: Token -> Doc
prettyLowerWord :: Token -> Doc
prettyLowerWord uw' :: Token
uw' = let uw :: String
uw = Token -> String
forall a. Show a => a -> String
show Token
uw' in String -> Doc
text (Char -> Char
toLower (String -> Char
forall a. [a] -> a
head String
uw) Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. [a] -> [a]
tail String
uw)

prettyUpperWord :: Token -> Doc
prettyUpperWord :: Token -> Doc
prettyUpperWord uw' :: Token
uw' = let uw :: String
uw = Token -> String
forall a. Show a => a -> String
show Token
uw' in String -> Doc
text (Char -> Char
toUpper (String -> Char
forall a. [a] -> a
head String
uw) Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. [a] -> [a]
tail String
uw)

orSign :: Doc
orSign :: Doc
orSign = String -> Doc
text "|"

andSign :: Doc
andSign :: Doc
andSign = String -> Doc
text "&"

applySign :: Doc
applySign :: Doc
applySign = String -> Doc
text "@"

arrowSign :: Doc
arrowSign :: Doc
arrowSign = String -> Doc
text ">"

starSign :: Doc
starSign :: Doc
starSign = String -> Doc
text "*"

plusSign :: Doc
plusSign :: Doc
plusSign = String -> Doc
text "+"

sepBy :: [Doc] -> Doc -> Doc
sepBy :: [Doc] -> Doc -> Doc
sepBy ls :: [Doc]
ls s :: Doc
s = case [Doc]
ls of
    (c :: Doc
c : []) -> Doc
c
    (c :: Doc
c : d :: [Doc]
d) -> Doc
c Doc -> Doc -> Doc
<+> Doc
s Doc -> Doc -> Doc
<+> [Doc] -> Doc -> Doc
sepBy [Doc]
d Doc
s
    [] -> Doc
empty