logic-TPTP 0.4.7.0 → 0.5.0.0

raw patch · 11 files changed

+113/−29 lines, 11 filesdep +optparse-applicativePVP ok

version bump matches the API change (PVP)

Dependencies added: optparse-applicative

API changes (from Hackage documentation)

Files

• Codec/TPTP/Base.hs +31/−1
• Codec/TPTP/Export.hs +11/−0
• Codec/TPTP/Pretty.hs +1/−0
• Parser.y +9/−3
• ParserC.y +7/−2
• changelog.markdown +10/−0
• logic-TPTP.cabal +2/−1
• testing/ParseRandom.hs +1/−2
• testing/PrettyPrintFile.hs +1/−2
• testing/TestImportExportImportFile.hs +36/−12
• testing/TestImportExportRandom.hs +4/−6

@@ -287,6 +287,7 @@                  | GNumber Rational                  | GDistinctObject String                  | GFormulaData String Formula+                 | GFormulaTerm String Term                    deriving (Eq,Ord,Show,Read,Data,Typeable)  -- | Metadata (the /general_term/ rule in TPTP's grammar)@@ -502,9 +503,38 @@                            ,arbNum GNumber                             ,GDistinctObject <$> arbPrintable-                           ,GFormulaData `fmap` ((:) '$' `fmap` arbLowerWord) `ap` (sized (\n -> resize (n `div` 2) arbitrary))+                           ,oneof+                            [ GFormulaData "$fof" `fmap` sized (\n -> resize (n `div` 2) arbitrary)+                            , GFormulaData "$cnf" `fmap` sized (\n -> resize (n `div` 2) arbCNF)+                            , GFormulaTerm "$fot" `fmap` sized (\n -> resize (n `div` 2) arbitrary)+                            ]                            ] +arbCNF :: Gen Formula+arbCNF = do+    (xs :: [Formula]) <- liftArbitrary arbLiteral `suchThat` (not . Prelude.null)+    return $ foldl1 (.|.) xs+++arbLiteral :: Gen Formula+arbLiteral = oneof+    [+      do+            p <- arbitrary+            x <- arbAtomicFormula+            return $ if p then x else (.~.) x+    , do+            x1 <- arbitrary+            x2 <- arbitrary+            return $ F $ point $ InfixPred x1 (:!=:) x2+    ]+++arbAtomicFormula :: Gen Formula+arbAtomicFormula = fmap (F . point) $ do+    x1 <- arbitrary+    x2 <- argsFreq vector+    return (PredApp x1 x2)   instance Arbitrary GTerm

@@ -141,7 +141,18 @@    GVar x -> toTPTP x    GNumber x -> showsRational x    GDistinctObject x -> showString (tptpQuote x)+   GFormulaData str@"$cnf" formu -> s str . s "(" . cnfToTPTP formu . s ")"+     where+       cnfToTPTP :: Formula -> ShowS+       cnfToTPTP (F (Identity (BinOp l (:|:) r))) = cnfToTPTP l . s " | " . cnfToTPTP r+       cnfToTPTP (F (Identity ((:~:) x@(F (Identity (PredApp _ _)))))) = s "~ " . toTPTP x+       cnfToTPTP x@(F (Identity (PredApp _ _))) = toTPTP x+       -- We do not call toTPTP directly on the formula in InfixPred case, because parenthesis should not be printed.+       cnfToTPTP (F (Identity (InfixPred x1 (:!=:) x2))) = toTPTP x1 . s " != " . toTPTP x2+       cnfToTPTP x = error $ show x ++ " is not a literal"+    GFormulaData str formu -> s str . s "(" . toTPTP formu . s ")"+   GFormulaTerm str term -> s str . s "(" . toTPTP term . s ")"  tptpQuote :: [Char] -> [Char] tptpQuote x = "\"" ++ concatMap go x ++ "\""

@@ -220,6 +220,7 @@     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 Pretty AtomicWord where

@@ -54,6 +54,10 @@  tok_cnf                { LowerWord "cnf" }  tok_include_           { LowerWord "include" } + tok_fd_fof             { DollarWord "$fof" }+ tok_fd_cnf             { DollarWord "$cnf" }+ tok_fd_fot             { DollarWord "$fot" }+  tok_single_quoted      { SingleQuoted $$ }  tok_distinct_object    { DoubleQuoted $$ }  tok_dollar_word        { DollarWord $$ }@@ -365,15 +369,17 @@  general_data  :: {GData} general_data  :  atomic_word  { GWord $1 }+               | formula_data  { $1 }                | atomic_word  lp general_terms  rp { GApp $1 $3 }                | variable  { GVar $1 }                | number  { GNumber $1 }                | distinct_object { GDistinctObject (stripQuotes '"' $1) }-               | formula_data  { $1 } + formula_data :: {GData}-formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 $3 }-              -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }+formula_data  :  tok_fd_fof lp fof_formula  rp { GFormulaData "$fof" $3 }+               | tok_fd_cnf lp cnf_formula  rp { GFormulaData "$cnf" $3 }+               | tok_fd_fot lp term rp         { GFormulaTerm "$fot" $3 }  general_list  :: {[GTerm]} general_list  : lbra rbra {[]}

