Safe Haskell	None
Language	Haskell2010

Jukebox.Form

Documentation

debugging :: Bool Source #

data Type Source #

Constructors

O
Type
Fields tname :: !Name

Instances

Instances details

Show Type Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
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 #
Typed Type Source #
Instance details Defined in Jukebox.Form Methods typ :: Type -> Type Source #
Named Type Source #
Instance details Defined in Jukebox.Form Methods name :: Type -> Name Source #
Pretty Type Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Type -> Doc # pPrint :: Type -> Doc # pPrintList :: PrettyLevel -> [Type] -> Doc #

indType :: Type Source #

intType :: Type Source #

ratType :: Type Source #

realType :: Type Source #

data FunType Source #

Constructors

FunType
Fields args :: [Type] res :: Type

Instances

Instances details

Show FunType Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> FunType -> ShowS # show :: FunType -> String # showList :: [FunType] -> ShowS #
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 Methods compare :: FunType -> FunType -> Ordering # (<) :: FunType -> FunType -> Bool # (<=) :: FunType -> FunType -> Bool # (>) :: FunType -> FunType -> Bool # (>=) :: FunType -> FunType -> Bool # max :: FunType -> FunType -> FunType # min :: FunType -> FunType -> FunType #
Typed FunType Source #
Instance details Defined in Jukebox.Form Methods typ :: FunType -> Type Source #
Pretty FunType Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> FunType -> Doc # pPrint :: FunType -> Doc # pPrintList :: PrettyLevel -> [FunType] -> Doc #

typeMaybeName :: Type -> Maybe Name Source #

class Typed a where Source #

Methods

typ :: a -> Type Source #

Instances

Instances details

Typed FunType Source #
Instance details Defined in Jukebox.Form Methods typ :: FunType -> Type Source #
Typed Term Source #
Instance details Defined in Jukebox.Form Methods typ :: Term -> 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 #

type Variable = Name ::: Type Source #

type Function = Name ::: FunType Source #

data Term Source #

Constructors

Var Variable
Function :@: [Term]

Instances

Instances details

Show Term Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
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 #
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 #
Unpack Term Source #
Instance details Defined in Jukebox.Form Methods rep' :: Term -> Rep Term Source #
Named Term Source #
Instance details Defined in Jukebox.Form Methods name :: Term -> Name Source #
TermLike Term Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Term Source # var :: Mode -> Map Symbol Variable -> Parser Term Source # parseFormula :: Parser Form -> Parser Term Source # parser :: Mode -> Map Symbol Variable -> Parser Term Source #
Pretty Term Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Term -> Doc # pPrint :: Term -> Doc # pPrintList :: PrettyLevel -> [Term] -> Doc #

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

newFunction :: Named a => a -> [Type] -> Type -> NameM Function Source #

newType :: Named a => a -> NameM Type Source #

funArgs :: Function -> [Type] Source #

arity :: Function -> Int Source #

size :: Term -> Int Source #

subterms :: Term -> [Term] Source #

contexts :: Term -> [(Term, Term -> Term)] Source #

data Atomic Source #

Constructors

Term :=: Term infix 8
Tru Term

Instances

Instances details

Show Atomic Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Atomic -> ShowS # show :: Atomic -> String # showList :: [Atomic] -> ShowS #
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 Methods compare :: Atomic -> Atomic -> Ordering # (<) :: Atomic -> Atomic -> Bool # (<=) :: Atomic -> Atomic -> Bool # (>) :: Atomic -> Atomic -> Bool # (>=) :: Atomic -> Atomic -> Bool # max :: Atomic -> Atomic -> Atomic # min :: Atomic -> Atomic -> Atomic #
Symbolic Atomic Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Atomic -> TypeOf Atomic Source #
Unpack Atomic Source #
Instance details Defined in Jukebox.Form Methods rep' :: Atomic -> Rep Atomic Source #
Pretty Atomic Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Atomic -> Doc # pPrint :: Atomic -> Doc # pPrintList :: PrettyLevel -> [Atomic] -> Doc #

