{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards
  , StandaloneDeriving
  , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
  , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
  , RankNTypes, PatternGuards
  #-}

{-# OPTIONS -Wall -fno-warn-orphans #-}

-- | Mainly just 'Pretty' instances
module Codec.TPTP.Pretty(PrettyAnsi(..),prettySimple,WithEnclosing(..),Enclosing(..)) where

import Prelude hiding ((<$>))

import Codec.TPTP.Base
import Codec.TPTP.Export
import Prettyprinter
import Prettyprinter.Render.Terminal
import Data.Data
import Control.Monad.Identity
import Data.Ratio
import qualified Data.Text.Lazy as TL

class PrettyAnsi a where
  prettyAnsi :: a -> Doc AnsiStyle
  prettyAnsiList :: [a] -> Doc AnsiStyle
  prettyAnsiList = Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
align (Doc AnsiStyle -> Doc AnsiStyle)
-> ([a] -> Doc AnsiStyle) -> [a] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
list ([Doc AnsiStyle] -> Doc AnsiStyle)
-> ([a] -> [Doc AnsiStyle]) -> [a] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc AnsiStyle) -> [a] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi

instance PrettyAnsi (Doc AnsiStyle) where
  prettyAnsi :: Doc AnsiStyle -> Doc AnsiStyle
prettyAnsi = Doc AnsiStyle -> Doc AnsiStyle
forall a. a -> a
id

instance PrettyAnsi a => PrettyAnsi [a] where
  prettyAnsi :: [a] -> Doc AnsiStyle
prettyAnsi = [a] -> Doc AnsiStyle
forall a. PrettyAnsi a => [a] -> Doc AnsiStyle
prettyAnsiList

oper :: String -> Doc AnsiStyle
oper :: String -> Doc AnsiStyle
oper = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
Yellow) (Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc AnsiStyle
forall ann. String -> Doc ann
text
psym :: forall a. (Pretty a) => a -> Doc AnsiStyle
psym :: forall a. Pretty a => a -> Doc AnsiStyle
psym = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Green) (Doc AnsiStyle -> Doc AnsiStyle)
-> (a -> Doc AnsiStyle) -> a -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc AnsiStyle
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty
fsym :: forall a. (Pretty a) => a -> Doc AnsiStyle
fsym :: forall a. Pretty a => a -> Doc AnsiStyle
fsym = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Yellow) (Doc AnsiStyle -> Doc AnsiStyle)
-> (a -> Doc AnsiStyle) -> a -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc AnsiStyle
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty

text :: String -> Doc ann
text :: forall ann. String -> Doc ann
text = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty

--wtext :: String -> Doc
--wtext = annotate (color White) . text

prettyargs :: forall a. (PrettyAnsi a) => [a] -> Doc AnsiStyle
--prettyargs = encloseSep (wtext "(") (wtext ")") (wtext ",") . fmap pretty
prettyargs :: forall a. PrettyAnsi a => [a] -> Doc AnsiStyle
prettyargs = [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
tupled ([Doc AnsiStyle] -> Doc AnsiStyle)
-> ([a] -> [Doc AnsiStyle]) -> [a] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc AnsiStyle) -> [a] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi
-- prettyargs [] = annotate (color White) $ text "()"
-- prettyargs (x:xs) =
--     let pxs = fmap ((annotate (color White) (text ",") <+>) . pretty) xs in

--     align (fillSep $ [    annotate (color White) (text "(") <+> pretty x ]
--                     ++ pxs
--                     ++ [ annotate (color White) (text ")") ] )

prational :: Rational -> Doc ann
prational :: forall ann. Rational -> Doc ann
prational Rational
q = (String -> Doc ann
forall ann. String -> Doc ann
text(String -> Doc ann) -> (Rational -> String) -> Rational -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Integer -> String
forall a. Show a => a -> String
show(Integer -> String) -> (Rational -> Integer) -> Rational -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Rational -> Integer
forall a. Ratio a -> a
numerator) Rational
q Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'/' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> (String -> Doc ann
forall ann. String -> Doc ann
text(String -> Doc ann) -> (Rational -> String) -> Rational -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Integer -> String
forall a. Show a => a -> String
show(Integer -> String) -> (Rational -> Integer) -> Rational -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Rational -> Integer
forall a. Ratio a -> a
denominator) Rational
q

