atp-haskell-1.10: Translation from Ocaml to Haskell of John Harrison's ATP code

Safe HaskellNone
LanguageHaskell98

Data.Logic.ATP.Apply

Synopsis

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

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

(IsPredicate predicate, IsTerm term) => HasApply (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term) => HasApply (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

JustApply ApAtom Source 
(IsPredicate predicate, IsTerm term) => JustApply (FOLAP predicate term) Source 

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

JustApply ApAtom Source 
IsFirstOrder ApFormula Source 
(Eq predicate, Eq term) => Eq (FOLAP predicate term) Source 
(Data predicate, Data term) => Data (FOLAP predicate term) Source 
(Ord predicate, Ord term) => Ord (FOLAP predicate term) Source 
(Read predicate, Read term) => Read (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term) => Pretty (FOLAP predicate term) Source 
HasFixity (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term) => IsAtom (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term) => JustApply (FOLAP predicate term) Source 
(IsPredicate predicate, IsTerm term) => HasApply (FOLAP predicate term) Source 
type PredOf (FOLAP predicate term) = predicate Source 
type TermOf (FOLAP predicate term) = term Source 

data Predicate Source

A predicate type with no distinct equality.

Instances

type ApAtom = FOLAP Predicate FTerm Source

An atom type with no equality predicate