Data.Logic.ATP.Lit

IsLiteral is a subclass of formulas that support negation and have true and false elements.

Documentation

class IsFormula lit => IsLiteral lit where

The class of formulas that can be negated. Literals are the building blocks of the clause and implicative normal forms. They support negation and must include true and false elements.

Minimal complete definition

naiveNegate, foldNegation, foldLiteral'

Methods

naiveNegate :: lit -> lit

Negate a formula in a naive fashion, the operators below prevent double negation.

foldNegation :: (lit -> r) -> (lit -> r) -> lit -> r

Test whether a lit is negated or normal

foldLiteral' :: (lit -> r) -> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r

This is the internal fold for literals, foldLiteral below should normally be used, but its argument must be an instance of JustLiteral.

Instances

(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom)

Methods

naiveNegate :: LFormula atom -> LFormula atom

foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r

foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r

(IsFormula (JL a), IsLiteral a) => IsLiteral (JL a)

Methods

naiveNegate :: JL a -> JL a

foldNegation :: (JL a -> r) -> (JL a -> r) -> JL a -> r

foldLiteral' :: (JL a -> r) -> (JL a -> r) -> (Bool -> r) -> (AtomOf (JL a) -> r) -> JL a -> r

IsAtom atom => IsLiteral (PFormula atom)

Methods

naiveNegate :: PFormula atom -> PFormula atom

foldNegation :: (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r

foldLiteral' :: (PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r

(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsLiteral (QFormula v atom)

Methods

naiveNegate :: QFormula v atom -> QFormula v atom

foldNegation :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> QFormula v atom -> r

foldLiteral' :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

(.~.) :: IsLiteral formula => formula -> formula infix 6

Negate the formula, avoiding double negation

(¬) :: IsLiteral formula => formula -> formula infix 6

Negate the formula, avoiding double negation

negate :: IsLiteral formula => formula -> formula

Negate the formula, avoiding double negation

negated :: IsLiteral formula => formula -> Bool

Is this formula negated at the top level?

negative :: IsLiteral formula => formula -> Bool

Some operations on IsLiteral formulas

positive :: IsLiteral formula => formula -> Bool

foldLiteral :: JustLiteral lit => (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r

class IsLiteral formula => JustLiteral formula

Class that indicates that a formula type *only* contains IsLiteral features - no combinations or quantifiers.

Instances

IsAtom atom => JustLiteral (LFormula atom)

(IsFormula (JL a), IsLiteral a) => JustLiteral (JL a)

onatomsLiteral :: JustLiteral lit => (AtomOf lit -> AtomOf lit) -> lit -> lit

Implementation of onatoms for JustLiteral types.

overatomsLiteral :: JustLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r

implementation of overatoms for JustLiteral types.

zipLiterals' :: (IsLiteral lit1, IsLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r

Combine two literals (internal version).

zipLiterals :: (JustLiteral lit1, JustLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r

Combine two literals.

convertLiteral :: (JustLiteral lit1, IsLiteral lit2) => (AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2

Convert a JustLiteral instance to any IsLiteral instance.

convertToLiteral :: (IsLiteral formula, JustLiteral lit) => (formula -> lit) -> (AtomOf formula -> AtomOf lit) -> formula -> lit

Convert any formula to a literal, passing non-IsLiteral structures to the first argument (typically a call to error.)

precedenceLiteral :: JustLiteral lit => lit -> Precedence

associativityLiteral :: JustLiteral lit => lit -> Associativity

prettyLiteral :: JustLiteral lit => PrettyLevel -> Rational -> lit -> Doc

Implementation of pPrint for -- JustLiteral types.

showLiteral :: JustLiteral lit => lit -> String

Instance

data LFormula atom

Example of a JustLiteral type.

Constructors

F

T

Atom atom

Not (LFormula atom)

Instances

Eq atom => Eq (LFormula atom)

Methods

(==) :: LFormula atom -> LFormula atom -> Bool

(/=) :: LFormula atom -> LFormula atom -> Bool

Data atom => Data (LFormula atom)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LFormula atom)

toConstr :: LFormula atom -> Constr

dataTypeOf :: LFormula atom -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (LFormula atom))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LFormula atom))

gmapT :: (forall b. Data b => b -> b) -> LFormula atom -> LFormula atom

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r

gmapQ :: (forall d. Data d => d -> u) -> LFormula atom -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LFormula atom -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom)

Ord atom => Ord (LFormula atom)

Methods

compare :: LFormula atom -> LFormula atom -> Ordering

(<) :: LFormula atom -> LFormula atom -> Bool

(<=) :: LFormula atom -> LFormula atom -> Bool

(>) :: LFormula atom -> LFormula atom -> Bool

(>=) :: LFormula atom -> LFormula atom -> Bool

max :: LFormula atom -> LFormula atom -> LFormula atom

min :: LFormula atom -> LFormula atom -> LFormula atom

Read atom => Read (LFormula atom)

Methods

readsPrec :: Int -> ReadS (LFormula atom)

readList :: ReadS [LFormula atom]

readPrec :: ReadPrec (LFormula atom)

readListPrec :: ReadPrec [LFormula atom]

Show atom => Show (LFormula atom)

Methods

showsPrec :: Int -> LFormula atom -> ShowS

show :: LFormula atom -> String

showList :: [LFormula atom] -> ShowS

IsAtom atom => Pretty (LFormula atom)

Methods

pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc

pPrint :: LFormula atom -> Doc

pPrintList :: PrettyLevel -> [LFormula atom] -> Doc

IsAtom atom => HasFixity (LFormula atom)

Methods

precedence :: LFormula atom -> Precedence

associativity :: LFormula atom -> Associativity

IsAtom atom => IsFormula (LFormula atom)

Associated Types

type AtomOf (LFormula atom) :: *

Methods

true :: LFormula atom

false :: LFormula atom

asBool :: LFormula atom -> Maybe Bool

atomic :: AtomOf (LFormula atom) -> LFormula atom

overatoms :: (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r

onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom)) -> LFormula atom -> LFormula atom

IsAtom atom => JustLiteral (LFormula atom)

(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom)

Methods

naiveNegate :: LFormula atom -> LFormula atom

foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r

foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r

type AtomOf (LFormula atom)

type AtomOf (LFormula atom) = atom

data Lit

Constructors

L

Fields

• lname :: String

Instances

Eq Lit

Methods

(==) :: Lit -> Lit -> Bool

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

Ord Lit

Methods

compare :: Lit -> Lit -> Ordering

(<) :: Lit -> Lit -> Bool

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

(>) :: Lit -> Lit -> Bool

(>=) :: Lit -> Lit -> Bool

max :: Lit -> Lit -> Lit

min :: Lit -> Lit -> Lit