From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- source/CommandLine.hs | 162 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 162 insertions(+) create mode 100644 source/CommandLine.hs (limited to 'source/CommandLine.hs') diff --git a/source/CommandLine.hs b/source/CommandLine.hs new file mode 100644 index 0000000..a9fb00d --- /dev/null +++ b/source/CommandLine.hs @@ -0,0 +1,162 @@ +{-# 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 + + +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) + 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 + + + +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 + 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. -- cgit v1.2.3