normAtomic :: Atomic -> Either (Term, Term) Term Source #

data Signed a Source #

Constructors

Pos a
Neg a

Instances

Instances details

Foldable Signed Source #
Instance details Defined in Jukebox.Form Methods fold :: Monoid m => Signed m -> m # foldMap :: Monoid m => (a -> m) -> Signed a -> 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) #
Functor Signed Source #
Instance details Defined in Jukebox.Form Methods fmap :: (a -> b) -> Signed a -> Signed b # (<$) :: a -> Signed b -> 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 #
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 #
Symbolic a => Symbolic (Signed a) Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Signed a -> TypeOf (Signed a) Source #
Symbolic a => Unpack (Signed a) Source #
Instance details Defined in Jukebox.Form Methods rep' :: Signed a -> Rep (Signed a) Source #

type Literal = Signed Atomic Source #

neg :: Signed a -> Signed a Source #

the :: Signed a -> a Source #

pos :: Signed a -> Bool Source #

signForm :: Signed a -> Form -> Form Source #

data Form Source #

Constructors

Literal Literal
Not Form
And [Form]
Or [Form]
Equiv Form Form
ForAll !(Bind Form)
Exists !(Bind Form)
Connective Connective Form Form

Instances

Instances details

Show Form Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Form -> ShowS # show :: Form -> String # showList :: [Form] -> ShowS #
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 #
Symbolic Form Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Form -> TypeOf Form Source #
Unpack Form Source #
Instance details Defined in Jukebox.Form Methods rep' :: Form -> Rep Form Source #
TermLike Form Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Form Source # var :: Mode -> Map Symbol Variable -> Parser Form Source # parseFormula :: Parser Form -> Parser Form Source # parser :: Mode -> Map Symbol Variable -> Parser Form Source #
Pretty Form Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Form -> Doc # pPrint :: Form -> Doc # pPrintList :: PrettyLevel -> [Form] -> Doc #

data Connective Source #

Constructors

Implies
Follows
Xor
Nor
Nand

Instances

Instances details

Show Connective Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Connective -> ShowS # show :: Connective -> String # showList :: [Connective] -> ShowS #
Eq Connective Source #
Instance details Defined in Jukebox.Form Methods (==) :: Connective -> Connective -> Bool # (/=) :: Connective -> Connective -> Bool #
Ord Connective Source #
Instance details Defined in Jukebox.Form Methods compare :: Connective -> Connective -> Ordering # (<) :: Connective -> Connective -> Bool # (<=) :: Connective -> Connective -> Bool # (>) :: Connective -> Connective -> Bool # (>=) :: Connective -> Connective -> Bool # max :: Connective -> Connective -> Connective # min :: Connective -> Connective -> Connective #

connective :: Connective -> Form -> Form -> Form Source #

data Bind a Source #

Constructors

Bind (Set Variable) a

Instances

Instances details

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 => Symbolic (Bind a) Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Bind a -> TypeOf (Bind a) Source #
Symbolic a => Unpack (Bind a) Source #
Instance details Defined in Jukebox.Form Methods rep' :: Bind a -> Rep (Bind a) Source #

true :: Form Source #

false :: Form Source #

isTrue :: Form -> Bool Source #

isFalse :: Form -> Bool Source #

nt :: Form -> Form Source #

(.=>.) :: Form -> Form -> Form Source #

(.=.) :: Term -> Term -> Form Source #

(/\) :: Form -> Form -> Form Source #

(\/) :: Form -> Form -> Form Source #

closeForm :: Form -> Form Source #

positive :: Form -> Form Source #

notInwards :: Form -> Form Source #

simple :: Form -> Form Source #

simplify :: Form -> Form Source #

data CNF Source #

Constructors

CNF
Fields axioms :: [Input Clause] conjectures :: [[Input Clause]] satisfiable :: Maybe Model -> Answer unsatisfiable :: Maybe CNFRefutation -> Answer

Instances

Instances details

Symbolic CNF Source #
Instance details Defined in Jukebox.Form Methods typeOf :: CNF -> TypeOf CNF Source #
Unpack CNF Source #
Instance details Defined in Jukebox.Form Methods rep' :: CNF -> Rep CNF Source #

