Safe Haskell	None

Data.Logic.Classes.Combine

Contents

Unicode aliases for Combinable class methods
Use in Harrison's code

Description

Class Logic defines the basic boolean logic operations, AND, OR, NOT, and so on. Definitions which pertain to both propositional and first order logic are here.

Synopsis

Documentation

class Negatable formula => Combinable formula whereSource

A type class for logical formulas. Minimal implementation: (.|.)

Methods

(.|.) :: formula -> formula -> formulaSource

Disjunction/OR

(.&.) :: formula -> formula -> formulaSource

Derived formula combinators. These could (and should!) be overridden with expressions native to the instance.

| Conjunction/AND

(.<=>.) :: formula -> formula -> formulaSource

Formula combinators: Equivalence

(.=>.) :: formula -> formula -> formulaSource

Implication

(.<=.) :: formula -> formula -> formulaSource

Reverse implication:

(.<~>.) :: formula -> formula -> formulaSource

Exclusive or

(.~|.) :: formula -> formula -> formulaSource

Nor

(.~&.) :: formula -> formula -> formulaSource

Nand

Instances

Negatable (PropForm a) => Combinable (PropForm a)
(Negatable (Formula atom), Ord atom) => Combinable (Formula atom)
Negatable (Formula a) => Combinable (Formula a)
Negatable (Formula a) => Combinable (Formula a)
(Negatable (Sentence v p f), Ord v, Ord p, Ord f) => Combinable (Sentence v p f)
(Negatable (Formula v p f), Constants (Formula v p f)) => Combinable (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)

data Combination formula Source

Combination is a helper type used in the signatures of the foldPropositional and foldFirstOrder methods so can represent all the ways that formulas can be combined using boolean logic - negation, logical And, and so forth.

Constructors

BinOp formula BinOp formula
:~: formula

Instances

Typeable1 Combination
Eq formula => Eq (Combination formula)
(Typeable (Combination formula), Data formula) => Data (Combination formula)
(Eq (Combination formula), Ord formula) => Ord (Combination formula)
Read formula => Read (Combination formula)
Show formula => Show (Combination formula)
SafeCopy formula0 => SafeCopy (Combination formula0)
Bijection (Combination (Formula v p f)) (Combination (Formula v p f))

combine :: Combinable formula => Combination formula -> formulaSource

A helper function for building folds: foldPropositional combine atomic is a no-op.

data BinOp Source

Represents the boolean logic binary operations, used in the Combination type above.

Constructors

:<=>:	Equivalence
:=>:	Implication
:&:	AND
:\|:	OR

Instances

Bounded BinOp
Enum BinOp
Eq BinOp
Data BinOp
Ord BinOp
Read BinOp
Show BinOp
Typeable BinOp
SafeCopy BinOp
Pretty BinOp

binop :: Combinable formula => formula -> BinOp -> formula -> formulaSource

Unicode aliases for Combinable class methods

(∧) :: Combinable formula => formula -> formula -> formulaSource

(∨) :: Combinable formula => formula -> formula -> formulaSource

(⇒) :: Combinable formula => formula -> formula -> formulaSource

⇒ can't be a function when -XUnicodeSyntax is enabled.

(⇔) :: Combinable formula => formula -> formula -> formulaSource

Use in Harrison's code

(==>) :: Combinable formula => formula -> formula -> formulaSource

(<=>) :: Combinable formula => formula -> formula -> formulaSource

prettyBinOp :: BinOp -> Doc Source