{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}

-- |
-- Module       : Data.TPTP.Pretty
-- Description  : Pretty printers for the TPTP language.
-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021
-- License      : GPL-3
-- Maintainer   : evgeny.kotelnikov@gmail.com
-- Stability    : experimental
--

module Data.TPTP.Pretty (
  Pretty(..)
) where

#if !MIN_VERSION_base(4, 8, 0)
import Data.Foldable (Foldable)
import Data.Functor ((<$>))
import Data.Monoid (mempty)
#endif

#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup ((<>))
#endif

import Data.Char (isAsciiLower, isAsciiUpper, isDigit)
import qualified Data.Foldable as Foldable (toList)
import Data.List (genericReplicate, intersperse)
import qualified Data.List.NonEmpty as NEL (nonEmpty)
import Data.Maybe (maybeToList)
import Data.Text (Text)
import qualified Data.Text as Text (
    all, head, tail, cons, snoc, pack, singleton, replace
  )
import Data.Text.Prettyprint.Doc (
    Doc, Pretty(..),
    hsep, sep, (<+>), parens, brackets, punctuate, space, comma, line
  )

import Data.TPTP


-- * Helper functions

comment :: Doc ann -> Doc ann
comment :: Doc ann -> Doc ann
comment Doc ann
c = Doc ann
"%" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
c Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
line

sepBy :: Foldable f => f (Doc ann) -> Doc ann -> Doc ann
sepBy :: f (Doc ann) -> Doc ann -> Doc ann
sepBy f (Doc ann)
as Doc ann
s = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
intersperse Doc ann
s (f (Doc ann) -> [Doc ann]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f (Doc ann)
as))

application :: Pretty f => f -> [Doc ann] -> Doc ann
application :: f -> [Doc ann] -> Doc ann
application f
f [] = f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty f
f
application f
f [Doc ann]
as = f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty f
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma [Doc ann]
as))

list :: Foldable f => f (Doc ann) -> Doc ann
list :: f (Doc ann) -> Doc ann
list = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann)
-> (f (Doc ann) -> Doc ann) -> f (Doc ann) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann)
-> (f (Doc ann) -> [Doc ann]) -> f (Doc ann) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ([Doc ann] -> [Doc ann])
-> (f (Doc ann) -> [Doc ann]) -> f (Doc ann) -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Doc ann) -> [Doc ann]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