toCNF :: [Input Clause] -> [[Input Clause]] -> CNF Source #

newtype Clause Source #

Constructors

Clause (Bind [Literal])

Instances

Instances details

Show Clause Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
Symbolic Clause Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Clause -> TypeOf Clause Source #
Unpack Clause Source #
Instance details Defined in Jukebox.Form Methods rep' :: Clause -> Rep Clause Source #
Pretty Clause Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Clause -> Doc # pPrint :: Clause -> Doc # pPrintList :: PrettyLevel -> [Clause] -> Doc #

clause :: [Literal] -> Clause Source #

toForm :: Clause -> Form Source #

toLiterals :: Clause -> [Literal] Source #

toClause :: Form -> Maybe Clause Source #

type Tag = String Source #

data Kind Source #

Constructors

Ax AxKind
Conj ConjKind

Instances

Instances details

Show Kind Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Kind -> ShowS # show :: Kind -> String # showList :: [Kind] -> ShowS #
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 #

data AxKind Source #

Constructors

Axiom
Hypothesis
Definition
Assumption
Lemma
TheoremKind
NegatedConjecture

Instances

Instances details

Show AxKind Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> AxKind -> ShowS # show :: AxKind -> String # showList :: [AxKind] -> ShowS #
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 Methods compare :: AxKind -> AxKind -> Ordering # (<) :: AxKind -> AxKind -> Bool # (<=) :: AxKind -> AxKind -> Bool # (>) :: AxKind -> AxKind -> Bool # (>=) :: AxKind -> AxKind -> Bool # max :: AxKind -> AxKind -> AxKind # min :: AxKind -> AxKind -> AxKind #

data ConjKind Source #

Constructors

Conjecture
Question

Instances

Instances details

Show ConjKind Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> ConjKind -> ShowS # show :: ConjKind -> String # showList :: [ConjKind] -> ShowS #
Eq ConjKind Source #
Instance details Defined in Jukebox.Form Methods (==) :: ConjKind -> ConjKind -> Bool # (/=) :: ConjKind -> ConjKind -> Bool #
Ord ConjKind Source #
Instance details Defined in Jukebox.Form Methods compare :: ConjKind -> ConjKind -> Ordering # (<) :: ConjKind -> ConjKind -> Bool # (<=) :: ConjKind -> ConjKind -> Bool # (>) :: ConjKind -> ConjKind -> Bool # (>=) :: ConjKind -> ConjKind -> Bool # max :: ConjKind -> ConjKind -> ConjKind # min :: ConjKind -> ConjKind -> ConjKind #

data Answer Source #

Constructors

Sat SatReason (Maybe Model)
Unsat UnsatReason (Maybe CNFRefutation)
NoAnswer NoAnswerReason

Instances

Instances details

Show Answer Source #
Instance details Defined in Jukebox.Form Methods showsPrec :: Int -> Answer -> ShowS # show :: Answer -> String # showList :: [Answer] -> ShowS #
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 Methods compare :: Answer -> Answer -> Ordering # (<) :: Answer -> Answer -> Bool # (<=) :: Answer -> Answer -> Bool # (>) :: Answer -> Answer -> Bool # (>=) :: Answer -> Answer -> Bool # max :: Answer -> Answer -> Answer # min :: Answer -> Answer -> Answer #

data NoAnswerReason Source #

Constructors

GaveUp
Timeout

Instances

Instances details

Show NoAnswerReason Source #
Instance details Defined in Jukebox.Form Methods showsPrec :: Int -> NoAnswerReason -> ShowS # show :: NoAnswerReason -> String # showList :: [NoAnswerReason] -> ShowS #
Eq NoAnswerReason Source #
Instance details Defined in Jukebox.Form Methods (==) :: NoAnswerReason -> NoAnswerReason -> Bool # (/=) :: NoAnswerReason -> NoAnswerReason -> Bool #
Ord NoAnswerReason Source #
Instance details Defined in Jukebox.Form Methods compare :: NoAnswerReason -> NoAnswerReason -> Ordering # (<) :: NoAnswerReason -> NoAnswerReason -> Bool # (<=) :: NoAnswerReason -> NoAnswerReason -> Bool # (>) :: NoAnswerReason -> NoAnswerReason -> Bool # (>=) :: NoAnswerReason -> NoAnswerReason -> Bool # max :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason # min :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason #

