logic-TPTP 0.5.1.0 → 0.6.0.0

raw patch · 14 files changed

+202/−235 lines, 14 filesdep +prettyprinterdep +prettyprinter-ansi-terminaldep +textdep −ansi-wl-pprintdep −transformers-compatdep ~basedep ~pcre-lightdep ~transformersPVP ok

version bump matches the API change (PVP)

Dependencies added: prettyprinter, prettyprinter-ansi-terminal, text

Dependencies removed: ansi-wl-pprint, transformers-compat

Dependency ranges changed: base, pcre-light, transformers

API changes (from Hackage documentation)

Files

• Codec/TPTP/Base.hs +10/−43
• Codec/TPTP/Diff.hs +41/−38
• Codec/TPTP/Export.hs +1/−1
• Codec/TPTP/Pretty.hs +111/−93
• Codec/TPTP/QuickCheck.hs +1/−2
• ParserC.y +3/−3
• Util.hs +0/−23
• changelog.markdown +5/−0
• logic-TPTP.cabal +15/−19
• testing/Common.hs +7/−7
• testing/ParseRandom.hs +0/−1
• testing/PrettyPrintFile.hs +0/−1
• testing/SimpleArgs.hs +1/−1
• testing/TestImportExportImportFile.hs +7/−3

@@ -2,24 +2,16 @@   , StandaloneDeriving   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving-  , OverlappingInstances, ScopedTypeVariables+  , ScopedTypeVariables   #-}  module Codec.TPTP.Base where -#ifndef MIN_VERSION_transformers-#define MIN_VERSION_transformers(a,b,c) 1-#endif-#ifndef MIN_VERSION_base-#define MIN_VERSION_base(a,b,c) 1-#endif--- Assume we are using the newest versions when using ghci without cabal- import Codec.TPTP.QuickCheck import Control.Applicative import Control.Monad import Control.Monad.Identity-import Control.Monad.State+import Control.Monad.Writer (Writer, runWriter) import Data.Data import Data.Function import Data.Monoid hiding(All)@@ -30,14 +22,7 @@ import Test.QuickCheck hiding ((.&.)) import Data.Pointed import Data.Copointed-#if !MIN_VERSION_transformers(0,4,0)-import Control.Monad.Trans.Instances () -- Import Eq,Ord,Show,Read,Data,Typeable orphan instances for Data.Functor.Identity from transformers-compat package-#endif -#if !MIN_VERSION_base(4,7,0)-import Util-#endif- -- * Basic undecorated formulae and terms  -- | Basic (undecorated) first-order formulae@@ -49,21 +34,21 @@ -- * Formulae and terms decorated with state  -- | First-order formulae decorated with state-type FormulaST s = F (State s)+type FormulaW s = F (Writer s)  -- | Terms decorated with state-type TermST s = T (State s)+type TermW s = T (Writer s)  -- | First-order formulae decorated with comments-type FormulaC = FormulaST [String]+type FormulaC = FormulaW [String]  -- | Terms decorated with comments-type TermC = TermST [String]+type TermC = TermW [String]  -- | Forget comments in formulae decorated with comments forgetFC :: FormulaC -> Formula forgetFC (F f) = F . return $-  case evalState f [] of+  case fst $ runWriter f of     BinOp f1 op f2       -> BinOp (forgetFC f1) op (forgetFC f2)     InfixPred t1 pred_ t2 -> InfixPred (forgetTC t1) pred_ (forgetTC t2)     PredApp aw ts        -> PredApp aw (fmap forgetTC ts)@@ -73,7 +58,7 @@ -- | Forget comments in terms decorated with comments forgetTC :: TermC -> Term forgetTC (T t) = T . return $-  case evalState t [] of+  case fst $ runWriter t of     Var v -> Var v     NumberLitTerm d -> NumberLitTerm d     DistinctObjectTerm s -> DistinctObjectTerm s@@ -231,8 +216,8 @@     deriving (Eq,Ord,Show,Read,Data,Typeable) -} --- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement-type TPTP_Input_C = TPTP_Input_ (State [String])+-- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the Writer monad ), comment or include statement+type TPTP_Input_C = TPTP_Input_ (Writer [String])  -- | Forget comments in a line of a TPTP file decorated with comments forgetTIC :: TPTP_Input_C -> TPTP_Input@@ -258,15 +243,8 @@ deriving instance Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) deriving instance Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) --#if MIN_VERSION_base(4,7,0) deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) deriving instance Typeable TPTP_Input_-#else-deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)-instance Typeable1 c => Typeable (TPTP_Input_ c) where-  typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "TPTP_Input_"-#endif  -- | Annotations about the formulas origin data Annotations = NoAnnotations | Annotations GTerm UsefulInfo@@ -607,22 +585,11 @@ DI(Show) DI(Read) -#if MIN_VERSION_base(4,7,0) deriving instance Typeable F deriving instance Typeable T  deriving instance (Typeable c, Data (c (Term0 (T c)))) => Data (T c) deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c)-#else-instance Typeable1 c => Typeable (F c) where-    typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "F"--instance Typeable1 c => Typeable (T c) where-    typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "T"--deriving instance (Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)-deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)-#endif  -- * Utility functions 

