jukebox-0.4.2: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Form

Documentation

data Type Source #

Constructors

O 
Type 

Fields

Instances
Eq Type Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Ord Type Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Type -> Type -> Ordering #

(<) :: Type -> Type -> Bool #

(<=) :: Type -> Type -> Bool #

(>) :: Type -> Type -> Bool #

(>=) :: Type -> Type -> Bool #

max :: Type -> Type -> Type #

min :: Type -> Type -> Type #

Show Type # 
Instance details

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Pretty Type # 
Instance details

Defined in Jukebox.TPTP.Print

Named Type Source # 
Instance details

Defined in Jukebox.Form

Methods

name :: Type -> Name Source #

Typed Type Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: Type -> Type Source #

data FunType Source #

Constructors

FunType 

Fields

Instances
Eq FunType Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: FunType -> FunType -> Bool #

(/=) :: FunType -> FunType -> Bool #

Ord FunType Source # 
Instance details

Defined in Jukebox.Form

Show FunType # 
Instance details

Defined in Jukebox.TPTP.Print

Pretty FunType # 
Instance details

Defined in Jukebox.TPTP.Print

Typed FunType Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: FunType -> Type Source #

class Typed a where Source #

Minimal complete definition

typ

Methods

typ :: a -> Type Source #

Instances
Typed Term Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: Term -> Type Source #

Typed FunType Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: FunType -> Type Source #

Typed Type Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: Type -> Type Source #

Typed b => Typed (a ::: b) Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: (a ::: b) -> Type Source #

data Term Source #

Constructors

Var Variable 
Function :@: [Term] 
Instances
Eq Term Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Term -> Term -> Bool #

(/=) :: Term -> Term -> Bool #

Ord Term Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Term -> Term -> Ordering #

(<) :: Term -> Term -> Bool #

(<=) :: Term -> Term -> Bool #

(>) :: Term -> Term -> Bool #

(>=) :: Term -> Term -> Bool #

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Show Term # 
Instance details

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

Pretty Term # 
Instance details

Defined in Jukebox.TPTP.Print

Named Term Source # 
Instance details

Defined in Jukebox.Form

Methods

name :: Term -> Name Source #

Unpack Term Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Term -> Rep Term Source #

Symbolic Term Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Term -> TypeOf Term Source #

Typed Term Source # 
Instance details

Defined in Jukebox.Form

Methods

typ :: Term -> Type Source #

TermLike Term Source # 
Instance details

Defined in Jukebox.TPTP.Parse.Core

newSymbol :: Named a => a -> b -> NameM (Name ::: b) Source #

data Atomic Source #

Constructors

Term :=: Term infix 8 
Tru Term 
Instances
Eq Atomic Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Atomic -> Atomic -> Bool #

(/=) :: Atomic -> Atomic -> Bool #

Ord Atomic Source # 
Instance details

Defined in Jukebox.Form

Show Atomic # 
Instance details

Defined in Jukebox.TPTP.Print

Pretty Atomic # 
Instance details

Defined in Jukebox.TPTP.Print

Unpack Atomic Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Atomic -> Rep Atomic Source #

Symbolic Atomic Source # 
Instance details

Defined in Jukebox.Form

data Signed a Source #

Constructors

Pos a 
Neg a 
Instances
Functor Signed Source # 
Instance details

Defined in Jukebox.Form

Methods

fmap :: (a -> b) -> Signed a -> Signed b #

(<$) :: a -> Signed b -> Signed a #

Foldable Signed Source # 
Instance details

Defined in Jukebox.Form

Methods

fold :: Monoid m => Signed m -> m #

foldMap :: Monoid m => (a -> m) -> Signed a -> m #

foldr :: (a -> b -> b) -> b -> Signed a -> b #

foldr' :: (a -> b -> b) -> b -> Signed a -> b #

foldl :: (b -> a -> b) -> b -> Signed a -> b #

foldl' :: (b -> a -> b) -> b -> Signed a -> b #

