Copyright | (c) Michal Konecny |
---|---|

License | BSD3 |

Maintainer | mikkonecny@gmail.com |

Stability | experimental |

Portability | portable |

Safe Haskell | None |

Language | Haskell98 |

## Synopsis

- type IsBool t = (HasBools t, CanNegSameType t, CanAndOrSameType t)
- specIsBool :: (IsBool t, CanTestCertainly t, Show t, Serial IO t) => T t -> Spec
- type HasBools t = ConvertibleExactly Bool t
- class HasBools t => CanTestCertainly t where
- isCertainlyTrue :: t -> Bool
- isCertainlyFalse :: t -> Bool

- specCanTestCertainly :: CanTestCertainly t => T t -> Spec
- type CanTestCertainlyX t = (CanTestCertainly t, Show t, Serial IO t)
- isNotTrue :: CanTestCertainly t => t -> Bool
- isNotFalse :: CanTestCertainly t => t -> Bool
- stronglyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
- stronglyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
- weaklyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
- weaklyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
- class CanNeg t where
- not :: CanNeg t => t -> NegType t
- type CanNegSameType t = (CanNeg t, NegType t ~ t)
- specCanNegBool :: (Show t, Show (NegType (NegType t)), Serial IO t, CanTestCertainly t, CanTestCertainly (NegType t), CanTestCertainly (NegType (NegType t)), CanNeg t, CanNeg (NegType t)) => T t -> Spec
- type CanAndOr t1 t2 = (CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t2 t1, AndOrType t1 t2 ~ AndOrType t2 t1)
- class CanAndOrAsymmetric t1 t2 where
- (&&) :: CanAndOrAsymmetric a b => a -> b -> AndOrType a b
- (||) :: CanAndOrAsymmetric a b => a -> b -> AndOrType a b
- type CanAndOrWith t1 t2 = (CanAndOr t1 t2, AndOrType t1 t2 ~ t1)
- type CanAndOrSameType t = CanAndOrWith t t
- and :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
- or :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
- specCanAndOr :: (Show t1, Show t2, Show t3, Show (AndOrType t1 t1), Show (AndOrType t1 t2), Show (AndOrType t2 t1), Show (AndOrType t1 (AndOrType t2 t3)), Show (AndOrType (AndOrType t1 t2) t3), Show (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)), Show (NegType (AndOrType t1 t2)), Show (AndOrType (NegType t1) (NegType t2)), Serial IO t1, Serial IO t2, Serial IO t3, CanTestCertainly t1, CanTestCertainly (AndOrType t1 t1), CanTestCertainly (AndOrType t1 t2), CanTestCertainly (AndOrType t2 t1), CanTestCertainly (AndOrType t1 (AndOrType t2 t3)), CanTestCertainly (AndOrType (AndOrType t1 t2) t3), CanTestCertainly (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)), CanTestCertainly (NegType (AndOrType t1 t2)), CanTestCertainly (AndOrType (NegType t1) (NegType t2)), CanNeg t1, CanNeg t2, CanNeg (AndOrType t1 t2), CanAndOrAsymmetric t1 t1, CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t1 t3, CanAndOrAsymmetric t1 (AndOrType t2 t3), CanAndOrAsymmetric t2 t1, CanAndOrAsymmetric t2 t3, CanAndOrAsymmetric (AndOrType t1 t2) t3, CanAndOrAsymmetric (AndOrType t1 t2) (AndOrType t1 t3), CanAndOrAsymmetric (NegType t1) (NegType t2)) => T t1 -> T t2 -> T t3 -> Spec
- specCanAndOrNotMixed :: (Show t, Show (AndOrType t t), Show (AndOrType t (AndOrType t t)), Show (AndOrType (AndOrType t t) t), Show (AndOrType (AndOrType t t) (AndOrType t t)), Show (NegType (AndOrType t t)), Show (AndOrType (NegType t) (NegType t)), Serial IO t, CanTestCertainly t, CanTestCertainly (AndOrType t t), CanTestCertainly (AndOrType t (AndOrType t t)), CanTestCertainly (AndOrType (AndOrType t t) t), CanTestCertainly (AndOrType (AndOrType t t) (AndOrType t t)), CanTestCertainly (NegType (AndOrType t t)), CanTestCertainly (AndOrType (NegType t) (NegType t)), CanNeg t, CanNeg (AndOrType t t), CanAndOrAsymmetric t t, CanAndOrAsymmetric t (AndOrType t t), CanAndOrAsymmetric (AndOrType t t) t, CanAndOrAsymmetric (AndOrType t t) (AndOrType t t), CanAndOrAsymmetric (NegType t) (NegType t)) => T t -> Spec