bracketList :: (Pretty a, Functor f, Foldable f) => f a -> Doc ann
bracketList :: f a -> Doc ann
bracketList = f (Doc ann) -> Doc ann
forall (f :: * -> *) ann. Foldable f => f (Doc ann) -> Doc ann
list (f (Doc ann) -> Doc ann) -> (f a -> f (Doc ann)) -> f a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc ann) -> f a -> f (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


-- * Names

quoted :: Char -> Text -> Text
quoted :: Char -> Text -> Text
quoted Char
q = Char -> Text -> Text
Text.cons Char
q (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Char -> Text) -> Char -> Text -> Text
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Char -> Text
Text.snoc Char
q
         (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Text -> Text
Text.replace (Char -> Text
Text.singleton Char
q) (String -> Text
Text.pack [Char
'\\', Char
q])
         (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Text -> Text
Text.replace Text
"\\" Text
"\\\\"

newtype SingleQuoted = SingleQuoted Text
  deriving (SingleQuoted -> SingleQuoted -> Bool
(SingleQuoted -> SingleQuoted -> Bool)
-> (SingleQuoted -> SingleQuoted -> Bool) -> Eq SingleQuoted
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SingleQuoted -> SingleQuoted -> Bool
$c/= :: SingleQuoted -> SingleQuoted -> Bool
== :: SingleQuoted -> SingleQuoted -> Bool
$c== :: SingleQuoted -> SingleQuoted -> Bool
Eq, Int -> SingleQuoted -> ShowS
[SingleQuoted] -> ShowS
SingleQuoted -> String
(Int -> SingleQuoted -> ShowS)
-> (SingleQuoted -> String)
-> ([SingleQuoted] -> ShowS)
-> Show SingleQuoted
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SingleQuoted] -> ShowS
$cshowList :: [SingleQuoted] -> ShowS
show :: SingleQuoted -> String
$cshow :: SingleQuoted -> String
showsPrec :: Int -> SingleQuoted -> ShowS
$cshowsPrec :: Int -> SingleQuoted -> ShowS
Show, Eq SingleQuoted
Eq SingleQuoted
-> (SingleQuoted -> SingleQuoted -> Ordering)
-> (SingleQuoted -> SingleQuoted -> Bool)
-> (SingleQuoted -> SingleQuoted -> Bool)
-> (SingleQuoted -> SingleQuoted -> Bool)
-> (SingleQuoted -> SingleQuoted -> Bool)
-> (SingleQuoted -> SingleQuoted -> SingleQuoted)
-> (SingleQuoted -> SingleQuoted -> SingleQuoted)
-> Ord SingleQuoted
SingleQuoted -> SingleQuoted -> Bool
SingleQuoted -> SingleQuoted -> Ordering
SingleQuoted -> SingleQuoted -> SingleQuoted
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SingleQuoted -> SingleQuoted -> SingleQuoted
$cmin :: SingleQuoted -> SingleQuoted -> SingleQuoted
max :: SingleQuoted -> SingleQuoted -> SingleQuoted
$cmax :: SingleQuoted -> SingleQuoted -> SingleQuoted
>= :: SingleQuoted -> SingleQuoted -> Bool
$c>= :: SingleQuoted -> SingleQuoted -> Bool
> :: SingleQuoted -> SingleQuoted -> Bool
$c> :: SingleQuoted -> SingleQuoted -> Bool
<= :: SingleQuoted -> SingleQuoted -> Bool
$c<= :: SingleQuoted -> SingleQuoted -> Bool
< :: SingleQuoted -> SingleQuoted -> Bool
$c< :: SingleQuoted -> SingleQuoted -> Bool
compare :: SingleQuoted -> SingleQuoted -> Ordering
$ccompare :: SingleQuoted -> SingleQuoted -> Ordering
$cp1Ord :: Eq SingleQuoted
Ord)

instance Pretty SingleQuoted where
  pretty :: SingleQuoted -> Doc ann
pretty (SingleQuoted Text
t) = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Char -> Text -> Text
quoted Char
'\'' Text
t)

instance Pretty Atom where
  pretty :: Atom -> Doc ann
pretty (Atom Text
s)
    | Text -> Bool
isLowerWord Text
s = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
s
    | Bool
otherwise = SingleQuoted -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> SingleQuoted
SingleQuoted Text
s)
    where
      isLowerWord :: Text -> Bool
isLowerWord Text
w = Char -> Bool
isAsciiLower (Text -> Char
Text.head Text
w)
                   Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAlphaNum (Text -> Text
Text.tail Text
w)
      isAlphaNum :: Char -> Bool
isAlphaNum Char
c = Char -> Bool
isAsciiLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isAsciiUpper Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

instance Pretty Var where
  pretty :: Var -> Doc ann
pretty (Var Text
s) = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
s

newtype DoubleQuoted = DoubleQuoted Text
  deriving (DoubleQuoted -> DoubleQuoted -> Bool
(DoubleQuoted -> DoubleQuoted -> Bool)
-> (DoubleQuoted -> DoubleQuoted -> Bool) -> Eq DoubleQuoted
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DoubleQuoted -> DoubleQuoted -> Bool
$c/= :: DoubleQuoted -> DoubleQuoted -> Bool
== :: DoubleQuoted -> DoubleQuoted -> Bool
$c== :: DoubleQuoted -> DoubleQuoted -> Bool
Eq, Int -> DoubleQuoted -> ShowS
[DoubleQuoted] -> ShowS
DoubleQuoted -> String
(Int -> DoubleQuoted -> ShowS)
-> (DoubleQuoted -> String)
-> ([DoubleQuoted] -> ShowS)
-> Show DoubleQuoted
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DoubleQuoted] -> ShowS
$cshowList :: [DoubleQuoted] -> ShowS
show :: DoubleQuoted -> String
$cshow :: DoubleQuoted -> String
showsPrec :: Int -> DoubleQuoted -> ShowS
$cshowsPrec :: Int -> DoubleQuoted -> ShowS
Show, Eq DoubleQuoted
Eq DoubleQuoted
-> (DoubleQuoted -> DoubleQuoted -> Ordering)
-> (DoubleQuoted -> DoubleQuoted -> Bool)
-> (DoubleQuoted -> DoubleQuoted -> Bool)
-> (DoubleQuoted -> DoubleQuoted -> Bool)
-> (DoubleQuoted -> DoubleQuoted -> Bool)
-> (DoubleQuoted -> DoubleQuoted -> DoubleQuoted)
-> (DoubleQuoted -> DoubleQuoted -> DoubleQuoted)
-> Ord DoubleQuoted
DoubleQuoted -> DoubleQuoted -> Bool
DoubleQuoted -> DoubleQuoted -> Ordering
DoubleQuoted -> DoubleQuoted -> DoubleQuoted
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DoubleQuoted -> DoubleQuoted -> DoubleQuoted
$cmin :: DoubleQuoted -> DoubleQuoted -> DoubleQuoted
max :: DoubleQuoted -> DoubleQuoted -> DoubleQuoted
$cmax :: DoubleQuoted -> DoubleQuoted -> DoubleQuoted
>= :: DoubleQuoted -> DoubleQuoted -> Bool
$c>= :: DoubleQuoted -> DoubleQuoted -> Bool
> :: DoubleQuoted -> DoubleQuoted -> Bool
$c> :: DoubleQuoted -> DoubleQuoted -> Bool
<= :: DoubleQuoted -> DoubleQuoted -> Bool
$c<= :: DoubleQuoted -> DoubleQuoted -> Bool
< :: DoubleQuoted -> DoubleQuoted -> Bool
$c< :: DoubleQuoted -> DoubleQuoted -> Bool
compare :: DoubleQuoted -> DoubleQuoted -> Ordering
$ccompare :: DoubleQuoted -> DoubleQuoted -> Ordering
$cp1Ord :: Eq DoubleQuoted
Ord)