@@ -55,6 +55,10 @@  tok_cnf                { LowerWord "cnf" }  tok_include_           { LowerWord "include" } + tok_fd_fof             { DollarWord "$fof" }+ tok_fd_cnf             { DollarWord "$cnf" }+ tok_fd_fot             { DollarWord "$fot" }+  tok_single_quoted      { SingleQuoted $$ }  tok_distinct_object    { DoubleQuoted $$ }  tok_dollar_word        { DollarWord $$ }@@ -373,8 +377,9 @@                | formula_data  { $1 }  formula_data :: {GData}-formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 (forgetFC $3) }-              -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }+formula_data  :  tok_fd_fof lp fof_formula  rp { GFormulaData "$fof" (forgetFC $3) }+               | tok_fd_cnf lp cnf_formula  rp { GFormulaData "$cnf" (forgetFC $3) }+               | tok_fd_fot lp term rp         { GFormulaTerm "$fot" (forgetTC $3) }  general_list  :: {[GTerm]} general_list  : lbra rbra {[]}

@@ -1,3 +1,13 @@+## 0.5.0.0++* Add `GFormulaTerm` constructor to `GData` and support `$fot` `formula_data` (#1, #2, #19, thanks to @agomezl)+* Produce valid `$cnf` `formula_data` (#23)+* Improve test suites++## 0.4.7.0++* Fix to work with happy >=1.19.10+ ## 0.4.6.0  * Add Semigroup instances for Monoids and fix cabal-version warning (Thanks to @msakai)

@@ -1,5 +1,5 @@ name: logic-TPTP-version: 0.4.7.0+version: 0.5.0.0 cabal-version: >= 1.8 build-type: Simple license: GPL@@ -96,6 +96,7 @@  build-depends:     logic-TPTP                   , base                   , ansi-wl-pprint+                  , optparse-applicative >=0.11 && <0.16                   , pcre-light                   , semigroups  if impl(ghc <7.10)

@@ -1,5 +1,4 @@ {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}-{-# LANGUAGE PackageImports #-}  module Main where @@ -25,7 +24,7 @@ import Common import SimpleArgs -import "logic-TPTP" Codec.TPTP+import Codec.TPTP  infilename = getArgs parseRes = return . parse =<< readFile =<< infilename

@@ -1,5 +1,4 @@ {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}-{-# LANGUAGE PackageImports #-}  module Main where @@ -24,7 +23,7 @@ import System.Exit import Text.Regex.PCRE.Light.Char8 -import "logic-TPTP" Codec.TPTP+import Codec.TPTP import SimpleArgs  main = putStrLn . prettySimple . parse =<< readFile =<< getArgs

@@ -1,39 +1,61 @@ {-# OPTIONS_GHC -Wall #-}-{-# LANGUAGE PackageImports #-} module Main where  import Control.Monad import Data.Monoid-import Text.PrettyPrint.ANSI.Leijen+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) import System.Exit import Common-import SimpleArgs+import Options.Applicative -import "logic-TPTP" Codec.TPTP+import Codec.TPTP +data Options+  = Options+  { optPrintExport :: Bool+  , optPrintFailureOnly :: Bool+  } +optionsParser :: Parser Options+optionsParser = Options <$> printExportOption <*> printFailureOnlyOption+  where+    printExportOption = argument auto+      $  metavar "True|False"+      <> help ("print exported result")+    printFailureOnlyOption = switch+      $  long "print-failure-only"+      <> help ("print failure only")++parserInfo :: ParserInfo Options+parserInfo = info (helper <*> optionsParser) $ mconcat+  [ fullDesc+  ]+ -- Note: This test expects a list of .p files (one per line) through stdin  main ::  IO () main = do   files <- lines `fmap` getContents   --print (length files)-  print_export <- getArgs-  forM_ files (diff_once_twice print_export)+  Options print_export print_failure_only <- execParser parserInfo+  forM_ files (diff_once_twice print_export print_failure_only)   exitWith ExitSuccess -diff_once_twice ::  Bool -> String -> IO ()-diff_once_twice print_export infilename'  = do+diff_once_twice ::  Bool -> Bool -> String -> IO ()+diff_once_twice print_export print_failure_only infilename'  = do   --let tmp = "/tmp/tmp.tptp"-  putStrLn infilename'+  unless print_failure_only $ putStrLn infilename'   input <- readFile infilename'   case findUnsupportedFormulaType input of-     Just x -> putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)+     Just x -> do+       unless print_failure_only $ +         putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)      Nothing -> do        let once = parse input       let tptp = toTPTP' once-      when print_export (putStrLn $ "new tptp = " ++tptp)+      when (print_export && not print_failure_only) $+        putStrLn $ "new tptp = " ++tptp       let twice = parse tptp       let dif = mconcat (zipWith diffAFormula once twice)       let success = (putStrLn . prettySimple . dullgreen . text $ "Ok")@@ -46,7 +68,9 @@       --     exitWith (ExitFailure 1)        if once==twice-         then success+         then do+           unless print_failure_only $ success          else do+           when print_failure_only $ putStrLn infilename'            putStrLn . prettySimple $ dif            exitWith (ExitFailure 1)

@@ -1,12 +1,11 @@ {-# OPTIONS_GHC -Wall #-}-{-# LANGUAGE PackageImports #-} module Main where  import Test.QuickCheck import Common import Data.Functor.Identity -import "logic-TPTP" Codec.TPTP+import Codec.TPTP  main ::  IO () main = quickCheckWith (stdArgs { maxSuccess = 5000 }) prop_test_ie@@ -20,10 +19,9 @@            dif = diffAFormula f g        in-          whenFail-          (putStrLn . prettySimple $ dif)--           (f==g)+          counterexample tptp $+           whenFail (putStrLn . prettySimple $ dif) $+            (f==g)            -- (case dif of           --    OtherSame -> True