diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/src/Data/TPTP.hs b/src/Data/TPTP.hs --- a/src/Data/TPTP.hs +++ b/src/Data/TPTP.hs @@ -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 diff --git a/src/Data/TPTP/Parse/Combinators.hs b/src/Data/TPTP/Parse/Combinators.hs --- a/src/Data/TPTP/Parse/Combinators.hs +++ b/src/Data/TPTP/Parse/Combinators.hs @@ -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)) diff --git a/src/Data/TPTP/Parse/Text.hs b/src/Data/TPTP/Parse/Text.hs --- a/src/Data/TPTP/Parse/Text.hs +++ b/src/Data/TPTP/Parse/Text.hs @@ -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 diff --git a/src/Data/TPTP/Parse/Text/Lazy.hs b/src/Data/TPTP/Parse/Text/Lazy.hs --- a/src/Data/TPTP/Parse/Text/Lazy.hs +++ b/src/Data/TPTP/Parse/Text/Lazy.hs @@ -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 diff --git a/src/Data/TPTP/Pretty.hs b/src/Data/TPTP/Pretty.hs --- a/src/Data/TPTP/Pretty.hs +++ b/src/Data/TPTP/Pretty.hs @@ -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 diff --git a/test-data/szs/fof/ski---Vampire.s b/test-data/szs/fof/ski---Vampire.s new file mode 100644 --- /dev/null +++ b/test-data/szs/fof/ski---Vampire.s @@ -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. + diff --git a/test/QuickCheckSpec/ArbitrarilyPretty.hs b/test/QuickCheckSpec/ArbitrarilyPretty.hs --- a/test/QuickCheckSpec/ArbitrarilyPretty.hs +++ b/test/QuickCheckSpec/ArbitrarilyPretty.hs @@ -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') diff --git a/test/QuickCheckSpec/Generators.hs b/test/QuickCheckSpec/Generators.hs --- a/test/QuickCheckSpec/Generators.hs +++ b/test/QuickCheckSpec/Generators.hs @@ -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 diff --git a/test/QuickCheckSpec/Main.hs b/test/QuickCheckSpec/Main.hs --- a/test/QuickCheckSpec/Main.hs +++ b/test/QuickCheckSpec/Main.hs @@ -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 diff --git a/test/QuickCheckSpec/Normalizers.hs b/test/QuickCheckSpec/Normalizers.hs --- a/test/QuickCheckSpec/Normalizers.hs +++ b/test/QuickCheckSpec/Normalizers.hs @@ -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 diff --git a/test/UnitTests.hs b/test/UnitTests.hs --- a/test/UnitTests.hs +++ b/test/UnitTests.hs @@ -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 diff --git a/tptp.cabal b/tptp.cabal --- a/tptp.cabal +++ b/tptp.cabal @@ -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: (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