-- | Carries information about the enclosing operation (for the purpose of printing stuff without parentheses if possible).
data WithEnclosing a = WithEnclosing Enclosing a

data Enclosing = EnclBinOp BinOp | EnclQuant | EnclNeg | EnclInfixPred InfixPred | EnclNothing
               deriving (Enclosing -> Enclosing -> Bool
(Enclosing -> Enclosing -> Bool)
-> (Enclosing -> Enclosing -> Bool) -> Eq Enclosing
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Enclosing -> Enclosing -> Bool
== :: Enclosing -> Enclosing -> Bool
$c/= :: Enclosing -> Enclosing -> Bool
/= :: Enclosing -> Enclosing -> Bool
Eq,Eq Enclosing
Eq Enclosing =>
(Enclosing -> Enclosing -> Ordering)
-> (Enclosing -> Enclosing -> Bool)
-> (Enclosing -> Enclosing -> Bool)
-> (Enclosing -> Enclosing -> Bool)
-> (Enclosing -> Enclosing -> Bool)
-> (Enclosing -> Enclosing -> Enclosing)
-> (Enclosing -> Enclosing -> Enclosing)
-> Ord Enclosing
Enclosing -> Enclosing -> Bool
Enclosing -> Enclosing -> Ordering
Enclosing -> Enclosing -> Enclosing
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
$ccompare :: Enclosing -> Enclosing -> Ordering
compare :: Enclosing -> Enclosing -> Ordering
$c< :: Enclosing -> Enclosing -> Bool
< :: Enclosing -> Enclosing -> Bool
$c<= :: Enclosing -> Enclosing -> Bool
<= :: Enclosing -> Enclosing -> Bool
$c> :: Enclosing -> Enclosing -> Bool
> :: Enclosing -> Enclosing -> Bool
$c>= :: Enclosing -> Enclosing -> Bool
>= :: Enclosing -> Enclosing -> Bool
$cmax :: Enclosing -> Enclosing -> Enclosing
max :: Enclosing -> Enclosing -> Enclosing
$cmin :: Enclosing -> Enclosing -> Enclosing
min :: Enclosing -> Enclosing -> Enclosing
Ord,Int -> Enclosing -> ShowS
[Enclosing] -> ShowS
Enclosing -> String
(Int -> Enclosing -> ShowS)
-> (Enclosing -> String)
-> ([Enclosing] -> ShowS)
-> Show Enclosing
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Enclosing -> ShowS
showsPrec :: Int -> Enclosing -> ShowS
$cshow :: Enclosing -> String
show :: Enclosing -> String
$cshowList :: [Enclosing] -> ShowS
showList :: [Enclosing] -> ShowS
Show,Typeable Enclosing
Typeable Enclosing =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Enclosing -> c Enclosing)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Enclosing)
-> (Enclosing -> Constr)
-> (Enclosing -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Enclosing))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Enclosing))
-> ((forall b. Data b => b -> b) -> Enclosing -> Enclosing)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Enclosing -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Enclosing -> r)
-> (forall u. (forall d. Data d => d -> u) -> Enclosing -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Enclosing -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Enclosing -> m Enclosing)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Enclosing -> m Enclosing)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Enclosing -> m Enclosing)
-> Data Enclosing
Enclosing -> Constr
Enclosing -> DataType
(forall b. Data b => b -> b) -> Enclosing -> Enclosing
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Enclosing -> u
forall u. (forall d. Data d => d -> u) -> Enclosing -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Enclosing
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Enclosing -> c Enclosing
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Enclosing)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Enclosing)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Enclosing -> c Enclosing
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Enclosing -> c Enclosing
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Enclosing
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Enclosing
$ctoConstr :: Enclosing -> Constr
toConstr :: Enclosing -> Constr
$cdataTypeOf :: Enclosing -> DataType
dataTypeOf :: Enclosing -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Enclosing)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Enclosing)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Enclosing)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Enclosing)
$cgmapT :: (forall b. Data b => b -> b) -> Enclosing -> Enclosing
gmapT :: (forall b. Data b => b -> b) -> Enclosing -> Enclosing
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Enclosing -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Enclosing -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Enclosing -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Enclosing -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Enclosing -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Enclosing -> m Enclosing
Data,Typeable,ReadPrec [Enclosing]
ReadPrec Enclosing
Int -> ReadS Enclosing
ReadS [Enclosing]
(Int -> ReadS Enclosing)
-> ReadS [Enclosing]
-> ReadPrec Enclosing
-> ReadPrec [Enclosing]
-> Read Enclosing
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Enclosing
readsPrec :: Int -> ReadS Enclosing
$creadList :: ReadS [Enclosing]
readList :: ReadS [Enclosing]
$creadPrec :: ReadPrec Enclosing
readPrec :: ReadPrec Enclosing
$creadListPrec :: ReadPrec [Enclosing]
readListPrec :: ReadPrec [Enclosing]
Read)

