Safe Haskell	None
Language	Haskell98

Data.Logic.ATP.Lit

Contents

Instance

Description

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

Synopsis

Documentation

class IsFormula lit => IsLiteral lit where Source #

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

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

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

Test whether a lit is negated or normal

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

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) Source #
Methods naiveNegate :: LFormula atom -> LFormula atom Source # foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r Source # foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r Source #
(IsFormula (JL a), IsLiteral a) => IsLiteral (JL a) Source #
Methods naiveNegate :: JL a -> JL a Source # foldNegation :: (JL a -> r) -> (JL a -> r) -> JL a -> r Source # foldLiteral' :: (JL a -> r) -> (JL a -> r) -> (Bool -> r) -> (AtomOf (JL a) -> r) -> JL a -> r Source #
IsAtom atom => IsLiteral (PFormula atom) Source #
Methods naiveNegate :: PFormula atom -> PFormula atom Source # foldNegation :: (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r Source # foldLiteral' :: (PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source #
(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsLiteral (QFormula v atom) Source #
Methods naiveNegate :: QFormula v atom -> QFormula v atom Source # foldNegation :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> QFormula v atom -> r Source # foldLiteral' :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source #

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

Negate the formula, avoiding double negation

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

Negate the formula, avoiding double negation

negate :: IsLiteral formula => formula -> formula Source #

Negate the formula, avoiding double negation

negated :: IsLiteral formula => formula -> Bool Source #

Is this formula negated at the top level?

negative :: IsLiteral formula => formula -> Bool Source #

Some operations on IsLiteral formulas

positive :: IsLiteral formula => formula -> Bool Source #

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

class IsLiteral formula => JustLiteral formula Source #

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

Instances

IsAtom atom => JustLiteral (LFormula atom) Source #

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

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

Implementation of onatoms for JustLiteral types.

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

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

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

Combine two literals.

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

Convert a JustLiteral instance to any IsLiteral instance.

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

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

precedenceLiteral :: JustLiteral lit => lit -> Precedence Source #

associativityLiteral :: JustLiteral lit => lit -> Associativity Source #

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

Implementation of pPrint for -- JustLiteral types.

showLiteral :: JustLiteral lit => lit -> String Source #

Instance

data LFormula atom Source #

Example of a JustLiteral type.

Constructors

F
T
Atom atom
Not (LFormula atom)

Instances

Eq atom => Eq (LFormula atom) Source #
Methods (==) :: LFormula atom -> LFormula atom -> Bool # (/=) :: LFormula atom -> LFormula atom -> Bool #
Data atom => Data (LFormula atom) Source #
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) Source #
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) Source #
Methods readsPrec :: Int -> ReadS (LFormula atom) # readList :: ReadS [LFormula atom] # readPrec :: ReadPrec (LFormula atom) # readListPrec :: ReadPrec [LFormula atom] #
Show atom => Show (LFormula atom) Source #
Methods showsPrec :: Int -> LFormula atom -> ShowS # show :: LFormula atom -> String # showList :: [LFormula atom] -> ShowS #
IsAtom atom => Pretty (LFormula atom) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc # pPrint :: LFormula atom -> Doc # pPrintList :: PrettyLevel -> [LFormula atom] -> Doc #
IsAtom atom => HasFixity (LFormula atom) Source #
Methods precedence :: LFormula atom -> Precedence Source # associativity :: LFormula atom -> Associativity Source #
IsAtom atom => IsFormula (LFormula atom) Source #
Associated Types type AtomOf (LFormula atom) :: * Source # Methods true :: LFormula atom Source # false :: LFormula atom Source # asBool :: LFormula atom -> Maybe Bool Source # atomic :: AtomOf (LFormula atom) -> LFormula atom Source # overatoms :: (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r Source # onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom)) -> LFormula atom -> LFormula atom Source #
IsAtom atom => JustLiteral (LFormula atom) Source #

(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source #
Methods naiveNegate :: LFormula atom -> LFormula atom Source # foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r Source # foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r Source #
type AtomOf (LFormula atom) Source #
type AtomOf (LFormula atom) = atom

data Lit Source #

Constructors

L
Fields lname :: String

Instances

Eq Lit Source #
Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Ord Lit Source #
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 #