jukebox 0.2.7 → 0.2.8

raw patch · 8 files changed

+199/−16 lines, 8 files

Files

dist/build/Jukebox/TPTP/Lexer.hs +179/−1
jukebox.cabal +1/−1
src/Jukebox/Form.hs +2/−1
src/Jukebox/Monotonox/ToFOF.hs +3/−1
src/Jukebox/SMTLIB.hs +2/−0
src/Jukebox/TPTP/Parse.hs +5/−6
src/Jukebox/TPTP/Print.hs +1/−1
src/Jukebox/Toolbox.hs +6/−5

dist/build/Jukebox/TPTP/Lexer.hs view

@@ -323,12 +323,190 @@   +{-# LINE 9 "<command-line>" #-}+{-# LINE 1 "/usr/lib/ghc-8.0.1/include/ghcversion.h" #-}    +++++++++++++ {-# LINE 9 "<command-line>" #-}-{-# LINE 1 "/usr/lib/ghc-7.10.3/include/ghcversion.h" #-}+{-# LINE 1 "/tmp/ghc684_0/ghc_2.h" #-}+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

jukebox.cabal view

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.7+Version: 0.2.8 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone

src/Jukebox/Form.hs view

@@ -543,7 +543,8 @@   term _ = mempty  isFof :: Symbolic a => a -> Bool-isFof f = length (types' f) <= 1+isFof _ = False+--isFof f = length (types' f) <= 1  uniqueNames :: Symbolic a => a -> NameM a uniqueNames t = evalStateT (aux Map.empty t) (Map.fromList [(x, t) | x ::: t <- Set.toList (free t)])

src/Jukebox/Monotonox/ToFOF.hs view

@@ -78,7 +78,9 @@                 Axiom -> prepare f                 Conjecture -> fmap notInwards (prepare (nt f))       typeI = Type (name "$i") (Finite 0) Infinite-  in Form.run (translate1 scheme mono f') (return . mapType (const typeI))+      trType O = O+      trType ty = typeI+  in Form.run (translate1 scheme mono f') (return . mapType trType)  -- Typing functions.

src/Jukebox/SMTLIB.hs view

@@ -25,6 +25,8 @@     , "and"     , "axiom"     , "inversion"+    , "bit0"+    , "bit1"     , "bitv"     , "bool"     , "check"

src/Jukebox/TPTP/Parse.hs view

@@ -8,7 +8,6 @@ import Jukebox.Form hiding (Pos, run) import Control.Exception import Data.List-import System.IO  parseString :: String -> IO (Problem Form) parseString xs =@@ -20,11 +19,11 @@     Parser.ParseStalled loc _ _ ->       error ("Include directive found at " ++ show loc) -parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))-parseProblem dirs name = parseProblemWith (findFileTPTP dirs) name+parseProblem :: (FilePath -> IO ()) -> [FilePath] -> FilePath -> IO (Either String (Problem Form))+parseProblem found dirs name = parseProblemWith found (findFileTPTP dirs) name -parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))-parseProblemWith findFile name =+parseProblemWith :: (FilePath -> IO ()) -> (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))+parseProblemWith found findFile name =   runExceptT $ do     file <- readInFile (Parser.Location "<command line>" 0 0) name     process (Parser.parseProblem name file)@@ -41,7 +40,7 @@           err pos ("File '" ++ name ++ "' not found")         Just file ->           ExceptT $ do-            liftIO $ hPutStrLn stderr $ "Reading " ++ file ++ "..."+            liftIO (found file)             fmap Right (readFile file) `catch`               \(e :: IOException) -> return (Left (show e))

src/Jukebox/TPTP/Print.hs view

@@ -37,7 +37,7 @@ showProblem = show . pPrintProblem  isReallyFof :: Symbolic a => a -> Bool-isReallyFof = all p . types+isReallyFof = const False -- all p . types   where     p O = True     p (Type ty _ _) | ty == i = True

src/Jukebox/Toolbox.hs view

@@ -59,11 +59,12 @@ allFiles f xs = mapM_ f xs  parseProblemBox :: OptionParser (FilePath -> IO (Problem Form))-parseProblemBox = parseProblemIO <$> findFileFlags+parseProblemBox = parseProblemIO <$> globalFlags <*> findFileFlags -parseProblemIO :: [FilePath] -> FilePath -> IO (Problem Form)-parseProblemIO dirs f = do-  r <- parseProblem dirs f+parseProblemIO :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form)+parseProblemIO flags dirs f = do+  let found file = unless (quiet flags) $ hPutStrLn stderr $ "Reading " ++ file ++ "..."+  r <- parseProblem found dirs f   case r of     Left err -> do       hPutStrLn stderr err@@ -197,7 +198,7 @@             NoAnswer x -> result (show x)         multi = length conjectures > 1         part i = show i ++ "/" ++ show (length conjectures)-        result x = putStrLn ("+++ RESULT: " ++ x)+        result x = putStrLn ("% SZS status " ++ x)  inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type)) inferBox = (\globals prob -> do