foldr1 :: (a -> a -> a) -> Signed a -> a #

foldl1 :: (a -> a -> a) -> Signed a -> a #

toList :: Signed a -> [a] #

null :: Signed a -> Bool #

length :: Signed a -> Int #

elem :: Eq a => a -> Signed a -> Bool #

maximum :: Ord a => Signed a -> a #

minimum :: Ord a => Signed a -> a #

sum :: Num a => Signed a -> a #

product :: Num a => Signed a -> a #

Traversable Signed Source # 
Instance details

Defined in Jukebox.Form

Methods

traverse :: Applicative f => (a -> f b) -> Signed a -> f (Signed b) #

sequenceA :: Applicative f => Signed (f a) -> f (Signed a) #

mapM :: Monad m => (a -> m b) -> Signed a -> m (Signed b) #

sequence :: Monad m => Signed (m a) -> m (Signed a) #

Eq a => Eq (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Signed a -> Signed a -> Bool #

(/=) :: Signed a -> Signed a -> Bool #

Ord a => Ord (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Signed a -> Signed a -> Ordering #

(<) :: Signed a -> Signed a -> Bool #

(<=) :: Signed a -> Signed a -> Bool #

(>) :: Signed a -> Signed a -> Bool #

(>=) :: Signed a -> Signed a -> Bool #

max :: Signed a -> Signed a -> Signed a #

min :: Signed a -> Signed a -> Signed a #

Show a => Show (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

showsPrec :: Int -> Signed a -> ShowS #

show :: Signed a -> String #

showList :: [Signed a] -> ShowS #

Symbolic a => Unpack (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Signed a -> Rep (Signed a) Source #

Symbolic a => Symbolic (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Signed a -> TypeOf (Signed a) Source #

the :: Signed a -> a Source #

data Form Source #

Instances
Eq Form Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Form -> Form -> Bool #

(/=) :: Form -> Form -> Bool #

Ord Form Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Form -> Form -> Ordering #

(<) :: Form -> Form -> Bool #

(<=) :: Form -> Form -> Bool #

(>) :: Form -> Form -> Bool #

(>=) :: Form -> Form -> Bool #

max :: Form -> Form -> Form #

min :: Form -> Form -> Form #

Show Form # 
Instance details

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Form -> ShowS #

show :: Form -> String #

showList :: [Form] -> ShowS #

Pretty Form # 
Instance details

Defined in Jukebox.TPTP.Print

Unpack Form Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Form -> Rep Form Source #

Symbolic Form Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Form -> TypeOf Form Source #

FormulaLike Form Source # 
Instance details

Defined in Jukebox.TPTP.Parse.Core

TermLike Form Source # 
Instance details

Defined in Jukebox.TPTP.Parse.Core

data Bind a Source #

Constructors

Bind (Set Variable) a 
Instances
Eq a => Eq (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Bind a -> Bind a -> Bool #

(/=) :: Bind a -> Bind a -> Bool #

Ord a => Ord (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Bind a -> Bind a -> Ordering #

(<) :: Bind a -> Bind a -> Bool #

(<=) :: Bind a -> Bind a -> Bool #

(>) :: Bind a -> Bind a -> Bool #

(>=) :: Bind a -> Bind a -> Bool #

max :: Bind a -> Bind a -> Bind a #

min :: Bind a -> Bind a -> Bind a #

Symbolic a => Unpack (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Bind a -> Rep (Bind a) Source #

Symbolic a => Symbolic (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Bind a -> TypeOf (Bind a) Source #

data CNF Source #

Instances
Unpack CNF Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: CNF -> Rep CNF Source #

Symbolic CNF Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: CNF -> TypeOf CNF Source #

newtype Clause Source #

Constructors

Clause (Bind [Literal]) 
Instances
Show Clause # 
Instance details

Defined in Jukebox.TPTP.Print

Pretty Clause # 
Instance details

Defined in Jukebox.TPTP.Print

Unpack Clause Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Clause -> Rep Clause Source #

Symbolic Clause Source # 
Instance details

Defined in Jukebox.Form

data Kind Source #

Constructors

Ax AxKind 
Conj ConjKind 
Instances
Eq Kind Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Kind -> Kind -> Bool #

(/=) :: Kind -> Kind -> Bool #

Ord Kind Source # 
Instance details

Defined in Jukebox.Form

Methods

compare :: Kind -> Kind -> Ordering #

(<) :: Kind -> Kind -> Bool #

(<=) :: Kind -> Kind -> Bool #

(>) :: Kind -> Kind -> Bool #

(>=) :: Kind -> Kind -> Bool #

max :: Kind -> Kind -> Kind #

min :: Kind -> Kind -> Kind #

Show Kind # 
Instance details

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

data AxKind Source #

Instances
Eq AxKind Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: AxKind -> AxKind -> Bool #

(/=) :: AxKind -> AxKind -> Bool #

Ord AxKind Source # 
Instance details

Defined in Jukebox.Form

Show AxKind # 
Instance details

Defined in Jukebox.TPTP.Print

data ConjKind Source #

Constructors

Conjecture 
Question 
Instances
Eq ConjKind Source # 
Instance details

Defined in Jukebox.Form

Ord ConjKind Source # 
Instance details

Defined in Jukebox.Form

Show ConjKind # 
Instance details

Defined in Jukebox.TPTP.Print

data Answer Source #

Instances
Eq Answer Source # 
Instance details

Defined in Jukebox.Form

Methods

(==) :: Answer -> Answer -> Bool #

(/=) :: Answer -> Answer -> Bool #

Ord Answer Source # 
Instance details

Defined in Jukebox.Form

Show Answer Source # 
Instance details

Defined in Jukebox.Form

type Model = [String] Source #

data Input a Source #

Constructors

Input 

Fields

Instances
Functor Input Source # 
Instance details

Defined in Jukebox.Form

Methods

fmap :: (a -> b) -> Input a -> Input b #

(<$) :: a -> Input b -> Input a #

Foldable Input Source # 
Instance details

Defined in Jukebox.Form

Methods

fold :: Monoid m => Input m -> m #

foldMap :: Monoid m => (a -> m) -> Input a -> m #

foldr :: (a -> b -> b) -> b -> Input a -> b #

foldr' :: (a -> b -> b) -> b -> Input a -> b #

foldl :: (b -> a -> b) -> b -> Input a -> b #

foldl' :: (b -> a -> b) -> b -> Input a -> b #

foldr1 :: (a -> a -> a) -> Input a -> a #

foldl1 :: (a -> a -> a) -> Input a -> a #

toList :: Input a -> [a] #

null :: Input a -> Bool #

length :: Input a -> Int #

elem :: Eq a => a -> Input a -> Bool #

maximum :: Ord a => Input a -> a #

minimum :: Ord a => Input a -> a #

sum :: Num a => Input a -> a #

product :: Num a => Input a -> a #

Traversable Input Source # 
Instance details

Defined in Jukebox.Form

Methods

traverse :: Applicative f => (a -> f b) -> Input a -> f (Input b) #

sequenceA :: Applicative f => Input (f a) -> f (Input a) #

mapM :: Monad m => (a -> m b) -> Input a -> m (Input b) #

sequence :: Monad m => Input (m a) -> m (Input a) #

Pretty a => Show (Input a) # 
Instance details

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Input a -> ShowS #

show :: Input a -> String #

showList :: [Input a] -> ShowS #

Pretty a => Pretty (Input a) # 
Instance details

Defined in Jukebox.TPTP.Print

Symbolic a => Unpack (Input a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Input a -> Rep (Input a) Source #

Symbolic a => Symbolic (Input a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Input a -> TypeOf (Input a) Source #

type Problem a = [Input a] Source #

data TypeOf a where Source #

Constructors

Form :: TypeOf Form 
Clause_ :: TypeOf Clause 
Term :: TypeOf Term 
Atomic :: TypeOf Atomic 
Signed :: (Symbolic a, Symbolic (Signed a)) => TypeOf (Signed a) 
Bind_ :: (Symbolic a, Symbolic (Bind a)) => TypeOf (Bind a) 
List :: (Symbolic a, Symbolic [a]) => TypeOf [a] 
Input_ :: (Symbolic a, Symbolic (Input a)) => TypeOf (Input a) 
CNF_ :: TypeOf CNF 

class Symbolic a where Source #

Minimal complete definition

typeOf

Methods

typeOf :: a -> TypeOf a Source #

Instances
Symbolic Clause Source # 
Instance details

Defined in Jukebox.Form

Symbolic CNF Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: CNF -> TypeOf CNF Source #

Symbolic Form Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Form -> TypeOf Form Source #

Symbolic Atomic Source # 
Instance details

Defined in Jukebox.Form

Symbolic Term Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Term -> TypeOf Term Source #

Symbolic a => Symbolic [a] Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: [a] -> TypeOf [a] Source #

Symbolic a => Symbolic (Input a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Input a -> TypeOf (Input a) Source #

Symbolic a => Symbolic (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Bind a -> TypeOf (Bind a) Source #

Symbolic a => Symbolic (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

typeOf :: Signed a -> TypeOf (Signed a) Source #

data Rep a where Source #

Constructors

Const :: !a -> Rep a 
Unary :: Symbolic a => (a -> b) -> a -> Rep b 
Binary :: (Symbolic a, Symbolic b) => (a -> b -> c) -> a -> b -> Rep c 

rep :: Symbolic a => a -> Rep a Source #

class Unpack a where Source #

Minimal complete definition

rep'

Methods

rep' :: a -> Rep a Source #

Instances
Unpack Clause Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Clause -> Rep Clause Source #

Unpack CNF Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: CNF -> Rep CNF Source #

Unpack Form Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Form -> Rep Form Source #

Unpack Atomic Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Atomic -> Rep Atomic Source #

Unpack Term Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Term -> Rep Term Source #

Symbolic a => Unpack [a] Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: [a] -> Rep [a] Source #

Symbolic a => Unpack (Input a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Input a -> Rep (Input a) Source #

Symbolic a => Unpack (Bind a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Bind a -> Rep (Bind a) Source #

Symbolic a => Unpack (Signed a) Source # 
Instance details

Defined in Jukebox.Form

Methods

rep' :: Signed a -> Rep (Signed a) Source #

recursively :: Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a Source #

recursivelyM :: (Monad m, Symbolic a) => (forall a. Symbolic a => a -> m a) -> a -> m a Source #

collect :: (Symbolic a, Monoid b) => (forall a. Symbolic a => a -> b) -> a -> b Source #

subst :: Symbolic a => Subst -> a -> a Source #

ground :: Symbolic a => a -> Bool Source #

bind :: Symbolic a => a -> Bind a Source #

termsAndBinders :: forall a b. Symbolic a => (Term -> DList b) -> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b] Source #

names :: Symbolic a => a -> [Name] Source #

run :: Symbolic a => a -> (a -> NameM b) -> b Source #

run_ :: Symbolic a => a -> NameM b -> b Source #

types :: Symbolic a => a -> [Type] Source #

types' :: Symbolic a => a -> [Type] Source #

terms :: Symbolic a => a -> [Term] Source #

vars :: Symbolic a => a -> [Variable] Source #

isFof :: Symbolic a => a -> Bool Source #

eraseTypes :: Symbolic a => a -> a Source #

force :: Symbolic a => a -> a Source #

check :: Symbolic a => a -> a Source #

mapName :: Symbolic a => (Name -> Name) -> a -> a Source #

mapType :: Symbolic a => (Type -> Type) -> a -> a Source #