packages feed

jukebox 0.2.19 → 0.2.20

raw patch · 12 files changed

+120/−78 lines, 12 files

Files

jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.19+Version: 0.2.20 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Clausify.hs view
@@ -23,7 +23,8 @@   inGroup "Input and clausifier options" $   ClausifyFlags <$>     bool "split"-      ["Split the conjecture into several sub-conjectures."]+      ["Split the conjecture into several sub-conjectures (off by default)."]+      False  ---------------------------------------------------------------------- -- clausify@@ -39,7 +40,9 @@     do cs <- clausForm axiom inp        clausifyInputs (cs ++ theory) obligs inps -  clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =+  clausifyInputs theory obligs (inp:inps)+      -- XX translate question in answer literal+    | Conjecture _ <- kind inp =     do clausifyObligs theory obligs inp (split' (what inp)) inps    clausifyObligs theory obligs _ [] inps =
src/Jukebox/Form.hs view
@@ -307,7 +307,7 @@  type Tag = String -data Kind = Axiom String | Conjecture | Question deriving (Eq, Ord)+data Kind = Axiom String | Conjecture String deriving (Eq, Ord)  data Answer = Sat SatReason | Unsat UnsatReason | NoAnswer NoAnswerReason   deriving (Eq, Ord)
src/Jukebox/Monotonox/ToFOF.hs view
@@ -43,7 +43,7 @@         aux _pos (Equiv _ _) = error "ToFOF.guard: equiv should have been eliminated"         aux _pos (Connective _ _ _) = error "ToFOF.guard: connective should have been eliminated"         pos Axiom{} = True-        pos Conjecture = False+        pos Conjecture{} = False  translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form translate1 scheme mono f = Form.run f $ \inps -> do@@ -77,7 +77,7 @@               Axiom{} ->                 fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $                   prepare f-              Conjecture ->+              Conjecture{} ->                 fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $                 fmap notInwards $ prepare $ nt f       typeI = Type (name "$i") (Finite 0) Infinite@@ -91,8 +91,9 @@ tagsFlags =   inGroup "Options for encoding types" $   bool "more-axioms"-    ["Add extra, redundant typing axioms for function arguments.",+    ["Add extra, redundant typing axioms for function arguments (off by default).",      "May help or hinder the prover. Only affects --encoding tags."]+    False  tags :: Bool -> Scheme tags moreAxioms = Scheme
src/Jukebox/Options.hs view
@@ -40,7 +40,7 @@ ---------------------------------------------------------------------- -- The ArgParser type: parsing of single flags. -type ArgParser = Annotated String SeqParser+type ArgParser = Annotated [String] SeqParser   -- annotated with a description, e.g. "<number>"  -- Called SeqParser because <*> is sequential composition.@@ -60,7 +60,7 @@ -- Combinators for building ArgParsers.  arg :: String -> String -> (String -> Maybe a) -> ArgParser a-arg desc err f = Annotated desc (SeqParser 1 c)+arg desc err f = Annotated [desc] (SeqParser 1 c)   where c [] = Left (Mistake err)         c (x:_) | "-" `isPrefixOf` x = Left (Mistake err)         c (x:_) =@@ -131,9 +131,14 @@ data Flag = Flag   { flagName :: String,     flagGroup :: String,+    flagMode :: FlagMode,     flagHelp :: [String],     flagArgs :: String } deriving (Eq, Show)+data FlagMode = NormalMode | ExpertMode | HiddenMode deriving (Eq, Show) +flagExpert :: Flag -> Bool+flagExpert f = flagMode f == ExpertMode+ -- Called ParParser because <*> is parallel composition. -- In other words, in f <*> x, f and x both see the whole command line. -- We want this when parsing command lines because@@ -185,57 +190,72 @@     No _ -> Left (Mistake ("Didn't recognise option " ++ x))     Error err -> Left err -awaitP :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a-awaitP p def par = ParParser (return def) f+await :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a+await p def par = ParParser (return def) f   where f (x:xs) | p x =           case par x xs of             Yes n r -> Yes (n+1) r             No _ ->               error "Options.await: got No"             Error err -> Error err-        f _ = No (awaitP p def par)+        f _ = No (await p def par) -await :: String -> a -> ([String] -> ParseResult a) -> ParParser a-await flag def f = awaitP (\x -> "--" ++ flag == x) def (const f)+----------------------------------------------------------------------+-- Low-level primitives for building OptionParsers. +-- Produce an OptionParser with maximum flexibility.+primFlag ::+  -- Name and description of options (for documentation)+  String -> [String] ->+  -- Predicate which checks if this argument is our option+  (String -> Bool) ->+  -- Handle repeated occurrences of the same option+  (a -> a -> Either Error a) ->+  -- Default argument value and argument parser+  -- The argument parser is given the option name.+  a -> ArgParser (String -> a) -> OptionParser a+primFlag name help p combine def (Annotated desc (SeqParser args f)) =+  Annotated [desc'] (await p def (g Right))+  where desc' = Flag name "General options" NormalMode help (unwords desc)+        g comb x xs =+          case f xs >>= comb . ($ x) of+            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))+            Left (Usage code err) -> Error (Usage code err)+            Right y ->+              Yes args (await p y (g (combine y)))+ ---------------------------------------------------------------------- -- Combinators for building OptionParsers.  -- From a flag name and description and argument parser, produce an OptionParser. 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 "General options" help desc-        g xs =-          case f xs of-            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))-            Left (Usage code err) -> Error (Usage code err)-            Right y -> Yes args (pure y <* noFlag)-        -- Give an error if the flag is repeated.-        noFlag =-          await name ()-            (const (Error (Mistake ("Option --" ++ name ++ " occurred twice"))))---- A boolean flag.-bool :: String -> [String] -> OptionParser Bool-bool name help = flag name help False (pure True)+flag name help def p =+  primFlag name help+    (\x -> x == "--" ++ name)+    (\x y -> return y) -- take second occurrence of flag+    def (const <$> p)  -- A variant of 'flag' that allows repeated flags. manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a]-manyFlags name help (Annotated desc (SeqParser args f)) =-  fmap reverse (Annotated [desc'] (go []))-  where desc' = Flag name "Common options" help desc-        go xs = await name xs (g xs)-        g xs ys =-          case f ys of-            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))-            Left (Usage code err) -> Error (Usage code err)-            Right x -> Yes args (go (x:xs))+manyFlags name help p =+  primFlag name help+    (\x -> x == "--" ++ name)+    (\x y -> return (x ++ y))+    [] (const <$> return <$> p) +-- A boolean flag.+bool :: String -> [String] -> Bool -> OptionParser Bool+bool name help def =+  primFlag ("(no-)" ++ name) help+    (\x -> x `elem` ["--" ++ name, "--no-" ++ name])+    (\x y -> return y)+    def+    (pure (\name' -> if "--" ++ name == name' then True else False))+ -- A parser that reads all file names from the command line. filenames :: OptionParser [String] filenames = Annotated [] (from [])-  where from xs = awaitP p xs (f xs)+  where from xs = await p xs (f xs)         p x = not ("-" `isPrefixOf` x) || x == "-"         f xs y _ = Yes 0 (from (xs ++ [y])) @@ -248,6 +268,14 @@ inGroup :: String -> OptionParser a -> OptionParser a inGroup x (Annotated fls f) = Annotated [fl{ flagGroup = x } | fl <- fls] f +-- Mark a flag as being for experts only.+expert :: OptionParser a -> OptionParser a+expert (Annotated fls f) = Annotated [fl{ flagMode = ExpertMode } | fl <- fls] f++-- Mark a flag as being hidden.+hidden :: OptionParser a -> OptionParser a+hidden (Annotated fls f) = Annotated [fl{ flagMode = HiddenMode } | fl <- fls] f+ -- Add a --version flag. version :: String -> OptionParser a -> OptionParser a version x p =@@ -275,25 +303,40 @@     p' =       p <*         (inGroup "Miscellaneous options" $-         flag "help" ["Show this help text."] () (argUsage ExitSuccess (helpText name description p')))+         flag "help" ["Show help text."] ()+        +           (argUsage ExitSuccess (helpText False name description p')))+        <*+        (if any flagExpert (descr p) then+          (inGroup "Miscellaneous options" $+           flag "expert-help" ["Show help text for hidden options."] ()+             (argUsage ExitSuccess (helpText True name description p')))+         else pure ())  usageText :: String -> String -> [String] usageText name descr =   [descr ++ ".",-   "Usage: " ++ name ++ " <option>* <file>*, where <file> should be in TPTP format."]+   "Usage: " ++ name ++ " <option>* <file>*, where <file> is in TPTP format."] -helpText :: String -> String -> OptionParser a -> [String]-helpText name description p =+helpText :: Bool -> String -> String -> OptionParser a -> [String]+helpText expert name description p =   intercalate [""] $     [usageText name description] ++     [[flagGroup f0 ++ ":"] ++      concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]-     | fs@(f0:_) <- groups (nub (descr p)) ]+     | fs@(f0:_) <- groups (filter ok (nub (descr p))) ] +++    [ ["To see hidden options too, try --expert-help."]+    | any flagExpert (descr p), not expert ]   where     groups [] = []     groups (f:fs) =       (f:[f' | f' <- fs, flagGroup f == flagGroup f']):       groups [f' | f' <- fs, flagGroup f /= flagGroup f']+    ok flag =+      case flagMode flag of+        NormalMode -> True+        ExpertMode -> expert+        HiddenMode -> False  justify :: String -> [String] -> [String] justify name help = ["  " ++ name] ++ map ("    " ++) help
src/Jukebox/Provers/E.hs view
@@ -25,18 +25,15 @@   inGroup "E prover options" $   EFlags <$>     flag "eprover"-      ["Path to the E theorem prover.",-       "Default: eprover"]+      ["Path to the E theorem prover (\"eprover\" by default)."]       "eprover"       argFile <*>     flag "timeout"-      ["Timeout for E, in seconds.",-       "Default: (off)"]+      ["Timeout for E, in seconds (off by default)."]       Nothing       (fmap Just argNum) <*>     flag "memory"-      ["Memory limit for E, in megabytes.",-       "Default: (off)"]+      ["Memory limit for E, in megabytes (unlimited by default)."]       Nothing       (fmap Just argNum)
src/Jukebox/Provers/SPASS.hs view
@@ -19,18 +19,15 @@   inGroup "SPASS prover options" $   SPASSFlags <$>     flag "spass"-      ["Path to SPASS.",-       "Default: SPASS"]+      ["Path to SPASS (\"SPASS\" by default)."]       "SPASS"       argFile <*>     flag "timeout"-      ["Timeout in seconds.",-       "Default: (none)"]+      ["Timeout in seconds (off by default)."]       Nothing       (fmap Just argNum) <*>     flag "sos"-      ["Use set-of-support strategy.",-       "Default: false"]+      ["Use set-of-support strategy (off by default)."]       False       (pure True)
src/Jukebox/SMTLIB.hs view
@@ -185,9 +185,7 @@ pPrintInput :: Input Form -> Doc pPrintInput Input{kind = Axiom _, what = form} =   sexp ["assert", pPrintForm form]-pPrintInput Input{kind = Conjecture, what = form} =-  sexp ["assert", sexp ["not", pPrintForm form]]-pPrintInput Input{kind = Question, what = form} =+pPrintInput Input{kind = Conjecture _, what = form} =   sexp ["assert", sexp ["not", pPrintForm form]]  pPrintForm :: Form -> Doc
src/Jukebox/TPTP/FindFile.hs view
@@ -36,9 +36,9 @@   concat <$>   sequenceA [     pure ["."],-    flag "root"-      ["Extra directories that will be searched for TPTP input files."]-      []-      argFiles,+    concat <$>+      manyFlags "root"+        ["Extra directories that will be searched for TPTP input files."]+        argFiles,     io getTPTPDirs     ]
src/Jukebox/TPTP/Parse/Core.hs view
@@ -25,7 +25,7 @@    keyword, defined, kind) import qualified Jukebox.TPTP.Lexer as L import qualified Jukebox.Form as Form-import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..), run, Theorem)+import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, newFunction, TypeOf(..), run, Theorem) import qualified Jukebox.Name as Name  -- The parser monad@@ -268,8 +268,8 @@   axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>     axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>     axiom NegatedConjecture <|>-    general Conjecture Form.Conjecture <|>-    general Question Form.Question+    general Conjecture (Form.Conjecture "conjecture") <|>+    general Question (Form.Conjecture "question")  -- A formula name. tag :: Parser Tag@@ -329,7 +329,7 @@                  else                    " has type " ++ showTypes (map rhs fs) ++                    " but was applied to " ++ plural (length args') "an argument" "arguments" ++-                   " of type " ++ prettyShow (map typ args')+                   " of type " ++ intercalate ", " (map (prettyShow . typ) args')  {-# INLINE lookupType #-} lookupType :: String -> Parser Type
src/Jukebox/TPTP/Print.hs view
@@ -298,8 +298,7 @@  instance Show Kind where   show (Axiom kind) = kind-  show Conjecture = "conjecture"-  show Question = "question"+  show (Conjecture kind) = kind  prettyNames :: Symbolic a => a -> a prettyNames x0 = mapName replace x
src/Jukebox/Toolbox.hs view
@@ -35,8 +35,11 @@ globalFlags =   inGroup "Output options" $   GlobalFlags <$>-    bool "quiet"-      ["Do not print any informational output."]+    -- Use flag rather than bool to avoid getting a --no-quiet option in the+    -- help message+    flag "quiet"+      ["Only print essential information."]+      False (pure True)  data TSTPFlags =   TSTPFlags {@@ -48,7 +51,8 @@   inGroup "Output options" $   TSTPFlags <$>     bool "tstp"-      ["Produce TSTP-friendly output."]+      ["Produce TSTP-compatible output (off by default)."]+      False  ---------------------------------------------------------------------- -- Printing output messages.@@ -122,7 +126,7 @@ writeFileBox =   inGroup "Output options" $   flag "output"-    ["Where to write the output file (defaults to stdout)."]+    ["Where to write the output file (stdout by default)."]     putStr     (fmap myWriteFile argFile)   where myWriteFile "/dev/null" _ = return ()@@ -145,8 +149,8 @@     flags =       inGroup "Input and clausifier options" $       flag "conjecture"-        ["If the problem has multiple conjectures, take only this one",-         "(conjectures are numbered from 1)"]+        ["If the problem has multiple conjectures, take only this one.",+         "Conjectures are numbered from 1."]         Nothing (Just <$> argNum)  oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)@@ -236,7 +240,7 @@   inGroup "Options for encoding types" $   choose <$>   flag "encoding"-    ["Which type encoding to use (defaults to guards)."]+    ["Which type encoding to use (guards by default)."]     "guards"     (argOption ["guards", "tags"])   <*> tagsFlags@@ -276,7 +280,7 @@     <$> expansive <*> universe   where universe = choose <$>                    flag "universe"-                   ["Which universe to find the model in (defaults to peano)."]+                   ["Which universe to find the model in (peano by default)."]                    "peano"                    (argOption ["peano", "trees"])         choose "peano" = Peano