data SatReason Source #

Constructors

Satisfiable
CounterSatisfiable

Instances

Instances details

Show SatReason Source #
Instance details Defined in Jukebox.Form Methods showsPrec :: Int -> SatReason -> ShowS # show :: SatReason -> String # showList :: [SatReason] -> ShowS #
Eq SatReason Source #
Instance details Defined in Jukebox.Form Methods (==) :: SatReason -> SatReason -> Bool # (/=) :: SatReason -> SatReason -> Bool #
Ord SatReason Source #
Instance details Defined in Jukebox.Form Methods compare :: SatReason -> SatReason -> Ordering # (<) :: SatReason -> SatReason -> Bool # (<=) :: SatReason -> SatReason -> Bool # (>) :: SatReason -> SatReason -> Bool # (>=) :: SatReason -> SatReason -> Bool # max :: SatReason -> SatReason -> SatReason # min :: SatReason -> SatReason -> SatReason #

data UnsatReason Source #

Constructors

Unsatisfiable
Theorem

Instances

Instances details

Show UnsatReason Source #
Instance details Defined in Jukebox.Form Methods showsPrec :: Int -> UnsatReason -> ShowS # show :: UnsatReason -> String # showList :: [UnsatReason] -> ShowS #
Eq UnsatReason Source #
Instance details Defined in Jukebox.Form Methods (==) :: UnsatReason -> UnsatReason -> Bool # (/=) :: UnsatReason -> UnsatReason -> Bool #
Ord UnsatReason Source #
Instance details Defined in Jukebox.Form Methods compare :: UnsatReason -> UnsatReason -> Ordering # (<) :: UnsatReason -> UnsatReason -> Bool # (<=) :: UnsatReason -> UnsatReason -> Bool # (>) :: UnsatReason -> UnsatReason -> Bool # (>=) :: UnsatReason -> UnsatReason -> Bool # max :: UnsatReason -> UnsatReason -> UnsatReason # min :: UnsatReason -> UnsatReason -> UnsatReason #

type Model = [String] Source #

type CNFRefutation = [String] Source #

explainAnswer :: Answer -> String Source #

answerSZS :: Answer -> [String] Source #

answerJustification :: Answer -> Maybe [String] Source #

data Input a Source #

Constructors

Input
Fields ident :: Maybe Name tag :: Tag kind :: Kind source :: InputSource what :: a

Instances

Instances details

Foldable Input Source #
Instance details Defined in Jukebox.Form Methods fold :: Monoid m => Input m -> m # foldMap :: Monoid m => (a -> m) -> Input a -> 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) #
Functor Input Source #
Instance details Defined in Jukebox.Form Methods fmap :: (a -> b) -> Input a -> Input b # (<$) :: a -> Input b -> Input a #
Pretty a => Show (Input a) Source #
Instance details Defined in Jukebox.TPTP.Print Methods showsPrec :: Int -> Input a -> ShowS # show :: Input a -> String # showList :: [Input a] -> ShowS #
Symbolic a => Symbolic (Input a) Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Input a -> TypeOf (Input a) Source #
Symbolic a => Unpack (Input a) Source #
Instance details Defined in Jukebox.Form Methods rep' :: Input a -> Rep (Input a) Source #
Pretty a => Pretty (Input a) Source #
Instance details Defined in Jukebox.TPTP.Print Methods pPrintPrec :: PrettyLevel -> Rational -> Input a -> Doc # pPrint :: Input a -> Doc # pPrintList :: PrettyLevel -> [Input a] -> Doc #

data InputSource Source #

Constructors

Unknown
FromFile String Int
Inference String String [InputPlus Form]

