Safe Haskell	None
Language	Haskell98

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

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

Minimal complete definition

(.|.)

Methods

(.|.) :: formula -> formula -> formula infixr 3 Source

Disjunction/OR

(.&.) :: formula -> formula -> formula infixl 4 Source

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

| Conjunction/AND

(.<=>.) :: formula -> formula -> formula infixl 1 Source

Formula combinators: Equivalence

(.=>.) :: formula -> formula -> formula infixr 2 Source

Implication

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

Reverse implication:

(.<~>.) :: formula -> formula -> formula infixl 1 Source

Exclusive or

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

Nor

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

Nand

Instances

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

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

Eq formula => Eq (Combination formula) Source
Data formula => Data (Combination formula) Source
Ord formula => Ord (Combination formula) Source
Read formula => Read (Combination formula) Source
Show formula => Show (Combination formula) Source
Bijection (Combination (Formula v p f)) (Combination (Formula v p f)) Source

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

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 Source
Enum BinOp Source
Eq BinOp Source
Data BinOp Source
Ord BinOp Source
Read BinOp Source
Show BinOp Source
Pretty BinOp Source

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

Unicode aliases for Combinable class methods

(∧) :: Combinable formula => formula -> formula -> formula infixl 4 Source

(∨) :: Combinable formula => formula -> formula -> formula infixr 3 Source

(⇒) :: Combinable formula => formula -> formula -> formula infixr 2 Source

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

(⇔) :: Combinable formula => formula -> formula -> formula infixl 1 Source

Use in Harrison's code

(==>) :: Combinable formula => formula -> formula -> formula infixr 2 Source

(<=>) :: Combinable formula => formula -> formula -> formula infixl 1 Source

prettyBinOp :: BinOp -> Doc Source