blob: 47efe2223bb7a022431934c34fff07f33cb9ff71 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RecordWildCards #-}
module CommandLine where
import Api
import Base
import Provers qualified
import Version qualified
import Control.Monad.Logger
import Control.Monad.Reader
import Data.Text.IO qualified as Text
import Data.Text.Lazy.IO qualified as LazyText
import Options.Applicative
import Text.Pretty.Simple (pShowNoColor)
import UnliftIO
import UnliftIO.Directory
import UnliftIO.Environment (lookupEnv)
import System.FilePath.Posix
import qualified Tptp.UnsortedFirstOrder as Syntax.Internal
runCommandLine :: IO ()
runCommandLine = do
options@Options{withLogging = logging} <- execParser (withInfo parseOptions)
case logging of
WithoutLogging -> runNoLoggingT (runReaderT run options)
WithLogging -> runStdoutLoggingT (runReaderT run options)
where
withInfo :: Parser a -> ParserInfo a
withInfo p = info (helper <*> p) (fullDesc <> header "Naproche/ZF")
run :: (MonadUnliftIO io, MonadLogger io, MonadReader Options io) => io ()
run = do
opts <- ask
case withVersion opts of
WithVersion -> liftIO (Text.putStrLn Version.info)
WithoutVersion -> skip
case withOmissions opts of
WithoutOmissions -> liftIO (Text.putStrLn "--safe is not implemented yet.")
WithOmissions -> skip
case withDump opts of
WithoutDump -> skip
WithDump dir -> do
let serials = [dir </> show n <.> "p" | n :: Int <- [1..]]
tasks <- zip serials <$> encodeTasks (inputPath opts)
createDirectoryIfMissing True dir
forM_ tasks (uncurry dumpTask)
case (withParseOnly opts, withMegalodon opts) of
(WithParseOnly, _) -> do
ast <- parse (inputPath opts)
liftIO (LazyText.putStrLn (pShowNoColor ast))
(_, WithMegalodon) -> do
megalodon <- exportMegalodon (inputPath opts)
let outputFile = "megalodon" </> replaceExtension (inputPath opts) "mg"
createDirectoryIfMissing True (takeDirectory outputFile)
liftIO (Text.writeFile outputFile megalodon)
(WithoutParseOnly, WithoutMegalodon) -> do
-- A custom E executable can be configured using environment variables.
-- If the environment variable is undefined we fall back to the
-- a globally installed E executable.
vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE"
eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER"
let prover = case withProver opts of
WithVampire -> Provers.vampire vampirePathPath
WithEprover -> Provers.eprover eproverPath
WithIprover -> Provers.iprover
WithDefaultProver -> Provers.vampire vampirePathPath
let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts)
result <- verify proverInstance (inputPath opts)
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!"
parseOptions :: Parser Options
parseOptions = do
inputPath <- strArgument (help "Source file" <> metavar "FILE")
withCache <- withCacheParser
withDump <- withDumpParser
withFilter <- withFilterParser
withLogging <- withLoggingParser
withMemoryLimit <- withMemoryLimitParser
withOmissions <- withOmissionsParser
withParseOnly <- withParseOnlyParser
withProver <- withProverParser
withTimeLimit <- withTimeLimitParser
withVersion <- withVersionParser
withMegalodon <- withMegalodonParser
withDumpPremselTraining <- withDumpPremselTrainingParser
withFailList <- withFailListParser
pure Options{..}
withTimeLimitParser :: Parser Provers.TimeLimit
withTimeLimitParser = Provers.Seconds <$> option auto (long "timelimit" <> short 't' <> value dflt <> help "Time limit for each proof task in seconds.")
where
Provers.Seconds dflt = Provers.defaultTimeLimit
withMemoryLimitParser :: Parser Provers.MemoryLimit
withMemoryLimitParser = Provers.Megabytes <$> option auto (long "memlimit" <> short 'm' <> value dflt <> help "Memory limit for each proof task in MB.")
where
Provers.Megabytes dflt = Provers.defaultMemoryLimit
withProverParser :: Parser WithProver
withProverParser = flag' WithEprover (long "eprover" <> help "Use E as external prover.")
<|> flag' WithVampire (long "vampire" <> help "Use Vampire as external prover.")
<|> flag' WithIprover (long "iprover" <> help "Use iProver as external prover.")
<|> pure WithDefaultProver
withFilterParser :: Parser WithFilter
withFilterParser = flag' WithoutFilter (long "nofilter" <> help "Do not perform relevance filtering.")
<|> flag' WithFilter (long "filter" <> help "Perform relevance filtering.")
<|> pure WithoutFilter
withOmissionsParser :: Parser WithOmissions
withOmissionsParser = flag' WithOmissions (long "unsafe" <> help "Allow proof omissions (default).")
<|> flag' WithoutOmissions (long "safe" <> help "Disallow proof omissions.")
<|> pure WithOmissions -- Default to allowing omissions.
withParseOnlyParser :: Parser WithParseOnly
withParseOnlyParser = flag' WithParseOnly (long "parseonly" <> help "Only parse and show the resulting AST.")
<|> pure WithoutParseOnly -- Default to allowing omissions.
withVersionParser :: Parser WithVersion
withVersionParser = flag' WithVersion (long "version" <> help "Show the current version.")
<|> pure WithoutVersion -- Default to not showing the version.
withLoggingParser :: Parser WithLogging
withLoggingParser = flag' WithLogging (long "log" <> help "Enable logging.")
<|> pure WithoutLogging -- Default to not showing the version.
withCacheParser :: Parser WithCache
withCacheParser = flag' WithoutCache (long "uncached" <> help "Do not use caching.")
<|> flag' WithCache (long "cached" <> help "Use caching (default).")
<|> pure WithCache -- Default to using the cache.
withDumpParser :: Parser WithDump
withDumpParser = WithDump <$> strOption (long "dump" <> metavar "DUMPDIR" <> help "Dump all proof tasks in a separate directory.")
<|> pure WithoutDump -- Default to using the cache.
withDumpPremselTrainingParser :: Parser WithDumpPremselTraining
withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump" <> help "Dump training data for premise selection.")
<|> pure WithoutDumpPremselTraining -- Default to using the cache.
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.
|
