Safe Haskell	None
Language	Haskell98

Data.Logic.Classes.Apply

Description

The Apply class represents a type of atom the only supports predicate application.

Synopsis

class Predicate p => Apply atom p term | atom -> p term where
- foldApply :: (p -> [term] -> r) -> (Bool -> r) -> atom -> r
- apply' :: p -> [term] -> atom
class (Arity p, Constants p, Eq p, Ord p, Data p, Pretty p) => Predicate p
apply :: Apply atom p term => p -> [term] -> atom
zipApplys :: Apply atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> atom -> atom -> Maybe r
apply0 :: Apply atom p term => p -> atom
apply1 :: Apply atom p term => p -> term -> atom
apply2 :: Apply atom p term => p -> term -> term -> atom
apply3 :: Apply atom p term => p -> term -> term -> term -> atom
apply4 :: Apply atom p term => p -> term -> term -> term -> term -> atom
apply5 :: Apply atom p term => p -> term -> term -> term -> term -> term -> atom
apply6 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> atom
apply7 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> term -> atom
showApply :: (Apply atom p term, Term term v f, Show v, Show p, Show f) => atom -> String
prettyApply :: (Apply atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc
varApply :: (Apply atom p term, Term term v f) => atom -> Set v
substApply :: (Apply atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom
pApp :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> [term] -> formula
pApp0 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> formula
pApp1 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> formula
pApp2 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> formula
pApp3 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> formula
pApp4 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> formula
pApp5 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula
pApp6 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
pApp7 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula

Documentation

class Predicate p => Apply atom p term | atom -> p term where Source

Methods

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

apply' :: p -> [term] -> atom Source

Instances

Apply FOL String TermType
Apply FOLEQ PredName TermType	Using PredName for the predicate type is not quite appropriate here, but we need to implement this instance so we can use it as a superclass of AtomEq below.
(Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f)

class (Arity p, Constants p, Eq p, Ord p, Data p, Pretty p) => Predicate p Source

Instances

Predicate String
Predicate PredName

apply :: Apply atom p term => p -> [term] -> atom Source

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

zipApplys :: Apply atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> atom -> atom -> Maybe r Source

apply0 :: Apply atom p term => p -> atom Source

apply1 :: Apply atom p term => p -> term -> atom Source

apply2 :: Apply atom p term => p -> term -> term -> atom Source

apply3 :: Apply atom p term => p -> term -> term -> term -> atom Source

apply4 :: Apply atom p term => p -> term -> term -> term -> term -> atom Source

apply5 :: Apply atom p term => p -> term -> term -> term -> term -> term -> atom Source

apply6 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> atom Source

apply7 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> term -> atom Source

showApply :: (Apply atom p term, Term term v f, Show v, Show p, Show f) => atom -> String Source

prettyApply :: (Apply atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc Source

varApply :: (Apply atom p term, Term term v f) => atom -> Set v Source

Return the variables that occur in an instance of Apply.

substApply :: (Apply atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom Source

pApp :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> [term] -> formula Source

pApp0 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> formula Source

Versions of pApp specialized for different argument counts.

pApp1 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> formula Source

pApp2 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> formula Source

pApp3 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> formula Source

pApp4 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> formula Source

pApp5 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula Source

pApp6 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula Source

pApp7 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula Source