Jukebox.Form

Documentation

debugging :: Bool

data Type

Constructors

O

Type

Fields

• tname :: !Name

Instances

Eq Type

Methods

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

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

Ord Type

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

Named Type

Methods

name :: Type -> Name

Typed Type

Methods

typ :: Type -> Type

indType :: Type

intType :: Type

ratType :: Type

realType :: Type

data FunType

Constructors

FunType

Fields

• args :: [Type]
• res :: Type

Instances

Eq FunType

Methods

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

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

Ord FunType

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

Methods

typ :: FunType -> Type

typeMaybeName :: Type -> Maybe Name

class Typed a where

Minimal complete definition

typ

Methods

typ :: a -> Type

Instances

Typed Term

Methods

typ :: Term -> Type

Typed FunType

Methods

typ :: FunType -> Type

Typed Type

Methods

typ :: Type -> Type

Typed b => Typed ((:::) a b)

Methods

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

type Variable = Name ::: Type

type Function = Name ::: FunType

data Term

Constructors

Var Variable

Function :@: [Term]

Instances

Eq Term

Methods

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

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

Ord Term

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

Named Term

Methods

name :: Term -> Name

Unpack Term

Methods

rep' :: Term -> Rep Term

Symbolic Term

Methods

typeOf :: Term -> TypeOf Term

Typed Term

Methods

typ :: Term -> Type

TermLike Term

Methods

fromThing :: Thing -> Parser Term

var :: Mode -> Map String Variable -> Parser Term

parser :: Mode -> Map String Variable -> Parser 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

Constructors

Term :=: Term infix 8

Tru Term

Instances

Eq Atomic

Methods

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

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

Ord Atomic

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

Unpack Atomic

Methods

rep' :: Atomic -> Rep Atomic

Symbolic Atomic

Methods

typeOf :: Atomic -> TypeOf Atomic

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

data Signed a

Constructors

Pos a

Neg a

Instances

Functor Signed

Methods

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

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

Foldable Signed

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

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)

Methods

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

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

Ord a => Ord (Signed a)

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)

Methods

showsPrec :: Int -> Signed a -> ShowS

show :: Signed a -> String

showList :: [Signed a] -> ShowS

Symbolic a => Unpack (Signed a)

Methods

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

Symbolic a => Symbolic (Signed a)

Methods

typeOf :: Signed a -> TypeOf (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

Constructors

Literal Literal

Not Form

And [Form]

Or [Form]

Equiv Form Form

ForAll !(Bind Form)

Exists !(Bind Form)

Connective Connective Form Form

Instances

Eq Form

Methods

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

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

Ord 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

Unpack Form

Methods

rep' :: Form -> Rep Form

Symbolic Form

Methods

typeOf :: Form -> TypeOf Form

FormulaLike Form

Methods

fromFormula :: Form -> Form

TermLike Form

Methods

fromThing :: Thing -> Parser Form

var :: Mode -> Map String Variable -> Parser Form

parser :: Mode -> Map String Variable -> Parser Form

data Connective

Constructors

Implies

Follows

Xor

Nor

Nand

Instances

Eq Connective

Methods

(==) :: Connective -> Connective -> Bool

(/=) :: Connective -> Connective -> Bool

Ord Connective

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

data Bind a

Constructors

Bind (Set Variable) a

Instances

Eq a => Eq (Bind a)

Methods

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

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

Ord a => Ord (Bind a)

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)

Methods

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

Symbolic a => Symbolic (Bind a)

Methods