unaryEncl :: Enclosing -> Bool
unaryEncl :: Enclosing -> Bool
unaryEncl Enclosing
EnclNeg = Bool
True
unaryEncl Enclosing
EnclQuant = Bool
True
unaryEncl Enclosing
_ = Bool
False

needsParens :: Enclosing -> Enclosing -> Bool
needsParens :: Enclosing -> Enclosing -> Bool
needsParens Enclosing
inner Enclosing
outer =
    case (Enclosing
inner,Enclosing
outer) of
      -- special handling for associative ops
      ((EnclBinOp BinOp
(:&:)),(EnclBinOp BinOp
(:&:))) -> Bool
False
      ((EnclBinOp BinOp
(:|:)),(EnclBinOp BinOp
(:|:))) -> Bool
False
      ((EnclBinOp BinOp
(:<~>:)),(EnclBinOp BinOp
(:<~>:))) -> Bool
False

      -- chains of quantifiers/negation don't need parentheses
      (Enclosing, Enclosing)
_
          | Enclosing -> Bool
unaryEncl Enclosing
inner, Enclosing -> Bool
unaryEncl Enclosing
outer
                -> Bool
False

      (Enclosing, Enclosing)
_ -> Enclosing -> Int
prec Enclosing
inner Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Enclosing -> Int
prec Enclosing
outer
  where
    prec :: Enclosing -> Int
    prec :: Enclosing -> Int
prec Enclosing
x = case Enclosing
x of
               (EnclInfixPred InfixPred
_) -> Int
60
               (Enclosing
EnclNeg) -> Int
50
               (Enclosing
EnclQuant) -> Int
50
               (EnclBinOp BinOp
(:&:)) -> Int
40
               (EnclBinOp BinOp
(:~&:)) -> Int
40
               (EnclBinOp BinOp
(:|:)) -> Int
30
               (EnclBinOp BinOp
(:~|:)) -> Int
30
               (EnclBinOp BinOp
(:=>:)) -> Int
20
               (EnclBinOp BinOp
(:<=:)) -> Int
20
               (EnclBinOp BinOp
(:<=>:)) -> Int
20
               (EnclBinOp BinOp
(:<~>:)) -> Int
20
               Enclosing
EnclNothing -> (-Int
1000) -- if there's no enclosing operation, we don't need parentheses


maybeParens :: Enclosing -> Enclosing -> Doc ann -> Doc ann
maybeParens :: forall ann. Enclosing -> Enclosing -> Doc ann -> Doc ann
maybeParens Enclosing
inner Enclosing
outer | Enclosing -> Enclosing -> Bool
needsParens Enclosing
inner Enclosing
outer = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens
maybeParens Enclosing
_ Enclosing
_ = Doc ann -> Doc ann
forall a. a -> a
id

instance PrettyAnsi TPTP_Input where
    prettyAnsi :: TPTP_Input -> Doc AnsiStyle
