Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Apply

Synopsis

class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate
class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where
- type PredOf atom
- type TermOf atom
- applyPredicate :: PredOf atom -> [TermOf atom] -> atom
- foldApply' :: (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
- overterms :: (TermOf atom -> r -> r) -> r -> atom -> r
- onterms :: (TermOf atom -> TermOf atom) -> atom -> atom
atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity)
functions :: (IsFormula formula, HasApply atom, Ord function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term) => formula -> Set (function, Arity)
class HasApply atom => JustApply atom
foldApply :: (JustApply atom, term ~ TermOf atom) => (PredOf atom -> [term] -> r) -> atom -> r
prettyApply :: (v ~ TVarOf term, IsPredicate predicate, IsTerm term) => predicate -> [term] -> Doc
overtermsApply :: JustApply atom => (TermOf atom -> r -> r) -> r -> atom -> r
ontermsApply :: JustApply atom => (TermOf atom -> TermOf atom) -> atom -> atom
zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1, JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) => (predicate -> [(term, term)] -> Maybe r) -> atom1 -> atom2 -> Maybe r
showApply :: (Show predicate, Show term) => predicate -> [term] -> String
convertApply :: (JustApply atom1, HasApply atom2) => (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
onformula :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom) => (term -> term) -> formula -> formula
pApp :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula) => PredOf atom -> [TermOf atom] -> formula
data FOLAP predicate term = AP predicate [term]
data Predicate
type ApAtom = FOLAP Predicate FTerm

Documentation

class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate Source #

A predicate is the thing we apply to a list of IsTerms to make an IsAtom.

Instances

Instances details

IsPredicate Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply

class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where Source #

The result of applying a predicate to some terms is an atomic formula whose type is an instance of HasApply.

Associated Types

type PredOf atom Source #

type TermOf atom Source #

Methods

applyPredicate :: PredOf atom -> [TermOf atom] -> atom Source #

foldApply' :: (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r Source #

overterms :: (TermOf atom -> r -> r) -> r -> atom -> r Source #

onterms :: (TermOf atom -> TermOf atom) -> atom -> atom Source #

Instances

Instances details

(IsPredicate predicate, IsTerm term) => HasApply (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Associated Types type PredOf (FOLAP predicate term) Source # type TermOf (FOLAP predicate term) Source # Methods applyPredicate :: PredOf (FOLAP predicate term) -> [TermOf (FOLAP predicate term)] -> FOLAP predicate term Source # foldApply' :: (FOLAP predicate term -> r) -> (PredOf (FOLAP predicate term) -> [TermOf (FOLAP predicate term)] -> r) -> FOLAP predicate term -> r Source # overterms :: (TermOf (FOLAP predicate term) -> r -> r) -> r -> FOLAP predicate term -> r Source # onterms :: (TermOf (FOLAP predicate term) -> TermOf (FOLAP predicate term)) -> FOLAP predicate term -> FOLAP predicate term Source #
(IsPredicate predicate, IsTerm term) => HasApply (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Associated Types type PredOf (FOL predicate term) Source # type TermOf (FOL predicate term) Source # Methods applyPredicate :: PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> FOL predicate term Source # foldApply' :: (FOL predicate term -> r) -> (PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r) -> FOL predicate term -> r Source # overterms :: (TermOf (FOL predicate term) -> r -> r) -> r -> FOL predicate term -> r Source # onterms :: (TermOf (FOL predicate term) -> TermOf (FOL predicate term)) -> FOL predicate term -> FOL predicate term Source #

atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity) Source #

The set of functions in an atom.

functions :: (IsFormula formula, HasApply atom, Ord function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term) => formula -> Set (function, Arity) Source #

The set of functions in a formula.

class HasApply atom => JustApply atom Source #

Atoms that have apply but do not support equate

Instances

Instances details

JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
(IsPredicate predicate, IsTerm term) => JustApply (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply

foldApply :: (JustApply atom, term ~ TermOf atom) => (PredOf atom -> [term] -> r) -> atom -> r Source #

prettyApply :: (v ~ TVarOf term, IsPredicate predicate, IsTerm term) => predicate -> [term] -> Doc Source #

Pretty print prefix application of a predicate

overtermsApply :: JustApply atom => (TermOf atom -> r -> r) -> r -> atom -> r Source #

Implementation of overterms for HasApply types.

ontermsApply :: JustApply atom => (TermOf atom -> TermOf atom) -> atom -> atom Source #

Implementation of onterms for HasApply types.

zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1, JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) => (predicate -> [(term, term)] -> Maybe r) -> atom1 -> atom2 -> Maybe r Source #

Zip two atoms if they are similar

showApply :: (Show predicate, Show term) => predicate -> [term] -> String Source #

Implementation of Show for JustApply types

convertApply :: (JustApply atom1, HasApply atom2) => (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2 Source #

Convert between two instances of HasApply

onformula :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom) => (term -> term) -> formula -> formula Source #

Special case of applying a subfunction to the top *terms*.

pApp :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula) => PredOf atom -> [TermOf atom] -> formula Source #

Build a formula from a predicate and a list of terms.

data FOLAP predicate term Source #

First order logic formula atom type.

Constructors

AP predicate [term]

Instances

Instances details

JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
IsFirstOrder ApFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
(IsPredicate predicate, IsTerm term) => HasApply (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Associated Types type PredOf (FOLAP predicate term) Source # type TermOf (FOLAP predicate term) Source # Methods applyPredicate :: PredOf (FOLAP predicate term) -> [TermOf (FOLAP predicate term)] -> FOLAP predicate term Source # foldApply' :: (FOLAP predicate term -> r) -> (PredOf (FOLAP predicate term) -> [TermOf (FOLAP predicate term)] -> r) -> FOLAP predicate term -> r Source # overterms :: (TermOf (FOLAP predicate term) -> r -> r) -> r -> FOLAP predicate term -> r Source # onterms :: (TermOf (FOLAP predicate term) -> TermOf (FOLAP predicate term)) -> FOLAP predicate term -> FOLAP predicate term Source #
(IsPredicate predicate, IsTerm term) => JustApply (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply
(IsPredicate predicate, IsTerm term) => IsAtom (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply
HasFixity (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods precedence :: FOLAP predicate term -> Precedence Source # associativity :: FOLAP predicate term -> Associativity Source #
(Data term, Data predicate) => Data (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOLAP predicate term -> c (FOLAP predicate term) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FOLAP predicate term) # toConstr :: FOLAP predicate term -> Constr # dataTypeOf :: FOLAP predicate term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FOLAP predicate term)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FOLAP predicate term)) # gmapT :: (forall b. Data b => b -> b) -> FOLAP predicate term -> FOLAP predicate term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOLAP predicate term -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOLAP predicate term -> r # gmapQ :: (forall d. Data d => d -> u) -> FOLAP predicate term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FOLAP predicate term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOLAP predicate term -> m (FOLAP predicate term) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOLAP predicate term -> m (FOLAP predicate term) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOLAP predicate term -> m (FOLAP predicate term) #
(Read predicate, Read term) => Read (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods readsPrec :: Int -> ReadS (FOLAP predicate term) # readList :: ReadS [FOLAP predicate term] # readPrec :: ReadPrec (FOLAP predicate term) # readListPrec :: ReadPrec [FOLAP predicate term] #
(IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods showsPrec :: Int -> FOLAP predicate term -> ShowS # show :: FOLAP predicate term -> String # showList :: [FOLAP predicate term] -> ShowS #
(Eq predicate, Eq term) => Eq (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods (==) :: FOLAP predicate term -> FOLAP predicate term -> Bool # (/=) :: FOLAP predicate term -> FOLAP predicate term -> Bool #
(Ord predicate, Ord term) => Ord (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods compare :: FOLAP predicate term -> FOLAP predicate term -> Ordering # (<) :: FOLAP predicate term -> FOLAP predicate term -> Bool # (<=) :: FOLAP predicate term -> FOLAP predicate term -> Bool # (>) :: FOLAP predicate term -> FOLAP predicate term -> Bool # (>=) :: FOLAP predicate term -> FOLAP predicate term -> Bool # max :: FOLAP predicate term -> FOLAP predicate term -> FOLAP predicate term # min :: FOLAP predicate term -> FOLAP predicate term -> FOLAP predicate term #
(IsPredicate predicate, IsTerm term) => Pretty (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods pPrintPrec :: PrettyLevel -> Rational -> FOLAP predicate term -> Doc # pPrint :: FOLAP predicate term -> Doc # pPrintList :: PrettyLevel -> [FOLAP predicate term] -> Doc #
type PredOf (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply type PredOf (FOLAP predicate term) = predicate
type TermOf (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply type TermOf (FOLAP predicate term) = term

data Predicate Source #

A predicate type with no distinct equality.

Instances

Instances details

IsPredicate Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply
JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
IsFirstOrder ApFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder EqFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder Formula Source #
Instance details Defined in Data.Logic.ATP.Skolem
Data Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Predicate -> c Predicate # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Predicate # toConstr :: Predicate -> Constr # dataTypeOf :: Predicate -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Predicate) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate) # gmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r # gmapQ :: (forall d. Data d => d -> u) -> Predicate -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Predicate -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #
IsString Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods fromString :: String -> Predicate #
Read Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods readsPrec :: Int -> ReadS Predicate # readList :: ReadS [Predicate] # readPrec :: ReadPrec Predicate # readListPrec :: ReadPrec [Predicate] #
Show Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods showsPrec :: Int -> Predicate -> ShowS # show :: Predicate -> String # showList :: [Predicate] -> ShowS #
Eq Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods (==) :: Predicate -> Predicate -> Bool # (/=) :: Predicate -> Predicate -> Bool #
Ord Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods compare :: Predicate -> Predicate -> Ordering # (<) :: Predicate -> Predicate -> Bool # (<=) :: Predicate -> Predicate -> Bool # (>) :: Predicate -> Predicate -> Bool # (>=) :: Predicate -> Predicate -> Bool # max :: Predicate -> Predicate -> Predicate # min :: Predicate -> Predicate -> Predicate #
Pretty Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods pPrintPrec :: PrettyLevel -> Rational -> Predicate -> Doc # pPrint :: Predicate -> Doc # pPrintList :: PrettyLevel -> [Predicate] -> Doc #
MonadFail m => Unify m (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif Associated Types type UTermOf (SkAtom, SkAtom) Source # Methods unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m () Source #
type UTermOf (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type ApAtom = FOLAP Predicate FTerm Source #

An atom type with no equality predicate