-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A first-order reasoning toolbox
--   
@package jukebox
@version 0.1

module Jukebox.Sat
data Solver :: *
newSolver :: IO Solver
deleteSolver :: Solver -> IO ()
data Lit :: *
neg :: Lit -> Lit
false :: Lit
true :: Lit
class SatSolver s
getSolver :: SatSolver s => s -> Solver
newLit :: SatSolver s => s -> IO Lit
addClause :: SatSolver s => s -> [Lit] -> IO ()
solve :: SatSolver s => s -> [Lit] -> IO Bool
conflict :: SatSolver s => s -> IO [Lit]
modelValue :: SatSolver s => s -> Lit -> IO (Maybe Bool)
value :: SatSolver s => s -> Lit -> IO (Maybe Bool)
instance SatSolver Solver

module Jukebox.SatMin
solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
localMin :: SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()

module Jukebox.Sat3
data Lit3
Lit3 :: Lit -> Lit -> Lit3
isFalse :: Lit3 -> Lit
isTrue :: Lit3 -> Lit
false3 :: Lit3
bottom3 :: Lit3
true3 :: Lit3
neg3 :: Lit3 -> Lit3
newLit3 :: SatSolver s => s -> IO Lit3
newLit2 :: SatSolver s => s -> IO Lit3
modelValue3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
value3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
val3 :: (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)

module Jukebox.SatEq
data SolverEq
SolverEq :: Solver -> IORef Int -> IORef (Map (Elt, Elt) Lit3) -> IORef (Maybe (Map Elt Elt)) -> SolverEq
satSolver :: SolverEq -> Solver
counter :: SolverEq -> IORef Int
table :: SolverEq -> IORef (Map (Elt, Elt) Lit3)
model :: SolverEq -> IORef (Maybe (Map Elt Elt))
newSolverEq :: Solver -> IO SolverEq
class SatSolver s => EqSolver s
getSolverEq :: EqSolver s => s -> SolverEq
newtype Elt
Elt :: Int -> Elt
newElt :: EqSolver s => s -> IO Elt
equal :: EqSolver s => s -> Elt -> Elt -> IO Lit3
solveEq :: EqSolver s => s -> [Lit] -> IO Bool
modelRep :: EqSolver s => s -> Elt -> IO (Maybe Elt)
instance Eq Elt
instance Ord Elt
instance Show Elt
instance EqSolver SolverEq
instance SatSolver SolverEq

