| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Logic.ATP.Lit
Contents
Description
IsLiteral is a subclass of formulas that support negation and
have true and false elements.
- 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
- data Lit = L {}
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.
Arguments
| :: (lit -> r) | called for normal formulas |
| -> (lit -> r) | called for negated formulas |
| -> lit | |
| -> r |
Test whether a lit is negated or normal
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.
(.~.) :: 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
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 |
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
Example of a JustLiteral type.
Instances
| Eq atom => Eq (LFormula atom) Source | |
| Data atom => Data (LFormula atom) Source | |
| Ord atom => Ord (LFormula atom) Source | |
| Read atom => Read (LFormula atom) Source | |
| Show atom => Show (LFormula atom) Source | |
| IsAtom atom => Pretty (LFormula atom) Source | |
| IsAtom atom => HasFixity (LFormula atom) Source | |
| IsAtom atom => IsFormula (LFormula atom) Source | |
| IsAtom atom => JustLiteral (LFormula atom) Source | |
| (IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source | |
| type AtomOf (LFormula atom) = atom Source |