instance Pretty DoubleQuoted where
  pretty :: DoubleQuoted -> Doc ann
pretty (DoubleQuoted Text
t) = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Char -> Text -> Text
quoted Char
'"' Text
t)

instance Pretty DistinctObject where
  pretty :: DistinctObject -> Doc ann
pretty (DistinctObject Text
s) = DoubleQuoted -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> DoubleQuoted
DoubleQuoted Text
s)

newtype DollarWord = DollarWord Text
  deriving (DollarWord -> DollarWord -> Bool
(DollarWord -> DollarWord -> Bool)
-> (DollarWord -> DollarWord -> Bool) -> Eq DollarWord
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DollarWord -> DollarWord -> Bool
$c/= :: DollarWord -> DollarWord -> Bool
== :: DollarWord -> DollarWord -> Bool
$c== :: DollarWord -> DollarWord -> Bool
Eq, Int -> DollarWord -> ShowS
[DollarWord] -> ShowS
DollarWord -> String
(Int -> DollarWord -> ShowS)
-> (DollarWord -> String)
-> ([DollarWord] -> ShowS)
-> Show DollarWord
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DollarWord] -> ShowS
$cshowList :: [DollarWord] -> ShowS
show :: DollarWord -> String
$cshow :: DollarWord -> String
showsPrec :: Int -> DollarWord -> ShowS
$cshowsPrec :: Int -> DollarWord -> ShowS
Show, Eq DollarWord
Eq DollarWord
-> (DollarWord -> DollarWord -> Ordering)
-> (DollarWord -> DollarWord -> Bool)
-> (DollarWord -> DollarWord -> Bool)
-> (DollarWord -> DollarWord -> Bool)
-> (DollarWord -> DollarWord -> Bool)
-> (DollarWord -> DollarWord -> DollarWord)
-> (DollarWord -> DollarWord -> DollarWord)
-> Ord DollarWord
DollarWord -> DollarWord -> Bool
DollarWord -> DollarWord -> Ordering
DollarWord -> DollarWord -> DollarWord
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DollarWord -> DollarWord -> DollarWord
$cmin :: DollarWord -> DollarWord -> DollarWord
max :: DollarWord -> DollarWord -> DollarWord
$cmax :: DollarWord -> DollarWord -> DollarWord
>= :: DollarWord -> DollarWord -> Bool
$c>= :: DollarWord -> DollarWord -> Bool
> :: DollarWord -> DollarWord -> Bool
$c> :: DollarWord -> DollarWord -> Bool
<= :: DollarWord -> DollarWord -> Bool
$c<= :: DollarWord -> DollarWord -> Bool
< :: DollarWord -> DollarWord -> Bool
$c< :: DollarWord -> DollarWord -> Bool
compare :: DollarWord -> DollarWord -> Ordering
$ccompare :: DollarWord -> DollarWord -> Ordering
$cp1Ord :: Eq DollarWord
Ord)