inference :: String -> String -> [Input Form] -> InputSource Source #

data InputPlus a Source #

Constructors

InputPlus
Fields inputNames :: [Name] inputFunctions :: [Function] inputTypes :: [Type] inputValue :: Input a

inputPlus :: Symbolic a => Input a -> InputPlus 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 :: forall a1. (Symbolic a1, Symbolic (Signed a1)) => TypeOf (Signed a1)
Bind_ :: forall a1. (Symbolic a1, Symbolic (Bind a1)) => TypeOf (Bind a1)
List :: forall a1. (Symbolic a1, Symbolic [a1]) => TypeOf [a1]
Input_ :: forall a1. (Symbolic a1, Symbolic (Input a1)) => TypeOf (Input a1)
CNF_ :: TypeOf CNF

class Symbolic a where Source #

Methods

typeOf :: a -> TypeOf a Source #

Instances

Instances details

Symbolic Atomic Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Atomic -> TypeOf Atomic Source #
Symbolic CNF Source #
Instance details Defined in Jukebox.Form Methods typeOf :: CNF -> TypeOf CNF Source #
Symbolic Clause Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Clause -> TypeOf Clause Source #
Symbolic Form Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Form -> TypeOf Form Source #
Symbolic Term Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Term -> TypeOf Term Source #
Symbolic a => Symbolic (Bind a) Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Bind a -> TypeOf (Bind 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 (Signed a) Source #
Instance details Defined in Jukebox.Form Methods typeOf :: Signed a -> TypeOf (Signed a) Source #
Symbolic a => Symbolic [a] Source #
Instance details Defined in Jukebox.Form Methods typeOf :: [a] -> TypeOf [a] Source #

data Rep a where Source #

Constructors

Const :: forall a. !a -> Rep a
Unary :: forall a1 a. Symbolic a1 => (a1 -> a) -> a1 -> Rep a
Binary :: forall a1 b a. (Symbolic a1, Symbolic b) => (a1 -> b -> a) -> a1 -> b -> Rep a

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

class Unpack a where Source #

Methods

rep' :: a -> Rep a Source #

Instances

Instances details

Unpack Atomic Source #
Instance details Defined in Jukebox.Form Methods rep' :: Atomic -> Rep Atomic Source #
Unpack CNF Source #
Instance details Defined in Jukebox.Form Methods rep' :: CNF -> Rep CNF Source #
Unpack Clause Source #
Instance details Defined in Jukebox.Form Methods rep' :: Clause -> Rep Clause Source #
Unpack Form Source #
Instance details Defined in Jukebox.Form Methods rep' :: Form -> Rep Form Source #
Unpack Term Source #
Instance details Defined in Jukebox.Form Methods rep' :: Term -> Rep Term Source #
Symbolic a => Unpack (Bind a) Source #
Instance details Defined in Jukebox.Form Methods rep' :: Bind a -> Rep (Bind 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 (Signed a) Source #
Instance details Defined in Jukebox.Form Methods rep' :: Signed a -> Rep (Signed a) Source #
Symbolic a => Unpack [a] Source #
Instance details Defined in Jukebox.Form Methods rep' :: [a] -> Rep [a] Source #

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

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

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

type Subst = Map Variable Term Source #

ids :: Subst Source #

(|=>) :: Variable -> Term -> Subst Source #

(|+|) :: Subst -> Subst -> Subst Source #

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

match :: Term -> Term -> Maybe Subst Source #

free :: Symbolic a => a -> Set Variable Source #

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

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

termsAndBinders :: Symbolic a => (Term -> DList b) -> (forall a1. Symbolic a1 => Bind a1 -> [b]) -> (forall a1. Symbolic a1 => Input a1 -> [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 #

functions :: Symbolic a => a -> [Function] Source #

funOcc :: Symbolic a => Function -> a -> Int Source #

funsOcc :: Symbolic a => a -> Map Function Int Source #

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

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

uniqueNames :: Symbolic a => a -> NameM a Source #

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

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

checkBinder :: Set Variable -> Subst -> Subst Source #

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

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