# Documentation

type IsBool t = (HasBools t, CanNegSameType t, CanAndOrSameType t) Source #

A type constraint synonym that stipulates that the type behaves very much like Bool, except it does not necessarily satisfy the law of excluded middle, which means that the type can contain a "do-not-know" value.

Examples: `Bool`

, `Maybe Bool`

, `Maybe (Maybe Bool)`

, `CollectErrors Bool`

specIsBool :: (IsBool t, CanTestCertainly t, Show t, Serial IO t) => T t -> Spec Source #

HSpec properties that each implementation of IsBool should satisfy.

# Conversion to/from Bool

type HasBools t = ConvertibleExactly Bool t Source #

class HasBools t => CanTestCertainly t where Source #

Tests for truth or falsity. Beware, when `isCertainlyTrue`

returns `False`

,
it does not mean that the proposition is false. It usually means that
we failed to prove the proposition.

isCertainlyTrue :: t -> Bool Source #

isCertainlyFalse :: t -> Bool Source #

## Instances

CanTestCertainly Bool Source # | |

Defined in Numeric.MixedTypes.Bool isCertainlyTrue :: Bool -> Bool Source # isCertainlyFalse :: Bool -> Bool Source # | |

CanTestCertainly t => CanTestCertainly (Maybe t) Source # | |

Defined in Numeric.MixedTypes.Bool isCertainlyTrue :: Maybe t -> Bool Source # isCertainlyFalse :: Maybe t -> Bool Source # | |

(CanTestCertainly t, SuitableForCE es) => CanTestCertainly (CollectErrors es t) Source # | |

Defined in Numeric.MixedTypes.Bool isCertainlyTrue :: CollectErrors es t -> Bool Source # isCertainlyFalse :: CollectErrors es t -> Bool Source # |

specCanTestCertainly :: CanTestCertainly t => T t -> Spec Source #

HSpec properties that each implementation of CanTestCertainly should satisfy.

type CanTestCertainlyX t = (CanTestCertainly t, Show t, Serial IO t) Source #

Compound type constraint useful for test definition.

isNotTrue :: CanTestCertainly t => t -> Bool Source #

isNotFalse :: CanTestCertainly t => t -> Bool Source #

stronglyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool Source #

If l is certainly True, then r is also certainly True.

stronglyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool Source #

weaklyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool Source #

If l is certainly True, then r is not certainly False.

weaklyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool Source #

# Negation

This is negation is both the numeric negation as well as the Boolean negation. Example of non-standard Boolean negation:

negate (Just True) = Just False

## Instances

CanNeg Bool Source # | |

CanNeg Double Source # | |

CanNeg Int Source # | |

CanNeg Integer Source # | |

CanNeg Rational Source # | |

CanNeg t => CanNeg (Maybe t) Source # | |

CanNeg t => CanNeg (Complex t) Source # | |

(CanNeg t, SuitableForCE es, CanEnsureCE es t, CanEnsureCE es (NegType t)) => CanNeg (CollectErrors es t) Source # | |

Defined in Numeric.MixedTypes.Bool type NegType (CollectErrors es t) :: Type Source # negate :: CollectErrors es t -> NegType (CollectErrors es t) Source # |

type CanNegSameType t = (CanNeg t, NegType t ~ t) Source #

## Tests