instance Pretty DollarWord where
  pretty :: DollarWord -> Doc ann
pretty (DollarWord Text
w) = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Char -> Text -> Text
Text.cons Char
'$' Text
w)

tType :: DollarWord
tType :: DollarWord
tType = Text -> DollarWord
DollarWord Text
"tType"

instance Named s => Pretty (Name s) where
  pretty :: Name s -> Doc ann
pretty = \case
    Reserved Reserved s
s -> DollarWord -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> DollarWord
DollarWord (Reserved s -> Text
forall a. Named a => a -> Text
name Reserved s
s))
    Defined  Atom
a -> Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
a

instance Named s => Named (Reserved s) where
  name :: Reserved s -> Text
name = \case
    Standard s
s -> s -> Text
forall a. Named a => a -> Text
name s
s
    Extended Text
w -> Text
w

instance Named s => Pretty (Reserved s) where
  pretty :: Reserved s -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Reserved s -> Text) -> Reserved s -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reserved s -> Text
forall a. Named a => a -> Text
name


-- * Sorts and types

instance Pretty TFF1Sort where
  pretty :: TFF1Sort -> Doc ann
pretty = \case
    SortVariable Var
v -> Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Var
v
    TFF1Sort  Name Sort
f [TFF1Sort]
ss -> Name Sort -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application Name Sort
f ((TFF1Sort -> Doc ann) -> [TFF1Sort] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TFF1Sort -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [TFF1Sort]
ss)

prettyMapping :: Pretty a => [a] -> a -> Doc ann
prettyMapping :: [a] -> a -> Doc ann
prettyMapping [a]
as a
r = Doc ann
forall ann. Doc ann
args Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
r
  where
    args :: Doc ann
args = case [a]
as of
      []  -> Doc ann
forall a. Monoid a => a
mempty
      [a
a] -> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
">" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
space
      [a]
_   -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ((a -> Doc ann) -> [a] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [a]
as [Doc ann] -> Doc ann -> Doc ann
forall (f :: * -> *) ann.
Foldable f =>
f (Doc ann) -> Doc ann -> Doc ann
`sepBy` Doc ann
"*") Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
">" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
space

instance Pretty Type where
  pretty :: Type -> Doc ann
pretty = \case
    Type [Name Sort]
as Name Sort
r -> [Name Sort] -> Name Sort -> Doc ann
forall a ann. Pretty a => [a] -> a -> Doc ann
prettyMapping [Name Sort]
as Name Sort
r
    TFF1Type [Var]
vs [TFF1Sort]
as TFF1Sort
r -> Doc ann
forall ann. Doc ann
prefix Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> if [TFF1Sort] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TFF1Sort]
as then Doc ann
forall ann. Doc ann
matrix else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
forall ann. Doc ann
matrix
      where
        prefix :: Doc ann
prefix = case [Var] -> Maybe (NonEmpty Var)
forall a. [a] -> Maybe (NonEmpty a)
NEL.nonEmpty [Var]
vs of
          Maybe (NonEmpty Var)
Nothing -> Doc ann
forall a. Monoid a => a
mempty
          Just{}  -> Doc ann
"!>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall (f :: * -> *) ann. Foldable f => f (Doc ann) -> Doc ann
list ((Var -> Doc ann) -> [Var] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
prettyVar [Var]
vs) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
space
        prettyVar :: a -> Doc ann
prettyVar a
v = a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DollarWord -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty DollarWord
tType
        matrix :: Doc ann
matrix = [TFF1Sort] -> TFF1Sort -> Doc ann
forall a ann. Pretty a => [a] -> a -> Doc ann
prettyMapping [TFF1Sort]
as TFF1Sort
r


-- * First-order logic

instance Pretty Number where
  pretty :: Number -> Doc ann
pretty = \case
    IntegerConstant    Integer
i -> Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i
    RationalConstant Integer
n Integer
d -> Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
n Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"/" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
d
    RealConstant       Scientific
r -> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Scientific -> String
forall a. Show a => a -> String
show Scientific
r)

instance Pretty Term where
  pretty :: Term -> Doc ann
pretty = \case
    Function  Name Function
f [Term]
ts -> Name Function -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application Name Function
f ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Term]
ts)
    Variable     Var
v -> Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Var
v
    Number       Number