typeOf :: Bind a -> TypeOf (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

positive :: Form -> Form

notInwards :: Form -> Form

simple :: Form -> Form

simplify :: Form -> Form

data CNF

Constructors

CNF

Fields

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

Instances

Unpack CNF

Methods

rep' :: CNF -> Rep CNF

Symbolic CNF

Methods

typeOf :: CNF -> TypeOf CNF

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

newtype Clause

Constructors

Clause (Bind [Literal])

Instances

Unpack Clause

Methods

rep' :: Clause -> Rep Clause

Symbolic Clause

Methods

typeOf :: Clause -> TypeOf Clause

clause :: [Literal] -> Clause

toForm :: Clause -> Form

toLiterals :: Clause -> [Literal]

toClause :: Form -> Maybe Clause

type Tag = String

data Kind

Constructors

Ax AxKind

Conj ConjKind

Instances

Eq Kind

Methods

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

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

Ord Kind

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

Constructors

Axiom

Hypothesis

Definition

Assumption

Lemma

TheoremKind

NegatedConjecture

Instances

Eq AxKind

Methods

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

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

Ord AxKind

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

Constructors

Conjecture

Question

Instances

Eq ConjKind

Methods

(==) :: ConjKind -> ConjKind -> Bool

(/=) :: ConjKind -> ConjKind -> Bool

Ord ConjKind

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

Constructors

Sat SatReason (Maybe Model)

Unsat UnsatReason (Maybe CNFRefutation)

NoAnswer NoAnswerReason

Instances

Eq Answer

Methods

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

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

Ord Answer

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

Show Answer

Methods

showsPrec :: Int -> Answer -> ShowS

show :: Answer -> String

showList :: [Answer] -> ShowS

data NoAnswerReason

Constructors

GaveUp

Timeout

Instances

Eq NoAnswerReason

Methods

(==) :: NoAnswerReason -> NoAnswerReason -> Bool

(/=) :: NoAnswerReason -> NoAnswerReason -> Bool

Ord NoAnswerReason

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

Show NoAnswerReason

Methods

showsPrec :: Int -> NoAnswerReason -> ShowS

show :: NoAnswerReason -> String

showList :: [NoAnswerReason] -> ShowS

data SatReason

Constructors

Satisfiable

CounterSatisfiable

Instances

Eq SatReason

Methods

(==) :: SatReason -> SatReason -> Bool

(/=) :: SatReason -> SatReason -> Bool

Ord SatReason

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

Show SatReason

Methods

showsPrec :: Int -> SatReason -> ShowS

show :: SatReason -> String

showList :: [SatReason] -> ShowS

data UnsatReason

Constructors

Unsatisfiable

Theorem

Instances

Eq UnsatReason

Methods

(==) :: UnsatReason -> UnsatReason -> Bool

(/=) :: UnsatReason -> UnsatReason -> Bool

Ord UnsatReason

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

Show UnsatReason

Methods

showsPrec :: Int -> UnsatReason -> ShowS

show :: UnsatReason -> String

showList :: [UnsatReason] -> ShowS

type Model = [String]

type CNFRefutation = [String]

explainAnswer :: Answer -> String

answerSZS :: Answer -> [String]

answerJustification :: Answer -> Maybe [String]

data Input a

Constructors

Input

Fields

• tag :: Tag
• kind :: Kind
• source :: InputSource
• what :: a

Instances

Functor Input

Methods

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

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

Foldable Input

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

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)

Symbolic a => Unpack (Input a)

Methods

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

Symbolic a => Symbolic (Input a)

Methods

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

data InputSource

Constructors

Unknown

FromFile String Int

Inference String String [Input Form]

type Problem a = [Input a]

data TypeOf a where

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

Minimal complete definition

typeOf

Methods

typeOf :: a -> TypeOf a

Instances

Symbolic Clause

Methods

typeOf :: Clause -> TypeOf Clause

Symbolic CNF

Methods

typeOf :: CNF -> TypeOf CNF

Symbolic Form

Methods

typeOf :: Form -> TypeOf Form

Symbolic Atomic

Methods

typeOf :: Atomic -> TypeOf Atomic

Symbolic Term

Methods

typeOf :: Term -> TypeOf Term

Symbolic a => Symbolic [a]

Methods

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

Symbolic a => Symbolic (Input a)

Methods

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

Symbolic a => Symbolic (Bind a)

Methods

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

Symbolic a => Symbolic (Signed a)

Methods

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

data Rep a where

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

class Unpack a where

Minimal complete definition

rep'

Methods

rep' :: a -> Rep a

Instances

Unpack Clause

Methods

rep' :: Clause -> Rep Clause

Unpack CNF

Methods

rep' :: CNF -> Rep CNF

Unpack Form

Methods

rep' :: Form -> Rep Form

Unpack Atomic

Methods

rep' :: Atomic -> Rep Atomic

Unpack Term

Methods

rep' :: Term -> Rep Term

Symbolic a => Unpack [a]

Methods

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

Symbolic a => Unpack (Input a)

Methods

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

Symbolic a => Unpack (Bind a)

Methods

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

Symbolic a => Unpack (Signed a)

Methods

rep' :: Signed a -> Rep (Signed 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 = Map Variable Term

ids :: Subst

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

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

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

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

ground :: Symbolic a => a -> Bool

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

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

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

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

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

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]

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

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

isFof :: Symbolic a => a -> Bool

eraseTypes :: Symbolic a => a -> a

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

force :: Symbolic a => a -> a

check :: Symbolic a => a -> a

checkBinder :: Set Variable -> Subst -> Subst

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

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