specCanNegBool :: (Show t, Show (NegType (NegType t)), Serial IO t, CanTestCertainly t, CanTestCertainly (NegType t), CanTestCertainly (NegType (NegType t)), CanNeg t, CanNeg (NegType t)) => T t -> Spec Source #

HSpec properties that each Boolean implementation of CanNeg should satisfy.

# And and or

type CanAndOr t1 t2 = (CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t2 t1, AndOrType t1 t2 ~ AndOrType t2 t1) Source #

class CanAndOrAsymmetric t1 t2 where Source #

Binary logical `and`

and `or`

for generalised Booleans. For example:

(Just True) && False = Just False (Just (Just True)) || False = (Just (Just True))

## Instances

type CanAndOrWith t1 t2 = (CanAndOr t1 t2, AndOrType t1 t2 ~ t1) Source #

type CanAndOrSameType t = CanAndOrWith t t Source #

and :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t Source #

or :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t Source #

## Tests

specCanAndOr :: (Show t1, Show t2, Show t3, Show (AndOrType t1 t1), Show (AndOrType t1 t2), Show (AndOrType t2 t1), Show (AndOrType t1 (AndOrType t2 t3)), Show (AndOrType (AndOrType t1 t2) t3), Show (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)), Show (NegType (AndOrType t1 t2)), Show (AndOrType (NegType t1) (NegType t2)), Serial IO t1, Serial IO t2, Serial IO t3, CanTestCertainly t1, CanTestCertainly (AndOrType t1 t1), CanTestCertainly (AndOrType t1 t2), CanTestCertainly (AndOrType t2 t1), CanTestCertainly (AndOrType t1 (AndOrType t2 t3)), CanTestCertainly (AndOrType (AndOrType t1 t2) t3), CanTestCertainly (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)), CanTestCertainly (NegType (AndOrType t1 t2)), CanTestCertainly (AndOrType (NegType t1) (NegType t2)), CanNeg t1, CanNeg t2, CanNeg (AndOrType t1 t2), CanAndOrAsymmetric t1 t1, CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t1 t3, CanAndOrAsymmetric t1 (AndOrType t2 t3), CanAndOrAsymmetric t2 t1, CanAndOrAsymmetric t2 t3, CanAndOrAsymmetric (AndOrType t1 t2) t3, CanAndOrAsymmetric (AndOrType t1 t2) (AndOrType t1 t3), CanAndOrAsymmetric (NegType t1) (NegType t2)) => T t1 -> T t2 -> T t3 -> Spec Source #

HSpec properties that each implementation of CanAndOr should satisfy.

specCanAndOrNotMixed :: (Show t, Show (AndOrType t t), Show (AndOrType t (AndOrType t t)), Show (AndOrType (AndOrType t t) t), Show (AndOrType (AndOrType t t) (AndOrType t t)), Show (NegType (AndOrType t t)), Show (AndOrType (NegType t) (NegType t)), Serial IO t, CanTestCertainly t, CanTestCertainly (AndOrType t t), CanTestCertainly (AndOrType t (AndOrType t t)), CanTestCertainly (AndOrType (AndOrType t t) t), CanTestCertainly (AndOrType (AndOrType t t) (AndOrType t t)), CanTestCertainly (NegType (AndOrType t t)), CanTestCertainly (AndOrType (NegType t) (NegType t)), CanNeg t, CanNeg (AndOrType t t), CanAndOrAsymmetric t t, CanAndOrAsymmetric t (AndOrType t t), CanAndOrAsymmetric (AndOrType t t) t, CanAndOrAsymmetric (AndOrType t t) (AndOrType t t), CanAndOrAsymmetric (NegType t) (NegType t)) => T t -> Spec Source #

HSpec properties that each implementation of CanAndOr should satisfy.

# Orphan instances

ConvertibleExactly Bool Bool Source # | |

ConvertibleExactly Bool t => ConvertibleExactly Bool (Maybe t) Source # | |

safeConvertExactly :: Bool -> ConvertResult (Maybe t) Source # |