i -> Number -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Number
i
    DistinctTerm DistinctObject
d -> DistinctObject -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty DistinctObject
d

instance Pretty Literal where
  pretty :: Literal -> Doc ann
pretty = \case
    Predicate Name Predicate
p [Term]
ts -> Name Predicate -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application Name Predicate
p ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Term]
ts)
    Equality Term
a Sign
s Term
b -> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Sign -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Sign
s Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Term
b

instance Pretty Sign where
  pretty :: Sign -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Sign -> Text) -> Sign -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Text
forall a. Named a => a -> Text
name

instance Pretty Clause where
  pretty :: Clause -> Doc ann
pretty = \case
    Clause NonEmpty (Sign, Literal)
ls -> ((Sign, Literal) -> Doc ann)
-> NonEmpty (Sign, Literal) -> NonEmpty (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sign, Literal) -> Doc ann
forall a ann. Pretty a => (Sign, a) -> Doc ann
p NonEmpty (Sign, Literal)
ls NonEmpty (Doc ann) -> Doc ann -> Doc ann
forall (f :: * -> *) ann.
Foldable f =>
f (Doc ann) -> Doc ann -> Doc ann
`sepBy` Connective -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Connective
Disjunction
      where
        p :: (Sign, a) -> Doc ann
p (Sign
Positive, a
l) = a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l
        -- TPTP v7.3.0.0 doesn't allow for wrapping atom in parentesis in
        -- a negated atom in CNF formulas. I.e. for example ~ (X = Y) is
        -- not allowed. See http://www.tptp.org/TPTP/SyntaxBNF.html#cnf_formula
        -- TODO: implement AB-test comparing this parser against some canonical
        -- implementation of the parser of TPTP BNF (like tptp4X).
        p (Sign
Negative, a
l) = Doc ann
"~" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l

instance Pretty Quantifier where
  pretty :: Quantifier -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Quantifier -> Text) -> Quantifier -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantifier -> Text
forall a. Named a => a -> Text
name

instance Pretty Connective where
  pretty :: Connective -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Connective -> Text) -> Connective -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Connective -> Text
forall a. Named a => a -> Text
name

instance Pretty Unsorted where
  pretty :: Unsorted -> Doc ann
pretty = Unsorted -> Doc ann
forall a. Monoid a => a
mempty

instance Pretty s => Pretty (Sorted s) where
  pretty :: Sorted s -> Doc ann
pretty = \case
    Sorted Maybe s
Nothing  -> Doc ann
forall a. Monoid a => a
mempty
    Sorted (Just s
s) -> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty s
s

instance Pretty QuantifiedSort where
  pretty :: QuantifiedSort -> Doc ann
pretty = Doc ann -> QuantifiedSort -> Doc ann
forall a b. a -> b -> a
const (DollarWord -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty DollarWord
tType)

instance Pretty (Either QuantifiedSort TFF1Sort) where
  pretty :: Either QuantifiedSort TFF1Sort -> Doc ann
pretty = (QuantifiedSort -> Doc ann)
-> (TFF1Sort -> Doc ann)
-> Either QuantifiedSort TFF1Sort
-> Doc ann
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either QuantifiedSort -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty TFF1Sort -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty

unitary :: FirstOrder s -> Bool
unitary :: FirstOrder s -> Bool
unitary = \case
  Atomic{}     -> Bool
True
  Negated{}    -> Bool
True
  Quantified{} -> Bool
True
  Connected{}  -> Bool
False