module Jukebox.TPTP.Lexer
scan :: ByteString -> TokenStream
data Pos
Pos :: {-# UNPACK #-} !Word -> {-# UNPACK #-} !Word -> Pos
data Token
Atom :: !Keyword -> !ByteString -> Token
keyword :: Token -> !Keyword
name :: Token -> !ByteString
Defined :: !Defined -> Token
defined :: Token -> !Defined
Var :: !ByteString -> Token
name :: Token -> !ByteString
DistinctObject :: !ByteString -> Token
name :: Token -> !ByteString
Number :: !Integer -> Token
value :: Token -> !Integer
Punct :: !Punct -> Token
kind :: Token -> !Punct
Eof :: Token
Error :: Token
data Punct
LParen :: Punct
RParen :: Punct
LBrack :: Punct
RBrack :: Punct
Comma :: Punct
Dot :: Punct
Or :: Punct
And :: Punct
Not :: Punct
Iff :: Punct
Implies :: Punct
Follows :: Punct
Xor :: Punct
Nor :: Punct
Nand :: Punct
Eq :: Punct
Neq :: Punct
ForAll :: Punct
Exists :: Punct
Let :: Punct
LetTerm :: Punct
Colon :: Punct
Times :: Punct
Plus :: Punct
FunArrow :: Punct
Lambda :: Punct
Apply :: Punct
ForAllLam :: Punct
ExistsLam :: Punct
DependentProduct :: Punct
DependentSum :: Punct
Some :: Punct
The :: Punct
Subtype :: Punct
SequentArrow :: Punct
data Defined
DTrue :: Defined
DFalse :: Defined
DEqual :: Defined
DDistinct :: Defined
DItef :: Defined
DItet :: Defined
DO :: Defined
DI :: Defined
DTType :: Defined
data Keyword
Normal :: Keyword
Thf :: Keyword
Tff :: Keyword
Fof :: Keyword
Cnf :: Keyword
Axiom :: Keyword
Hypothesis :: Keyword
Definition :: Keyword
Assumption :: Keyword
Lemma :: Keyword
Theorem :: Keyword
Conjecture :: Keyword
NegatedConjecture :: Keyword
Question :: Keyword
Plain :: Keyword
FiDomain :: Keyword
FiHypothesis :: Keyword
FiPredicates :: Keyword
Type :: Keyword
Unknown :: Keyword
Include :: Keyword
data TokenStream
At :: {-# UNPACK #-} !Pos -> !Contents -> TokenStream
data Contents
Cons :: !Token -> TokenStream -> Contents
instance Show Pos
instance Eq Keyword
instance Ord Keyword
instance Eq Defined
instance Ord Defined
instance Eq Punct
instance Ord Punct
instance Functor AlexLastAcc
instance Show Punct
instance Show Defined
instance Show Keyword

module Jukebox.TPTP.Parsec
newtype Parsec a b
Parsec :: (forall c. (b -> Reply a c -> a -> Reply a c) -> Reply a c -> a -> Reply a c) -> Parsec a b
runParsec :: Parsec a b -> forall c. (b -> Reply a c -> a -> Reply a c) -> Reply a c -> a -> Reply a c
type Reply a b = [String] -> Result (Position a) b
data Result a b
Ok :: a -> b -> Result a b
Error :: a -> String -> Result a b
Expected :: a -> [String] -> Result a b
parseError :: [String] -> Parsec a b
fatalError :: Stream a c => String -> Parsec a b
nonempty :: Parsec a b -> Parsec a b
skipSome :: Parsec a b -> Parsec a ()
skipMany :: Parsec a b -> Parsec a ()
(<?>) :: Parsec a b -> String -> Parsec a b
between :: Parsec a b -> Parsec a c -> Parsec a d -> Parsec a d
sepBy1 :: Parsec a b -> Parsec a c -> Parsec a [b]
run_ :: Stream a c => Parsec a b -> a -> Result (Position a) b
run :: Stream a c => (Position a -> [String]) -> Parsec a b -> a -> (Position a, Either [String] b)
expected :: [String] -> [String] -> [String]
class Stream a b | a -> b where type family Position a
primToken :: Stream a b => a -> (a -> b -> c) -> c -> (String -> c) -> c
position :: Stream a b => a -> Position a
next :: Stream a b => Parsec a b
cut :: Stream a b => Parsec a ()
cut' :: Stream a b => Parsec a c -> Parsec a c
satisfy :: Stream a b => (b -> Bool) -> Parsec a b
eof :: Stream a b => Parsec a ()
data UserState state stream
UserState :: !state -> !stream -> UserState state stream
userState :: UserState state stream -> !state
userStream :: UserState state stream -> !stream
getState :: Parsec (UserState state a) state
putState :: state -> Parsec (UserState state a) ()
instance Stream a b => Stream (UserState state a) b
instance Alternative (Parsec a)
instance Applicative (Parsec a)
instance MonadPlus (Parsec a)
instance Monad (Parsec a)
instance Functor (Parsec a)

module Jukebox.ProgressBar
data ProgressBar
ProgressBar :: IO () -> (String -> IO ()) -> IO () -> ProgressBar
tick :: ProgressBar -> IO ()
enter :: ProgressBar -> String -> IO ()
leave :: ProgressBar -> IO ()
tickOnRead :: ProgressBar -> ByteString -> IO ByteString
withProgressBar :: (ProgressBar -> IO a) -> IO a

module Jukebox.Options
data Annotated d p a
Annotated :: d -> p a -> Annotated d p a
descr :: Annotated d p a -> d
parser :: Annotated d p a -> p a
type ArgParser = Annotated ArgDesc SeqParser
type ArgDesc = String
data SeqParser a
SeqParser :: Int -> ([String] -> Either Error a) -> SeqParser a
args :: SeqParser a -> Int
consume :: SeqParser a -> [String] -> Either Error a
arg :: ArgDesc -> String -> (String -> Maybe a) -> ArgParser a
argNum :: (Read a, Num a) => ArgParser a
argFile :: ArgParser FilePath
argFiles :: ArgParser [FilePath]
argName :: ArgParser FilePath
argNums :: ArgParser [Int]
argOption :: [String] -> ArgParser String
argList :: [String] -> ArgParser [String]
argUsage :: ExitCode -> [String] -> ArgParser a
type OptionParser = Annotated [Flag] ParParser
data ParParser a
ParParser :: IO a -> ([String] -> ParseResult a) -> ParParser a
val :: ParParser a -> IO a
peek :: ParParser a -> [String] -> ParseResult a
data ParseResult a
Yes :: Int -> (ParParser a) -> ParseResult a
No :: (ParParser a) -> ParseResult a
Error :: Error -> ParseResult a
data Error
Mistake :: String -> Error
Usage :: ExitCode -> [String] -> Error
runPar :: ParParser a -> [String] -> Either Error (IO a)
awaitP :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a
await :: String -> a -> ([String] -> ParseResult a) -> ParParser a
data Flag
Flag :: String -> String -> [String] -> String -> Flag
flagName :: Flag -> String
flagGroup :: Flag -> String
flagHelp :: Flag -> [String]
flagArgs :: Flag -> String
flag :: String -> [String] -> a -> ArgParser a -> OptionParser a
manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a]
filenames :: OptionParser [String]
io :: IO a -> OptionParser a
bool :: String -> [String] -> OptionParser Bool
inGroup :: String -> OptionParser a -> OptionParser a
type ToolParser = Annotated [Tool] PrefixParser
data Tool
Tool :: String -> String -> String -> String -> Tool
toolProgName :: Tool -> String
toolName :: Tool -> String
toolVersion :: Tool -> String
toolHelp :: Tool -> String
newtype PrefixParser a
PrefixParser :: (String -> Maybe (Tool, ParParser a)) -> PrefixParser a
runPref :: PrefixParser a -> [String] -> Either Error (IO a)
tool :: Tool -> OptionParser a -> ToolParser a
getEffectiveArgs :: ToolParser a -> IO [String]
parseCommandLine :: Tool -> ToolParser a -> IO a
printHelp :: ExitCode -> [String] -> IO a
argError :: Tool -> String -> [String]
usageTool :: Tool -> String -> [String] -> String -> ToolParser a
versionTool :: Tool -> ToolParser a
helpTool :: Tool -> ToolParser a -> ToolParser a
help :: Tool -> OptionParser a -> [String]
greeting :: Tool -> String
usage :: Tool -> String -> [String]
justify :: String -> [String] -> [String]
instance Eq Flag
instance Show Flag
instance Monoid (PrefixParser a)
instance Functor PrefixParser
instance Applicative ParseResult
instance Functor ParseResult
instance Applicative ParParser
instance Functor ParParser
instance Applicative SeqParser
instance Functor SeqParser
instance (Monoid d, Monoid (p a)) => Monoid (Annotated d p a)
instance (Monoid d, Applicative p) => Applicative (Annotated d p)
instance Functor p => Functor (Annotated d p)

module Jukebox.TPTP.FindFile
findFile :: [FilePath] -> FilePath -> IO (Maybe FilePath)
findFileTPTP :: [FilePath] -> FilePath -> IO (Maybe FilePath)
getTPTPDirs :: IO [FilePath]
findFileFlags :: Annotated [Flag] ParParser [[Char]]

module Jukebox.Map
type Map a b = HashMap a b
fromList :: (Hashable k, Eq k) => [(k, v)] -> HashMap k v
toList :: HashMap k v -> [(k, v)]
insertWith :: (Hashable k, Eq k) => (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
empty :: HashMap k v
findWithDefault :: (Hashable k, Eq k) => v -> k -> HashMap k v -> v
lookup :: (Hashable k, Eq k) => k -> HashMap k v -> Maybe v
insert :: (Hashable k, Eq k) => k -> v -> HashMap k v -> HashMap k v
delete :: (Hashable k, Eq k) => k -> HashMap k v -> HashMap k v
elems :: HashMap k v -> [v]
union :: (Hashable k, Eq k) => HashMap k v -> HashMap k v -> HashMap k v
intersection :: (Hashable k, Eq k) => HashMap k v -> HashMap k w -> HashMap k v
null :: HashMap k v -> Bool
(!) :: (Hashable k, Eq k) => HashMap k v -> k -> v
member :: (Hashable k, Eq k) => k -> HashMap k v -> Bool
(\\) :: (Hashable k, Eq k) => HashMap k v1 -> HashMap k v -> HashMap k v1

module Jukebox.UnionFind
type UF a = State (S a)
data Replacement a
(:>) :: a -> a -> Replacement a
(=:=) :: (Hashable a, Ord a) => a -> a -> UF a (Maybe (Replacement a))
rep :: (Hashable a, Ord a) => a -> UF a a
evalUF :: S a -> UF a b -> b
execUF :: S a -> UF a b -> S a
runUF :: S a -> UF a b -> (b, S a)
type S a = Map a a
isRep :: (Hashable a, Ord a) => a -> UF a Bool
initial :: S a
reps :: (Hashable a, Ord a) => UF a (a -> a)

module Jukebox.Seq
data Seq a
Append :: (Seq a) -> (Seq a) -> Seq a
Unit :: a -> Seq a
Nil :: Seq a
class List f
fromList :: List f => f a -> Seq a
toList :: List f => f a -> [a]
appendA :: Seq a -> Seq a -> Seq a
cons :: a -> Seq a -> Seq a
snoc :: Seq a -> a -> Seq a
append :: (List f, List g) => f a -> g a -> Seq a
concat :: (List f, List g) => f (g a) -> Seq a
concatMap :: (List f, List g) => (a -> g b) -> f a -> Seq b
concatMapA :: (a -> Seq b) -> Seq a -> Seq b
fold :: (b -> b -> b) -> (a -> b) -> b -> Seq a -> b
unique :: (Ord a, Hashable a, List f) => f a -> [a]
length :: Seq a -> Int
mapM :: Monad m => (a -> m b) -> Seq a -> m (Seq b)
mapM_ :: Monad m => (a -> m ()) -> Seq a -> m ()
sequence :: Monad m => Seq (m a) -> m (Seq a)
instance Monoid (Seq a)
instance MonadPlus Seq
instance Monad Seq
instance Functor Seq
instance Show a => Show (Seq a)
instance List Seq
instance List []

module Jukebox.Utils
usort :: Ord a => [a] -> [a]
merge :: Ord a => [a] -> [a] -> [a]
nub :: (List f, Ord a, Hashable a) => f a -> [a]
popen :: FilePath -> [String] -> ByteString -> IO (ExitCode, ByteString)

module Jukebox.Name
data Name
uniqueId :: Name -> Int64
base :: Name -> ByteString
stringBaseName :: Named a => a -> String
unsafeMakeName :: Int64 -> ByteString -> Name
data (:::) a b
(:::) :: !a -> !b -> (:::) a b
lhs :: (a ::: b) -> a
rhs :: (a ::: b) -> b
class Named a where baseName = base . name
name :: Named a => a -> Name
baseName :: Named a => a -> ByteString
data Closed a
close :: Closed a -> (a -> NameM b) -> Closed b
close_ :: Closed a -> NameM b -> Closed b
closedIO :: Closed (IO a) -> IO (Closed a)
open :: Closed a -> a
closed0 :: Closed ()
stdNames :: Closed [Name]
nameO :: Name
nameI :: Name
data NameM a
newName :: Named a => a -> NameM Name
unsafeClose :: Int64 -> a -> Closed a
maxIndex :: Closed a -> Int64
supply :: (Closed () -> Closed a) -> NameM a
uniquify :: [Name] -> (Name -> ByteString)
instance Typeable Name
instance Typeable (:::)
instance Typeable Closed
instance (Show a, Show b) => Show (a ::: b)
instance Functor NameM
instance Monad NameM
instance Functor Closed
instance Named a => Named (a ::: b)
instance Named a => Hashable (a ::: b)
instance Named a => Ord (a ::: b)
instance Named a => Eq (a ::: b)
instance Named Name
instance Named [Char]
instance Named ByteString
instance Show Name
instance Hashable Name
instance Ord Name
instance Eq Name

module Jukebox.NameMap
type NameMap a = Map Int64 a
lookup :: Name -> NameMap a -> Maybe a
lookup_ :: Named a => a -> NameMap b -> b
insert :: Named a => a -> NameMap a -> NameMap a
member :: Named a => a -> NameMap a -> Bool
delete :: Named a => a -> NameMap a -> NameMap a
(!) :: NameMap a -> Name -> a
fromList :: (List f, Named a) => f a -> NameMap a
toList :: NameMap a -> [a]
singleton :: Named a => a -> NameMap a

module Jukebox.Form
debugging :: Bool
data DomainSize
Finite :: Int -> DomainSize
Infinite :: DomainSize
data Type
O :: Type
Type :: {-# UNPACK #-} !Name -> DomainSize -> DomainSize -> Type
tname :: Type -> {-# UNPACK #-} !Name
tmonotone :: Type -> DomainSize
tsize :: Type -> DomainSize
data FunType
FunType :: [Type] -> Type -> FunType
args :: FunType -> [Type]
res :: FunType -> Type
typeMaybeName :: Type -> Maybe Name
class Typed a
typ :: Typed a => a -> Type
type Variable = Name ::: Type
type Function = Name ::: FunType
data Term
Var :: Variable -> Term
(:@:) :: Function -> [Term] -> Term
newSymbol :: Named a => a -> b -> NameM (Name ::: b)
newFunction :: Named a => a -> [Type] -> Type -> NameM Function
newType :: Named a => a -> NameM Type
funArgs :: Function -> [Type]
arity :: Function -> Int
size :: Term -> Int
data Atomic
(:=:) :: Term -> Term -> Atomic
Tru :: Term -> Atomic
normAtomic :: Atomic -> Either (Term, Term) Term
data Signed a
Pos :: a -> Signed a
Neg :: a -> Signed a
type Literal = Signed Atomic
neg :: Signed a -> Signed a
the :: Signed a -> a
pos :: Signed a -> Bool
signForm :: Signed a -> Form -> Form
data Form
Literal :: Literal -> Form
Not :: Form -> Form
And :: (Seq Form) -> Form
Or :: (Seq Form) -> Form
Equiv :: Form -> Form -> Form
ForAll :: {-# UNPACK #-} !(Bind Form) -> Form
Exists :: {-# UNPACK #-} !(Bind Form) -> Form
Connective :: Connective -> Form -> Form -> Form
data Connective
Implies :: Connective
Follows :: Connective
Xor :: Connective
Nor :: Connective
Nand :: Connective
connective :: Connective -> Form -> Form -> Form
data Bind a
Bind :: (NameMap Variable) -> a -> Bind a
true :: Form
false :: Form
isTrue :: Form -> Bool
isFalse :: Form -> Bool
nt :: Form -> Form
(.=>.) :: Form -> Form -> Form
(.=.) :: Term -> Term -> Form
(/\) :: Form -> Form -> Form
(\/) :: Form -> Form -> Form
closeForm :: Form -> Form
conj :: List f => f Form -> Form
disj :: List f => f Form -> Form
positive :: Form -> Form
notInwards :: Form -> Form
simple :: Form -> Form
simplify :: Form -> Form
type CNF = Closed Obligs
data Obligs
Obligs :: [Input Clause] -> [[Input Clause]] -> String -> String -> Obligs
axioms :: Obligs -> [Input Clause]
conjectures :: Obligs -> [[Input Clause]]
satisfiable :: Obligs -> String
unsatisfiable :: Obligs -> String
toObligs :: [Input Clause] -> [[Input Clause]] -> Obligs
newtype Clause
Clause :: (Bind [Literal]) -> Clause
clause :: List f => f (Signed Atomic) -> Clause
toForm :: Clause -> Form
toLiterals :: Clause -> [Literal]
type Tag = ByteString
data Kind
Axiom :: Kind
Conjecture :: Kind
Question :: Kind
data Answer
Satisfiable :: Answer
Unsatisfiable :: Answer
NoAnswer :: NoAnswerReason -> Answer
data NoAnswerReason
GaveUp :: NoAnswerReason
Timeout :: NoAnswerReason
data Input a
Input :: Tag -> Kind -> a -> Input a
tag :: Input a -> Tag
kind :: Input a -> Kind
what :: Input a -> a
type Problem a = Closed [Input a]
data TypeOf a
Form :: TypeOf Form
Clause_ :: TypeOf Clause
Term :: TypeOf Term
Atomic :: TypeOf Atomic
Signed :: TypeOf (Signed a)
Bind_ :: TypeOf (Bind a)
List :: TypeOf [a]
Seq :: TypeOf (Seq a)
Input_ :: TypeOf (Input a)
Obligs_ :: TypeOf Obligs
class Symbolic a
typeOf :: Symbolic a => a -> TypeOf a
data Rep a
Const :: !a -> Rep a
Unary :: (a -> b) -> a -> Rep b
Binary :: (a -> b -> c) -> a -> b -> Rep c
rep :: Symbolic a => a -> Rep a
class Unpack a
rep' :: Unpack a => a -> Rep a
recursively :: Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursivelyM :: (Monad m, Symbolic a) => (forall a. Symbolic a => a -> m a) -> a -> m a
collect :: (Symbolic a, Monoid b) => (forall a. Symbolic a => a -> b) -> a -> b
type Subst = NameMap (Name ::: Term)
ids :: Subst
(|=>) :: Named a => a -> Term -> Subst
(|+|) :: Subst -> Subst -> Subst
subst :: Symbolic a => Subst -> a -> a
free :: Symbolic a => a -> NameMap Variable
ground :: Symbolic a => a -> Bool
bind :: Symbolic a => a -> Bind a
termsAndBinders :: Symbolic a => (Term -> Seq b) -> (forall a. Symbolic a => Bind a -> Seq b) -> a -> Seq b
names :: Symbolic a => a -> [Name]
types :: Symbolic a => a -> [Type]
types' :: Symbolic a => a -> [Type]
terms :: Symbolic a => a -> [Term]
vars :: Symbolic a => a -> [Variable]
functions :: Symbolic a => a -> [Function]
isFof :: Symbolic a => a -> Bool
uniqueNames :: Symbolic a => a -> NameM a
force :: Symbolic a => a -> a
check :: Symbolic a => a -> a
checkBinder :: NameMap Variable -> Subst -> Subst
type ShareState = (NameMap Type, NameMap Variable, NameMap Function)
share :: Symbolic a => a -> a
mapType :: Symbolic a => (Type -> Type) -> a -> a
instance Typeable DomainSize
instance Typeable Type
instance Typeable FunType
instance Eq DomainSize
instance Ord DomainSize
instance Show DomainSize
instance Eq FunType
instance Eq Term
instance Ord Term
instance Show a => Show (Signed a)
instance Eq a => Eq (Signed a)
instance Ord a => Ord (Signed a)
instance Eq Kind
instance Ord Kind
instance Eq NoAnswerReason
instance Ord NoAnswerReason
instance Show NoAnswerReason
instance Eq Answer
instance Ord Answer
instance Unpack Obligs
instance Symbolic a => Unpack (Input a)
instance Symbolic a => Unpack (Seq a)
instance Symbolic a => Unpack [a]
instance Symbolic a => Unpack (Bind a)
instance Symbolic a => Unpack (Signed a)
instance Unpack Atomic
instance Unpack Term
instance Unpack Clause
instance Unpack Form
instance Symbolic Obligs
instance Symbolic a => Symbolic (Input a)
instance Symbolic a => Symbolic (Seq a)
instance Symbolic a => Symbolic [a]
instance Symbolic a => Symbolic (Bind a)
instance Symbolic a => Symbolic (Signed a)
instance Symbolic Atomic
instance Symbolic Term
instance Symbolic Clause
instance Symbolic Form
instance Functor Input
instance Show Answer
instance Functor Signed
instance Hashable a => Hashable (Signed a)
instance Hashable Atomic
instance Ord Atomic
instance Eq Atomic
instance Typed Term
instance Named Term
instance Hashable Term
instance Typed b => Typed (a ::: b)
instance Typed FunType
instance Typed Type
instance Named Type
instance Hashable Type
instance Ord Type
instance Eq Type

module Jukebox.TPTP.Print
prettyShow :: Pretty a => a -> String
chattyShow :: Pretty a => a -> String
prettyFormula :: (Pretty a, Symbolic a) => a -> String
prettyProblem :: (Symbolic a, Pretty a) => String -> Level -> Problem a -> Doc
data Level
Normal :: Level
Chatty :: Level
class Pretty a
instance Eq Level
instance Ord Level
instance Show Kind
instance Show Connective
instance Show Form
instance Pretty Form
instance Show Clause
instance Pretty Clause
instance Show Atomic
instance Pretty Atomic
instance Show Term
instance Pretty [Term]
instance Pretty Term
instance Pretty a => Show (Input a)
instance Pretty a => Pretty (Input a)
instance (Symbolic a, Pretty a) => Show (Problem a)
instance Pretty [Type]
instance Show FunType
instance Pretty FunType
instance Show Token
instance Show Type
instance Pretty Type
instance Pretty Name

module Jukebox.HighSat
newtype Sat1 a b
Sat1 :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b
runSat1_ :: Sat1 a b -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b
newtype Sat a b c
Sat :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Sat a b c
runSat_ :: Sat a b c -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c
data SatState a
SatState :: Solver -> (Map a Lit) -> SatState a
type Watch a = a -> Sat1 a ()
data Form a
Lit :: (Signed a) -> Form a
And :: (Seq (Form a)) -> Form a
Or :: (Seq (Form a)) -> Form a
nt :: Form a -> Form a
conj :: List f => f (Form a) -> Form a
disj :: List f => f (Form a) -> Form a
true :: Form a
false :: Form a
unique :: List f => f (Form a) -> Form a
runSat :: (Hashable b, Ord b) => Watch a -> [b] -> Sat a b c -> IO c
runSat1 :: (Ord a, Hashable a) => Watch a -> Sat1 a b -> IO b
atIndex :: (Ord a, Hashable a, Ord b, Hashable b) => b -> Sat1 a c -> Sat a b c
solve :: (Ord a, Hashable a) => [Signed a] -> Sat1 a Bool
model :: (Ord a, Hashable a) => Sat1 a (a -> Bool)
modelValue :: (Ord a, Hashable a) => a -> Sat1 a Bool
addForm :: (Ord a, Hashable a) => Form a -> Sat1 a ()
flatten :: (Ord a, Hashable a) => Form a -> Sat1 a (Seq (Seq Lit))
lit :: (Ord a, Hashable a) => Signed a -> Sat1 a Lit
var :: (Ord a, Hashable a) => a -> Sat1 a Lit
instance Functor (Sat1 a)
instance Monad (Sat1 a)
instance MonadIO (Sat1 a)
instance Functor (Sat a b)
instance Monad (Sat a b)
instance MonadIO (Sat a b)

module Jukebox.InferTypes
type Function' = Name ::: ([Type'], Type')
type Variable' = Name ::: Type'
type Type' = Name ::: Type
inferTypes :: [Input Clause] -> NameM ([Input Clause], Type -> Type)
solve :: NameMap Function' -> NameMap Variable' -> [Input Clause] -> ([Input Clause], Name -> Name)
generate :: NameMap Function' -> NameMap Variable' -> [Input Clause] -> UF Name ()

module Jukebox.Monotonox.Monotonicity
data Extension
TrueExtend :: Extension
FalseExtend :: Extension
CopyExtend :: Extension
data Var
FalseExtended :: Function -> Var
TrueExtended :: Function -> Var
annotateMonotonicity :: Problem Clause -> IO (Problem Clause)
monotone :: [Clause] -> IO (NameMap (Type ::: Maybe (NameMap (Function ::: Extension))))
fromModel :: [Function] -> Type -> (Var -> Bool) -> NameMap (Function ::: Extension)
extension :: Function -> (Var -> Bool) -> Extension
clause :: [Literal] -> Sat Var Type ()
literal :: [Literal] -> Literal -> Sat Var Type ()
safe :: [Literal] -> Term -> Form Var
guards :: Literal -> Variable -> Form Var
instance Show Extension
instance Eq Var
instance Ord Var
instance Hashable Var

module Jukebox.TPTP.ClauseParser
data ParseState
MkState :: ![Input Form] -> !(Map ByteString Type) -> !(Map ByteString (Name ::: FunType)) -> !(Map ByteString (Name ::: Type)) -> Type -> !(Closed ()) -> ParseState
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream
data IncludeStatement
Include :: ByteString -> (Maybe [Tag]) -> IncludeStatement
initialState :: ParseState
testParser :: Parser a -> String -> Either [String] a
getProblem :: Parser [Input Form]
keyword' :: Stream a Token => (Keyword -> Bool) -> Parsec a Token
keyword :: Stream a Token => Keyword -> Parsec a Token
punct' :: Stream a Token => (Punct -> Bool) -> Parsec a Token
punct :: Stream a Token => Punct -> Parsec a Token
defined' :: Stream a Token => (Defined -> Bool) -> Parsec a Defined
defined :: Stream a Token => Defined -> Parsec a Defined
variable :: Parsec ParsecState ByteString
number :: Parsec ParsecState Integer
atom :: Parsec ParsecState ByteString
parens :: Parser a -> Parser a
bracks :: Parser a -> Parser a
binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a
section :: (Tag -> Bool) -> Parser (Maybe IncludeStatement)
input :: (Tag -> Bool) -> Parser ()
kind :: Parser (Tag -> Form -> Input Form)
tag :: Parser Tag
include :: Parser IncludeStatement
newFormula :: Input Form -> Parser ()
newNameFrom :: Named a => Closed () -> a -> (Closed (), Name)
findType :: ByteString -> Parser Type
newFunction :: ByteString -> FunType -> Parser (Name ::: FunType)
applyFunction :: ByteString -> [Term] -> Type -> Parser Term
typeError :: Stream a c => (:::) Name FunType -> [Term] -> Parsec a b
lookupFunction :: FunType -> ByteString -> Parser (Name ::: FunType)
individual :: Parser Type
cnf :: Parser Form
fof :: Parser Form
tff :: Parser Form
data Thing
Apply :: !ByteString -> ![Term] -> Thing
Term :: !Term -> Thing
Formula :: !Form -> Thing
class TermLike a
fromThing :: TermLike a => Thing -> Parser a
var :: (TermLike a, ?ctx :: Maybe (Map ByteString Variable)) => Parser a
parser :: (TermLike a, ?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable)) => Parser a
class TermLike a => FormulaLike a
fromFormula :: FormulaLike a => Form -> a
term :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), TermLike a) => Parser a
literal :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
formula :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
quantified :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
unitary :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
varDecl :: Bool -> Parser Variable
type_ :: Parser Type
data Type_
TType :: Type_
Fun :: [Type] -> Type -> Type_
Prod :: [Type] -> Type_
prod :: Type_ -> Type_ -> Parser Type_
arrow :: Type_ -> Type_ -> Parser Type_
leaf :: Parser Type_
compoundType :: Parser Type_
typeDeclaration :: Parser ()
instance Show IncludeStatement
instance FormulaLike Thing
instance FormulaLike Form
instance TermLike Thing
instance TermLike Term
instance TermLike Form
instance Show Thing
instance Stream TokenStream Token

module Jukebox.TPTP.ParseSnippet
tff :: [(String, Type)] -> [(String, Function)] -> String -> NameM Form
cnf :: [(String, Type)] -> [(String, Function)] -> String -> NameM Form
form :: Parsec (UserState ParseState TokenStream) a -> [([Char], Type)] -> [(String, (:::) Name FunType)] -> [Char] -> NameM a
form' :: Parsec (UserState ParseState TokenStream) b -> [([Char], Type)] -> [(String, (:::) Name FunType)] -> [Char] -> Closed () -> Closed b

module Jukebox.Provers.E
data EFlags
EFlags :: String -> Maybe Int -> Maybe Int -> EFlags
eprover :: EFlags -> String
timeout :: EFlags -> Maybe Int
memory :: EFlags -> Maybe Int
eflags :: OptionParser EFlags
mangleAnswer :: Symbolic a => a -> NameM a
runE :: (Pretty a, Symbolic a) => EFlags -> Problem a -> IO (Either Answer [Term])
extractAnswer :: Symbolic a => a -> String -> Either Answer [Term]

module Jukebox.TPTP.ParseProblem
parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> ProgressBar -> FilePath -> IO (Either String (Problem Form))

module Jukebox.Clausify
newtype ClausifyFlags
ClausifyFlags :: Bool -> ClausifyFlags
splitting :: ClausifyFlags -> Bool
clausifyFlags :: OptionParser ClausifyFlags
clausify :: ClausifyFlags -> Problem Form -> CNF
split :: Form -> [Form]
clausForm :: ByteString -> Form -> M [Input Clause]
miniscope :: Form -> M Form
forAll :: NameMap Variable -> Form -> M Form
forAllOr :: NameMap Variable -> [(Form, NameMap Variable)] -> M Form
removeEquiv :: Form -> M [Form]
removeEquivAux :: Bool -> Form -> M (Seq Form, Form, Form)
makeCopyable :: Bool -> Form -> Form -> M (Seq Form, Form, Form)
removeExists :: Form -> M Form
removeExpensiveOr :: Form -> M [Form]
type Cost = (Integer, Integer)
unitCost :: Cost
andCost :: [Cost] -> Cost
orCost :: [Cost] -> Cost
removeExpensiveOrAux :: Form -> M (Seq Form, Form, Cost)
makeOr :: [(Form, Cost)] -> M (Seq Form, Form, Cost)
cnf :: Form -> Seq (Seq Literal)
cross :: Seq (Seq (Seq Literal)) -> Seq (Seq Literal)
simplifyCNF :: Seq [Literal] -> [[Literal]]
type M = ReaderT Tag (StateT Int NameM)
run :: M a -> NameM a
skolemName :: Named a => String -> a -> M Name
nextSk :: M Int
withName :: Tag -> M a -> M a
getName :: M Tag
skolem :: Variable -> NameMap Variable -> M Term
literal :: String -> NameMap Variable -> M Atomic
instance Show ClausifyFlags

module Jukebox.GuessModel
data Universe
Peano :: Universe
Trees :: Universe
universe :: Universe -> Type -> NameM ([Function], [Form])
peano :: Type -> NameM ([Function], [Form])
trees :: Type -> NameM ([Function], [Form])
guessModel :: [String] -> Universe -> Problem Form -> Problem Form
ind :: Symbolic a => a -> Type
function :: [Function] -> Function -> Bool -> Function -> NameM [Form]
rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form]
cases :: [Function] -> [Type] -> NameM [[Term]]
cases1 :: [Function] -> Type -> NameM [Term]

module Jukebox.Monotonox.ToFOF
data Scheme
Scheme :: (Type -> NameM Function) -> ((Type -> Bool) -> (Type -> Function) -> Scheme1) -> Scheme
makeFunction :: Scheme -> Type -> NameM Function
scheme1 :: Scheme -> (Type -> Bool) -> (Type -> Function) -> Scheme1
data Scheme1
Scheme1 :: (Bind Form -> Form) -> (Bind Form -> Form) -> (Term -> Term -> Form) -> (Function -> NameM Form) -> (Type -> NameM Form) -> Scheme1
forAll :: Scheme1 -> Bind Form -> Form
exists :: Scheme1 -> Bind Form -> Form
equals :: Scheme1 -> Term -> Term -> Form
funcAxiom :: Scheme1 -> Function -> NameM Form
typeAxiom :: Scheme1 -> Type -> NameM Form
guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
translate :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
tagsFlags :: OptionParser Bool
tags :: Bool -> Scheme
tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form
guards :: Scheme
guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
naked :: Symbolic a => Bool -> Variable -> a -> Bool
guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form

module Jukebox.Toolbox
data GlobalFlags
GlobalFlags :: Bool -> GlobalFlags
quiet :: GlobalFlags -> Bool
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)
instance Show GlobalFlags