tptp 0.1.1.0 → 0.1.2.0
raw patch · 15 files changed
+862/−155 lines, 15 filesdep +filepathdep ~basedep ~scientificdep ~semigroupsPVP ok
version bump matches the API change (PVP)
Dependencies added: filepath
Dependency ranges changed: base, scientific, semigroups
API changes (from Hackage documentation)
+ Data.TPTP: instance GHC.Base.Monoid Data.TPTP.DistinctObject
+ Data.TPTP: instance GHC.Base.Monoid Data.TPTP.TPTP
+ Data.TPTP: instance GHC.Base.Semigroup Data.TPTP.Atom
+ Data.TPTP: instance GHC.Base.Semigroup Data.TPTP.Clause
+ Data.TPTP: instance GHC.Base.Semigroup Data.TPTP.DistinctObject
+ Data.TPTP: instance GHC.Base.Semigroup Data.TPTP.TPTP
+ Data.TPTP: instance GHC.Base.Semigroup Data.TPTP.Var
+ Data.TPTP: unitClause :: (Sign, Literal) -> Clause
Files
- CHANGELOG.md +16/−0
- src/Data/TPTP.hs +80/−42
- src/Data/TPTP/Parse/Combinators.hs +42/−29
- src/Data/TPTP/Pretty.hs +38/−36
- test-data/szs/fof/group-theory---E.s +25/−0
- test-data/szs/fof/group-theory---Vampire.s +97/−0
- test-data/szs/fof/syllogism---E.s +17/−0
- test-data/szs/fof/syllogism---Vampire.s +37/−0
- test-data/tptp/fof/group-theory.p +5/−0
- test-data/tptp/fof/syllogism.p +3/−0
- test/QuickCheckSpec/ArbitrarilyPretty.hs +333/−0
- test/QuickCheckSpec/Generators.hs +1/−1
- test/QuickCheckSpec/Main.hs +111/−16
- test/UnitTests.hs +47/−24
- tptp.cabal +10/−7
CHANGELOG.md view
@@ -1,5 +1,21 @@ # Revision history for tptp +## 0.1.2.0 -- 2020-04-03++* Consume leading whitespace in the TSTP parser.++* Do not pretty print parenthesis in negated equality literals.++* Parse superfluous parenthesis in types, terms and clauses.++* Add a helper function 'unitClause'.++* Add more tests and improve documentation.++* Set more accurate lower bounds of the base and scientific dependencies.++* Support compilation with GHC 8.8.3 and 8.10.1.+ ## 0.1.1.0 -- 2019-12-07 * Parse SZS ontology information in the TSTP input.
src/Data/TPTP.hs view
@@ -56,6 +56,7 @@ Literal(..), Sign(..), Clause(..),+ unitClause, clause, Quantifier(..), Connective(..),@@ -106,10 +107,15 @@ import Data.Text (Text) #if !MIN_VERSION_base(4, 8, 0)+import Data.Monoid (Monoid(..)) import Data.Foldable (Foldable) import Data.Traversable (Traversable, traverse) #endif +#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif+ -- $setup -- >>> :set -XOverloadedStrings -- >>> :load Data.TPTP.Pretty@@ -158,6 +164,9 @@ newtype Atom = Atom Text deriving (Eq, Show, Ord, IsString) +instance Semigroup Atom where+ Atom t <> Atom s = Atom (t <> s)+ -- | Check whether a given character is in the ASCII range 0x20 to 0x7E. isAsciiPrint :: Char -> Bool isAsciiPrint c = isAscii c && isPrint c@@ -184,6 +193,9 @@ newtype Var = Var Text deriving (Eq, Show, Ord, IsString) +instance Semigroup Var where+ Var v <> Var w = Var (v <> w)+ -- | Check whether a given character matches the regular expression -- @[a-zA-Z0-9_]@. isAlphaNumeric :: Char -> Bool@@ -229,6 +241,13 @@ newtype DistinctObject = DistinctObject Text deriving (Eq, Show, Ord, IsString) +instance Semigroup DistinctObject where+ DistinctObject d <> DistinctObject b = DistinctObject (d <> b)++instance Monoid DistinctObject where+ mempty = DistinctObject mempty+ mappend = (<>)+ -- | Check whether a given string is a valid distinct object. -- -- >>> isValidDistinctObject ""@@ -312,25 +331,26 @@ -- | The standard function symbol in TPTP. -- Represents an operation in a first-order theory of arithmetic.+-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details. data Function- = Uminus- | Sum- | Difference- | Product- | Quotient- | QuotientE- | QuotientT- | QuotientF- | RemainderE- | RemainderT- | RemainderF- | Floor- | Ceiling- | Truncate- | Round- | ToInt- | ToRat- | ToReal+ = Uminus -- ^ @$uminus@ - Unary minus of a number.+ | Sum -- ^ @$sum@ - Sum of two numbers.+ | Difference -- ^ @$difference@ - Difference between two numbers.+ | Product -- ^ @$product@ - Product of two numbers.+ | Quotient -- ^ @$quotient@ - Exact quotient of two @$rat@ or @$real@ numbers.+ | QuotientE -- ^ @$quotient_e@ - Integral quotient of two numbers.+ | QuotientT -- ^ @$quotient_t@ - Integral quotient of two numbers.+ | QuotientF -- ^ @$quotient_f@ - Integral quotient of two numbers.+ | RemainderE -- ^ @$remainder_e@ - Remainder after integral division of two numbers.+ | RemainderT -- ^ @$remainder_t@ - Remainder after integral division of two numbers.+ | RemainderF -- ^ @$remainder_f@ - Remainder after integral division of two numbers.+ | Floor -- ^ @$floor@ - Floor of a number.+ | Ceiling -- ^ @$ceiling@ - Ceiling of a number.+ | Truncate -- ^ @$truncate@ - Truncation of a number.+ | Round -- ^ @$round@ - Rounding of a number.+ | ToInt -- ^ @$to_int@ - Coercion of a number to @$int@.+ | ToRat -- ^ @$to_rat@ - Coercion of a number to @$rat@.+ | ToReal -- ^ @$to_real@ - Coercion of a number to @$real@. deriving (Eq, Show, Ord, Enum, Bounded) instance Named Function where@@ -355,16 +375,17 @@ ToReal -> "to_real" -- | The standard predicate symbol in TPTP.+-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details. data Predicate- = Tautology- | Falsum- | Distinct- | Less- | Lesseq- | Greater- | Greatereq- | IsInt- | IsRat+ = Tautology -- ^ @$true@ - Logical tautology.+ | Falsum -- ^ @$false@ - Logical falsum.+ | Distinct -- ^ @$distinct@ - Denotes that its arguments are unequal to each other.+ | Less -- ^ @$less@ - Less-than comparison of two numbers.+ | Lesseq -- ^ @$lesseq@ - Less-than-or-equal-to comparison of two numbers.+ | Greater -- ^ @$greater@ - Greater-than comparison of two numbers.+ | Greatereq -- ^ @$greatereq@ - Greater-than-or-equal-to comparison of two numbers.+ | IsInt -- ^ @$is_nat@ - Test for coincidence with an integer.+ | IsRat -- ^ @$is_rat@ - Test for coincidence with a rational. deriving (Eq, Show, Ord, Enum, Bounded) instance Named Predicate where@@ -406,11 +427,11 @@ -- | The standard sort in TPTP. data Sort- = I -- ^ The sort of individuals.- | O -- ^ The sort of booleans.- | Int -- ^ The sort of integers.- | Real -- ^ The sort of real numbers.- | Rat -- ^ The sort of rational numbers.+ = I -- ^ @$i@ - The sort of individuals.+ | O -- ^ @$o@ - The sort of booleans.+ | Int -- ^ @$int@ - The sort of integers.+ | Real -- ^ @$real@ - The sort of real numbers.+ | Rat -- ^ @$rat@ - The sort of rational numbers. deriving (Eq, Show, Ord, Enum, Bounded) instance Named Sort where@@ -459,7 +480,10 @@ -- | A smart constructor of a TFF1 type. 'tff1Type' constructs a TFF0 type with -- its arguments, if it is possible, and otherwise constructs a TFF1 type.-tff1Type :: [Var] -> [TFF1Sort] -> TFF1Sort -> Type+tff1Type :: [Var] -- ^ Quantified type variables.+ -> [TFF1Sort] -- ^ Sort arguments.+ -> TFF1Sort -- ^ Return sort.+ -> Type tff1Type [] ss s | Just ss' <- traverse monomorphizeTFF1Sort ss , Just s' <- monomorphizeTFF1Sort s = Type ss' s'@@ -523,13 +547,20 @@ newtype Clause = Clause (NonEmpty (Sign, Literal)) deriving (Eq, Show, Ord) +instance Semigroup Clause where+ Clause ls <> Clause ks = Clause (ls <> ks)++-- | Construct a unit clause from a given signed literal.+unitClause :: (Sign, Literal) -> Clause+unitClause l = Clause (l :| [])+ -- | A smart constructor for 'Clause'. 'clause' constructs a clause from a -- possibly empty list of signed literals. If the provided list is empty, -- the unit clause @$false@ is constructed instead. clause :: [(Sign, Literal)] -> Clause clause ls | Just ls' <- nonEmpty ls = Clause ls'- | otherwise = Clause ((Positive, falsum) :| [])+ | otherwise = unitClause (Positive, falsum) where falsum = Predicate (Reserved (Standard Falsum)) [] @@ -546,14 +577,14 @@ -- | The connective in full first-order logic. data Connective- = Conjunction- | Disjunction- | Implication- | Equivalence- | ExclusiveOr- | NegatedConjunction- | NegatedDisjunction- | ReversedImplication+ = Conjunction -- ^ @&@.+ | Disjunction -- ^ @|@.+ | Implication -- ^ @=>@.+ | Equivalence -- ^ @<=>@.+ | ExclusiveOr -- ^ @<~>@ - XOR.+ | NegatedConjunction -- ^ @~&@ - NAND.+ | NegatedDisjunction -- ^ @~|@ - NOR.+ | ReversedImplication -- ^ @<=@. deriving (Eq, Show, Ord, Enum, Bounded) -- | Check associativity of a given connective.@@ -727,6 +758,13 @@ newtype TPTP = TPTP { units :: [Unit] } deriving (Eq, Show, Ord)++instance Semigroup TPTP where+ TPTP us <> TPTP ys = TPTP (us <> ys)++instance Monoid TPTP where+ mempty = TPTP mempty+ mappend = (<>) -- | The TSTP output - zero or more TSTP units, possibly annotated with the -- status of the proof search and the resulting dataform.
src/Data/TPTP/Parse/Combinators.hs view
@@ -1,5 +1,6 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE CPP #-} @@ -68,7 +69,9 @@ import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NEL (fromList, toList) #if !MIN_VERSION_base(4, 11, 0)-import Data.Semigroup (Semigroup(..))+import Data.Semigroup (Semigroup(..), sconcat)+#else+import Data.Semigroup (sconcat) #endif import qualified Data.Scientific as Sci (base10Exponent, coefficient)@@ -153,7 +156,7 @@ {-# INLINE parens #-} optionalParens :: Parser a -> Parser a-optionalParens p = parens p <|> p+optionalParens p = p <|> parens (optionalParens p) {-# INLINE optionalParens #-} brackets :: Parser a -> Parser a@@ -170,7 +173,7 @@ {-# INLINE bracketList1 #-} application :: Parser f -> Parser a -> Parser (f, [a])-application f a = (,) <$> f <*> option [] (parens (a `sepBy1` op ','))+application f a = (,) <$> f <*> option [] (parens (optionalParens a `sepBy1` op ',')) {-# INLINE application #-} labeled :: Text -> Parser a -> Parser a@@ -280,8 +283,8 @@ <?> "type" where prefix = token "!>" *> bracketList1 sortVar <* op ':'- sortVar = var <* op ':' <* token "$tType"- matrix = optionalParens (mapping tff1Sort)+ sortVar = var <* op ':' <* optionalParens (token "$tType")+ matrix = optionalParens (mapping (optionalParens tff1Sort)) -- ** First-order logic@@ -297,41 +300,50 @@ | otherwise = RealConstant n -- | Parse a term.+--+-- @term@ supports parsing superfluous parenthesis around arguments+-- of the function application, which are not present in the TPTP grammar. term :: Parser Term-term = parens term- <|> uncurry Function <$> application function term+term = uncurry Function <$> application function term <|> Variable <$> var <|> Number <$> number <|> DistinctTerm <$> distinctObject <?> "term" --- | Parse the equality and the unequality sign.+-- | Parse the equality and the inequality sign. eq :: Parser Sign eq = enum <?> "eq" {-# INLINE eq #-} -- | Parse a literal.+--+-- @literal@ supports parsing superfluous parenthesis around arguments+-- of the predicate application, which are not present in the TPTP grammar. literal :: Parser Literal-literal = parens literal- <|> Equality <$> term <*> eq <*> term+literal = Equality <$> optionalParens term <*> eq <*> optionalParens term <|> uncurry Predicate <$> application predicate term <?> "literal" --- | Parse the negation sign.-sign :: Parser Sign-sign = option Positive (op '~' $> Negative)-{-# INLINE sign #-}- -- | Parse a signed literal.+--+-- @signedLiteral@ supports parsing superfluous parenthesis around the literal+-- under the negation sign, which are not present in the TPTP grammar. signedLiteral :: Parser (Sign, Literal)-signedLiteral = (,) <$> sign <*> literal <?> "signed literal"+signedLiteral = fmap (Negative,) (op '~' *> optionalParens literal)+ <|> fmap (Positive,) literal+ <?> "signed literal" {-# INLINE signedLiteral #-} -- | Parse a clause.+--+-- @clause@ supports parsing superfluous parenthesis around any of the+-- subclauses of the clause, which are not present in the TPTP grammar. clause :: Parser Clause-clause = parens clause- <|> Clause . NEL.fromList <$> signedLiteral `sepBy1` op '|'- <?> "clause"+clause = sconcat . NEL.fromList <$> subclause `sepBy1` op '|'+ where+ subclause = unitClause <$> signedLiteral+ <|> parens clause+ <?> "subclause" -- | Parse a quantifier. quantifier :: Parser Quantifier@@ -349,10 +361,10 @@ f <- unitary option f (Connected f <$> connective <*> firstOrder p) where- unitary = parens (firstOrder p)- <|> Atomic <$> literal- <|> Quantified <$> quantifier <*> vs <* op ':' <*> unitary+ unitary = Atomic <$> literal <|> Negated <$> (op '~' *> unitary)+ <|> Quantified <$> quantifier <*> vs <* op ':' <*> unitary+ <|> parens (firstOrder p) <?> "unitary first order" vs = bracketList1 $ (,) <$> var <*> p@@ -363,7 +375,7 @@ where unsorted = pure (Unsorted ()) <?> "unsorted" sorted :: Parser s -> Parser (Sorted s)-sorted s = Sorted <$> optional (op ':' *> s) <?> "sorted"+sorted s = Sorted <$> optional (op ':' *> optionalParens s) <?> "sorted" -- | An alias for 'monomorphicFirstOrder'. sortedFirstOrder :: Parser SortedFirstOrder@@ -414,11 +426,11 @@ -- | Parse a declaration with the @type@ role - either a typing relation or -- a sort declaration. typeDeclaration :: Parser Declaration-typeDeclaration = Sort <$> atom <* op ':' <*> arity- <|> Typing <$> atom <* op ':' <*> type_+typeDeclaration = Sort <$> atom <* op ':' <*> optionalParens arity+ <|> Typing <$> atom <* op ':' <*> optionalParens type_ <?> "type declaration" where- arity = genericLength . fst <$> mapping (token "$tType")+ arity = genericLength . fst <$> mapping (optionalParens (token "$tType")) -- | Parse a unit name. unitName :: Parser (Either Atom Integer)@@ -455,7 +467,8 @@ -- | Parse a TSTP input. tstp :: Parser TSTP-tstp = TSTP <$> szs <*> manyTill unit endOfInput <* endOfInput <?> "tstp"+tstp = skipSpace *> (TSTP <$> szs <*> manyTill unit endOfInput) <* endOfInput+ <?> "tstp" -- ** Annotations@@ -524,8 +537,8 @@ -- | Parse and expression expr :: Parser Expression-expr = char '$' *> (labeled "fot" (Term <$> term)- <|> Logical <$> (language >>= parens . formula))+expr = char '$' *> (labeled "fot" (Term <$> optionalParens term)+ <|> Logical <$> (language >>= parens . optionalParens . formula)) <?> "expression" -- | Parse a parent.
src/Data/TPTP/Pretty.hs view
@@ -18,6 +18,7 @@ ) where #if !MIN_VERSION_base(4, 8, 0)+import Data.Foldable (Foldable) import Data.Functor ((<$>)) import Data.Monoid (mempty) #endif@@ -27,9 +28,9 @@ #endif 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 qualified Data.Foldable as Foldable (toList)+import Data.List (genericReplicate, intersperse)+import qualified Data.List.NonEmpty as NEL (nonEmpty) import Data.Maybe (maybeToList) import Data.Text (Text) import qualified Data.Text as Text (@@ -37,7 +38,7 @@ ) import Data.Text.Prettyprint.Doc ( Doc, Pretty(..),- hsep, sep, (<+>), brackets, parens, punctuate, comma, space, line+ hsep, sep, (<+>), parens, brackets, punctuate, space, comma, line ) import Data.TPTP@@ -48,21 +49,18 @@ comment :: Doc ann -> Doc ann comment c = "%" <+> c <> line -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))+sepBy :: Foldable f => f (Doc ann) -> Doc ann -> Doc ann+sepBy as s = hsep (intersperse s (Foldable.toList as)) application :: Pretty f => f -> [Doc ann] -> Doc ann application f [] = pretty f-application f as = pretty f <> parens (as `sepBy` comma)+application f as = pretty f <> parens (hsep (punctuate comma as)) -bracketList :: Pretty a => [a] -> Doc ann-bracketList as = brackets (fmap pretty as `sepBy` comma)+list :: Foldable f => f (Doc ann) -> Doc ann+list = brackets . hsep . punctuate comma . Foldable.toList -bracketList1 :: Pretty a => NonEmpty a -> Doc ann-bracketList1 as = brackets (fmap pretty as `sepBy1` comma)+bracketList :: (Pretty a, Functor f, Foldable f) => f a -> Doc ann+bracketList = list . fmap pretty -- * Names@@ -135,7 +133,7 @@ args = case as of [] -> mempty [a] -> pretty a <+> ">" <> space- _ -> parens (fmap pretty as `sepBy` (space <> "*")) <+> ">" <> space+ _ -> parens (fmap pretty as `sepBy` "*") <+> ">" <> space instance Pretty Type where pretty = \case@@ -143,9 +141,8 @@ 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+ Nothing -> mempty+ Just{} -> "!>" <+> list (fmap prettyVar vs) <> ":" <> space prettyVar v = pretty v <> ":" <+> pretty tType matrix = prettyMapping as r @@ -175,10 +172,15 @@ instance Pretty Clause where pretty = \case- Clause ls -> fmap p ls `sepBy1` (space <> pretty Disjunction)+ Clause ls -> fmap p ls `sepBy` pretty Disjunction where p (Positive, l) = pretty l- p (Negative, l) = "~" <+> parens (pretty l)+ -- TPTP v7.3.0.0 doesn't allow for wrapping atom in parentesis in+ -- a negated atom in CNF formulas. I.e. for example ~ (X = Y) is+ -- not allowed. See http://www.tptp.org/TPTP/SyntaxBNF.html#cnf_formula+ -- TODO: implement AB-test comparing this parser against some canonical+ -- implementation of the parser of TPTP BNF (like tptp4X).+ p (Negative, l) = "~" <+> pretty l instance Pretty Quantifier where pretty = pretty . name@@ -207,24 +209,24 @@ Quantified{} -> True Connected{} -> False -pretty' :: Pretty s => FirstOrder s -> Doc ann-pretty' f- | unitary f = pretty f- | otherwise = parens (pretty f)+ppretty :: Pretty s => (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann+ppretty skipParens f+ | skipParens f = pretty f+ | otherwise = parens (pretty f) +under :: Connective -> FirstOrder s -> Bool+under c = \case+ Connected _ c' _ -> c' == c && isAssociative c+ f -> unitary 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- -- Nested applications of associative connectives do not require- -- parenthesis. Otherwise, the connectives do not have precedence- pretty'' e@(Connected _ c' _) | c' == c && isAssociative c = pretty e- pretty'' e = pretty' e- Quantified q vs f -> pretty q <+> vs' <> ":" <+> pretty' f+ Negated f -> "~" <+> ppretty unitary f+ Connected f c g -> ppretty (under c) f <+> pretty c <+> ppretty (under c) g+ Quantified q vs f -> pretty q <+> list vs' <> ":" <+> ppretty unitary f where- vs' = brackets (fmap var vs `sepBy1` comma)+ vs' = fmap var (Foldable.toList vs) var (v, s) = pretty v <> pretty s @@ -255,7 +257,7 @@ pretty = \case Include (Atom f) ns -> application (Atom "include") args <> "." where- args = pretty (SingleQuoted f) : maybeToList (fmap bracketList1 ns)+ args = pretty (SingleQuoted f) : maybeToList (fmap bracketList ns) Unit nm decl a -> application (declarationLanguage decl) args <> "." where args = pretty nm : role : pretty decl : ann@@ -286,7 +288,7 @@ dataform p = case d of Nothing -> p Just df -> szsComment ["output", "start", pretty df]- <> p+ <> p <> line <> szsComment ["output", "end", pretty df] @@ -316,7 +318,7 @@ 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]+ Assumptions u -> application (Atom "assumptions") [bracketList 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]
+ test-data/szs/fof/group-theory---E.s view
@@ -0,0 +1,25 @@++# Proof found!+# SZS status Theorem+# SZS output start CNFRefutation+fof(3, axiom, ![X3, X1, X2]:mult(mult(X3,X1),X2)=mult(X3,mult(X1,X2)), file('<stdin>', 3)).+fof(4, axiom, ![X2]:mult(X2,X2)=e, file('<stdin>', 4)).+fof(1, axiom, ![X2]:mult(e,X2)=X2, file('<stdin>', 1)).+fof(0, conjecture, ![X1, X2]:mult(X1,X2)=mult(X2,X1), file('<stdin>', 0)).+fof(c_0_4, plain, ![X8, X9, X10]:mult(mult(X8,X9),X10)=mult(X8,mult(X9,X10)), inference(variable_rename,[status(thm)],[3])).+fof(c_0_5, plain, ![X11]:mult(X11,X11)=e, inference(variable_rename,[status(thm)],[4])).+fof(c_0_6, plain, ![X6]:mult(e,X6)=X6, inference(variable_rename,[status(thm)],[1])).+cnf(c_0_7, plain, (mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_4])).+cnf(c_0_8, plain, (mult(X1,X1)=e), inference(split_conjunct,[status(thm)],[c_0_5])).+cnf(c_0_9, plain, (mult(e,X1)=X1), inference(split_conjunct,[status(thm)],[c_0_6])).+cnf(c_0_10, plain, (mult(X1,mult(X1,X2))=X2), inference(rw,[status(thm)],[inference(pm,[status(thm)],[c_0_7, c_0_8]), c_0_9])).+fof(c_0_11, negated_conjecture, ~(![X1, X2]:mult(X1,X2)=mult(X2,X1)), inference(assume_negation,[status(cth)],[0])).+cnf(c_0_12, plain, (mult(X1,mult(X2,mult(X1,X2)))=e), inference(pm,[status(thm)],[c_0_8, c_0_7])).+cnf(c_0_13, plain, (mult(X1,e)=X1), inference(pm,[status(thm)],[c_0_10, c_0_8])).+fof(c_0_14, negated_conjecture, mult(esk1_0,esk2_0)!=mult(esk2_0,esk1_0), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).+cnf(c_0_15, plain, (mult(X1,mult(X2,X1))=X2), inference(rw,[status(thm)],[inference(pm,[status(thm)],[c_0_10, c_0_12]), c_0_13])).+cnf(c_0_16, negated_conjecture, (mult(esk1_0,esk2_0)!=mult(esk2_0,esk1_0)), inference(split_conjunct,[status(thm)],[c_0_14])).+cnf(c_0_17, plain, (mult(X1,X2)=mult(X2,X1)), inference(pm,[status(thm)],[c_0_10, c_0_15])).+cnf(c_0_18, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])]), ['proof']).+# SZS output end CNFRefutation+# Training examples: 0 positive, 0 negative
+ test-data/szs/fof/group-theory---Vampire.s view
@@ -0,0 +1,97 @@+% Refutation found. Thanks to Tanya!+% SZS status Theorem for +% SZS output start Proof for +fof(f276,plain,(+ $false),+ inference(trivial_inequality_removal,[],[f275])).+fof(f275,plain,(+ mult(sK0,sK1) != mult(sK0,sK1)),+ inference(superposition,[],[f16,f131])).+fof(f131,plain,(+ ( ! [X2,X3] : (mult(X2,X3) = mult(X3,X2)) )),+ inference(superposition,[],[f27,f96])).+fof(f96,plain,(+ ( ! [X4,X3] : (mult(X4,mult(X3,X4)) = X3) )),+ inference(forward_demodulation,[],[f81,f33])).+fof(f33,plain,(+ ( ! [X2] : (mult(inverse(X2),e) = X2) )),+ inference(superposition,[],[f27,f18])).+fof(f18,plain,(+ ( ! [X0] : (e = mult(inverse(X0),X0)) )),+ inference(cnf_transformation,[],[f9])).+fof(f9,plain,(+ ! [X0] : e = mult(inverse(X0),X0)),+ inference(rectify,[],[f4])).+fof(f4,axiom,(+ ! [X1] : e = mult(inverse(X1),X1)),+ file(unknown,unknown)).+fof(f81,plain,(+ ( ! [X4,X3] : (mult(X4,mult(X3,X4)) = mult(inverse(X3),e)) )),+ inference(superposition,[],[f28,f25])).+fof(f25,plain,(+ ( ! [X0,X1] : (e = mult(X0,mult(X1,mult(X0,X1)))) )),+ inference(superposition,[],[f19,f20])).+fof(f20,plain,(+ ( ! [X0] : (e = mult(X0,X0)) )),+ inference(cnf_transformation,[],[f12])).+fof(f12,plain,(+ ! [X0] : e = mult(X0,X0)),+ inference(rectify,[],[f6])).+fof(f6,axiom,(+ ! [X1] : e = mult(X1,X1)),+ file(unknown,unknown)).+fof(f19,plain,(+ ( ! [X2,X0,X1] : (mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))) )),+ inference(cnf_transformation,[],[f11])).+fof(f11,plain,(+ ! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))),+ inference(flattening,[],[f10])).+fof(f10,plain,(+ ! [X0] : ! [X1] : ! [X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))),+ inference(rectify,[],[f5])).+fof(f5,axiom,(+ ! [X2] : ! [X0] : ! [X1] : mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1))),+ file(unknown,unknown)).+fof(f28,plain,(+ ( ! [X4,X5] : (mult(inverse(X4),mult(X4,X5)) = X5) )),+ inference(forward_demodulation,[],[f23,f17])).+fof(f17,plain,(+ ( ! [X0] : (mult(e,X0) = X0) )),+ inference(cnf_transformation,[],[f8])).+fof(f8,plain,(+ ! [X0] : mult(e,X0) = X0),+ inference(rectify,[],[f3])).+fof(f3,axiom,(+ ! [X1] : mult(e,X1) = X1),+ file(unknown,unknown)).+fof(f23,plain,(+ ( ! [X4,X5] : (mult(inverse(X4),mult(X4,X5)) = mult(e,X5)) )),+ inference(superposition,[],[f19,f18])).+fof(f27,plain,(+ ( ! [X2,X3] : (mult(X2,mult(X2,X3)) = X3) )),+ inference(forward_demodulation,[],[f22,f17])).+fof(f22,plain,(+ ( ! [X2,X3] : (mult(X2,mult(X2,X3)) = mult(e,X3)) )),+ inference(superposition,[],[f19,f20])).+fof(f16,plain,(+ mult(sK0,sK1) != mult(sK1,sK0)),+ inference(cnf_transformation,[],[f15])).+fof(f15,plain,(+ mult(sK0,sK1) != mult(sK1,sK0)),+ inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f13,f14])).+fof(f14,plain,(+ ? [X0,X1] : mult(X0,X1) != mult(X1,X0) => mult(sK0,sK1) != mult(sK1,sK0)),+ introduced(choice_axiom,[])).+fof(f13,plain,(+ ? [X0,X1] : mult(X0,X1) != mult(X1,X0)),+ inference(ennf_transformation,[],[f7])).+fof(f7,plain,(+ ~! [X0,X1] : mult(X0,X1) = mult(X1,X0)),+ inference(flattening,[],[f2])).+fof(f2,negated_conjecture,(+ ~! [X0] : ! [X1] : mult(X0,X1) = mult(X1,X0)),+ inference(negated_conjecture,[],[f1])).+fof(f1,conjecture,(+ ! [X0] : ! [X1] : mult(X0,X1) = mult(X1,X0)),+ file(unknown,unknown)).+% SZS output end Proof for
+ test-data/szs/fof/syllogism---E.s view
@@ -0,0 +1,17 @@++# Proof found!+# SZS status Theorem+# SZS output start CNFRefutation+fof(0, conjecture, mortal(socrates), file('<stdin>', 0)).+fof(1, axiom, ![X1]:(human(X1)=>mortal(X1)), file('<stdin>', 1)).+fof(2, axiom, human(socrates), file('<stdin>', 2)).+fof(c_0_3, negated_conjecture, ~(mortal(socrates)), inference(assume_negation,[status(cth)],[0])).+fof(c_0_4, plain, ![X2]:(~human(X2)|mortal(X2)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[1])])).+fof(c_0_5, negated_conjecture, ~mortal(socrates), inference(fof_simplification,[status(thm)],[c_0_3])).+cnf(c_0_6, plain, (mortal(X1)|~human(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).+cnf(c_0_7, plain, (human(socrates)), inference(split_conjunct,[status(thm)],[2])).+cnf(c_0_8, negated_conjecture, (~mortal(socrates)), inference(split_conjunct,[status(thm)],[c_0_5])).+cnf(c_0_9, plain, (mortal(socrates)), inference(pm,[status(thm)],[c_0_6, c_0_7])).+cnf(c_0_10, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_8, c_0_9])]), ['proof']).+# SZS output end CNFRefutation+# Training examples: 0 positive, 0 negative
+ test-data/szs/fof/syllogism---Vampire.s view
@@ -0,0 +1,37 @@+% Refutation found. Thanks to Tanya!+% SZS status Theorem for +% SZS output start Proof for +fof(f11,plain,(+ $false),+ inference(subsumption_resolution,[],[f10,f7])).+fof(f7,plain,(+ ~mortal(socrates)),+ inference(cnf_transformation,[],[f5])).+fof(f5,plain,(+ ~mortal(socrates)),+ inference(flattening,[],[f2])).+fof(f2,negated_conjecture,(+ ~mortal(socrates)),+ inference(negated_conjecture,[],[f1])).+fof(f1,conjecture,(+ mortal(socrates)),+ file(unknown,unknown)).+fof(f10,plain,(+ mortal(socrates)),+ inference(resolution,[],[f8,f9])).+fof(f9,plain,(+ human(socrates)),+ inference(cnf_transformation,[],[f4])).+fof(f4,axiom,(+ human(socrates)),+ file(unknown,unknown)).+fof(f8,plain,(+ ( ! [X0] : (~human(X0) | mortal(X0)) )),+ inference(cnf_transformation,[],[f6])).+fof(f6,plain,(+ ! [X0] : (mortal(X0) | ~human(X0))),+ inference(ennf_transformation,[],[f3])).+fof(f3,axiom,(+ ! [X0] : (human(X0) => mortal(X0))),+ file(unknown,unknown)).+% SZS output end Proof for
+ test-data/tptp/fof/group-theory.p view
@@ -0,0 +1,5 @@+fof(0, conjecture, ! [Z]: ! [Y]: mult(Z, Y) = mult(Y, Z)).+fof(1, axiom, ! [Y]: mult(e, Y) = Y).+fof(2, axiom, ! [Y]: mult(inverse(Y), Y) = e).+fof(3, axiom, ! [P]: ! [Z]: ! [Y]: mult(mult(P, Z), Y) = mult(P, mult(Z, Y))).+fof(4, axiom, ! [Y]: mult(Y, Y) = e).
+ test-data/tptp/fof/syllogism.p view
@@ -0,0 +1,3 @@+fof(0, conjecture, mortal(socrates)).+fof(1, axiom, ! [Y]: (human(Y) => mortal(Y))).+fof(2, axiom, human(socrates)).
+ test/QuickCheckSpec/ArbitrarilyPretty.hs view
@@ -0,0 +1,333 @@+{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}+{-# 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+-- License : GPL-3+-- Maintainer : evgeny.kotelnikov@gmail.com+-- Stability : experimental+--+-- Defines a class 'ArbitrarilyPretty' used for randomized pretty printing along+-- with instances of this class implementing substandard ways to pretty print+-- a TPTP expression.+--++module ArbitrarilyPretty (+ ArbitrarilyPretty(..),+ SuperfluousParenthesis(..),+ randomSplit,+ randomTree+) where++import Data.List.NonEmpty (NonEmpty(..))+import qualified Data.List.NonEmpty as NEL (splitAt, fromList, length)++#if MIN_VERSION_base(4, 8, 0)+import Prelude hiding ((<$>), (<*>))+#else+import Prelude hiding (mapM)+import Data.Foldable (Foldable)+import Data.Traversable (Traversable, mapM)+import Data.Monoid (mempty)+#endif++import qualified Data.Foldable as F (toList)+import Data.List (genericReplicate, intersperse)+import Data.Maybe (maybeToList)+import Data.Text (Text)++#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup ((<>))+#endif++import Control.Applicative ((<$>), (<*>))++import Test.QuickCheck (Gen, choose, frequency)++import Data.Text.Prettyprint.Doc (+ Doc, (<+>), parens, brackets, punctuate, surround, hsep, space, comma+ )++import Data.TPTP+import Data.TPTP.Pretty+++-- | The class whose instances provide various ways of randomly pretty print+-- an expression.+class ArbitrarilyPretty e where+ apretty :: forall a. e -> Gen (Doc a)+++-- * Helpers++(&) :: (a -> b) -> (b -> c) -> a -> c+(&) = flip (.)++-- | Randomply split a non-empty list into two lists.+randomSplit :: NonEmpty a -> Gen ([a], NonEmpty a)+randomSplit lst = do+ index <- choose (0, NEL.length lst - 1)+ let (prefix, suffix) = NEL.splitAt index lst+ return (prefix, NEL.fromList suffix)++-- | Randomly split a non-empty list into a binary tree such that collecting+-- the leafs of that tree from left to right results in the original list.+--+-- This splitting is used to generate randomly nested disjunctions with+-- superfluous parenthesis compared to an equivalent clause.+randomTree :: NonEmpty a -> Gen (BinTree a)+randomTree = \case+ a :| [] -> return (Leaf a)+ a :| a' : as -> do+ (prefix, suffix) <- randomSplit (a' :| as)+ Fork <$> randomTree (a :| prefix) <*> randomTree suffix++star, arrow, tType, colon, negation :: Text+star = "*"+arrow = ">"+tType = "$tType"+colon = ":"+negation = "~"+++-- * Superfluous parenthesis++-- | An auxiliary wrapper used to generate pretty printed TPTP expressions+-- with superfluous parenthesis.+newtype SuperfluousParenthesis a = SuperfluousParenthesis {+ unSuperfluousParenthesis :: a+} deriving (Eq, Show, Ord, Functor, Traversable, Foldable)++-- | Randomly pretty print a TPTP expression with superflouous parenthesis+-- somewhere inside the expression but not on the outer level.+sppretty :: ArbitrarilyPretty (SuperfluousParenthesis e)+ => e -> forall a. Gen (Doc a)+sppretty = apretty . SuperfluousParenthesis++-- | Map a given 'Doc' generator to a one that randomly wraps the document+-- in zero, one or two pairs of parenthesis.+superfluousParenthesis :: Gen (Doc a) -> Gen (Doc a)+superfluousParenthesis g = frequency [+ (2, g),+ (2, parens <$> g),+ (1, parens . parens <$> g)+ ]+++-- ** SuperfluousParenthesis instances for common types++instance (ArbitrarilyPretty (SuperfluousParenthesis a),+ ArbitrarilyPretty (SuperfluousParenthesis b)) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Either a b)) where+ apretty = either sppretty sppretty . unSuperfluousParenthesis++instance ArbitrarilyPretty (SuperfluousParenthesis Text) where+ apretty = return . pretty . unSuperfluousParenthesis+++-- ** Auxiliary data types and their SuperfluousParenthesis instances++-- | An auxiliary wrapper used to pretty print applications of function and+-- predicate symbols with superfluous parenthesis.+data Application s e = Application_ s [e]+ deriving (Eq, Ord, Show)++-- | Pretty print an application of a symbol to a list of arguments.+application :: Pretty f => f -> [Doc a] -> Doc a+application f [] = pretty f+application f as = pretty f <> parens (hsep (punctuate comma as))++instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty s) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Application s e)) where+ apretty = unSuperfluousParenthesis & \case+ Application_ s ts -> application s+ <$> mapM (superfluousParenthesis . sppretty) ts++-- | An auxiliary wrapper used to pretty print applications of infix operators+-- with superfluous parenthesis.+data Infix e o = Infix o e e+ deriving (Eq, Ord, Show)++instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty o) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Infix e o)) where+ apretty = unSuperfluousParenthesis & \case+ Infix o a b -> surround (space <> pretty o <> space)+ <$> superfluousParenthesis (sppretty a)+ <*> superfluousParenthesis (sppretty b)++-- | An auxiliary wrapper used to pretty print applications of prefix operators+-- with superfluous parenthesis.+data Prefix e o = Prefix o e+ deriving (Eq, Ord, Show)++instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty o) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Prefix e o)) where+ apretty = unSuperfluousParenthesis & \case+ Prefix o e -> (pretty o <+>) <$> superfluousParenthesis (sppretty e)++-- | An auxiliary wrapper used to pretty print expressions with superfluous+-- parenthesis with a condition that mandates at least one pair of parenthesis.+data ParensUnless e = ParensUnless Bool e+ deriving (Show, Eq, Ord)++instance ArbitrarilyPretty (SuperfluousParenthesis e) =>+ ArbitrarilyPretty (SuperfluousParenthesis (ParensUnless e)) where+ apretty = unSuperfluousParenthesis & \case+ ParensUnless p e -> if p then sppretty e else parens <$> sppretty e++-- | An auxiliary data structure used to pretty print a binary tree of disjunctions.+data BinTree t+ = Leaf t+ | Fork (BinTree t) (BinTree t)+ deriving (Eq, Ord, Show, Functor, Traversable, Foldable)++instance ArbitrarilyPretty (SuperfluousParenthesis l) =>+ ArbitrarilyPretty (SuperfluousParenthesis (BinTree l)) where+ apretty = unSuperfluousParenthesis & \case+ Leaf l -> sppretty l+ Fork a b -> sppretty (Infix Disjunction a b)++-- | An auxiliary wrapper used to pretty print a typing of a symbol or a variable+-- with superfluous parenthesis around the type.+data Typing a t = Typing_ a t+ deriving (Eq, Show, Ord)++instance (ArbitrarilyPretty (SuperfluousParenthesis t), Pretty a) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Typing a t)) where+ apretty = unSuperfluousParenthesis & \case+ Typing_ a t -> (pretty a <>) <$> sppretty (Prefix colon t)++-- | An auxiliary wrapper used to pretty print a mapping type with superfluous+-- parenthesis around the argument type and the return type.+data Mapping s = Mapping [s] s+ deriving (Eq, Show, Ord, Functor, Traversable, Foldable)++instance ArbitrarilyPretty (SuperfluousParenthesis s) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Mapping s)) where+ apretty = unSuperfluousParenthesis & \case+ Mapping [] s -> sppretty s+ m -> do+ Mapping as s <- mapM (superfluousParenthesis . sppretty) m+ let starSeparated = hsep . intersperse (pretty star)+ return (parens (starSeparated as) <+> pretty arrow <+> s)+++-- ** First-order logic++instance ArbitrarilyPretty (SuperfluousParenthesis Term) where+ apretty = unSuperfluousParenthesis & \case+ Function f ts -> sppretty (Application_ f ts)+ Variable v -> return (pretty v)+ Number i -> return (pretty i)+ DistinctTerm d -> return (pretty d)++instance ArbitrarilyPretty (SuperfluousParenthesis Literal) where+ apretty = unSuperfluousParenthesis & \case+ Predicate p ts -> sppretty (Application_ p ts)+ Equality a s b -> sppretty (Infix s a b)++instance ArbitrarilyPretty (SuperfluousParenthesis (Sign, Literal)) where+ apretty = unSuperfluousParenthesis & \case+ (Positive, l) -> sppretty l+ (Negative, l) -> sppretty (Prefix negation l)++instance ArbitrarilyPretty (SuperfluousParenthesis Clause) where+ apretty = unSuperfluousParenthesis & \case+ Clause ls -> randomTree ls >>= sppretty++unitary :: FirstOrder s -> Bool+unitary = \case+ Atomic{} -> True+ Negated{} -> True+ Quantified{} -> True+ Connected{} -> False++under :: Connective -> FirstOrder s -> Bool+under c = \case+ Connected _ c' _ -> c' == c && isAssociative c+ f -> unitary f++instance ArbitrarilyPretty (SuperfluousParenthesis s) =>+ ArbitrarilyPretty (SuperfluousParenthesis (FirstOrder s)) where+ apretty = unSuperfluousParenthesis & \case+ Atomic l -> sppretty l+ Negated g -> sppretty (Prefix negation (ParensUnless (unitary g) g))+ Connected g c h -> sppretty (Infix c (ParensUnless (under c g) g)+ (ParensUnless (under c h) h))+ Quantified q vs g -> do+ let var (v, s) = (pretty v <>) <$> sppretty s+ vs' <- mapM var (F.toList vs)+ g' <- sppretty (Prefix colon (ParensUnless (unitary g) g))+ return (pretty q <+> brackets (hsep (punctuate comma vs')) <> g')+++-- ** Sorts and types++instance ArbitrarilyPretty (SuperfluousParenthesis Unsorted) where+ apretty = return . pretty . unSuperfluousParenthesis++instance ArbitrarilyPretty (SuperfluousParenthesis s) =>+ ArbitrarilyPretty (SuperfluousParenthesis (Sorted s)) where+ apretty = unSuperfluousParenthesis & \case+ Sorted Nothing -> return mempty+ Sorted (Just s) -> sppretty (Prefix colon s)++instance ArbitrarilyPretty (SuperfluousParenthesis (Name Sort)) where+ apretty = return . pretty . unSuperfluousParenthesis++instance ArbitrarilyPretty (SuperfluousParenthesis QuantifiedSort) where+ apretty = return . pretty . unSuperfluousParenthesis++instance ArbitrarilyPretty (SuperfluousParenthesis TFF1Sort) where+ apretty = unSuperfluousParenthesis & \case+ SortVariable v -> return (pretty v)+ TFF1Sort f ss -> sppretty (Application_ f ss)++instance ArbitrarilyPretty (SuperfluousParenthesis Type) where+ apretty = unSuperfluousParenthesis & \case+ 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)+ t' <- sppretty (Prefix colon (ParensUnless (null as) (TFF1Type [] as r)))+ return ("!>" <+> brackets (hsep (punctuate comma vs')) <> t')+++-- ** Units++instance ArbitrarilyPretty (SuperfluousParenthesis Formula) where+ apretty = unSuperfluousParenthesis & \case+ CNF c -> sppretty c+ FOF g -> sppretty g+ TFF0 g -> sppretty g+ TFF1 g -> sppretty g++instance ArbitrarilyPretty (SuperfluousParenthesis Declaration) where+ apretty = unSuperfluousParenthesis & \case+ Formula _ f -> sppretty f+ Typing s t -> sppretty (Typing_ s t)+ Sort s n -> sppretty (Typing_ s (Mapping (genericReplicate n tType) tType))++instance ArbitrarilyPretty (SuperfluousParenthesis Unit) where+ apretty = unSuperfluousParenthesis & \case+ i@Include{} -> return (pretty i)+ Unit nm decl a -> do+ decl' <- superfluousParenthesis (sppretty decl)+ let args = pretty nm : prettyRole decl : decl' : ann+ return (application (declarationLanguage decl) args <> ".")+ where+ prettyRole = \case+ Sort{} -> "type"+ Typing{} -> "type"+ Formula r _ -> pretty (name r)++ ann = case a of+ Just (s, i) -> pretty s : maybeToList (fmap prettyList i)+ Nothing -> []
test/QuickCheckSpec/Generators.hs view
@@ -204,7 +204,7 @@ deriving instance Generic Unit instance Arbitrary Unit where- arbitrary = genericArbitraryU+ arbitrary = genericArbitraryRec (1 % 10 % ()) shrink = \case Include f ns -> Include f <$> shrink ns Unit n d a -> Unit n <$> shrink d <*> shrinkAnnotation a
test/QuickCheckSpec/Main.hs view
@@ -1,5 +1,8 @@ {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE CPP #-} -- |@@ -20,40 +23,90 @@ #endif import Control.Applicative ((<*))+import Control.Monad (unless)+import Data.Foldable (toList)+import Data.List.NonEmpty (NonEmpty)+import qualified Data.List.NonEmpty as NEL (cons)+import Data.Text (Text) import Data.Attoparsec.Text (Parser, parseOnly, endOfInput)-import Data.Text.Prettyprint.Doc (layoutPretty, defaultLayoutOptions)+import Data.Text.Prettyprint.Doc (Doc, layoutPretty, defaultLayoutOptions) import Data.Text.Prettyprint.Doc.Render.Text (renderStrict)-import Test.QuickCheck (Property, Args(..), stdArgs, (===), whenFail,- forAllProperties, quickCheckWithResult)+import Test.QuickCheck (Gen, Property, Args(..), stdArgs, (===), whenFail,+ forAll, forAllProperties, quickCheckWithResult)+import Test.QuickCheck.Poly (A) +import System.Exit (exitFailure)+ import Data.TPTP hiding (clause) import Data.TPTP.Parse.Combinators import Data.TPTP.Pretty +import ArbitrarilyPretty import Generators () import Normalizers + -- * Helper functions --- | Idempotent parsing / pretty printing modulo normalization-ippModulo :: (Show a, Eq a, Pretty a) => (a -> a) -> Parser a -> a -> Property-ippModulo normalize p a =- whenFail (print t) $ case parseOnly (p <* endOfInput) t of- Left err -> whenFail (putStrLn $ "Parsing error: " ++ err) False- Right a' -> normalize a' === normalize a- where- t = renderStrict $ layoutPretty defaultLayoutOptions (pretty a)+-- | Generalized idempotent parsing / pretty printing.+ippWith :: (Show e, Show e', Eq e')+ => (e -> Gen (Doc a)) -- ^ Pretty printer.+ -> (Doc a -> Gen Text) -- ^ Renderer.+ -> Parser e -- ^ Parser.+ -> (e -> e') -- ^ Normalizer.+ -> e -> Property+ippWith pprint render parse normalize expr =+ forAll (pprint expr) $ \doc ->+ forAll (render doc) $ \text ->+ case parseOnly (parse <* endOfInput) text of+ Left err -> whenFail (putStrLn $ "Parsing error: " ++ err) False+ Right expr' -> normalize expr' === normalize expr --- | Idempotent parsing / pretty printing-ipp :: (Show a, Eq a, Pretty a) => Parser a -> a -> Property-ipp = ippModulo id+defaultRender :: Doc a -> Gen Text+defaultRender = return . renderStrict . layoutPretty defaultLayoutOptions +defaultNormalize :: e -> e+defaultNormalize = id +-- | Idempotent parsing / pretty printing modulo normalization.+ippModulo :: (Show e, Eq e, Pretty e) => (e -> e) -> Parser e -> e -> Property+ippModulo = flip $ ippWith (return . pretty) defaultRender++-- | Idempotent parsing / pretty printing.+ipp :: (Show e, Eq e, Pretty e) => Parser e -> e -> Property+ipp = ippModulo defaultNormalize++-- | Idempotent arbitrary parsing / pretty printing modulo normalization.+aippModulo :: (Show e, Eq e, ArbitrarilyPretty e, Show e', Eq e')+ => (e -> e') -> Parser e -> e -> Property+aippModulo = flip $ ippWith apretty defaultRender++-- | Idempotent parsing / pretty printing.+aipp :: (Show e, Eq e, ArbitrarilyPretty e) => Parser e -> e -> Property+aipp = aippModulo defaultNormalize++-- | Idempotent parsing / pretty printing with superfluous parenthesis+-- modulo normalization.+spAippModulo :: (Show e, Eq e, ArbitrarilyPretty (SuperfluousParenthesis e))+ => (e -> e) -> Parser e -> e -> Property+spAippModulo normalize parser expr =+ aippModulo (normalize . unSuperfluousParenthesis)+ (fmap SuperfluousParenthesis parser)+ (SuperfluousParenthesis expr)++-- | Idempotent parsing / pretty printing with superfluous parenthesis.+spAipp :: (Show e, Eq e, ArbitrarilyPretty (SuperfluousParenthesis e))+ => Parser e -> e -> Property+spAipp = spAippModulo defaultNormalize++ -- * Properties -- ** Generators +-- *** Well-formed names+ prop_validAtom :: Atom -> Bool prop_validAtom (Atom t) = isValidAtom t @@ -63,7 +116,19 @@ prop_validDistinctObject :: DistinctObject -> Bool prop_validDistinctObject (DistinctObject t) = isValidDistinctObject t +-- *** Auxiliary data structures +prop_randomSplit :: NonEmpty A -> Property+prop_randomSplit list = forAll (randomSplit list)+ $ \(prefix, suffix) -> appendr prefix suffix === list+ where+ appendr l nel = foldr NEL.cons nel l++prop_randomTree :: NonEmpty A -> Property+prop_randomTree list = forAll (randomTree list)+ $ \tree -> toList tree === toList list++ -- ** Names prop_ipp_Atom :: Atom -> Property@@ -90,10 +155,16 @@ prop_ipp_TFF1Sort :: TFF1Sort -> Property prop_ipp_TFF1Sort = ipp tff1Sort +prop_ipp_sp_TFF1Sort :: TFF1Sort -> Property+prop_ipp_sp_TFF1Sort = spAipp tff1Sort+ prop_ipp_Type :: Type -> Property prop_ipp_Type = ippModulo normalizeType type_ +prop_ipp_sp_Type :: Type -> Property+prop_ipp_sp_Type = spAippModulo normalizeType type_ + -- ** First-order logic prop_ipp_Number :: Number -> Property@@ -102,27 +173,48 @@ prop_ipp_Term :: Term -> Property prop_ipp_Term = ipp term +prop_ipp_sp_Term :: Term -> Property+prop_ipp_sp_Term = spAipp term+ prop_ipp_Literal :: Literal -> Property prop_ipp_Literal = ipp literal +prop_ipp_sp_Literal :: Literal -> Property+prop_ipp_sp_Literal = spAipp literal+ prop_ipp_Clause :: Clause -> Property prop_ipp_Clause = ipp clause +prop_ipp_sp_Clause :: Clause -> Property+prop_ipp_sp_Clause = spAipp clause+ prop_ipp_UnsortedFO :: UnsortedFirstOrder -> Property prop_ipp_UnsortedFO = ippModulo reassociate unsortedFirstOrder +prop_ipp_sp_UnsortedFO :: UnsortedFirstOrder -> Property+prop_ipp_sp_UnsortedFO = spAippModulo reassociate unsortedFirstOrder+ prop_ipp_MonomorphicFO :: MonomorphicFirstOrder -> Property prop_ipp_MonomorphicFO = ippModulo reassociate monomorphicFirstOrder +prop_ipp_sp_MonomorphicFO :: MonomorphicFirstOrder -> Property+prop_ipp_sp_MonomorphicFO = spAippModulo reassociate monomorphicFirstOrder+ prop_ipp_PolymorphicFO :: PolymorphicFirstOrder -> Property prop_ipp_PolymorphicFO = ippModulo reassociate polymorphicFirstOrder +prop_ipp_sp_PolymorphicFO :: PolymorphicFirstOrder -> Property+prop_ipp_sp_PolymorphicFO = spAippModulo reassociate polymorphicFirstOrder + -- ** Units prop_ipp_Unit :: Unit -> Property prop_ipp_Unit = ippModulo normalizeUnit unit +prop_ipp_sp_Unit :: Unit -> Property+prop_ipp_sp_Unit = spAippModulo normalizeUnit unit+ prop_ipp_TPTP :: TPTP -> Property prop_ipp_TPTP = ippModulo normalizeTPTP tptp @@ -146,5 +238,8 @@ return [] -main :: IO Bool-main = $forAllProperties $ quickCheckWithResult stdArgs{maxSuccess=1000}+main :: IO ()+main = do+ success <- $forAllProperties $ quickCheckWithResult stdArgs{maxSuccess=1000}+ unless success exitFailure+
test/UnitTests.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE CPP #-} -- |@@ -13,59 +14,81 @@ module UnitTests (tests) where -import Distribution.TestSuite (Test(..), TestInstance(..),- Progress(..), Result(..))--import System.Directory (listDirectory)-+import Control.Monad.Extra (concatMapM) #if !MIN_VERSION_base(4, 8, 0) import Data.Functor ((<$>)) #endif- import Data.Text (Text) import qualified Data.Text.IO as Text.IO (readFile)-import Data.List (intercalate)-import Control.Monad.Extra (concatMapM) -import Data.TPTP.Parse.Text+import System.Directory (listDirectory)+import System.FilePath.Posix (joinPath, (</>)) +import Distribution.TestSuite (Test(..), TestInstance(..),+ Progress(..), Result(..))++import Data.TPTP (TPTP(..), TSTP(..), SZS(..))+import Data.TPTP.Parse.Text (parseTPTPOnly, parseTSTPOnly)++ testDataDir :: FilePath testDataDir = "test-data" listTestDirectory :: FilePath -> IO [FilePath]-listTestDirectory d = listDirectory (testDataDir ++ "/" ++ d)+listTestDirectory d = listDirectory (testDataDir </> d) readTestFile :: FilePath -> IO Text-readTestFile f = Text.IO.readFile (testDataDir ++ "/" ++ f)+readTestFile f = Text.IO.readFile (testDataDir </> f) -parseFile :: FilePath -> IO Result-parseFile path = buildResult . parseTSTPOnly <$> readTestFile path+testParsingTPTP :: FilePath -> IO Result+testParsingTPTP path = buildResult . parseTPTPOnly <$> readTestFile path where- buildResult (Left e) = Error e- buildResult (Right _) = Pass+ buildResult = \case+ Left e -> Error e+ Right (TPTP []) -> Error "empty list of parsed units"+ Right _ -> Pass +testParsingTSTP :: FilePath -> IO Result+testParsingTSTP path = buildResult . parseTSTPOnly <$> readTestFile path+ where+ buildResult = \case+ Left e -> Error e+ Right (TSTP _ []) -> Error "empty list of parsed units"+ Right (TSTP (SZS (Just _) (Just _)) _) -> Pass+ Right (TSTP _ _) -> Error "failed to parse SZS ontology"+ type TestCase = (FilePath, FilePath, FilePath) +testCasePath :: TestCase -> FilePath+testCasePath (space, lang, file) = joinPath [space, lang, file]++runTestCase :: (FilePath, FilePath, FilePath) -> IO Result+runTestCase testCase@(space, _, _) = test (testCasePath testCase)+ where+ test = case space of+ "szs" -> testParsingTSTP+ _ -> testParsingTPTP+ testFile :: TestCase -> Test-testFile (space, lang, file) = Test $ TestInstance {- run = Finished <$> parseFile path,- name = path,- tags = [space, lang],- options = [],+testFile testCase@(space, lang, _) = Test $ TestInstance {+ run = Finished <$> runTestCase testCase,+ name = testCasePath testCase,+ tags = [space, lang],+ options = [], setOption = const . const $ Left "not supported"-} where path = intercalate "/" [space, lang, file]+} listSpaces :: IO [FilePath]-listSpaces = listTestDirectory ""+listSpaces = listDirectory testDataDir listLangs :: FilePath -> IO [(FilePath, FilePath)] listLangs s = fmap (s,) <$> listTestDirectory s listFiles :: (FilePath, FilePath) -> IO [(FilePath, FilePath, FilePath)]-listFiles (s, l) = fmap (s, l,) <$> listTestDirectory (s ++ "/" ++ l)+listFiles (s, l) = fmap (s, l,) <$> listTestDirectory (s </> l) cases :: IO [TestCase] cases = listSpaces >>= concatMapM listLangs >>= concatMapM listFiles tests :: IO [Test]-tests = fmap testFile <$> cases+tests = fmap testFile <$> cases
tptp.cabal view
@@ -1,7 +1,7 @@ cabal-version: 2.4 name: tptp-version: 0.1.1.0-synopsis: A parser and a pretty printer for the TPTP language+version: 0.1.2.0+synopsis: Parser and pretty printer for the TPTP language description: <http://www.tptp.org TPTP> (Thousands of Problems for Theorem Provers) is the standard language of problems, proofs, and models, used by automated@@ -10,7 +10,7 @@ This library provides definitions of data types, a <https://hackage.haskell.org/package/prettyprinter pretty printer> and an <https://hackage.haskell.org/package/attoparsec attoparsec> parser for the- CNF, FOF, TFF0 and TFF1 subsets of the TPTP language.+ CNF, FOF, TFF0 and TFF1 subsets of TPTP. homepage: https://github.com/aztek/tptp bug-reports: https://github.com/aztek/tptp/issues license: GPL-3.0-only@@ -25,7 +25,8 @@ GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.1+ GHC == 8.8.3,+ GHC == 8.10.1 extra-source-files: CHANGELOG.md@@ -59,16 +60,16 @@ if flag(Werror) ghc-options: -Werror build-depends:- base >= 4.5 && < 5.0,+ base >= 4.7 && < 5.0, text >= 1.2.3 && < 1.3, attoparsec >= 0.13.2 && < 0.14,- scientific >= 0.3.6 && < 0.4,+ scientific >= 0.3.1 && < 0.4, prettyprinter >= 1.2.1 && < 1.5 if impl(ghc < 8) ghc-options: -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns build-depends:- semigroups >= 0.16.1 && < 0.19+ semigroups >= 0.16.1 && < 1.0 if impl(ghc >= 8) ghc-options: -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns@@ -80,6 +81,7 @@ default-language: Haskell2010 main-is: Main.hs other-modules:+ ArbitrarilyPretty Generators Normalizers ghc-options:@@ -121,6 +123,7 @@ Cabal >= 1.16.0, extra >= 1.4.4 && < 1.7, directory >= 1.2.5 && < 1.4,+ filepath >= 1.3 && < 1.5, tptp test-suite doctests