jukebox 0.2.10 → 0.2.11

raw patch · 4 files changed

+3/−9 lines, 4 files

Files

• jukebox.cabal +1/−1
• src/Jukebox/Form.hs +1/−1
• src/Jukebox/TPTP/Print.hs +1/−1
• src/Jukebox/Toolbox.hs +0/−6

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

@@ -41,7 +41,7 @@       -- if there is a model of size >= tsize then there is a model of size tsize       tsize :: DomainSize } deriving Typeable -data FunType = FunType { args :: [Type], res :: Type } deriving (Eq, Typeable)+data FunType = FunType { args :: [Type], res :: Type } deriving (Eq, Ord, Typeable)  -- Helper function for defining (Eq, Ord) instances typeMaybeName :: Type -> Maybe Name

@@ -57,7 +57,7 @@     funcDecl (f ::: ty) = typeClause f (pPrint ty)     typeClause name ty =       pPrintClause "tff" "type" "type"-        (pPrint name <> colon <+> ty)+        (text (escapeAtom (show name)) <> colon <+> ty)  instance Pretty a => Pretty (Input a) where   pPrint = pPrintInput "tff" pPrint

@@ -76,7 +76,6 @@  clausifyIO :: GlobalFlags -> ClausifyFlags -> Problem Form -> IO CNF clausifyIO globals flags prob = do-  unless (quiet globals) $ hPutStrLn stderr "Clausifying problem..."   return $! clausify flags prob  toFofBox :: OptionParser (Problem Form -> IO (Problem Form))@@ -95,7 +94,6 @@ toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form) toFofIO globals clausify scheme f = do   CNF{..} <- clausify f-  unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."   -- In some cases we might get better results by considering each   -- problem (axioms + conjecture) separately, but no big deal.   m <- monotone (map what (axioms ++ concat conjectures))@@ -123,7 +121,6 @@  monotonicity :: GlobalFlags -> Problem Clause -> IO String monotonicity globals cs = do-  unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."   m <- monotone (map what cs)   let info (ty, Nothing) = [base ty ++ ": not monotone"]       info (ty, Just m) =@@ -139,7 +136,6 @@  annotateMonotonicityBox :: OptionParser (Problem Clause -> IO (Problem Clause)) annotateMonotonicityBox = (\globals x -> do-  unless (quiet globals) $ putStrLn "Monotonicity analysis..."   annotateMonotonicity x) <$> globalFlags  prettyPrintProblemBox :: OptionParser (Problem Form -> IO ())@@ -153,7 +149,6 @@  prettyPrintIO :: (a -> String) -> GlobalFlags -> (String -> IO ()) -> a -> IO () prettyPrintIO shw globals write prob = do-  unless (quiet globals) $ hPutStrLn stderr "Writing output..."   write (shw prob ++ "\n")  writeFileBox :: OptionParser (String -> IO ())@@ -202,7 +197,6 @@  inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type)) inferBox = (\globals prob -> do-  unless (quiet globals) $ putStrLn "Inferring types..."   return (run prob inferTypes)) <$> globalFlags  printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))