ppretty :: Pretty s => (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty :: (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty FirstOrder s -> Bool
skipParens FirstOrder s
f
  | FirstOrder s -> Bool
skipParens FirstOrder s
f = FirstOrder s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty FirstOrder s
f
  | Bool
otherwise    = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (FirstOrder s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty FirstOrder s
f)

under :: Connective -> FirstOrder s -> Bool
under :: Connective -> FirstOrder s -> Bool
under Connective
c = \case
  Connected FirstOrder s
_ Connective
c' FirstOrder s
_ -> Connective
c' Connective -> Connective -> Bool
forall a. Eq a => a -> a -> Bool
== Connective
c Bool -> Bool -> Bool
&& Connective -> Bool
isAssociative Connective
c
  FirstOrder s
f -> FirstOrder s -> Bool
forall s. FirstOrder s -> Bool
unitary FirstOrder s
f

instance Pretty s => Pretty (FirstOrder s) where
  pretty :: FirstOrder s -> Doc ann
pretty = \case
    Atomic Literal
l -> Literal -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Literal
l
    Negated FirstOrder s
f -> Doc ann
"~" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
forall s ann.
Pretty s =>
(FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty FirstOrder s -> Bool
forall s. FirstOrder s -> Bool
unitary FirstOrder s
f
    Connected FirstOrder s
f Connective
c FirstOrder s
g -> (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
forall s ann.
Pretty s =>
(FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty (Connective -> FirstOrder s -> Bool
forall s. Connective -> FirstOrder s -> Bool
under Connective
c) FirstOrder s
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Connective -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Connective
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
forall s ann.
Pretty s =>
(FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty (Connective -> FirstOrder s -> Bool
forall s. Connective -> FirstOrder s -> Bool
under Connective
c) FirstOrder s
g
    Quantified Quantifier
q NonEmpty (Var, s)
vs FirstOrder s
f -> Quantifier -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Quantifier
q Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall (f :: * -> *) ann. Foldable f => f (Doc ann) -> Doc ann
list [Doc ann]
forall ann. [Doc ann]
vs' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
forall s ann.
Pretty s =>
(FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
ppretty FirstOrder s -> Bool
forall s. FirstOrder s -> Bool
unitary FirstOrder s
f
      where
        vs' :: [Doc ann]
vs' = ((Var, s) -> Doc ann) -> [(Var, s)] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var, s) -> Doc ann
forall a a ann. (Pretty a, Pretty a) => (a, a) -> Doc ann
var (NonEmpty (Var, s) -> [(Var, s)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList NonEmpty (Var, s)
vs)
        var :: (a, a) -> Doc ann
var (a
v, a
s) = a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
s


-- ** Units

instance Pretty Language where
  pretty :: Language -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Language -> Text) -> Language -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Language -> Text
forall a. Named a => a -> Text
name

instance Pretty Formula where
  pretty :: Formula -> Doc ann
pretty = \case
    CNF  Clause
c -> Clause -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Clause
c
    FOF  UnsortedFirstOrder
f -> UnsortedFirstOrder -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty UnsortedFirstOrder
f
    TFF0 MonomorphicFirstOrder
f -> MonomorphicFirstOrder -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty MonomorphicFirstOrder
f
    TFF1 PolymorphicFirstOrder
f -> PolymorphicFirstOrder -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty PolymorphicFirstOrder
f

instance Pretty UnitName where
  pretty :: UnitName -> Doc ann
pretty = (Atom -> Doc ann) -> (Integer -> Doc ann) -> UnitName -> Doc ann
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty
  prettyList :: [UnitName] -> Doc ann
prettyList = [UnitName] -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList

instance Pretty Declaration where
  pretty :: Declaration -> Doc ann
pretty = \case
    Formula Reserved Role
_ Formula
f -> Formula -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Formula
f
    Typing  Atom
s Type
t -> Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
t
    Sort    Atom
s Integer
n -> Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [DollarWord] -> DollarWord -> Doc ann
forall a ann. Pretty a => [a] -> a -> Doc ann
prettyMapping [DollarWord]
tTypes DollarWord
tType
      where tTypes :: [DollarWord]
tTypes = Integer -> DollarWord -> [DollarWord]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n DollarWord
tType

instance Pretty Unit where
  pretty :: Unit -> Doc ann
pretty = \case
    Include (Atom Text
f) Maybe (NonEmpty UnitName)
ns -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"include") [Doc ann]
forall ann. [Doc ann]
args Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      where
        args :: [Doc ann]
args = SingleQuoted -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> SingleQuoted
SingleQuoted Text
f) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Maybe (Doc ann) -> [Doc ann]
forall a. Maybe a -> [a]
maybeToList ((NonEmpty UnitName -> Doc ann)
-> Maybe (NonEmpty UnitName) -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty UnitName -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList Maybe (NonEmpty UnitName)
ns)
    Unit UnitName
nm Declaration
decl Maybe Annotation
a -> Language -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Declaration -> Language
declarationLanguage Declaration
decl) [Doc ann]
forall ann. [Doc ann]
args Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      where
        args :: [Doc ann]
args = UnitName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty UnitName
nm Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Doc ann
forall ann. Doc ann
role Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Declaration -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Declaration
decl Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
forall ann. [Doc ann]
ann

        role :: Doc ann
role = case Declaration
decl of
          Sort{}      -> Doc ann
"type"
          Typing{}    -> Doc ann
"type"
          Formula Reserved Role
r Formula
_ -> Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Reserved Role -> Text
forall a. Named a => a -> Text
name Reserved Role
r)

        ann :: [Doc ann]
ann = case Maybe Annotation
a of
          Just (Source
s, Maybe [Info]
i) -> Source -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Source
s Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Maybe (Doc ann) -> [Doc ann]
forall a. Maybe a -> [a]
maybeToList (([Info] -> Doc ann) -> Maybe [Info] -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList Maybe [Info]
i)
          Maybe Annotation
Nothing -> []

  prettyList :: [Unit] -> Doc ann
prettyList [Unit]
us = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep ((Unit -> Doc ann) -> [Unit] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Unit -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Unit]
us)

instance Pretty TPTP where
  pretty :: TPTP -> Doc ann
pretty (TPTP [Unit]
us) = [Unit] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Unit]
us

szsComment :: [Doc ann] -> Doc ann
szsComment :: [Doc ann] -> Doc ann
szsComment = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
comment (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann)
-> ([Doc ann] -> [Doc ann]) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"SZS"Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
:)