@@ -1,8 +1,8 @@-{-# LANGUAGE CPP, NoMonomorphismRestriction, RecordWildCards+{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards   , StandaloneDeriving, MultiParamTypeClasses, FunctionalDependencies   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving-  , OverlappingInstances, OverloadedStrings, RankNTypes+  , OverloadedStrings, RankNTypes   #-} {-# OPTIONS -Wall #-} @@ -11,19 +11,20 @@  -- Warning: This module is a MESS (but it seems to work :)). -#if MIN_VERSION_base(4,8,0) import Prelude hiding ((<$>))-#endif  import Data.Generics import Test.QuickCheck hiding((.&.)) import Codec.TPTP.Base import Codec.TPTP.Pretty-import Text.PrettyPrint.ANSI.Leijen+import Prettyprinter+import Prettyprinter.Render.Terminal import Control.Monad import Control.Monad.Identity  +text :: String -> Doc ann+text = pretty   data DiffResult d =@@ -197,10 +198,10 @@       _ -> let plug=plugSubformulae (T DontCare) (F DontCare) in Differ (plug f1) (plug f2)  -instance Show (T DiffResult) where+instance {-# OVERLAPPING #-} Show (T DiffResult) where     show (T t) = show t -instance Show (F DiffResult) where+instance {-# OVERLAPPING #-} Show (F DiffResult) where     show (F f) = show f  type T0Diff = DiffResult (Term0 (T DiffResult))@@ -210,55 +211,55 @@ wildcard :: AtomicWord wildcard = "_" -instance Pretty (WithEnclosing T0Diff) where-    pretty = prettyHelper --(plugSubterms (fApp wildcard []))+instance PrettyAnsi (WithEnclosing T0Diff) where+    prettyAnsi = prettyHelper --(plugSubterms (fApp wildcard [])) -instance Pretty (WithEnclosing F0Diff) where-    pretty = prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard []))+instance PrettyAnsi (WithEnclosing F0Diff) where+    prettyAnsi = prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard []))  prettyHelper :: forall t.-                (Pretty (WithEnclosing t)) =>-                WithEnclosing (DiffResult t) -> Doc+                (PrettyAnsi (WithEnclosing t)) =>+                WithEnclosing (DiffResult t) -> Doc AnsiStyle prettyHelper (WithEnclosing _ d) =         let-            pwe = pretty . WithEnclosing EnclNothing+            pwe = prettyAnsi . WithEnclosing EnclNothing         in           case d of-                 DontCare -> dullwhite.pretty $ wildcard-                 Same -> dullgreen.text $ "Same"-                 SameHead x -> blue . encloseSep (text "{ SameHead ") (text "}") semi $+                 DontCare -> annotate (colorDull White).pretty $ wildcard+                 Same -> annotate (colorDull Green).text $ "Same"+                 SameHead x -> annotate (color Blue) . encloseSep (text "{ SameHead ") (text "}") semi $                               [  pwe x                               ]   -                 Differ x y -> red . encloseSep (text "{ Differ ") rbrace (text "; ") $+                 Differ x y -> annotate (color Red) . encloseSep (text "{ Differ ") rbrace (text "; ") $                                [ pwe x                               , pwe y                               ] -deriving instance Pretty (T DiffResult)+deriving instance PrettyAnsi (T DiffResult) -deriving instance Pretty (F DiffResult)+deriving instance PrettyAnsi (F DiffResult) -instance Pretty (WithEnclosing (T DiffResult)) where-    pretty (WithEnclosing x (T y)) = pretty (WithEnclosing x y)+instance PrettyAnsi (WithEnclosing (T DiffResult)) where+    prettyAnsi (WithEnclosing x (T y)) = prettyAnsi (WithEnclosing x y) -instance Pretty (WithEnclosing (F DiffResult)) where-    pretty (WithEnclosing x (F y)) = pretty (WithEnclosing x y)+instance PrettyAnsi (WithEnclosing (F DiffResult)) where+    prettyAnsi (WithEnclosing x (F y)) = prettyAnsi (WithEnclosing x y) -instance Pretty (T0Diff) where-    pretty = pretty . WithEnclosing EnclNothing+instance PrettyAnsi (T0Diff) where+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing -instance Pretty (F0Diff) where-    pretty = pretty . WithEnclosing EnclNothing+instance PrettyAnsi (F0Diff) where+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing --- instance Pretty (DiffResult (T DiffResult)) where---     pretty = pretty . WithEnclosing EnclNothing . T+-- instance PrettyAnsi (DiffResult (T DiffResult)) where+--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . T --- instance Pretty (DiffResult (T DiffResult) (F DiffResult)) where---     pretty = pretty . WithEnclosing EnclNothing . F+-- instance PrettyAnsi (DiffResult (T DiffResult) (F DiffResult)) where+--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . F   -- runFormulaDiff :: Formula@@ -300,12 +301,14 @@   xs <- sample' diffGenF   ys <- sample' diffGenF -  let item x y = text (replicate 50 '=')-                 <$> pretty x-                 <$> text (replicate 40 '-')-                 <$> pretty y-                 <$> text (replicate 40 '-')-                 <$> pretty (diffFormula x y)+  let item x y = vsep+                 [ text (replicate 50 '=')+                 , prettyAnsi x+                 , text (replicate 40 '-')+                 , prettyAnsi y+                 , text (replicate 40 '-')+                 , prettyAnsi (diffFormula x y)+                 ]    mapM_ (putStrLn . prettySimple . uncurry item) (zip xs ys) 

@@ -2,7 +2,7 @@   , StandaloneDeriving   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving-  , OverlappingInstances, RankNTypes+  , RankNTypes   #-} {-# OPTIONS -Wall #-} module Codec.TPTP.Export(toTPTP',ToTPTP(..),isLowerWord) where

@@ -1,49 +1,63 @@-{-# LANGUAGE CPP, NoMonomorphismRestriction, RecordWildCards+{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards   , StandaloneDeriving   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving-  , OverlappingInstances, RankNTypes, PatternGuards+  , RankNTypes, PatternGuards   #-}  {-# OPTIONS -Wall -fno-warn-orphans #-}  -- | Mainly just 'Pretty' instances-module Codec.TPTP.Pretty(prettySimple,WithEnclosing(..),Enclosing(..)) where+module Codec.TPTP.Pretty(PrettyAnsi(..),prettySimple,WithEnclosing(..),Enclosing(..)) where -#if MIN_VERSION_base(4,8,0) import Prelude hiding ((<$>))-#endif  import Codec.TPTP.Base import Codec.TPTP.Export-import Text.PrettyPrint.ANSI.Leijen+import Prettyprinter+import Prettyprinter.Render.Terminal import Data.Data import Control.Monad.Identity import Data.Ratio+import qualified Data.Text.Lazy as TL -oper :: String -> Doc-oper = dullyellow . text-psym :: forall a. (Pretty a) => a -> Doc-psym = green . pretty-fsym :: forall a. (Pretty a) => a -> Doc-fsym = yellow . pretty+class PrettyAnsi a where+  prettyAnsi :: a -> Doc AnsiStyle+  prettyAnsiList :: [a] -> Doc AnsiStyle+  prettyAnsiList = align . list . map prettyAnsi +instance PrettyAnsi (Doc AnsiStyle) where+  prettyAnsi = id++instance PrettyAnsi a => PrettyAnsi [a] where+  prettyAnsi = prettyAnsiList++oper :: String -> Doc AnsiStyle+oper = annotate (colorDull Yellow) . text+psym :: forall a. (Pretty a) => a -> Doc AnsiStyle+psym = annotate (color Green) . pretty+fsym :: forall a. (Pretty a) => a -> Doc AnsiStyle+fsym = annotate (color Yellow) . pretty++text :: String -> Doc ann+text = pretty+ --wtext :: String -> Doc---wtext = white . text+--wtext = annotate (color White) . text -prettyargs :: forall a. (Pretty a) => [a] -> Doc+prettyargs :: forall a. (PrettyAnsi a) => [a] -> Doc AnsiStyle --prettyargs = encloseSep (wtext "(") (wtext ")") (wtext ",") . fmap pretty-prettyargs = tupled . fmap pretty--- prettyargs [] = white $ text "()"+prettyargs = tupled . fmap prettyAnsi+-- prettyargs [] = annotate (color White) $ text "()" -- prettyargs (x:xs) =---     let pxs = fmap ((white (text ",") <+>) . pretty) xs in+--     let pxs = fmap ((annotate (color White) (text ",") <+>) . pretty) xs in ---     align (fillSep $ [    white (text "(") <+> pretty x ]+--     align (fillSep $ [    annotate (color White) (text "(") <+> pretty x ] --                     ++ pxs---                     ++ [ white (text ")") ] )+--                     ++ [ annotate (color White) (text ")") ] ) -prational :: Rational -> Doc-prational q = (text.show.numerator) q <> char '/' <> (text.show.denominator) q+prational :: Rational -> Doc ann+prational q = (text.show.numerator) q <> pretty '/' <> (text.show.denominator) q  -- | Carries information about the enclosing operation (for the purpose of printing stuff without parentheses if possible). data WithEnclosing a = WithEnclosing Enclosing a@@ -87,36 +101,37 @@                EnclNothing -> (-1000) -- if there's no enclosing operation, we don't need parentheses  -maybeParens :: Enclosing -> Enclosing -> Doc -> Doc+maybeParens :: Enclosing -> Enclosing -> Doc ann -> Doc ann maybeParens inner outer | needsParens inner outer = parens maybeParens _ _ = id -instance Pretty TPTP_Input where-    pretty AFormula{..}-        = (text) "Formula " <+> (dullwhite.text) "name:"-          </>-          vsep-          [-            (red.pretty) name <+> dullwhite (text "role:") <+> (magenta.text.unrole) role-          , pretty formula-          , pretty annotations-          ,empty+instance PrettyAnsi TPTP_Input where+    prettyAnsi AFormula{..}+        = fillSep+          [ (text) "Formula " <+> (annotate (colorDull White).text) "name:"+          , vsep+            [+              (annotate (color Red).pretty) name <+> annotate (colorDull White) (text "role:") <+> (annotate (color Magenta).text.unrole) role+            , prettyAnsi formula+            , prettyAnsi annotations+            , mempty+            ]           ] -    pretty (Comment str)-        = magenta . string $ str+    prettyAnsi (Comment str)+        = annotate (color Magenta) . pretty $ str -    pretty (Include f sel) = text "include" <> parens (squotes (text f) <> (case sel of { [] -> empty; _ -> comma <+> sep (punctuate comma (fmap pretty sel)) } ))+    prettyAnsi (Include f sel) = text "include" <> parens (squotes (text f) <> (case sel of { [] -> mempty; _ -> comma <+> sep (punctuate comma (fmap pretty sel)) } ))  -    prettyList = foldr (\x xs -> pretty x <$> xs) empty+    prettyAnsiList = foldr (\x xs -> vsep [prettyAnsi x, xs]) mempty -instance Pretty Quant where-    pretty All = oper "∀"-    pretty Exists = oper "∃"+instance PrettyAnsi Quant where+    prettyAnsi All = oper "∀"+    prettyAnsi Exists = oper "∃" -instance (Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty ((WithEnclosing (Formula0 t f))) where-    pretty (WithEnclosing enclosing formu) =+instance (PrettyAnsi (WithEnclosing t), PrettyAnsi (WithEnclosing f)) => PrettyAnsi ((WithEnclosing (Formula0 t f))) where+    prettyAnsi (WithEnclosing enclosing formu) =         let             newEnclosing =              case formu of@@ -134,25 +149,27 @@           case formu of              Quant q vars f ->-               pretty q-               <+> brackets (hsep (punctuate comma (fmap pretty vars)))-               <> dot-               </> pretty (wne f)+               fillSep+               [ prettyAnsi q+                 <+> brackets (hsep (punctuate comma (fmap prettyAnsi vars)))+                 <> dot+               , prettyAnsi (wne f)+               ] -            (:~:) f -> oper "¬" <+> pretty (wne f)+            (:~:) f -> oper "¬" <+> prettyAnsi (wne f)              PredApp p [] -> psym p             PredApp p args -> psym p <> prettyargs (fmap wne args)               BinOp f1 op f2 ->-                align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]+                align $ sep [indent 0 $ prettyAnsi (wne f1), prettyAnsi op, indent 0 $ prettyAnsi (wne f2)]              InfixPred f1 op f2 ->-                align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]+                align $ sep [indent 0 $ prettyAnsi (wne f1), prettyAnsi op, indent 0 $ prettyAnsi (wne f2)] -instance Pretty BinOp where-    pretty x = case x of+instance PrettyAnsi BinOp where+    prettyAnsi x = case x of         (:<=>:) -> oper "⇔"         (:=>:)  -> oper "⇒"         (:<=:)  -> oper "⇐"@@ -162,78 +179,79 @@         (:~|:)  -> oper "NOR"         (:<~>:) -> oper "XOR" -instance Pretty InfixPred where-    pretty x = case x of+instance PrettyAnsi InfixPred where+    prettyAnsi x = case x of         (:=:)   -> oper "="         (:!=:)  -> oper "≠" -instance (Pretty (WithEnclosing t)) => Pretty (WithEnclosing (Term0 t)) where-    pretty (WithEnclosing _ x) =+instance (PrettyAnsi (WithEnclosing t)) => PrettyAnsi (WithEnclosing (Term0 t)) where+    prettyAnsi (WithEnclosing _ x) =         case x of-          Var s -> pretty s+          Var s -> prettyAnsi s           NumberLitTerm d -> prational d-          DistinctObjectTerm s -> cyan (dquotes (text s))+          DistinctObjectTerm s -> annotate (color Cyan) (dquotes (text s))           FunApp f [] -> fsym f           FunApp f args -> fsym f <> prettyargs (fmap (WithEnclosing EnclNothing) args)   -instance Pretty (Formula0 Term Formula) where-    pretty = pretty . WithEnclosing EnclNothing . F . Identity+instance PrettyAnsi (Formula0 Term Formula) where+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . F . Identity -instance Pretty (Term0 Term) where-    pretty = pretty . WithEnclosing EnclNothing . T . Identity+instance PrettyAnsi (Term0 Term) where+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . T . Identity -instance Pretty (WithEnclosing Formula) where-    pretty (WithEnclosing x (F (Identity y))) = pretty (WithEnclosing x y)+instance PrettyAnsi (WithEnclosing Formula) where+    prettyAnsi (WithEnclosing x (F (Identity y))) = prettyAnsi (WithEnclosing x y) -instance Pretty (WithEnclosing Term) where-    pretty (WithEnclosing x (T (Identity y))) = pretty (WithEnclosing x y)+instance PrettyAnsi (WithEnclosing Term) where+    prettyAnsi (WithEnclosing x (T (Identity y))) = prettyAnsi (WithEnclosing x y) -deriving instance Pretty Formula-deriving instance Pretty Term-deriving instance Pretty a => Pretty (Identity a)+deriving instance PrettyAnsi Formula+deriving instance PrettyAnsi Term+deriving instance PrettyAnsi a => PrettyAnsi (Identity a) --- instance (Pretty f, Pretty t) => Pretty (Formula0 t f) where+-- instance (Pretty f, Pretty t) => PrettyAnsi (Formula0 t f) where --     pretty = pretty . WithEnclosing ""  -- instance (Pretty t) => Pretty (Term0 t) where --     pretty = pretty . WithEnclosing "" -prettySimple :: Pretty a => a -> String-prettySimple x = displayS (renderPretty 0.9 80 (pretty x)) ""+prettySimple :: PrettyAnsi a => a -> String+prettySimple x = TL.unpack $ renderLazy $ layoutSmart LayoutOptions{ layoutPageWidth = AvailablePerLine 80 0.9 } $ prettyAnsi x -instance Pretty Annotations where-    pretty NoAnnotations = dullwhite . text $ "NoAnnotations"-    pretty (Annotations a b) = dullwhite (text "SourceInfo: ") <+> pretty a <+> pretty b -instance Pretty UsefulInfo where-    pretty NoUsefulInfo = empty-    pretty (UsefulInfo x) = dullwhite (text "UsefulInfo: ") <+> pretty x+instance PrettyAnsi Annotations where+    prettyAnsi NoAnnotations = annotate (colorDull White) . text $ "NoAnnotations"+    prettyAnsi (Annotations a b) = annotate (colorDull White) (text "SourceInfo: ") <+> prettyAnsi a <+> prettyAnsi b +instance PrettyAnsi UsefulInfo where+    prettyAnsi NoUsefulInfo = mempty+    prettyAnsi (UsefulInfo x) = annotate (colorDull White) (text "UsefulInfo: ") <+> prettyAnsi x  -instance Pretty GData where-    pretty (GWord x) = pretty x-    pretty (GNumber x) = prational x-    pretty (GDistinctObject x) = cyan (dquotes (text x))-    pretty (GApp x []) = fsym x-    pretty (GApp x args) = fsym x <+> prettyargs args-    pretty (GFormulaData s f) = text s <> align (parens (pretty f))-    pretty (GFormulaTerm s t) = text s <> align (parens (pretty t))-    pretty (GVar x) = pretty x +instance PrettyAnsi GData where+    prettyAnsi (GWord x) = pretty x+    prettyAnsi (GNumber x) = prational x+    prettyAnsi (GDistinctObject x) = annotate (color Cyan) (dquotes (text x))+    prettyAnsi (GApp x []) = fsym x+    prettyAnsi (GApp x args) = fsym x <+> prettyargs args+    prettyAnsi (GFormulaData s f) = text s <> align (parens (prettyAnsi f))+    prettyAnsi (GFormulaTerm s t) = text s <> align (parens (prettyAnsi t))+    prettyAnsi (GVar x) = prettyAnsi x+ instance Pretty AtomicWord where     pretty (AtomicWord x) = (if isLowerWord x then text else squotes.text) x -instance Pretty GTerm where-    pretty (GTerm x) = pretty x-    pretty (ColonSep x y) = pretty x <+> oper ":" <+> pretty y-    pretty (GList xs) = let f = oper-                        in-                          f "[" <+> (fillSep . punctuate comma . fmap pretty) xs <+> f "]"+instance PrettyAnsi GTerm where+    prettyAnsi (GTerm x) = prettyAnsi x+    prettyAnsi (ColonSep x y) = prettyAnsi x <+> oper ":" <+> prettyAnsi y+    prettyAnsi (GList xs) = let f = oper+                            in+                              f "[" <+> (fillSep . punctuate comma . fmap prettyAnsi) xs <+> f "]"   -instance Pretty V where-    pretty (V x) = blue . text $ x+instance PrettyAnsi V where+    prettyAnsi (V x) = annotate (color Blue) . text $ x

@@ -2,14 +2,13 @@   , StandaloneDeriving   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving-  , OverlappingInstances, RankNTypes, PatternGuards+  , RankNTypes, PatternGuards   #-} {-# OPTIONS -Wall #-} module Codec.TPTP.QuickCheck where  import Test.QuickCheck import Control.Monad-import Control.Applicative import Data.Char import Data.Array.ST import Data.Array.IArray

@@ -12,7 +12,7 @@ import System.IO import System.IO.Unsafe import Control.Monad.Identity-import Control.Monad.State+import Control.Monad.Writer }  %name parseTPTPwithComment@@ -505,8 +505,8 @@ instance Commented Identity where   withComments = const -instance Commented (State [String]) where-  withComments (F mf) s = F $ do { f <- mf; put s; return f }+instance Commented (Writer [String]) where+  withComments (F mf) s = F $ do { f <- mf; tell s; return f }   stripQuotes which (x:xs) = go xs

@@ -6,26 +6,3 @@ #ifndef MIN_VERSION_base #define MIN_VERSION_base(X,Y,Z) 1 #endif--#if !MIN_VERSION_base(4,7,0)-import Data.Typeable--#if ! MIN_VERSION_base(4,4,0)-mkTyCon3 _ m t = mkTyCon $ m++"."++t-#endif--packageName :: String-packageName = "logic-TPTP"----- | Gets the TypeRep of @c@ (not of @c ()@)-getTyRep1 :: forall c. Typeable1 c => c () -> TypeRep-getTyRep1 _ = mkTyConApp (typeRepTyCon (typeOf1 (undefined :: c ()))) []---mkTypeOfForRank2Kind :: forall x c. Typeable1 c => String -> String -> x c -> TypeRep-mkTypeOfForRank2Kind moduleName typeName = const tr-    where-        tc = mkTyCon3 packageName moduleName typeName-        tr = mkTyConApp tc [getTyRep1 (undefined :: c ())]-#endif

@@ -1,3 +1,8 @@+## 0.6.0.0++* Migrate to `prettyprinter` package family from `ansi-wl-pprint` package+* Use `Writer` moand instead of `State` to annotate comments+ ## 0.5.1.0  * Fix compilation error with `mtl >=2.3`

@@ -1,5 +1,5 @@ name: logic-TPTP-version: 0.5.1.0+version: 0.6.0.0 cabal-version: >= 1.10 build-type: Simple license: GPL@@ -8,7 +8,7 @@ bug-reports: http://github.com/DanielSchuessler/logic-TPTP/issues synopsis: Import, export etc. for TPTP, a syntax for first-order logic description:- For information about the TPTP format, see <http://www.cs.miami.edu/~tptp/>.+ For information about the TPTP format, see <https://www.tptp.org/>.  .  Components:  .@@ -60,17 +60,18 @@ Library  ghc-options: -Wall -O2 - build-depends:      base >=4 && < 5+ build-depends:      base >=4.8.0.0 && < 5                    , array                    , syb                    , containers-                   , ansi-wl-pprint < 1.0+                   , prettyprinter >=1.2.1.1 && <1.8+                   , prettyprinter-ansi-terminal >=1.0 && <1.2+                   , text                    , QuickCheck >= 2                    , mtl                    , pointed                    , semigroups-                   , transformers-                   , transformers-compat >= 0.5+                   , transformers >= 0.5   exposed-modules:   Codec.TPTP.Import                   , Codec.TPTP.Base@@ -97,12 +98,11 @@  hs-source-dirs:    testing  build-depends:     logic-TPTP                   , base-                  , ansi-wl-pprint+                  , prettyprinter+                  , prettyprinter-ansi-terminal                   , optparse-applicative >=0.11 && <0.19                   , pcre-light                   , semigroups- if impl(ghc <7.10)-  build-depends:    pcre-light <0.4.1  default-language:  Haskell2010  other-extensions:  CPP  if !flag(BuildTestPrograms)@@ -115,14 +115,12 @@  hs-source-dirs:    testing  build-depends:     logic-TPTP                   , base-                  , ansi-wl-pprint+                  , prettyprinter+                  , prettyprinter-ansi-terminal                   , pcre-light                   , QuickCheck                   , semigroups                   , transformers-                  , transformers-compat >= 0.5- if impl(ghc <7.10)-  build-depends:    pcre-light <0.4.1  default-language:  Haskell2010  other-extensions:  CPP @@ -132,7 +130,8 @@                   , SimpleArgs  hs-source-dirs:    testing  build-depends:     logic-TPTP-                  , ansi-wl-pprint+                  , prettyprinter+                  , prettyprinter-ansi-terminal                   , base                   , bytestring                   , containers@@ -142,8 +141,6 @@                   , QuickCheck                   , semigroups                   , syb- if impl(ghc <7.10)-  build-depends:    pcre-light <0.4.1  default-language:  Haskell2010  other-extensions:  CPP  if !flag(BuildTestPrograms)@@ -155,7 +152,8 @@                   , SimpleArgs  hs-source-dirs:    testing  build-depends:     logic-TPTP-                  , ansi-wl-pprint+                  , prettyprinter+                  , prettyprinter-ansi-terminal                   , base                   , bytestring                   , containers@@ -165,8 +163,6 @@                   , QuickCheck                   , semigroups                   , syb- if impl(ghc <7.10)-  build-depends:    pcre-light <0.4.1  default-language:  Haskell2010  other-extensions:  CPP  if !flag(BuildTestPrograms)

@@ -4,9 +4,9 @@  module Common where -import Data.Monoid import qualified Data.Semigroup as Semigroup-import Text.PrettyPrint.ANSI.Leijen+import Prettyprinter+import Prettyprinter.Render.Terminal import Text.Regex.PCRE.Light.Char8 import Codec.TPTP @@ -28,14 +28,14 @@     mappend = (Semigroup.<>) #endif -instance Pretty AFormulaComparison where-    pretty (OtherSame) = dullgreen.text$"OtherSame"-    pretty (OtherDiff x y) = sep-                             [dullred.text$"OtherDiff"+instance PrettyAnsi AFormulaComparison where+    prettyAnsi (OtherSame) = annotate (colorDull Green).pretty$"OtherSame"+    prettyAnsi (OtherDiff x y) = sep+                             [annotate (colorDull Red).pretty$"OtherDiff"                              ,pretty x                              ,pretty y                              ]-    pretty (FormulaDiff fd) = pretty fd+    prettyAnsi (FormulaDiff fd) = prettyAnsi fd  compareOther ::  (Eq a, Show a) => a -> a -> AFormulaComparison compareOther x y = if x==y then OtherSame else OtherDiff (show x) (show y)

@@ -18,7 +18,6 @@ import Data.Generics import Test.QuickCheck import Data.Monoid-import Text.PrettyPrint.ANSI.Leijen import System.Exit import Text.Regex.PCRE.Light.Char8 import Common

@@ -19,7 +19,6 @@ import Data.Generics import Test.QuickCheck import Data.Monoid-import Text.PrettyPrint.ANSI.Leijen import System.Exit import Text.Regex.PCRE.Light.Char8 

@@ -1,4 +1,4 @@-{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}  -- Copied and modified from https://hackage.haskell.org/package/simpleargs-0.2.1 -- which is licensed under GNU LESSER GENERAL PUBLIC LICENSE Version 2.1

@@ -3,7 +3,8 @@  import Control.Monad import Data.Monoid-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))+import Prettyprinter+import Prettyprinter.Render.Terminal import System.Exit import Common import Options.Applicative@@ -49,7 +50,7 @@   case findUnsupportedFormulaType input of      Just x -> do        unless print_failure_only $ -         putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)+         putStrLn . prettySimple . annotate (color Yellow) . text $ ("Skipping unsupported formula type "++x)      Nothing -> do        let once = parse input@@ -58,7 +59,7 @@         putStrLn $ "new tptp = " ++tptp       let twice = parse tptp       let dif = mconcat (zipWith diffAFormula once twice)-      let success = (putStrLn . prettySimple . dullgreen . text $ "Ok")+      let success = (putStrLn . prettySimple . annotate (colorDull Green) . text $ "Ok")        -- case dif of       --   OtherSame -> success@@ -74,3 +75,6 @@            when print_failure_only $ putStrLn infilename'            putStrLn . prettySimple $ dif            exitWith (ExitFailure 1)++text :: String -> Doc ann+text = pretty