prettyAnsi AFormula{F Identity
AtomicWord
Role
Annotations
name :: AtomicWord
role :: Role
formula :: F Identity
annotations :: Annotations
name :: forall (c :: * -> *). TPTP_Input_ c -> AtomicWord
role :: forall (c :: * -> *). TPTP_Input_ c -> Role
formula :: forall (c :: * -> *). TPTP_Input_ c -> F c
annotations :: forall (c :: * -> *). TPTP_Input_ c -> Annotations
..}
        = [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
fillSep
          [ (forall ann. String -> Doc ann
text) String
"Formula " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White)(Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> Doc AnsiStyle
forall ann. String -> Doc ann
text) String
"name:"
          , [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
vsep
            [
              (AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Red)(Doc AnsiStyle -> Doc AnsiStyle)
-> (AtomicWord -> Doc AnsiStyle) -> AtomicWord -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.AtomicWord -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomicWord -> Doc ann
pretty) AtomicWord
name Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White) (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"role:") Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Magenta)(Doc AnsiStyle -> Doc AnsiStyle)
-> (Role -> Doc AnsiStyle) -> Role -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> Doc AnsiStyle
forall ann. String -> Doc ann
text(String -> Doc AnsiStyle)
-> (Role -> String) -> Role -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Role -> String
unrole) Role
role
            , F Identity -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi F Identity
formula
            , Annotations -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi Annotations
annotations
            , Doc AnsiStyle
forall a. Monoid a => a
mempty
            ]
          ]

    prettyAnsi (Comment String
str)
        = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Magenta) (Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ String
str

    prettyAnsi (Include String
f [AtomicWord]
sel) = String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"include" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
squotes (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
f) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> (case [AtomicWord]
sel of { [] -> Doc AnsiStyle
forall a. Monoid a => a
mempty; [AtomicWord]
_ -> Doc AnsiStyle
forall ann. Doc ann
comma Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
sep (Doc AnsiStyle -> [Doc AnsiStyle] -> [Doc AnsiStyle]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc AnsiStyle
forall ann. Doc ann
comma ((AtomicWord -> Doc AnsiStyle) -> [AtomicWord] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AtomicWord -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomicWord -> Doc ann
pretty [AtomicWord]
sel)) } ))


    prettyAnsiList :: [TPTP_Input] -> Doc AnsiStyle
prettyAnsiList = (TPTP_Input -> Doc AnsiStyle -> Doc AnsiStyle)
-> Doc AnsiStyle -> [TPTP_Input] -> Doc AnsiStyle
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\TPTP_Input
x Doc AnsiStyle
xs -> [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
vsep [TPTP_Input -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi TPTP_Input
x, Doc AnsiStyle
xs]) Doc AnsiStyle
forall a. Monoid a => a
mempty

instance PrettyAnsi Quant where
    prettyAnsi :: Quant -> Doc AnsiStyle
prettyAnsi Quant
All = String -> Doc AnsiStyle
oper String
"∀"
    prettyAnsi Quant
Exists = String -> Doc AnsiStyle
oper String
"∃"

instance (PrettyAnsi (WithEnclosing t), PrettyAnsi (WithEnclosing f)) => PrettyAnsi ((WithEnclosing (Formula0 t f))) where
    prettyAnsi :: WithEnclosing (Formula0 t f) -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
enclosing Formula0 t f
formu) =
        let
            newEnclosing :: Enclosing
newEnclosing =
             case Formula0 t f
formu of
               Quant Quant
_ [V]
_ f
_ -> Enclosing
EnclQuant
               PredApp AtomicWord
_ [t]
_ -> Enclosing
EnclNothing -- arguments are comma-seperated, so they don't need any parens
               (:~:) f
_ -> Enclosing
EnclNeg
               BinOp f
_ BinOp
op f
_ -> BinOp -> Enclosing
EnclBinOp BinOp
op
               InfixPred t
_ InfixPred
op t
_ -> InfixPred -> Enclosing
EnclInfixPred InfixPred
op

            wne :: a -> WithEnclosing a
wne = Enclosing -> a -> WithEnclosing a
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
newEnclosing

        in
          Enclosing -> Enclosing -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Enclosing -> Enclosing -> Doc ann -> Doc ann
