logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Data.Logic.Types.FirstOrderPublic

Description

An instance of FirstOrderFormula which implements Eq and Ord by comparing after conversion to normal form. This helps us notice that formula which only differ in ways that preserve identity, e.g. swapped arguments to a commutative operator.

Synopsis

# Documentation

data Formula v p f Source

The new Formula type is just a wrapper around the Native instance (which eventually should be renamed the Internal instance.) No derived Eq or Ord instances.

Constructors

 Formula FieldsunFormula :: Formula v p f

Instances

 Typeable3 Formula Bijection (Combination (Formula v p f)) (Combination (Formula v p f)) (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v, Constants (Predicate p (PTerm v f)), FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v) => 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), Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v) => Ord (Formula v p f) Here are the magic Ord and Eq instances (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) (Predicate p, Function f v) => HasFixity (Formula v p f) (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Pretty v, Show v, Variable v, Pretty p, Show p, Predicate p, Pretty f, Show f, Function f v) => Pretty (Formula v p f) (Negatable (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Constants (Formula v p f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => Combinable (Formula v p f) (Constants (Formula v p f), Predicate p, Variable v, Function f v) => 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), 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)) (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 Bijection (Formula v p f) (Formula v p f)

class Bijection p i whereSource

Convert between the public and internal representations.

Methods

public :: i -> pSource

intern :: p -> iSource

Instances

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