Data.Logic.Classes.Equals

Support for equality.

Documentation

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

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

Methods

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

equals :: term -> term -> atom

applyEq' :: p -> [term] -> atom

Instances

AtomEq FOLEQ PredName TermType

Predicate p => AtomEq (Predicate p (PTerm v f)) p (PTerm v f)

Predicate p => AtomEq (Sentence v p f) p (CTerm v f)

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

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

data PredicateName p

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.

Constructors

Named p Int

Equals

Instances

Eq 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 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

Versions of pApp specialized for different argument counts.

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 :: forall fof atom v p term. (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 infix 5

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

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

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

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

Return the variables that occur in an instance of AtomEq.

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)