{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.TPTP.Pretty (
Pretty(..)
) where
import Data.Char (isAsciiLower, isAsciiUpper, isDigit)
import Data.List (genericReplicate)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NEL (nonEmpty, toList)
import Data.Maybe (maybeToList)
import Data.Text (Text)
import qualified Data.Text as Text (all, head, tail, cons, snoc,
pack, singleton, replace)
#if __GLASGOW_HASKELL__ >= 803
import Prelude hiding ((<>))
#endif
import Data.TPTP
import Data.Text.Prettyprint.Doc (Doc, Pretty(..), hsep, sep, (<>), (<+>),
brackets, parens, punctuate, comma, space)
sepBy :: [Doc ann] -> Doc ann -> Doc ann
sepBy as s = hsep (punctuate s as)
sepBy1 :: NonEmpty (Doc ann) -> Doc ann -> Doc ann
sepBy1 as s = hsep (punctuate s (NEL.toList as))
application :: Pretty f => f -> [Doc ann] -> Doc ann
application f [] = pretty f
application f as = pretty f <> parens (as `sepBy` comma)
bracketList :: Pretty a => [a] -> Doc ann
bracketList as = brackets (fmap pretty as `sepBy` comma)
bracketList1 :: Pretty a => NonEmpty a -> Doc ann
bracketList1 as = brackets (fmap pretty as `sepBy1` comma)
quoted :: Char -> Text -> Text
quoted q = Text.cons q . flip Text.snoc q
. Text.replace (Text.singleton q) (Text.pack ['\\', q])
. Text.replace "\\" "\\\\"
newtype SingleQuoted = SingleQuoted Text
deriving (Eq, Show, Ord)
instance Pretty SingleQuoted where
pretty (SingleQuoted t) = pretty (quoted '\'' t)
instance Pretty Atom where
pretty (Atom s)
| isLowerWord s = pretty s
| otherwise = pretty (SingleQuoted s)
where
isLowerWord w = isAsciiLower (Text.head w)
&& Text.all isAlphaNum (Text.tail w)
isAlphaNum c = isAsciiLower c || isAsciiUpper c || isDigit c || c == '_'
instance Pretty Var where
pretty (Var s) = pretty s
newtype DoubleQuoted = DoubleQuoted Text
deriving (Eq, Show, Ord)
instance Pretty DoubleQuoted where
pretty (DoubleQuoted t) = pretty (quoted '"' t)
instance Pretty DistinctObject where
pretty (DistinctObject s) = pretty (DoubleQuoted s)
newtype DollarWord = DollarWord Text
deriving (Eq, Show, Ord)
instance Pretty DollarWord where
pretty (DollarWord w) = pretty (Text.cons '$' w)
tType :: DollarWord
tType = DollarWord "tType"
instance Named s => Pretty (Name s) where
pretty = \case
Reserved s -> pretty (DollarWord (name s))
Defined a -> pretty a
instance Named s => Named (Reserved s) where
name = \case
Standard s -> name s
Extended w -> w
instance Named s => Pretty (Reserved s) where
pretty = pretty . name
instance Pretty TFF1Sort where
pretty = \case
SortVariable v -> pretty v
TFF1Sort f ss -> application f (fmap pretty ss)
prettyMapping :: Pretty a => [a] -> a -> Doc ann
prettyMapping as r = args <> pretty r
where
args = case as of
[] -> mempty
[a] -> pretty a <+> ">" <> space
_ -> parens (fmap pretty as `sepBy` (space <> "*")) <+> ">" <> space
instance Pretty Type where
pretty = \case
Type as r -> prettyMapping as r
TFF1Type vs as r -> prefix <> if null as then matrix else parens matrix
where
prefix = case NEL.nonEmpty vs of
Nothing -> mempty
Just vs' -> "!>" <+> brackets (vars vs') <> ":" <> space
vars vs' = fmap prettyVar vs' `sepBy1` comma
prettyVar v = pretty v <> ":" <+> pretty tType
matrix = prettyMapping as r
instance Pretty Number where
pretty = \case
IntegerConstant i -> pretty i
RationalConstant n d -> pretty n <> "/" <> pretty d
RealConstant r -> pretty (show r)
instance Pretty Term where
pretty = \case
Function f ts -> application f (fmap pretty ts)
Variable v -> pretty v
Number i -> pretty i
DistinctTerm d -> pretty d
instance Pretty Literal where
pretty = \case
Predicate p ts -> application p (fmap pretty ts)
Equality a s b -> pretty a <+> pretty s <+> pretty b
instance Pretty Sign where
pretty = pretty . name
instance Pretty Clause where
pretty = \case
Clause ls -> fmap p ls `sepBy1` (space <> pretty Disjunction)
where
p (Positive, l) = pretty l
p (Negative, l) = "~" <+> parens (pretty l)
instance Pretty Quantifier where
pretty = pretty . name
instance Pretty Connective where
pretty = pretty . name
instance Pretty Unsorted where
pretty = mempty
instance Pretty s => Pretty (Sorted s) where
pretty = \case
Sorted Nothing -> mempty
Sorted (Just s) -> ":" <+> pretty s
instance Pretty QuantifiedSort where
pretty = const (pretty tType)
instance Pretty (Either QuantifiedSort TFF1Sort) where
pretty = either pretty pretty
unitary :: FirstOrder s -> Bool
unitary = \case
Atomic{} -> True
Negated{} -> True
Quantified{} -> True
Connected{} -> False
pretty' :: Pretty s => FirstOrder s -> Doc ann
pretty' f
| unitary f = pretty f
| otherwise = parens (pretty f)
instance Pretty s => Pretty (FirstOrder s) where
pretty = \case
Atomic l -> pretty l
Negated f -> "~" <+> pretty' f
Connected f c g -> pretty'' f <+> pretty c <+> pretty'' g
where
pretty'' e@(Connected _ c' _) | c' == c && isAssociative c = pretty e
pretty'' e = pretty' e
Quantified q vs f -> pretty q <+> vs' <> ":" <+> pretty' f
where
vs' = brackets (fmap var vs `sepBy1` comma)
var (v, s) = pretty v <> pretty s
instance Pretty Language where
pretty = pretty . name
instance Pretty Formula where
pretty = \case
CNF c -> pretty c
FOF f -> pretty f
TFF0 f -> pretty f
TFF1 f -> pretty f
instance Pretty UnitName where
pretty = either pretty pretty
prettyList = bracketList
instance Pretty Declaration where
pretty = \case
Formula _ f -> pretty f
Typing s t -> pretty s <> ":" <+> pretty t
Sort s n -> pretty s <> ":" <+> prettyMapping tTypes tType
where tTypes = genericReplicate n tType
instance Pretty Unit where
pretty = \case
Include (Atom f) ns -> application (Atom "include") args <> "."
where
args = pretty (SingleQuoted f) : maybeToList (fmap bracketList1 ns)
Unit nm decl a -> application (declarationLanguage decl) args <> "."
where
args = pretty nm : role : pretty decl : ann
role = case decl of
Sort{} -> "type"
Typing{} -> "type"
Formula r _ -> pretty (name r)
ann = case a of
Just (s, i) -> pretty s : maybeToList (fmap prettyList i)
Nothing -> []
prettyList us = sep (fmap pretty us)
instance Pretty TPTP where
pretty (TPTP us) = prettyList us
instance Pretty Intro where
pretty = pretty . name
instance Pretty Status where
pretty = pretty . name
instance Pretty (Either Var Atom) where
pretty = either pretty pretty
prettyList = bracketList
instance Pretty Info where
pretty = \case
Description a -> application (Atom "description") [pretty a]
Iquote a -> application (Atom "iquote") [pretty a]
Status s -> application (Atom "status") [pretty s]
Assumptions u -> application (Atom "assumptions") [bracketList1 u]
NewSymbols n ss -> application (Atom "new_symbols") [pretty n, prettyList ss]
Refutation a -> application (Atom "refutation") [pretty a]
Bind v e -> application (Atom "bind") [pretty v, pretty e]
Application f as -> application f (fmap pretty as)
Expression e -> pretty e
InfoNumber n -> pretty n
Infos is -> prettyList is
prettyList = bracketList
instance Pretty Expression where
pretty = \case
Logical f -> application (DollarWord . name $ formulaLanguage f) [pretty f]
Term t -> application (DollarWord "fot") [pretty t]
instance Pretty Parent where
pretty = \case
Parent s [] -> pretty s
Parent s gts -> pretty s <> ":" <> prettyList gts
prettyList = bracketList
instance Pretty Source where
pretty = \case
UnitSource un -> pretty un
UnknownSource -> "unknown"
File (Atom n) i -> source "file" (SingleQuoted n) (pretty <$> i)
Theory n i -> source "theory" n (prettyList <$> i)
Creator n i -> source "creator" n (prettyList <$> i)
Introduced n i -> source "introduced" n (prettyList <$> i)
Inference n i ps ->
application (Atom "inference") [pretty n, pretty i, prettyList ps]
where
source f n i = application (Atom f) (pretty n : maybeToList i)
prettyList = bracketList