tptp 0.1.2.0 → 0.1.3.0

raw patch · 13 files changed

+118/−27 lines, 13 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• src/Data/TPTP.hs +34/−7
• src/Data/TPTP/Parse/Combinators.hs +6/−3
• src/Data/TPTP/Parse/Text.hs +1/−1
• src/Data/TPTP/Parse/Text/Lazy.hs +1/−1
• src/Data/TPTP/Pretty.hs +1/−1
• test-data/szs/fof/ski---Vampire.s +37/−0
• test/QuickCheckSpec/ArbitrarilyPretty.hs +7/−4
• test/QuickCheckSpec/Generators.hs +1/−1
• test/QuickCheckSpec/Main.hs +14/−1
• test/QuickCheckSpec/Normalizers.hs +1/−1
• test/UnitTests.hs +1/−1
• tptp.cabal +6/−6

@@ -1,5 +1,13 @@ # Revision history for tptp +## 0.1.3.0 -- 2021-01-11++* Parse SZS comment annotations more liberally.++* Add functions 'sortFirstOrder', 'unsortFirstOrder', and 'polymorphizeFirstOrder'.++* Support compilation with GHC 8.8.4 and 8.10.3.+ ## 0.1.2.0 -- 2020-04-03  * Consume leading whitespace in the TSTP parser.

