Safe Haskell | None |
---|

Support for equality.

- class Predicate p => AtomEq atom p term | atom -> p term, term -> atom p where
- foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r
- equals :: term -> term -> atom
- applyEq' :: p -> [term] -> atom

- applyEq :: AtomEq atom p term => p -> [term] -> atom
- data PredicateName p
- zipAtomsEq :: AtomEq atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (term -> term -> term -> term -> Maybe r) -> atom -> atom -> Maybe r
- apply0 :: AtomEq atom p term => p -> atom
- apply1 :: AtomEq atom p a => p -> a -> atom
- apply2 :: AtomEq atom p a => p -> a -> a -> atom
- apply3 :: AtomEq atom p a => p -> a -> a -> a -> atom
- apply4 :: AtomEq atom p a => p -> a -> a -> a -> a -> atom
- apply5 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> atom
- apply6 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> atom
- apply7 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> a -> atom
- pApp :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> [term] -> formula
- pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> formula
- pApp1 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> formula
- pApp2 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> formula
- pApp3 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> formula
- pApp4 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> formula
- pApp5 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> formula
- pApp6 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
- pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
- showFirstOrderFormulaEq :: (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String
- (.=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (≡) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (.!=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (≢) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- fromAtomEq :: (AtomEq atom1 p1 term1, Term term1 v1 f1, AtomEq atom2 p2 term2, Term term2 v2 f2, Constants atom2) => (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> atom1 -> atom2
- showAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f, Show v, Show p, Show f) => atom -> String
- prettyAtomEq :: (AtomEq atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc
- varAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f) => atom -> Set v
- substAtomEq :: (AtomEq atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom
- funcsAtomEq :: (AtomEq atom p term, Term term v f, Ord f) => atom -> Set (f, Int)

# Documentation

class Predicate p => AtomEq atom p term | atom -> p term, term -> atom p whereSource

Its not safe to make Atom a superclass of AtomEq, because the Atom methods will fail on AtomEq instances.

foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> rSource

applyEq :: AtomEq atom p term => p -> [term] -> atomSource

applyEq' with an arity check - clients should always call this.

data PredicateName p Source

A way to represent any predicate's name. Frequently the equality predicate has no standalone representation in the p type, it is just a constructor in the atom type, or even the formula type.

Eq p => Eq (PredicateName p) | |

(Eq (PredicateName p), Ord p) => Ord (PredicateName p) | |

Show p => Show (PredicateName p) | |

(Pretty p, Ord p) => Pretty (PredicateName p) |

zipAtomsEq :: AtomEq atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (term -> term -> term -> term -> Maybe r) -> atom -> atom -> Maybe rSource

pApp :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> [term] -> formulaSource

pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> formulaSource

Versions of pApp specialized for different argument counts.

pApp1 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> formulaSource

pApp2 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> formulaSource

pApp3 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> formulaSource

pApp4 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> formulaSource

pApp5 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> formulaSource

pApp6 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> formulaSource

pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formulaSource

showFirstOrderFormulaEq :: (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> StringSource

(.=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fofSource

(≡) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fofSource

(.!=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fofSource

(≢) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fofSource

fromAtomEq :: (AtomEq atom1 p1 term1, Term term1 v1 f1, AtomEq atom2 p2 term2, Term term2 v2 f2, Constants atom2) => (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> atom1 -> atom2Source

showAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f, Show v, Show p, Show f) => atom -> StringSource

prettyAtomEq :: (AtomEq atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> DocSource

varAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f) => atom -> Set vSource

Return the variables that occur in an instance of AtomEq.