hylotab-1.2.0: src/Main.hs
module Main
where
import Form ( Form, parse )
import Hylotab
import System.IO ( hPrint, stderr, hSetBuffering, stdin, BufferMode(LineBuffering))
import System.Exit ( exitWith, ExitCode(ExitFailure) )
import System.Console.GetOpt ( OptDescr(..), ArgDescr(..), ArgOrder(..),
getOpt, usageInfo )
import System.Environment ( getArgs, getProgName )
import System.CPUTime( getCPUTime )
import System.Timeout ( timeout )
import Control.Monad.Error (MonadError(..))
import Control.Applicative ( (<$>) )
import Prelude hiding ( catch, log )
import Control.Exception ( catch, SomeException )
import Control.Monad(unless)
main :: IO ()
main = do r <- runCmdLineVersion
`catch` \e -> do
let msg = show (e::SomeException)
unless (msg == "ExitSuccess") $ hPrint stderr msg
exit r_RUNTIME_ERROR
--
case r of
Nothing -> exit r_DID_NOT_RUN
Just Nothing -> exit r_TIMEOUT
Just (Just UNSAT) -> exit r_UNSAT
Just (Just (SAT _)) -> exit r_SAT
--
where r_SAT = 1
r_UNSAT = 2
r_TIMEOUT = 3
r_DID_NOT_RUN = 10
r_RUNTIME_ERROR = 13
exit :: Int -> IO a
exit = exitWith . ExitFailure
runCmdLineVersion :: IO (Maybe (Maybe SatFlag))
runCmdLineVersion =
do p_clp <- getParams
case p_clp of
Left err -> do putStrLn header
putStrLn err
progName <- getProgName
putStrLn $ "Try `" ++ progName ++ " --help' " ++
"for more information"
return Nothing
--
Right clp -> if showhelp clp
then do putStrLn header
progName <- getProgName
putStrLn $ usage (progName ++ " [OPTIONS]")
putStrLn gplTag
return Nothing
--
else Just <$> runWithParams clp
runWithParams :: Params -> IO (Maybe SatFlag)
runWithParams par =
do start <- getCPUTime
--
let myPutStrLn = if quietmode par then const (return ()) else putStrLn
--
let fromStdIn = do myPutStrLn $ "Reading from stdin (run again with" ++
"`--help' for usage options)"
hSetBuffering stdin LineBuffering
getContents
f <- parse <$> maybe fromStdIn readFile (filename par)
--
f `seq` myPutStrLn $ "\nInput:\n{ " ++ show f ++" }\nEnd of input\n"
--
let fcs = frameconds par
let md = expandmode par
let verbose = log par
--
unless (null fcs) $ myPutStrLn $ "\nAxioms:\n{ " ++ show fcs ++ " }\n"
--
result <- if maxtimeout par == 0
then Just <$> genSat verbose md fcs f
else timeout (maxtimeout par * (10::Int)^(6::Int))
(genSat verbose md fcs f)
--
case result of
Nothing -> myPutStrLn "TIMEOUT"
Just UNSAT -> myPutStrLn "not satisfiable"
Just (SAT nodes) -> myPutStrLn $ "satisfiable:\n" ++ extract (head nodes)
--
end <- getCPUTime
let elapsedTime = fromInteger (end - start) / 1000000000000.0
myPutStrLn $ "Elapsed time: " ++ show (elapsedTime :: Double)
--
return result
{- Command line parameters handling -}
data Params = Params { expandmode :: Mode,
maxtimeout :: Int,
showhelp :: Bool,
quietmode :: Bool,
frameconds :: [Form],
filename :: Maybe FilePath,
log :: Bool}
defaultParams :: Params
defaultParams = Params { expandmode = Extend,
maxtimeout = 0,
showhelp = False,
frameconds = [],
filename = Nothing,
quietmode = False,
log = False }
type ParamsModifier = Params -> Either ParsingErrMsg Params
type ParsingErrMsg = String
parseCmds :: [String] -> Params -> Either ParsingErrMsg Params
parseCmds argv par = case getOpt RequireOrder options argv of
(clpMods, [], []) -> thread clpMods par
( _,unk, []) -> fail $ "Unknown option: " ++
unwords unk
( _, _,errs) -> fail $ unlines errs
thread :: Monad m => [a -> m a] -> a -> m a
thread = foldr (\f g -> \a -> f a >>= g) return
options :: [OptDescr ParamsModifier]
options =
[Option ['h','?']
["help"]
(NoArg $ \p -> return p{showhelp = True})
"display this help and exit",
Option ['f']
["input-file"]
(ReqArg ((not . null) ?-> \s p -> return p{filename = Just s}) "file")
"obtain input formulas from file instead of stdin",
Option ['t']
["timeout"]
(ReqArg ((not . null) ?-> \s p -> return p{maxtimeout = read s}) "T")
"run for at most T seconds",
Option ['q']
["quiet", "silent"]
(NoArg $ \p -> return p{quietmode = True})
"suppress all normal output",
Option []
["min"]
(NoArg $ \p -> return p{expandmode = Try})
"search minimal model",
Option ['v']
["verbose"]
(NoArg $ \p -> return p{log = True})
"log tableau calculus"
] ++
map genAxiomOptions
[(["trans","k4"], trans, "transitivity (k4) axiom"),
(["intrans"], intrans, "intransitivity axiom"),
(["refl","kt"],refl, "reflexivity axiom"),
(["irrefl"], irrefl, "irreflexivity axiom"),
(["symm","kb"], symm, "symmetry axiom"),
(["asymm"], asymm, "asymmetry axiom"),
(["s4","kt4"], s4, "s4 axiom"),
(["s5"], s5, "s5 axiom"),
(["serial","kd"], serial, "serial (kd) axiom"),
(["euclid","k5"], euclid, "euclid (k5) axiom"),
(["kdb"], kdb, "kdb axiom"),
(["kd4"], kd4, "kd4 axiom"),
(["kd5"], kd5, "kd5 axiom"),
(["k45"], k45, "k45 axiom"),
(["kd45"], kd45, "kd45 axiom"),
(["kb4"], kb4, "kb4 axiom"),
(["ktb"], ktb, "ktb axiom"),
(["antisymm"], antisymm, "antisymmetry axiom")]
genAxiomOptions :: ([String],Form,String) -> OptDescr ParamsModifier
genAxiomOptions (flags, form, description)
= Option []
flags
(NoArg $ \p -> return p{frameconds = form:frameconds p})
description
(?->) :: (String -> Bool) -> (String -> ParamsModifier) -> String -> ParamsModifier
p ?-> m = \s -> if not (null s) && p s
then m s
else \_ -> throwError ("Invalid argument: '" ++ s ++ "'")
getParams :: IO (Either ParsingErrMsg Params)
getParams =
do cmdline_args <- getArgs
return $ parseCmds cmdline_args defaultParams
usage :: String -> String
usage hdr = usageInfo hdr options
showInfo :: IO ()
showInfo = putStrLn ("HyLoTab 1.2.0: no input file.\n" ++
"Usage: `--help' option gives basic information.\n")
header :: String
header = unlines ["Hylotab 1.2.0",
"J. van Eijck, G. Hoffmann. (c) 2002-2010."]
gplTag :: String
gplTag = unlines [
"This program is distributed in the hope that it will be useful,",
"but WITHOUT ANY WARRANTY; without even the implied warranty of",
"MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the",
"GNU General Public License for more details."]