Copyright	(c) Nils Anders Danielsson 2004-2021
License	See the file LICENCE.
Maintainer	http://www.cse.chalmers.se/~nad/
Stability	experimental
Portability	non-portable (GHC-specific)
Safe Haskell	None
Language	Haskell2010

Test.ChasingBottoms.SemanticOrd

Description

Generic semantic equality and order. The semantic order referred to is that of a typical CPO for Haskell types, where e.g. (True, bottom) <=! (True, False), but where (True, True) and (True, False) are incomparable.

The implementation is based on isBottom, and has the same limitations. Note that non-bottom functions are not handled by any of the functions described below.

One could imagine using QuickCheck for testing equality of functions, but I have not managed to tweak the type system so that it can be done transparently.

Synopsis

data Tweak = Tweak {
- approxDepth :: Maybe Nat
- timeOutLimit :: Maybe Int
}
noTweak :: Tweak
class SemanticEq a where
- (==!), (/=!) :: a -> a -> Bool
- semanticEq :: Tweak -> a -> a -> Bool
class SemanticEq a => SemanticOrd a where
- (<!), (<=!), (>=!), (>!) :: a -> a -> Bool
- semanticCompare :: Tweak -> a -> a -> Maybe Ordering
- (\/!) :: a -> a -> Maybe a
- (/\!) :: a -> a -> a
- semanticJoin :: Tweak -> a -> a -> Maybe a
- semanticMeet :: Tweak -> a -> a -> a

Documentation

data Tweak Source #

The behaviour of some of the functions below can be tweaked.

Constructors

Tweak
Fields approxDepth :: Maybe Nat If equal to `Just n`, an `approxAll n` is performed on all arguments before doing whatever the function is supposed to be doing. timeOutLimit :: Maybe Int If equal to `Just n`, then all computations that take more than `n` seconds to complete are considered to be equal to `bottom`. This functionality is implemented using `isBottomTimeOut`.

Instances

Instances details

Eq Tweak Source #
Instance details Defined in Test.ChasingBottoms.SemanticOrd Methods (==) :: Tweak -> Tweak -> Bool # (/=) :: Tweak -> Tweak -> Bool #
Ord Tweak Source #
Instance details Defined in Test.ChasingBottoms.SemanticOrd Methods compare :: Tweak -> Tweak -> Ordering # (<) :: Tweak -> Tweak -> Bool # (<=) :: Tweak -> Tweak -> Bool # (>) :: Tweak -> Tweak -> Bool # (>=) :: Tweak -> Tweak -> Bool # max :: Tweak -> Tweak -> Tweak # min :: Tweak -> Tweak -> Tweak #
Show Tweak Source #
Instance details Defined in Test.ChasingBottoms.SemanticOrd Methods showsPrec :: Int -> Tweak -> ShowS # show :: Tweak -> String # showList :: [Tweak] -> ShowS #

noTweak :: Tweak Source #

No tweak (both fields are Nothing).

class SemanticEq a where Source #

SemanticEq contains methods for testing whether two terms are semantically equal.

Minimal complete definition

semanticEq

Methods

(==!) :: a -> a -> Bool infix 4 Source #

(/=!) :: a -> a -> Bool infix 4 Source #

semanticEq :: Tweak -> a -> a -> Bool Source #

Instances

Instances details

Data a => SemanticEq a Source #
Instance details Defined in Test.ChasingBottoms.SemanticOrd Methods (==!) :: a -> a -> Bool Source # (/=!) :: a -> a -> Bool Source # semanticEq :: Tweak -> a -> a -> Bool Source #

class SemanticEq a => SemanticOrd a where Source #

SemanticOrd contains methods for testing whether two terms are related according to the semantic domain ordering.

Minimal complete definition

semanticCompare, semanticJoin, semanticMeet

Methods

(<!) :: a -> a -> Bool infix 4 Source #

(<=!) :: a -> a -> Bool infix 4 Source #

(>=!) :: a -> a -> Bool infix 4 Source #

(>!) :: a -> a -> Bool infix 4 Source #

semanticCompare :: Tweak -> a -> a -> Maybe Ordering Source #

semanticCompare tweak x y returns Nothing if x and y are incomparable, and Just o otherwise, where o :: Ordering represents the relation between x and y.

(\/!) :: a -> a -> Maybe a infix 5 Source #

(/\!) :: a -> a -> a infixl 5 Source #

semanticJoin :: Tweak -> a -> a -> Maybe a Source #

semanticMeet :: Tweak -> a -> a -> a Source #

x \/! y and x /\! y compute the least upper and greatest lower bounds, respectively, of x and y in the semantical domain ordering. Note that the least upper bound may not always exist. This functionality was implemented just because it was possible (and to provide analogues of max and min in the Ord class). If anyone finds any use for it, please let me know.

Instances

Instances details

Data a => SemanticOrd a Source #

Instance details

Defined in Test.ChasingBottoms.SemanticOrd

Methods

(<!) :: a -> a -> Bool Source #

(<=!) :: a -> a -> Bool Source #

(>=!) :: a -> a -> Bool Source #

(>!) :: a -> a -> Bool Source #

semanticCompare :: Tweak -> a -> a -> Maybe Ordering Source #

(\/!) :: a -> a -> Maybe a Source #

(/\!) :: a -> a -> a Source #

semanticJoin :: Tweak -> a -> a -> Maybe a Source #

semanticMeet :: Tweak -> a -> a -> a Source #