instance Pretty TSTP where
  pretty :: TSTP -> Doc ann
pretty (TSTP (SZS Maybe Status
s Maybe Dataform
d) [Unit]
us) = Doc ann
forall ann. Doc ann
status Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dataform ([Unit] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Unit]
us)
    where
      status :: Doc ann
status = case Maybe Status
s of
        Maybe Status
Nothing -> Doc ann
forall a. Monoid a => a
mempty
        Just Status
st -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
szsComment [Doc ann
"status", Status -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Status
st]
      dataform :: Doc ann -> Doc ann
dataform Doc ann
p = case Maybe Dataform
d of
        Maybe Dataform
Nothing -> Doc ann
p
        Just Dataform
df -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
szsComment [Doc ann
"output", Doc ann
"start", Dataform -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Dataform
df]
                Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
p Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
line
                Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
szsComment [Doc ann
"output", Doc ann
"end", Dataform -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Dataform
df]


-- * Annotations

instance Pretty Intro where
  pretty :: Intro -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Intro -> Text) -> Intro -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Intro -> Text
forall a. Named a => a -> Text
name

instance Pretty Success where
  pretty :: Success -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Success -> Text) -> Success -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SZSOntology Success -> Text
forall a. Named a => a -> Text
name (SZSOntology Success -> Text)
-> (Success -> SZSOntology Success) -> Success -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Success -> SZSOntology Success
forall a. a -> SZSOntology a
SZSOntology

instance Pretty NoSuccess where
  pretty :: NoSuccess -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (NoSuccess -> Text) -> NoSuccess -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SZSOntology NoSuccess -> Text
forall a. Named a => a -> Text
name (SZSOntology NoSuccess -> Text)
-> (NoSuccess -> SZSOntology NoSuccess) -> NoSuccess -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NoSuccess -> SZSOntology NoSuccess
forall a. a -> SZSOntology a
SZSOntology

instance Pretty Status where
  pretty :: Status -> Doc ann
pretty = (NoSuccess -> Doc ann) -> (Success -> Doc ann) -> Status -> Doc ann
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either NoSuccess -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Success -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty

instance Pretty Dataform where
  pretty :: Dataform -> Doc ann
pretty = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> (Dataform -> Text) -> Dataform -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SZSOntology Dataform -> Text
forall a. Named a => a -> Text
name (SZSOntology Dataform -> Text)
-> (Dataform -> SZSOntology Dataform) -> Dataform -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dataform -> SZSOntology Dataform
forall a. a -> SZSOntology a
SZSOntology

instance Pretty (Either Var Atom) where
  pretty :: Either Var Atom -> Doc ann
pretty = (Var -> Doc ann) -> (Atom -> Doc ann) -> Either Var Atom -> Doc ann
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty
  prettyList :: [Either Var Atom] -> Doc ann
prettyList = [Either Var Atom] -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList

instance Pretty Info where
  pretty :: Info -> Doc ann
pretty = \case
    Description    Atom
a -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"description") [Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
a]
    Iquote         Atom
a -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"iquote")      [Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
a]
    Status         Reserved Success
s -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"status")      [Reserved Success -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Reserved Success
s]
    Assumptions    NonEmpty UnitName
