Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Lit

Contents

Instance

Description

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

Synopsis

class IsFormula lit => IsLiteral lit where
- naiveNegate :: lit -> lit
- foldNegation :: (lit -> r) -> (lit -> r) -> lit -> r
- foldLiteral' :: (lit -> r) -> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
(.~.) :: IsLiteral formula => formula -> formula
(¬) :: IsLiteral formula => formula -> formula
negate :: IsLiteral formula => formula -> formula
negated :: IsLiteral formula => formula -> Bool
negative :: IsLiteral formula => formula -> Bool
positive :: IsLiteral formula => formula -> Bool
foldLiteral :: JustLiteral lit => (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
class IsLiteral formula => JustLiteral formula
onatomsLiteral :: JustLiteral lit => (AtomOf lit -> AtomOf lit) -> lit -> lit
overatomsLiteral :: JustLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r
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
zipLiterals :: (JustLiteral lit1, JustLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r
convertLiteral :: (JustLiteral lit1, IsLiteral lit2) => (AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertToLiteral :: (IsLiteral formula, JustLiteral lit) => (formula -> lit) -> (AtomOf formula -> AtomOf lit) -> formula -> lit
precedenceLiteral :: JustLiteral lit => lit -> Precedence
associativityLiteral :: JustLiteral lit => lit -> Associativity
prettyLiteral :: JustLiteral lit => PrettyLevel -> Rational -> lit -> Doc
showLiteral :: JustLiteral lit => lit -> String
data LFormula atom
- = F
- | T
- | Atom atom
- | Not (LFormula atom)
data Lit = L {
- lname :: String
}

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.

Methods

naiveNegate :: lit -> lit Source #

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

foldNegation Source #

Arguments

:: (lit -> r)	called for normal formulas
-> (lit -> r)	called for negated formulas
-> lit
-> r

Test whether a lit is negated or normal

foldLiteral' Source #

Arguments

:: (lit -> r)	Called for higher order formulas (non-literal)
-> (lit -> r)	Called for negated formulas
-> (Bool -> r)	Called for true and false formulas
-> (AtomOf lit -> r)	Called for atomic formulas
-> 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

Instances details

(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit 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 #
Instance details Defined in Data.Logic.ATP.LitWrapper 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 #
Instance details Defined in Data.Logic.ATP.Prop 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 #
Instance details Defined in Data.Logic.ATP.Quantified 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

Instances details

IsAtom atom => JustLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit
(IsFormula (JL a), IsLiteral a) => JustLiteral (JL a) Source #
Instance details Defined in Data.Logic.ATP.LitWrapper

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

Instances details

IsAtom atom => IsFormula (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit 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 #
(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit 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 #
IsAtom atom => JustLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit
IsAtom atom => HasFixity (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods precedence :: LFormula atom -> Precedence Source # associativity :: LFormula atom -> Associativity Source #
Data atom => Data (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit 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 :: forall r r'. (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) #
Read atom => Read (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods readsPrec :: Int -> ReadS (LFormula atom) # readList :: ReadS [LFormula atom] # readPrec :: ReadPrec (LFormula atom) # readListPrec :: ReadPrec [LFormula atom] #
Show atom => Show (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods showsPrec :: Int -> LFormula atom -> ShowS # show :: LFormula atom -> String # showList :: [LFormula atom] -> ShowS #
Eq atom => Eq (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods (==) :: LFormula atom -> LFormula atom -> Bool # (/=) :: LFormula atom -> LFormula atom -> Bool #
Ord atom => Ord (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit 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 #
IsAtom atom => Pretty (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc # pPrint :: LFormula atom -> Doc # pPrintList :: PrettyLevel -> [LFormula atom] -> Doc #
type AtomOf (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit type AtomOf (LFormula atom) = atom

data Lit Source #

Constructors

L
Fields lname :: String

Instances

Instances details

Eq Lit Source #
Instance details Defined in Data.Logic.ATP.Lit Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Ord Lit Source #
Instance details Defined in Data.Logic.ATP.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 #