Jukebox.Form

Documentation

debugging :: Bool

data DomainSize

Constructors

Finite Int

Infinite

Instances

Eq DomainSize

Methods

(==) :: DomainSize -> DomainSize -> Bool

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

Ord DomainSize

Methods

compare :: DomainSize -> DomainSize -> Ordering

(<) :: DomainSize -> DomainSize -> Bool

(<=) :: DomainSize -> DomainSize -> Bool

(>) :: DomainSize -> DomainSize -> Bool

(>=) :: DomainSize -> DomainSize -> Bool

max :: DomainSize -> DomainSize -> DomainSize

min :: DomainSize -> DomainSize -> DomainSize

Show DomainSize

Methods

showsPrec :: Int -> DomainSize -> ShowS

show :: DomainSize -> String

showList :: [DomainSize] -> ShowS

data Type

Constructors

O

Type

Fields

• tname :: !Name
• tmonotone :: DomainSize
• tsize :: DomainSize

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

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

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 :: String
• unsatisfiable :: String

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 :: [Signed Atomic] -> Clause

toForm :: Clause -> Form

toLiterals :: Clause -> [Literal]

toClause :: Form -> Maybe Clause

type Tag = String

data Kind

Constructors

Axiom String

Conjecture

Question

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 Answer

Constructors

Satisfiable

Unsatisfiable

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

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

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

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