jukebox 0.2.11 → 0.2.13
raw patch · 6 files changed
+74/−46 lines, 6 files
Files
- jukebox.cabal +1/−1
- src/Jukebox/Clausify.hs +2/−3
- src/Jukebox/Monotonox/ToFOF.hs +3/−3
- src/Jukebox/Options.hs +26/−17
- src/Jukebox/TPTP/FindFile.hs +1/−0
- src/Jukebox/Toolbox.hs +41/−22
jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.11+Version: 0.2.13 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Clausify.hs view
@@ -20,11 +20,10 @@ newtype ClausifyFlags = ClausifyFlags { splitting :: Bool } deriving Show clausifyFlags =- inGroup "Clausifier options" $+ inGroup "Input and clausifier options" $ ClausifyFlags <$> bool "split"- ["Split the conjecture into several sub-conjectures.",- "Default: (off)"]+ ["Split the conjecture into several sub-conjectures."] ---------------------------------------------------------------------- -- clausify
src/Jukebox/Monotonox/ToFOF.hs view
@@ -86,10 +86,10 @@ tagsFlags :: OptionParser Bool tagsFlags =+ inGroup "Options for encoding types" $ bool "more-axioms"- ["Add extra typing axioms for function arguments,",- "when using typing tags.",- "These are unnecessary for completeness but may help (or hinder!) the prover."]+ ["Add extra, redundant typing axioms for function arguments.",+ "May help or hinder the prover. Only affects --encoding tags."] tags :: Bool -> Scheme tags moreAxioms = Scheme
src/Jukebox/Options.hs view
@@ -193,7 +193,7 @@ flag :: String -> [String] -> a -> ArgParser a -> OptionParser a flag name help def (Annotated desc (SeqParser args f)) = Annotated [desc'] (await name def g)- where desc' = Flag name "Common options" help desc+ where desc' = Flag name "General options" help desc g xs = case f xs of Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))@@ -271,8 +271,12 @@ where f x | x == toolProgName t = Just (t, parser p') f _ = Nothing p' = p <* versionParser <* helpParser- helpParser = flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p'))- versionParser = flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t])+ helpParser =+ inGroup "Miscellaneous options" $+ flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p'))+ versionParser =+ inGroup "Miscellaneous options" $+ flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t]) -- Use the program name as a tool name if possible. getEffectiveArgs :: ToolParser a -> IO [String]@@ -328,22 +332,28 @@ helpTool :: Tool -> ToolParser a -> ToolParser a helpTool t0 p = usageTool t0 "help" help "help for"- where help = concat [+ where help = intercalate [""] [ [greeting t0], usage t0 "<toolname> ",- ["<toolname> can be any of the following:"],- concat [ justify (toolProgName t) [toolHelp t] | t <- descr p ],- ["", "Use " ++ toolProgName t0 ++ " <toolname> --help for help on a particular tool."]- ]+ ["Please run " ++ toolProgName t0 ++ " <toolname> --help, where <toolname> can be any of the following:"],+ intercalate [""] [ justify (toolProgName t) [toolHelp t] | t <- descr p ]] help :: Tool -> OptionParser a -> [String]-help t p = concat [- [greeting t],- usage t "",- ["<option> can be any of the following:"],- concat [ justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- nub (descr p) ]- ]+help t p =+ intercalate [""]+ [[greeting t],+ usage t "",+ intercalate [""] [+ [flagGroup f0 ++ ":"] +++ concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]+ | fs@(f0:_) <- groups (nub (descr p)) ]] + where+ groups [] = []+ groups (f:fs) =+ (f:[f' | f' <- fs, flagGroup f == flagGroup f']):+ groups [f' | f' <- fs, flagGroup f /= flagGroup f']+ greeting :: Tool -> String greeting t = toolName t ++ ", version " ++ toolVersion t ++ "." @@ -352,9 +362,8 @@ "Usage: " ++ toolProgName t ++ " " ++ opts ++ "<option>* <file>*", toolHelp t ++ ".", "",- "<file> should be in TPTP format.",- ""+ "<file> should be in TPTP format." ] justify :: String -> [String] -> [String]-justify name help = ["", " " ++ name] ++ map (" " ++) help+justify name help = [" " ++ name] ++ map (" " ++) help
src/Jukebox/TPTP/FindFile.hs view
@@ -32,6 +32,7 @@ f _ = return [] findFileFlags =+ inGroup "Input and clausifier options" $ concat <$> sequenceA [ pure ["."],
src/Jukebox/Toolbox.hs view
@@ -28,11 +28,10 @@ globalFlags :: OptionParser GlobalFlags globalFlags =- inGroup "Global options" $+ inGroup "Output options" $ GlobalFlags <$> bool "quiet"- ["Do not print any informational output.",- "Default: (off)"]+ ["Do not print any informational output."] (=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c) f =>>= g = (>=>) <$> f <*> g@@ -46,9 +45,18 @@ greetingBox t = greetingBoxIO t <$> globalFlags greetingBoxIO :: Tool -> GlobalFlags -> IO ()-greetingBoxIO t GlobalFlags{quiet = quiet} =- unless quiet $ hPutStrLn stderr (greeting t)+greetingBoxIO t globals = message globals (greeting t) +message :: GlobalFlags -> String -> IO ()+message globals msg =+ putStr (comment globals msg)++comment :: GlobalFlags -> String -> String+comment globals msg+ | quiet globals = ""+ | otherwise =+ unlines ["% " ++ line | line <- lines msg]+ allFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ()) allFilesBox = flip allFiles <$> filenames @@ -63,7 +71,7 @@ parseProblemIO :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form) parseProblemIO flags dirs f = do- let found file = unless (quiet flags) $ hPutStrLn stderr $ "Reading " ++ file ++ "..."+ let found file = message flags $ "Reading " ++ file ++ "..." r <- parseProblem found dirs f case r of Left err -> do@@ -106,10 +114,10 @@ schemeBox :: OptionParser Scheme schemeBox =+ inGroup "Options for encoding types" $ choose <$> flag "encoding"- ["Which type encoding to use.",- "Default: --encoding guards"]+ ["Which type encoding to use (defaults to guards)."] "guards" (argOption ["guards", "tags"]) <*> tagsFlags@@ -153,47 +161,58 @@ writeFileBox :: OptionParser (String -> IO ()) writeFileBox =+ inGroup "Output options" $ flag "output"- ["Where to write the output.",- "Default: stdout"]+ ["Where to write the output file (defaults to stdout)."] putStr (fmap myWriteFile argFile) where myWriteFile "/dev/null" _ = return ()+ myWriteFile "-" contents = putStr contents myWriteFile file contents = writeFile file contents guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))-guessModelBox = guessModelIO <$> expansive <*> universe+guessModelBox =+ inGroup "Options for the model guesser:" $+ guessModelIO <$> expansive <*> universe where universe = choose <$> flag "universe"- ["Which universe to find the model in.",- "Default: peano"]+ ["Which universe to find the model in (defaults to peano)."] "peano" (argOption ["peano", "trees"]) choose "peano" = Peano choose "trees" = Trees expansive = manyFlags "expansive"- ["Allow a function to construct 'new' terms in its base base."]+ ["Allow a function to construct 'new' terms in its base case."] (arg "<function>" "expected a function name" Just) guessModelIO :: [String] -> Universe -> Problem Form -> IO (Problem Form) guessModelIO expansive univ prob = return (guessModel expansive univ prob) allObligsBox :: OptionParser ((Problem Clause -> IO Answer) -> CNF -> IO ())-allObligsBox = pure allObligsIO+allObligsBox = allObligsIO <$> globalFlags -allObligsIO solve CNF{..} = loop 1 conjectures- where loop _ [] = result unsatisfiable+allObligsIO globals solve CNF{..} = loop 1 conjectures+ where loop _ [] =+ result unsatisfiable+ "PROVED.\nThe conjecture is true or the axioms are contradictory." loop i (c:cs) = do- when multi $ putStrLn $ "Part " ++ part i+ when multi $ putStr $ comment globals $ "Part " ++ part i answer <- solve (axioms ++ c)- when multi $ putStrLn $ "+++ PARTIAL (" ++ part i ++ "): " ++ show answer+ when multi $ putStr $ comment globals $ "Partial result (" ++ part i ++ "): " ++ show answer case answer of- Satisfiable -> result satisfiable+ Satisfiable ->+ result satisfiable+ "DISPROVED.\nThe conjecture is not true and the axioms are consistent." Unsatisfiable -> loop (i+1) cs- NoAnswer x -> result (show x)+ NoAnswer x ->+ result (show x)+ "GAVE UP.\nCouldn't prove or disprove the conjecture." multi = length conjectures > 1 part i = show i ++ "/" ++ show (length conjectures)- result x = putStrLn ("% SZS status " ++ x)+ result x hint = do+ message globals ("SZS status " ++ x)+ putStrLn ""+ message globals hint inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type)) inferBox = (\globals prob -> do