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

Named Type

Typed Type

data FunType

Constructors

FunType

Fields

args :: [Type]

res :: Type

Instances

Eq FunType

Typed 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

Named Term

Unpack Term

Symbolic Term

Typed Term

TermLike 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

Unpack Atomic

Symbolic 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)

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 [Form]

Or [Form]

Equiv Form Form

ForAll !(Bind Form)

Exists !(Bind Form)

Connective Connective Form Form

Instances

Unpack Form

Symbolic Form

FormulaLike Form

TermLike Form

data Connective

Constructors

Implies

Follows

Xor

Nor

Nand

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

data Bind a

Constructors

Bind (Set 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

positive :: Form -> Form

notInwards :: Form -> Form

simple :: Form -> Form

simplify :: Form -> Form

data CNF

Constructors

CNF

Fields

axioms :: [Input Clause]

conjectures :: [[Input Clause]]

satisfiable :: String

unsatisfiable :: String

Instances

Unpack CNF

Symbolic CNF

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

newtype Clause

Constructors

Clause (Bind [Literal])

Instances

Unpack Clause

Symbolic Clause

clause :: [Signed Atomic] -> Clause

toForm :: Clause -> Form

toLiterals :: Clause -> [Literal]

type Tag = String

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)

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

Methods

typeOf :: a -> TypeOf a

Instances

Symbolic Clause

Symbolic CNF

Symbolic Form

Symbolic Atomic

Symbolic Term

Symbolic a => Symbolic [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 CNF

Unpack Form

Unpack Atomic

Unpack Term

Symbolic a => Unpack [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 = 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

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 :: Set Variable -> Subst -> Subst

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

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