maybeParens Enclosing
newEnclosing Enclosing
enclosing (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$

          case Formula0 t f
formu of

            Quant Quant
q [V]
vars f
f ->
               [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
fillSep
               [ Quant -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi Quant
q
                 Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
brackets ([Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
hsep (Doc AnsiStyle -> [Doc AnsiStyle] -> [Doc AnsiStyle]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc AnsiStyle
forall ann. Doc ann
comma ((V -> Doc AnsiStyle) -> [V] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi [V]
vars)))
                 Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
forall ann. Doc ann
dot
               , WithEnclosing f -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (f -> WithEnclosing f
forall {a}. a -> WithEnclosing a
wne f
f)
               ]

            (:~:) f
f -> String -> Doc AnsiStyle
oper String
"¬" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> WithEnclosing f -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (f -> WithEnclosing f
forall {a}. a -> WithEnclosing a
wne f
f)

            PredApp AtomicWord
p [] -> AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
psym AtomicWord
p
            PredApp AtomicWord
p [t]
args -> AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
psym AtomicWord
p Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> [WithEnclosing t] -> Doc AnsiStyle
forall a. PrettyAnsi a => [a] -> Doc AnsiStyle
prettyargs ((t -> WithEnclosing t) -> [t] -> [WithEnclosing t]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> WithEnclosing t
forall {a}. a -> WithEnclosing a
wne [t]
args)


            BinOp f
f1 BinOp
op f
f2 ->
                Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
align (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
sep [Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
indent Int
0 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ WithEnclosing f -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (f -> WithEnclosing f
forall {a}. a -> WithEnclosing a
wne f
f1), BinOp -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi BinOp
op, Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
indent Int
0 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ WithEnclosing f -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (f -> WithEnclosing f
forall {a}. a -> WithEnclosing a
wne f
f2)]

            InfixPred t
f1 InfixPred
op t
f2 ->
                Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
align (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
sep [Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
indent Int
0 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ WithEnclosing t -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (t -> WithEnclosing t
forall {a}. a -> WithEnclosing a
wne t
f1), InfixPred -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi InfixPred
op, Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
indent Int
0 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ WithEnclosing t -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (t -> WithEnclosing t
forall {a}. a -> WithEnclosing a
wne t
f2)]

instance PrettyAnsi BinOp where
    prettyAnsi :: BinOp -> Doc AnsiStyle
prettyAnsi BinOp
x = case BinOp
x of
        BinOp
(:<=>:) -> String -> Doc AnsiStyle
oper String
"⇔"
        BinOp
(:=>:)  -> String -> Doc AnsiStyle
oper String
"⇒"
        BinOp
(:<=:)  -> String -> Doc AnsiStyle
oper String
"⇐"
        BinOp
(:&:)   -> String -> Doc AnsiStyle
oper String
"∧"
        BinOp
(:|:)   -> String -> Doc AnsiStyle
oper String
"∨"
        BinOp
(:~&:)  -> String -> Doc AnsiStyle
oper String
"NAND"
        BinOp
(:~|:)  -> String -> Doc AnsiStyle
oper String
"NOR"
        BinOp
(:<~>:) -> String -> Doc AnsiStyle
oper String
"XOR"

instance PrettyAnsi InfixPred where
    prettyAnsi :: InfixPred -> Doc AnsiStyle
prettyAnsi InfixPred
x = case InfixPred
x of
        InfixPred
(:=:)   -> String -> Doc AnsiStyle
oper String
"="
        InfixPred
(:!=:)  -> String -> Doc AnsiStyle
oper String
"≠"

instance (PrettyAnsi (WithEnclosing t)) => PrettyAnsi (WithEnclosing (Term0 t)) where
    prettyAnsi :: WithEnclosing (Term0 t) -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
_ Term0 t
x) =
        case Term0 t
x of
          Var V
s -> V -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi V
s
          NumberLitTerm Rational
d -> Rational -> Doc AnsiStyle
forall ann. Rational -> Doc ann
prational Rational
d
          DistinctObjectTerm String
s -> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Cyan) (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
dquotes (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
s))
          FunApp AtomicWord
f [] -> AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
fsym AtomicWord
f
          FunApp AtomicWord
f [t]
args -> AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
fsym AtomicWord
f Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> [WithEnclosing t] -> Doc AnsiStyle
forall a. PrettyAnsi a => [a] -> Doc AnsiStyle
prettyargs ((t -> WithEnclosing t) -> [t] -> [WithEnclosing t]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Enclosing -> t -> WithEnclosing t
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing) [t]
args)



instance PrettyAnsi (Formula0 Term Formula) where
    prettyAnsi :: Formula0 Term (F Identity) -> Doc AnsiStyle
prettyAnsi = WithEnclosing (F Identity) -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (WithEnclosing (F Identity) -> Doc AnsiStyle)
-> (Formula0 Term (F Identity) -> WithEnclosing (F Identity))
-> Formula0 Term (F Identity)
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enclosing -> F Identity -> WithEnclosing (F Identity)
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing (F Identity -> WithEnclosing (F Identity))
-> (Formula0 Term (F Identity) -> F Identity)
-> Formula0 Term (F Identity)
-> WithEnclosing (F Identity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Formula0 Term (F Identity)) -> F Identity
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (Identity (Formula0 Term (F Identity)) -> F Identity)
-> (Formula0 Term (F Identity)
    -> Identity (Formula0 Term (F Identity)))
-> Formula0 Term (F Identity)
-> F Identity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 Term (F Identity) -> Identity (Formula0 Term (F Identity))
forall a. a -> Identity a
Identity

instance PrettyAnsi (Term0 Term) where
    prettyAnsi :: Term0 Term -> Doc AnsiStyle
prettyAnsi = WithEnclosing Term -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (WithEnclosing Term -> Doc AnsiStyle)
-> (Term0 Term -> WithEnclosing Term)
-> Term0 Term
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enclosing -> Term -> WithEnclosing Term
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing (Term -> WithEnclosing Term)
-> (Term0 Term -> Term) -> Term0 Term -> WithEnclosing Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Term0 Term) -> Term
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (Identity (Term0 Term) -> Term)
-> (Term0 Term -> Identity (Term0 Term)) -> Term0 Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 Term -> Identity (Term0 Term)
forall a. a -> Identity a
Identity

instance PrettyAnsi (WithEnclosing Formula) where
    prettyAnsi :: WithEnclosing (F Identity) -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
x (F (Identity Formula0 Term (F Identity)
y))) = WithEnclosing (Formula0 Term (F Identity)) -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (Enclosing
-> Formula0 Term (F Identity)
-> WithEnclosing (Formula0 Term (F Identity))
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
x Formula0 Term (F Identity)
y)