u -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"assumptions") [NonEmpty UnitName -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList NonEmpty UnitName
u]
    NewSymbols  Atom
n [Either Var Atom]
ss -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"new_symbols") [Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
n, [Either Var Atom] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Either Var Atom]
ss]
    Refutation     Atom
a -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"refutation")  [Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
a]
    Bind         Var
v Expression
e -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"bind")        [Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Var
v, Expression -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Expression
e]
    Application Atom
f [Info]
as -> Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application Atom
f                    ((Info -> Doc ann) -> [Info] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Info -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Info]
as)
    Expression     Expression
e -> Expression -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Expression
e
    InfoNumber     Number
n -> Number -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Number
n
    Infos         [Info]
is -> [Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Info]
is

  prettyList :: [Info] -> Doc ann
prettyList = [Info] -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList

instance Pretty Expression where
  pretty :: Expression -> Doc ann
pretty = \case
    Logical Formula
f -> DollarWord -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> DollarWord
DollarWord (Text -> DollarWord)
-> (Language -> Text) -> Language -> DollarWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Language -> Text
forall a. Named a => a -> Text
name (Language -> DollarWord) -> Language -> DollarWord
forall a b. (a -> b) -> a -> b
$ Formula -> Language
formulaLanguage Formula
f) [Formula -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Formula
f]
    Term    Term
t -> DollarWord -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> DollarWord
DollarWord Text
"fot") [Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Term
t]

instance Pretty Parent where
  pretty :: Parent -> Doc ann
pretty = \case
    Parent Source
s  [] -> Source -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Source
s
    Parent Source
s [Info]
gts -> Source -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Source
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Info]
gts
  prettyList :: [Parent] -> Doc ann
prettyList = [Parent] -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList

instance Pretty Source where
  pretty :: Source -> Doc ann
pretty = \case
    UnitSource UnitName
un -> UnitName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty UnitName
un
    Source
UnknownSource -> Doc ann
"unknown"
    File (Atom Text
n) Maybe UnitName
i -> Text -> SingleQuoted -> Maybe (Doc ann) -> Doc ann
forall a ann. Pretty a => Text -> a -> Maybe (Doc ann) -> Doc ann
source Text
"file" (Text -> SingleQuoted
SingleQuoted Text
n) (UnitName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty     (UnitName -> Doc ann) -> Maybe UnitName -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe UnitName
i)
    Theory     Atom
n  Maybe [Info]
i -> Text -> Atom -> Maybe (Doc ann) -> Doc ann
forall a ann. Pretty a => Text -> a -> Maybe (Doc ann) -> Doc ann
source Text
"theory"             Atom
n  ([Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList ([Info] -> Doc ann) -> Maybe [Info] -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Info]
i)
    Creator    Atom
n  Maybe [Info]
i -> Text -> Atom -> Maybe (Doc ann) -> Doc ann
forall a ann. Pretty a => Text -> a -> Maybe (Doc ann) -> Doc ann
source Text
"creator"            Atom
n  ([Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList ([Info] -> Doc ann) -> Maybe [Info] -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Info]
i)
    Introduced Reserved Intro
n  Maybe [Info]
i -> Text -> Reserved Intro -> Maybe (Doc ann) -> Doc ann
forall a ann. Pretty a => Text -> a -> Maybe (Doc ann) -> Doc ann
source Text
"introduced"         Reserved Intro
n  ([Info] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList ([Info] -> Doc ann) -> Maybe [Info] -> Maybe (Doc ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Info]
i)
    Inference  Atom
n  [Info]
i [Parent]
ps ->
      Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
"inference") [Atom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Atom
n, [Info] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Info]
i, [Parent] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
prettyList [Parent]
ps]
    where
      source :: Text -> a -> Maybe (Doc ann) -> Doc ann
source Text
f a
n Maybe (Doc ann)
i = Atom -> [Doc ann] -> Doc ann
forall f ann. Pretty f => f -> [Doc ann] -> Doc ann
application (Text -> Atom
Atom Text
f) (a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
n Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Maybe (Doc ann) -> [Doc ann]
forall a. Maybe a -> [a]
maybeToList Maybe (Doc ann)
i)

  prettyList :: [Source] -> Doc ann
prettyList = [Source] -> Doc ann
forall a (f :: * -> *) ann.
(Pretty a, Functor f, Foldable f) =>
f a -> Doc ann
bracketList