Data.Logic.Types.FirstOrderPublic

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.

Documentation

data Formula v p f

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

Fields

unFormula :: Formula v p f

Instances

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)

(Data v, Data p, Data f) => Data (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 v p f)

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)

(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))

(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))

(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 where

Convert between the public and internal representations.

Methods

public :: i -> p

intern :: p -> i

Instances

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

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