instance PrettyAnsi (WithEnclosing Term) where
    prettyAnsi :: WithEnclosing Term -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
x (T (Identity Term0 Term
y))) = WithEnclosing (Term0 Term) -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (Enclosing -> Term0 Term -> WithEnclosing (Term0 Term)
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
x Term0 Term
y)

deriving instance PrettyAnsi Formula
deriving instance PrettyAnsi Term
deriving instance PrettyAnsi a => PrettyAnsi (Identity a)

-- instance (Pretty f, Pretty t) => PrettyAnsi (Formula0 t f) where
--     pretty = pretty . WithEnclosing ""

-- instance (Pretty t) => Pretty (Term0 t) where
--     pretty = pretty . WithEnclosing ""

prettySimple :: PrettyAnsi a => a -> String
prettySimple :: forall a. PrettyAnsi a => a -> String
prettySimple a
x = Text -> String
TL.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ SimpleDocStream AnsiStyle -> Text
renderLazy (SimpleDocStream AnsiStyle -> Text)
-> SimpleDocStream AnsiStyle -> Text
forall a b. (a -> b) -> a -> b
$ LayoutOptions -> Doc AnsiStyle -> SimpleDocStream AnsiStyle
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutSmart LayoutOptions{ layoutPageWidth :: PageWidth
layoutPageWidth = Int -> Double -> PageWidth
AvailablePerLine Int
80 Double
0.9 } (Doc AnsiStyle -> SimpleDocStream AnsiStyle)
-> Doc AnsiStyle -> SimpleDocStream AnsiStyle
forall a b. (a -> b) -> a -> b
$ a -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi a
x