@@ -1,21 +1,25 @@-{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}+{-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ == 708+{-# LANGUAGE DeriveFunctor, DeriveFoldable #-}+#endif+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE CPP #-}  -- | -- Module       : Data.TPTP -- Description  : Data type definitions for the syntax of the TPTP language.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental --+-- The syntax of the TPTP language. -- See [the BNF grammar](http://tptp.cs.miami.edu/TPTP/SyntaxBNF.html)--- definition of the TPTP language for details.+-- definition of TPTP for details. --  module Data.TPTP (@@ -69,7 +73,10 @@   UnsortedFirstOrder,   SortedFirstOrder,   MonomorphicFirstOrder,+  sortFirstOrder,+  unsortFirstOrder,   PolymorphicFirstOrder,+  polymorphizeFirstOrder,   monomorphizeFirstOrder,    -- * Units@@ -655,6 +662,20 @@ -- | The formula in sorted monomorphic first-order logic. type MonomorphicFirstOrder = FirstOrder (Sorted (Name Sort)) +-- | Convert a formula in unsorted first-order logic to a formula in sorted+-- monomorphic first-order logic trivially by omitting the sort annotations+-- in all of its quantifiers. This function always succeeds.+sortFirstOrder :: UnsortedFirstOrder -> SortedFirstOrder+sortFirstOrder = fmap omit where omit _ = Sorted Nothing++-- | Attempt to erase the sort annotations in a sorted monomorphic first-order+-- formula. This function succeeds iff each of the quantifiers omits the sorts+-- of its variables.+unsortFirstOrder :: MonomorphicFirstOrder -> Maybe UnsortedFirstOrder+unsortFirstOrder = traverse $ \case+  Sorted Nothing -> Just (Unsorted ())+  Sorted Just{}  -> Nothing+ -- | The marker of quantified sort. newtype QuantifiedSort = QuantifiedSort ()   deriving (Eq, Show, Ord)@@ -662,12 +683,18 @@ -- | The formula in sorted polymorphic first-order logic. type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort)) +-- | Polymorphize a sorted monomorphic first-order formula.+-- This function always succeeds.+polymorphizeFirstOrder :: MonomorphicFirstOrder -> PolymorphicFirstOrder+polymorphizeFirstOrder = fmap (fmap polymorphize)+  where polymorphize s = Right (TFF1Sort s [])+ -- | Attempt to monomorphize a polymorphic sorted first-order formula. -- This function succeeds iff each of the quantifiers only uses sort--- constructors with zero arity.+-- constructors with zero arity and there are no quantified sorts. monomorphizeFirstOrder :: PolymorphicFirstOrder -> Maybe MonomorphicFirstOrder-monomorphizeFirstOrder = traverse . traverse-                       $ either (const Nothing) monomorphizeTFF1Sort+monomorphizeFirstOrder = traverse (traverse monomorphize)+  where monomorphize = either (const Nothing) monomorphizeTFF1Sort   -- * Units

@@ -7,7 +7,7 @@ -- | -- Module       : Data.TPTP.Parse.Combinators -- Description  : Parser combinators for the TPTP language.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental@@ -485,7 +485,10 @@ szs = fromMaybe mempty . mconcat <$> many szsComment  szsComment :: Parser (Maybe SZS)-szsComment =  commented (skipSpace *> optional szsAnnotation) <* skipSpace+szsComment =  commented (skipSpace *>+                         optional (skipBeginComment *> skipSpace) *>+                         optional szsAnnotation)+          <*  skipSpace           <?> "szs comment"  szsAnnotation :: Parser SZS@@ -535,7 +538,7 @@ infos = bracketList info <?> "infos" {-# INLINE infos #-} --- | Parse and expression+-- | Parse an expression. expr :: Parser Expression expr =  char '$' *> (labeled "fot" (Term <$> optionalParens term)                 <|>  Logical <$> (language >>= parens . optionalParens . formula))

@@ -1,7 +1,7 @@ -- | -- Module       : Data.TPTP.Parse.Text -- Description  : An attoparsec-based parser for the TPTP language.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental

@@ -1,7 +1,7 @@ -- | -- Module       : Data.TPTP.Parse.Text.Lazy -- Description  : An attoparsec-based parser for the TPTP language.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental

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

@@ -0,0 +1,37 @@+% SZS status CounterSatisfiable for +% # SZS output start Saturation.+tff(u47,axiom,+    trace(s,nil,bot)).++tff(u46,axiom,+    trace(i,nil,bot)).++tff(u45,axiom,+    (![X0] : (trace(ap(k,X0),nil,bot)))).++tff(u44,axiom,+    (![X0] : (trace(ap(s,X0),nil,bot)))).++tff(u43,axiom,+    (![X1, X0] : (trace(ap(ap(s,X0),X1),nil,bot)))).++tff(u42,axiom,+    trace(k,nil,bot)).++tff(u41,axiom,+    (![X0] : (trace(ap(i,X0),nil,X0)))).++tff(u40,axiom,+    (![X1, X0] : (trace(ap(ap(k,X0),X1),nil,X0)))).++tff(u39,axiom,+    (![X1, X0, X2] : (trace(ap(ap(ap(s,X0),X1),X2),nil,ap(ap(X0,X2),ap(X1,X2)))))).++tff(u38,negated_conjecture,+    trace(ap(ap(ap(s,i),i),k),sK0,bot)).++tff(u37,axiom,+    (![X1, X3, X0, X2] : ((trace(X0,cons(X1,X3),X2) | ~trace(X1,nil,X2) | ~trace(X0,X3,X1))))).++% # SZS output end Saturation.+

@@ -1,15 +1,18 @@-{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}+{-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ == 708+{-# LANGUAGE DeriveFunctor, DeriveFoldable #-}+#endif+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE CPP #-}  -- | -- Module       : ArbitrarilyPretty -- Description  : Generators for randomized pretty outputs of TPTP expressions.--- Copyright    : (c) Evgenii Kotelnikov, 2020+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental@@ -295,7 +298,7 @@     Type        as r -> sppretty (Mapping as r)     TFF1Type [] as r -> sppretty (Mapping as r)     TFF1Type vs as r -> do-      vs' <- mapM sppretty (fmap (flip Typing_ tType) vs)+      vs' <- mapM sppretty (fmap (`Typing_` tType) vs)       t' <- sppretty (Prefix colon (ParensUnless (null as) (TFF1Type [] as r)))       return ("!>" <+> brackets (hsep (punctuate comma vs')) <> t') 

@@ -7,7 +7,7 @@ -- | -- Module       : Generators -- Description  : QuickCheck generators for datatypes in the tptp library.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental

@@ -8,7 +8,7 @@ -- | -- Module       : Main -- Description  : QuickCheck specification for the tptp library.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental@@ -100,7 +100,11 @@        => Parser e -> e -> Property spAipp = spAippModulo defaultNormalize +-- | Idempotent encoding / decoding.+(~=) :: (Eq a, Show a) => (a -> b) -> (b -> Maybe a) -> a -> Property+(~=) to from a = Just a === from (to a) + -- * Properties  -- ** Generators@@ -232,6 +236,15 @@  prop_ipp_Info :: Info -> Property prop_ipp_Info = ippModulo normalizeInfo info+++-- ** Conversions++prop_unsortFirstOrder :: UnsortedFirstOrder -> Property+prop_unsortFirstOrder = sortFirstOrder ~= unsortFirstOrder++prop_monomorphizeFirstOrder :: MonomorphicFirstOrder -> Property+prop_monomorphizeFirstOrder = polymorphizeFirstOrder ~= monomorphizeFirstOrder   -- * Runner

@@ -3,7 +3,7 @@ -- | -- Module       : Normalizers -- Description  : Normalization of the Data.TPTP datatypes.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental

@@ -6,7 +6,7 @@ -- | -- Module       : UnitTests -- Description  : Run the TPTP parser on selected examples from the TPTP World.--- Copyright    : (c) Evgenii Kotelnikov, 2019+-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021 -- License      : GPL-3 -- Maintainer   : evgeny.kotelnikov@gmail.com -- Stability    : experimental

@@ -1,6 +1,6 @@ cabal-version: 2.4 name: tptp-version: 0.1.2.0+version: 0.1.3.0 synopsis: Parser and pretty printer for the TPTP language description:   <http://www.tptp.org TPTP> (Thousands of Problems for Theorem Provers)@@ -25,8 +25,8 @@   GHC == 8.2.2,   GHC == 8.4.4,   GHC == 8.6.5,-  GHC == 8.8.3,-  GHC == 8.10.1+  GHC == 8.8.4,+  GHC == 8.10.3  extra-source-files:   CHANGELOG.md@@ -75,7 +75,7 @@       -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns       -Wredundant-constraints -test-suite quickcheck-spec+test-suite quickcheck   type: exitcode-stdio-1.0   hs-source-dirs: test/QuickCheckSpec   default-language: Haskell2010@@ -104,7 +104,7 @@     build-depends:       bifunctors   >= 3.0.1   && < 6 -test-suite unit-tests+test-suite unit   type: detailed-0.9   hs-source-dirs: test   default-language: Haskell2010@@ -126,7 +126,7 @@     filepath  >= 1.3   && < 1.5,     tptp -test-suite doctests+test-suite doctest   type: exitcode-stdio-1.0   hs-source-dirs: test/DocTests   default-language: Haskell2010