Jukebox.Form

Documentation

debugging :: Bool

data DomainSize

Constructors

Finite Int

Infinite

Instances

Eq DomainSize

Ord DomainSize

Show DomainSize

data Type

Constructors

O

Type

Fields

tname :: !Name

tmonotone :: DomainSize

tsize :: DomainSize

Instances

Eq Type

Ord Type

Hashable Type

Named Type

Typed Type

Pretty Type

Pretty [Type]

data FunType

Constructors

FunType

Fields

args :: [Type]

res :: Type

Instances

Eq FunType

Typed FunType

Pretty FunType

typeMaybeName :: Type -> Maybe Name

class Typed a where

Methods

typ :: a -> Type

Instances

Typed Term

Typed FunType

Typed Type

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

type Variable = Name ::: Type

type Function = Name ::: FunType

data Term

Constructors

Var Variable

Function :@: [Term]

Instances

Eq Term

Ord Term

Hashable Term

Named Term

Unpack Term

Symbolic Term

Typed Term

Pretty Term

TermLike Term

Pretty [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

Ord Atomic

Hashable Atomic

Unpack Atomic

Symbolic Atomic

Pretty Atomic

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

data Signed a

Constructors

Pos a

Neg a

Instances

Functor Signed

Eq a => Eq (Signed a)

Ord a => Ord (Signed a)

Show a => Show (Signed a)

Hashable a => Hashable (Signed a)

Symbolic a => Unpack (Signed a)

Symbolic a => Symbolic (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 (Seq Form)

Or (Seq Form)

Equiv Form Form

ForAll !(Bind Form)

Exists !(Bind Form)

Connective Connective Form Form

Instances

Unpack Form

Symbolic Form

Pretty Form

FormulaLike Form

TermLike Form

data Connective

Constructors

Implies

Follows

Xor

Nor

Nand

connective :: Connective -> Form -> Form -> Form

data Bind a

Constructors

Bind (NameMap Variable) a

Instances

Symbolic a => Unpack (Bind a)

Symbolic a => Symbolic (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

Constructors

Obligs

Fields

axioms :: [Input Clause]

conjectures :: [[Input Clause]]

satisfiable :: String

unsatisfiable :: String

Instances

Unpack Obligs

Symbolic Obligs

toObligs :: [Input Clause] -> [[Input Clause]] -> Obligs

newtype Clause

Constructors

Clause (Bind [Literal])

Instances

Unpack Clause

Symbolic Clause

Pretty Clause

clause :: List f => f (Signed Atomic) -> Clause

toForm :: Clause -> Form

toLiterals :: Clause -> [Literal]

type Tag = ByteString

data Kind

Constructors

Axiom

Conjecture

Question

Instances

Eq Kind

Ord Kind

data Answer

Constructors

Satisfiable

Unsatisfiable

NoAnswer NoAnswerReason

Instances

Eq Answer

Ord Answer

Show Answer

data NoAnswerReason

Constructors

GaveUp

Timeout

Instances

Eq NoAnswerReason

Ord NoAnswerReason

Show NoAnswerReason

data Input a

Constructors

Input

Fields

tag :: Tag

kind :: Kind

what :: a

Instances

Functor Input

Symbolic a => Unpack (Input a)

Symbolic a => Symbolic (Input a)

Pretty a => Pretty (Input a)

type Problem a = Closed [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]

Seq :: (Symbolic a, Symbolic (Seq a)) => TypeOf (Seq a)

Input_ :: (Symbolic a, Symbolic (Input a)) => TypeOf (Input a)

Obligs_ :: TypeOf Obligs

class Symbolic a where

Methods

typeOf :: a -> TypeOf a

Instances

Symbolic Clause

Symbolic Obligs

Symbolic Form

Symbolic Atomic

Symbolic Term

Symbolic a => Symbolic [a]

Symbolic a => Symbolic (Seq a)

Symbolic a => Symbolic (Input a)

Symbolic a => Symbolic (Bind a)

Symbolic a => Symbolic (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

Methods

rep' :: a -> Rep a

Instances

Unpack Clause

Unpack Obligs

Unpack Form

Unpack Atomic

Unpack Term

Symbolic a => Unpack [a]

Symbolic a => Unpack (Seq a)

Symbolic a => Unpack (Input a)

Symbolic a => Unpack (Bind a)

Symbolic a => Unpack (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 = 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 :: forall a b. 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