instance PrettyAnsi Annotations where
    prettyAnsi :: Annotations -> Doc AnsiStyle
prettyAnsi Annotations
NoAnnotations = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White) (Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ String
"NoAnnotations"
    prettyAnsi (Annotations GTerm
a UsefulInfo
b) = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White) (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"SourceInfo: ") Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GTerm -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi GTerm
a Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UsefulInfo -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi UsefulInfo
b

instance PrettyAnsi UsefulInfo where
    prettyAnsi :: UsefulInfo -> Doc AnsiStyle
prettyAnsi UsefulInfo
NoUsefulInfo = Doc AnsiStyle
forall a. Monoid a => a
mempty
    prettyAnsi (UsefulInfo [GTerm]
x) = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White) (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"UsefulInfo: ") Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [GTerm] -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi [GTerm]
x



instance PrettyAnsi GData where
    prettyAnsi :: GData -> Doc AnsiStyle
prettyAnsi (GWord AtomicWord
x) = AtomicWord -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomicWord -> Doc ann
pretty AtomicWord
x
    prettyAnsi (GNumber Rational
x) = Rational -> Doc AnsiStyle
forall ann. Rational -> Doc ann
prational Rational
x
    prettyAnsi (GDistinctObject String
x) = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Cyan) (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
dquotes (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
x))
    prettyAnsi (GApp AtomicWord
x []) = AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
fsym AtomicWord
x
    prettyAnsi (GApp AtomicWord
x [GTerm]
args) = AtomicWord -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
fsym AtomicWord
x Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [GTerm] -> Doc AnsiStyle
forall a. PrettyAnsi a => [a] -> Doc AnsiStyle
prettyargs [GTerm]
args
    prettyAnsi (GFormulaData String
s F Identity
f) = String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
s Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
align (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (F Identity -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi F Identity
f))
    prettyAnsi (GFormulaTerm String
s Term
t) = String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
s Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
align (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (Term -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi Term
t))
    prettyAnsi (GVar V
x) = V -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi V
x

instance Pretty AtomicWord where
    pretty :: forall ann. AtomicWord -> Doc ann
pretty (AtomicWord String
x) = (if String -> Bool
isLowerWord String
x then String -> Doc ann
forall ann. String -> Doc ann
text else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes(Doc ann -> Doc ann) -> (String -> Doc ann) -> String -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> Doc ann
forall ann. String -> Doc ann
text) String
x

instance PrettyAnsi GTerm where
    prettyAnsi :: GTerm -> Doc AnsiStyle
prettyAnsi (GTerm GData
x) = GData -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi GData
x
    prettyAnsi (ColonSep GData
x GTerm
y) = GData -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi GData
x Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc AnsiStyle
oper String
":" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GTerm -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi GTerm
y
    prettyAnsi (GList [GTerm]
xs) = let f :: String -> Doc AnsiStyle
f = String -> Doc AnsiStyle
oper
                            in
                              String -> Doc AnsiStyle
f String
"[" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ([Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
fillSep ([Doc AnsiStyle] -> Doc AnsiStyle)
-> ([GTerm] -> [Doc AnsiStyle]) -> [GTerm] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> [Doc AnsiStyle] -> [Doc AnsiStyle]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc AnsiStyle
forall ann. Doc ann
comma ([Doc AnsiStyle] -> [Doc AnsiStyle])
-> ([GTerm] -> [Doc AnsiStyle]) -> [GTerm] -> [Doc AnsiStyle]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GTerm -> Doc AnsiStyle) -> [GTerm] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GTerm -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi) [GTerm]
xs Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc AnsiStyle
f String
"]"



instance PrettyAnsi V where
    prettyAnsi :: V -> Doc AnsiStyle
prettyAnsi (V String
x) = AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Blue) (Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ String
x