Jukebox.Toolbox

Documentation

data GlobalFlags

Constructors

GlobalFlags

Fields

quiet :: Bool

Instances

Show GlobalFlags

globalFlags :: OptionParser GlobalFlags

(=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c)

(=>>) :: (Monad m, Applicative f) => f (m a) -> f (m b) -> f (m b)

greetingBox :: Tool -> OptionParser (IO ())

greetingBoxIO :: Tool -> GlobalFlags -> IO ()

allFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())

allFiles :: (FilePath -> IO ()) -> [FilePath] -> IO ()

parseProblemBox :: OptionParser (FilePath -> IO (Problem Form))

parseProblemIO :: [FilePath] -> FilePath -> IO (Problem Form)

withString :: (Symbolic a, Pretty a) => String -> (Problem Form -> IO (Problem a)) -> String -> IO String

encodeString :: String -> IO String

clausifyBox :: OptionParser (Problem Form -> IO CNF)

clausifyIO :: GlobalFlags -> ClausifyFlags -> Problem Form -> IO CNF

toFofBox :: OptionParser (Problem Form -> IO (Problem Form))

oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))

oneConjecture :: CNF -> IO (Problem Clause)

toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)

schemeBox :: OptionParser Scheme

monotonicityBox :: OptionParser (Problem Clause -> IO String)

monotonicity :: GlobalFlags -> Problem Clause -> IO String

annotateMonotonicityBox :: OptionParser (Problem Clause -> IO (Problem Clause))

prettyPrintBox :: (Symbolic a, Pretty a) => OptionParser (Problem a -> IO ())

prettyFormIO :: (Symbolic a, Pretty a) => GlobalFlags -> (String -> IO ()) -> Problem a -> IO ()

prettyClauseBox :: OptionParser (Problem Clause -> IO ())

prettyPrintIO :: (Symbolic a, Pretty a) => GlobalFlags -> String -> (String -> IO ()) -> Problem a -> IO ()

writeFileBox :: OptionParser (String -> IO ())

guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))

guessModelIO :: [String] -> Universe -> Problem Form -> IO (Problem Form)

allObligsBox :: OptionParser ((Problem Clause -> IO Answer) -> Closed Obligs -> IO ())

allObligsIO :: (Closed [Input Clause] -> IO Answer) -> Closed Obligs -> IO ()

inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))

printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))

equinoxBox :: OptionParser (Problem Clause -> IO Answer)