diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Api.hs | 17 | ||||
| -rw-r--r-- | source/CommandLine.hs | 60 | ||||
| -rw-r--r-- | source/Provers.hs | 4 | ||||
| -rw-r--r-- | source/Test/Golden.hs | 1 |
4 files changed, 62 insertions, 20 deletions
diff --git a/source/Api.hs b/source/Api.hs index 95d5c8c..f597153 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -17,6 +17,7 @@ module Api , dumpTask , verify, ProverAnswer(..), VerificationResult(..) , exportMegalodon + , showFailedTask , WithCache(..) , WithFilter(..) , WithOmissions(..) @@ -29,6 +30,7 @@ module Api , WithParseOnly(..) , Options(..) , WithDumpPremselTraining(..) + , WithFailList(..) ) where @@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token) import UnliftIO import UnliftIO.Directory import UnliftIO.Environment +import Syntax.Abstract (Formula) -- | Follow all @\\import@ statements recursively and build a theory graph from them. -- The @\\import@ statements should be on their own separate line and precede all @@ -285,6 +288,17 @@ exportMegalodon file = do pure (Megalodon.encodeBlocks lexicon blocks) + +-- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use +showFailedTask :: (a, ProverAnswer) -> IO() +showFailedTask (_, Yes ) = Text.putStrLn "" +showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("Prover found countermodel: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("Contradictory axioms: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("Out of resources: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("Error at: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +--showFailedTask (_, _) = Text.putStrLn "Error!" + + -- | Should we use caching? data WithCache = WithoutCache | WithCache deriving (Show, Eq) @@ -312,6 +326,8 @@ pattern WithoutDump = WithDump "" data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq) +data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq) + data Options = Options { inputPath :: FilePath @@ -327,4 +343,5 @@ data Options = Options , withVersion :: WithVersion , withMegalodon :: WithMegalodon , withDumpPremselTraining :: WithDumpPremselTraining + , withFailList :: WithFailList } diff --git a/source/CommandLine.hs b/source/CommandLine.hs index a9fb00d..47efe22 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,7 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix - +import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -69,23 +69,42 @@ run = do WithDefaultProver -> Provers.vampire vampirePathPath let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts) result <- verify proverInstance (inputPath opts) - liftIO case result of - VerificationSuccess -> (Text.putStrLn "Verification successful.") - VerificationFailure [] -> error "Empty verification fail" - VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of - Yes -> - skip - No tptp -> do - putStrLn "Verification failed: prover found countermodel" - Text.hPutStrLn stderr tptp - ContradictoryAxioms tptp -> do - putStrLn "Verification failed: contradictory axioms" - Text.hPutStrLn stderr tptp - Uncertain tptp -> do - putStrLn "Verification failed: out of resources" - Text.hPutStrLn stderr tptp - Error err -> - Text.hPutStrLn stderr err + case withFailList opts of + WithoutFailList -> liftIO case result of + VerificationSuccess -> putStrLn "Verification successful." + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of + Yes -> + skip + No tptp -> do + putStrLn "Verification failed: prover found countermodel" + Text.hPutStrLn stderr tptp + ContradictoryAxioms tptp -> do + putStrLn "Verification failed: contradictory axioms" + Text.hPutStrLn stderr tptp + Uncertain tptp -> do + putStrLn "Verification failed: out of resources" + Text.hPutStrLn stderr tptp + Error err tptp task -> do + putStr "Error at:" + Text.putStrLn task + Text.putStrLn err + Text.putStrLn tptp + + WithFailList -> liftIO case result of + VerificationSuccess -> putStrLn "Verification successful." + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure fails -> do + putStrLn "Following task couldn't be solved by the ATP: " + traverse_ showFailedTask fails + Text.hPutStrLn stderr "Don't give up!" + + + + + + + @@ -104,6 +123,7 @@ parseOptions = do withVersion <- withVersionParser withMegalodon <- withMegalodonParser withDumpPremselTraining <- withDumpPremselTrainingParser + withFailList <- withFailListParser pure Options{..} withTimeLimitParser :: Parser Provers.TimeLimit @@ -160,3 +180,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump withMegalodonParser :: Parser WithMegalodon withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.") <|> pure WithoutMegalodon -- Default to using the cache. + +withFailListParser :: Parser WithFailList +withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") + <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file diff --git a/source/Provers.hs b/source/Provers.hs index 203ee82..37e02ca 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -110,7 +110,7 @@ data ProverAnswer | No Text | ContradictoryAxioms Text | Uncertain Text - | Error Text + | Error Text Text Text deriving (Show, Eq) nominalDiffTimeToText :: NominalDiffTime -> Text @@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr = | saidNo -> No tptp | doesNotKnow -> Uncertain tptp | warned -> ContradictoryAxioms tptp - | otherwise -> Error (answer <> answerErr) + | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task))) diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs index 705aaa5..c01c249 100644 --- a/source/Test/Golden.hs +++ b/source/Test/Golden.hs @@ -39,6 +39,7 @@ testOptions = Api.Options , withTimeLimit = Provers.defaultTimeLimit , withVersion = Api.WithoutVersion , withMegalodon = Api.WithoutMegalodon + , withFailList = Api.WithoutFailList } goldenTests :: IO TestTree |