Data.Logic.Types.FirstOrder

Data types which are instances of the Logic type class for use when you just want to use the classes and you don't have a particular representation you need to use.

Documentation

data Formula v p f

The range of a formula is {True, False} when it has no free variables.

Constructors

Predicate (Predicate p (PTerm v f))

Combine (Combination (Formula v p f))

Quant Quant v (Formula v p f)

Instances

Typeable3 Formula

Bijection (Combination (Formula v p f)) (Combination (Formula v p f))

(Eq v, Eq p, Eq f) => Eq (Formula v p f)

(Typeable (Formula v p f), Data v, Data p, Data f) => Data (Formula v p f)

(Eq (Formula v p f), Ord v, Ord p, Ord f) => Ord (Formula v p f)

(Read v, Read p, Read f) => Read (Formula v p f)

(Show v, Show p, Show f) => Show (Formula v p f)

(SafeCopy v0, SafeCopy p0, SafeCopy f0) => SafeCopy (Formula v0 p0 f0)

Negatable (Formula v p f)

(Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Variable v, Function f v, HasFixity (Predicate p (PTerm v f))) => HasFixity (Formula v p f)

(Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => Pretty (Formula v p f)

(Negatable (Formula v p f), Constants (Formula v p f)) => Combinable (Formula v p f)

Constants p => Constants (Formula v p f)

(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))

(Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))

(Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f))

(Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v

Bijection (Formula v p f) (Formula v p f)

data PTerm v f

The range of a term is an element of a set.

Constructors

Var v

A variable, either free or bound by an enclosing quantifier.

FunApp f [PTerm v f]

Function application. Constants are encoded as nullary functions. The result is another term.

Instances

Typeable2 PTerm

(Eq v, Eq f) => Eq (PTerm v f)

(Typeable (PTerm v f), Data v, Data f) => Data (PTerm v f)

(Eq (PTerm v f), Ord v, Ord f) => Ord (PTerm v f)

(Read v, Read f) => Read (PTerm v f)

(Show v, Show f) => Show (PTerm v f)

(SafeCopy v0, SafeCopy f0) => SafeCopy (PTerm v0 f0)

(Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f))

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

(Ord (PTerm v f), Variable v, Function f v) => Term (PTerm v f) v f

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

(Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v

(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))

(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))

(Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))

(Ord (Formula v p f), Negatable (Formula v p f), Combinable (Formula v p f), Constants (Formula v p f), Pretty (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Show v, Show p, Show f, HasFixity (Formula v p f), Variable v, Predicate p, Function f v) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))

(Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f))

(Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v

(Combinable (Formula v p f), Constants (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v

data Predicate p term

A temporary type used in the fold method to represent the combination of a predicate and its arguments. This reduces the number of arguments to foldFirstOrder and makes it easier to manage the mapping of the different instances to the class methods.

Constructors

Equal term term

Apply p [term]

Instances

Typeable2 Predicate

(Eq p, Eq term) => Eq (Predicate p term)

(Typeable (Predicate p term), Data p, Data term) => Data (Predicate p term)

(Eq (Predicate p term), Ord p, Ord term) => Ord (Predicate p term)

(Read p, Read term) => Read (Predicate p term)

(Show p, Show term) => Show (Predicate p term)

(SafeCopy (MigrateFrom (Predicate p term)), SafeCopy p, SafeCopy term) => Migrate (Predicate p term)

(SafeCopy p0, SafeCopy term0) => SafeCopy (Predicate p0 term0)

HasFixity (Predicate p term)

(Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f))

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

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

(Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v

(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))

(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))

(Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))

(Ord (Formula v p f), Negatable (Formula v p f), Combinable (Formula v p f), Constants (Formula v p f), Pretty (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Show v, Show p, Show f, HasFixity (Formula v p f), Variable v, Predicate p, Function f v) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))

(Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f))

(Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v

(Combinable (Formula v p f), Constants (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v