Safe Haskell	None
Language	Haskell98

Data.Logic.Types.FirstOrder

Description

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.

Synopsis

Documentation

data Formula v p f Source

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

Bijection (Combination (Formula v p f)) (Combination (Formula v p f))
Typeable (* -> * -> * -> *) Formula
(Eq v, Eq p, Eq f) => Eq (Formula v p f)
(Data v, Data p, Data f) => Data (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 v p f)
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)
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))
(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))
(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))
(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 Source

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

(Eq v, Eq f) => Eq (PTerm v f)
(Data v, Data f) => Data (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 v f)
(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))
Typeable (* -> * -> *) PTerm
(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))
(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))
(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))
(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))
(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
(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 Source

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

(Eq p, Eq term) => Eq (Predicate p term)
(Data p, Data term) => Data (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 p, SafeCopy term) => Migrate (Predicate p term)
(SafeCopy p0, SafeCopy term0) => SafeCopy (Predicate p term)
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))
Typeable (* -> * -> *) Predicate
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))
(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))
(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))
(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))
(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
(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
type MigrateFrom (Predicate p term)