diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,7 @@ -# Revision history for orders +# Revision history for connections -## 0.0.1 -- YYYY-mm-dd +## 0.0.3 -- 2020-02-17 -* First version. Released on an unsuspecting world. +* `Data.Float` : add cmath utils +* `Data.Connection.Ratio` : add rational connections +* `Numeric.Prelude` : add numeric prelude diff --git a/connections.cabal b/connections.cabal --- a/connections.cabal +++ b/connections.cabal @@ -1,7 +1,7 @@ name: connections -version: 0.0.2.2 -synopsis: Partial orders, lattices, & Galois connections. -description: A library for precision rounding using Galois connections. +version: 0.0.3 +synopsis: Partial orders, Galois connections, and lattices. +description: A library for numerical conversions using Galois connections. homepage: https://github.com/cmk/connections license: BSD3 license-file: LICENSE @@ -14,24 +14,37 @@ cabal-version: >=1.10 library + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall -optc-std=c99 exposed-modules: Data.Prd - , Data.Prd.Property - , Data.Prd.Lattice , Data.Prd.Nan + , Data.Prd.Property + , Data.Float + , Data.Semigroup.Join + , Data.Semigroup.Meet , Data.Connection - , Data.Connection.Property - , Data.Connection.Word , Data.Connection.Int + , Data.Connection.Word , Data.Connection.Float - , Data.Connection.Yoneda - , Data.Float + , Data.Connection.Ratio + , Data.Connection.Round + , Data.Connection.Property + , Data.Semilattice + , Data.Semilattice.N5 + , Data.Semilattice.Top + , Data.Semilattice.MaxMin + , Data.Semilattice.Property + , Numeric.Prelude + build-depends: - base >= 4.10 && < 5.0 - , lawz >= 0.0.1 && < 1.0 - , containers >= 0.4.0 && < 0.7 - , semigroupoids == 5.* + base >= 4.10 && < 5.0 + , lawz >= 0.1.1 && < 1.0 + , rings >= 0.0.3.1 && < 0.0.4 + , containers >= 0.4.0 && < 0.7 + , semigroupoids >= 5.0 && < 6.0 default-extensions: ScopedTypeVariables @@ -39,20 +52,24 @@ , MultiParamTypeClasses , UndecidableInstances , FlexibleInstances - hs-source-dirs: src - default-language: Haskell2010 + , FlexibleContexts + , TypeOperators test-suite test type: exitcode-stdio-1.0 other-modules: - Test.Data.Float + Test.Data.Prd + , Test.Data.Connection , Test.Data.Connection.Int , Test.Data.Connection.Word + , Test.Data.Connection.Float + , Test.Data.Connection.Ratio build-depends: base == 4.* , connections -any , hedgehog - , property + , rings + , lawz default-extensions: ScopedTypeVariables, TypeApplications diff --git a/src/Data/Connection.hs b/src/Data/Connection.hs --- a/src/Data/Connection.hs +++ b/src/Data/Connection.hs @@ -1,6 +1,7 @@ {-# Language TypeFamilies #-} {-# Language TypeApplications #-} {-# Language AllowAmbiguousTypes #-} +{-# Language ConstraintKinds #-} module Data.Connection ( -- * Connection @@ -11,19 +12,18 @@ , counit , pcomparing , dual - , (&&&) - , (|||) - , just - , list , first , second , left , right , strong , choice - , binord + , (&&&) + , (|||) + , just + , list , ordbin - + , binord -- * Triple , Trip(..) , tripl @@ -32,37 +32,34 @@ , unitr , counitl , counitr - , forked - , joined , bound - , maybel - , mayber , first' , second' , left' , right' , strong' , choice' - , ceiling' - , floor' + , forked + , joined + , maybel + , mayber ) where + import Control.Category (Category, (>>>)) import Data.Bifunctor (bimap) -import Data.Word -import Data.Int +import Data.Bool import Data.Prd -import Data.Prd.Lattice -import Data.Ord (Down(..)) -import Prelude +import Data.Semigroup.Join +import Data.Semigroup.Meet +import Prelude hiding (Ord(..), Num(..), Fractional(..), RealFrac(..)) -import qualified Data.Ord as O import qualified Control.Category as C --- | A Galois connection between two monotone functions: \(connl \dashv connr \) +-- | A Galois connection between two monotone functions. -- --- Each side of the adjunction may be defined in terms of the other: +-- Each side of the connection may be defined in terms of the other: -- -- \( connr(x) = \sup \{y \in E \mid connl(y) \leq x \} \) -- @@ -92,60 +89,92 @@ -- data Conn a b = Conn (a -> b) (b -> a) +instance Category Conn where + id = Conn id id + Conn f' g' . Conn f g = Conn (f' . f) (g . g') + +-- | Extract the left side of a connection. +-- connl :: Prd a => Prd b => Conn a b -> a -> b connl (Conn f _) = f +-- | Extract the right side of a connection. +-- connr :: Prd a => Prd b => Conn a b -> b -> a connr (Conn _ g) = g --- @x <~ unit x@ +-- | Round trip through a connection. +-- +-- @x '<=' 'unit' x@ +-- unit :: Prd a => Prd b => Conn a b -> a -> a unit (Conn f g) = g . f --- @counit x <~ x@ +-- | Reverse round trip through a connection. +-- +-- @'counit' x '<=' x@ +-- counit :: Prd a => Prd b => Conn a b -> b -> b counit (Conn f g) = f . g -- | Partial version of 'Data.Ord.comparing'. -- --- Helpful in conjunction with the @xxxBy@ functions from 'Data.List'. --- -pcomparing :: Eq b => Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering +pcomparing :: Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering pcomparing (Conn f _) x y = f x `pcompare` f y -instance Category Conn where - id = Conn id id - Conn f' g' . Conn f g = Conn (f' . f) (g . g') - --------------------------------------------------------------------- --- Instances +-- Instances --------------------------------------------------------------------- +-- | Reverse a connection using the dual partial order on each side. +-- dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a) dual (Conn f g) = Conn (\(Down b) -> Down $ g b) (\(Down a) -> Down $ f a) -just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b) -just (Conn f g) = Conn (fmap f) (fmap g) - -list :: Prd a => Prd b => Conn a b -> Conn [a] [b] -list (Conn f g) = Conn (fmap f) (fmap g) - --- @'first' (ab >>> cd) = 'first' ab >>> 'first' cd@ +-- | @'first' (ab '>>>' cd) = 'first' ab '>>>' 'first' cd@ -- first :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c) first = flip strong C.id +-- | @'second' (ab '>>>' cd) = 'second' ab '>>>' 'second' cd@ +-- second :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b) second = strong C.id --- @'left' (ab >>> cd) = 'left' ab >>> 'left' cd@ +-- | @'left' (ab '>>>' cd) = 'left' ab '>>>' 'left' cd@ -- left :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c) left = flip choice C.id +-- | @'right' (ab '>>>' cd) = 'right' ab '>>>' 'right' cd@ +-- right :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b) right = choice C.id +infixr 3 &&& +(&&&) :: Prd a => Prd b => JoinSemilattice c => MeetSemilattice c => Conn c a -> Conn c b -> Conn c (a, b) +f &&& g = tripr forked >>> f `strong` g + +infixr 2 ||| +(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c +f ||| g = f `choice` g >>> tripr joined + +strong :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d) +strong (Conn ab ba) (Conn cd dc) = Conn f g where + f = bimap ab cd + g = bimap ba dc + +choice :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d) +choice (Conn ab ba) (Conn cd dc) = Conn f g where + f = either (Left . ab) (Right . cd) + g = either (Left . ba) (Right . dc) + +just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b) +just (Conn f g) = Conn (fmap f) (fmap g) + +list :: Prd a => Prd b => Conn a b -> Conn [a] [b] +list (Conn f g) = Conn (fmap f) (fmap g) + ordbin :: Conn Ordering Bool ordbin = Conn f g where f GT = True @@ -162,38 +191,28 @@ g LT = False g _ = True -(&&&) :: Prd a => Prd b => Lattice c => Conn c a -> Conn c b -> Conn c (a, b) -f &&& g = tripr forked >>> f `strong` g - -(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c -f ||| g = f `choice` g >>> tripr joined - -strong :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d) -strong (Conn ab ba) (Conn cd dc) = Conn f g where - f = bimap ab cd - g = bimap ba dc - -choice :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d) -choice (Conn ab ba) (Conn cd dc) = Conn f g where - f = either (Left . ab) (Right . cd) - g = either (Left . ba) (Right . dc) - --------------------------------------------------------------------- --- 'Trip' +-- Adjoint triples --------------------------------------------------------------------- -- | An adjoint triple. -- -- @'Trip' f g h@ satisfies: -- +-- @ -- f ⊣ g -- ⊥ ⊥ -- g ⊣ h +-- @ -- -- See -- data Trip a b = Trip (a -> b) (b -> a) (a -> b) +instance Category Trip where + id = Trip id id id + Trip f' g' h' . Trip f g h = Trip (f' . f) (g . g') (h' . h) + tripl :: Prd a => Prd b => Trip a b -> Conn a b tripl (Trip f g _) = Conn f g @@ -212,16 +231,6 @@ counitr :: Prd a => Prd b => Trip a b -> a -> a counitr = counit . tripr -ceiling' :: Prd a => Prd b => Trip a b -> a -> b -ceiling' = connl . tripl - -floor' :: Prd a => Prd b => Trip a b -> a -> b -floor' = connr . tripr - -instance Category Trip where - id = Trip id id id - Trip f' g' h' . Trip f g h = Trip (f' . f) (g . g') (h' . h) - --------------------------------------------------------------------- -- Instances --------------------------------------------------------------------- @@ -229,24 +238,6 @@ bound :: Prd a => Bound a => Trip () a bound = Trip (const minimal) (const ()) (const maximal) -forked :: Lattice a => Trip (a, a) a -forked = Trip (uncurry (\/)) (\x -> (x,x)) (uncurry (/\)) - -joined :: Prd a => Trip a (Either a a) -joined = Trip Left (either id id) Right - -maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b) -maybel = Trip f g h where - f = maybe (Right minimal) Left - g = either Just (const Nothing) - h = maybe (Right maximal) Left - -mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b) -mayber = Trip f g h where - f = maybe (Left minimal) Right - g = either (const Nothing) Just - h = maybe (Left maximal) Right - first' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c) first' = flip strong' C.id @@ -270,3 +261,21 @@ f = either (Left . ab) (Right . cd) g = either (Left . ba) (Right . dc) h = either (Left . ab') (Right . cd') + +forked :: JoinSemilattice a => MeetSemilattice a => Trip (a, a) a +forked = Trip (uncurry (∨)) (\x -> (x,x)) (uncurry (∧)) + +joined :: Prd a => Trip a (Either a a) +joined = Trip Left (either id id) Right + +maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b) +maybel = Trip f g h where + f = maybe (Right minimal) Left + g = either Just (const Nothing) + h = maybe (Right maximal) Left + +mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b) +mayber = Trip f g h where + f = maybe (Left minimal) Right + g = either (const Nothing) Just + h = maybe (Left maximal) Right diff --git a/src/Data/Connection/Float.hs b/src/Data/Connection/Float.hs --- a/src/Data/Connection/Float.hs +++ b/src/Data/Connection/Float.hs @@ -1,145 +1,173 @@ -module Data.Connection.Float where +module Data.Connection.Float ( + -- * Float + f32i08 + , f32i16 + , f32i32 + , i32f32 + -- * Double + --, f64f32 + , f64i08 + , f64i16 + , f64i32 + , f64i64 + , i64f64 +) where -import Control.Category ((>>>)) -import Data.Bits ((.&.)) +import Data.Connection +import Data.Float import Data.Int -import Data.Prd.Nan -import Data.Word import Data.Prd -import Data.Function (on) -import Data.Connection -import Data.Connection.Int -import Data.Connection.Word -import GHC.Num (subtract) -import qualified Data.Bits as B -import qualified GHC.Float as F +import Data.Prd.Nan +import Data.Semifield +import Data.Semilattice +import Data.Semilattice.Top +import Data.Semiring +import GHC.Real hiding ((^),(/)) +import Prelude as P hiding (Ord(..), Num(..), Fractional(..), (^), Bounded) -import Prelude +-- | All 'Int08' values are exactly representable in a 'Float'. +f32i08 :: Trip Float (Extended Int8) +f32i08 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling x -newtype Ulp32 = Ulp32 { unUlp32 :: Int32 } deriving Show + g = bounded ninf P.fromIntegral pinf -ulp32Nan :: Ulp32 -> Bool -ulp32Nan (Ulp32 x) = x /= (min 2139095040 . max (- 2139095041)) x + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor x -instance Eq Ulp32 where - x == y | ulp32Nan x && ulp32Nan y = True - | ulp32Nan x || ulp32Nan y = False - | otherwise = on (==) unUlp32 x y + imax = 127 -instance Prd Ulp32 where - x <~ y | ulp32Nan x && ulp32Nan y = True - | ulp32Nan x || ulp32Nan y = False - | otherwise = on (<~) unUlp32 x y + imin = -128 -instance Minimal Ulp32 where - minimal = Ulp32 $ -2139095041 +-- | All 'Int16' values are exactly representable in a 'Float'. +f32i16 :: Trip Float (Extended Int16) +f32i16 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling x -instance Maximal Ulp32 where - maximal = Ulp32 $ 2139095040 + g = bounded ninf P.fromIntegral pinf -instance Bounded Ulp32 where - minBound = minimal - maxBound = maximal + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor x -f32u32 :: Conn Float Ulp32 -f32u32 = Conn (Ulp32 . floatInt32) (int32Float . unUlp32) + imax = 32767 -u32f32 :: Conn Ulp32 Float -u32f32 = Conn (int32Float . unUlp32) (Ulp32 . floatInt32) + imin = -32768 --- fromIntegral (maxBound :: Ulp32) + 1 , image of aNan +-- | Exact embedding up to the largest representable 'Int32'. +f32i32 :: Conn Float (Nan Int32) +f32i32 = Conn (liftNan f) (nan' g) where + f x | abs x <= 2**24-1 = P.ceiling x + | otherwise = if x >= 0 then 2^24 else minimal -u32w64 :: Conn Ulp32 (Nan Word64) -u32w64 = Conn f g where - conn = i32w32' >>> w32w64 + g i | abs' i <= 2^24-1 = fromIntegral i + | otherwise = if i >= 0 then 1/0 else -2**24 - offset = 2139095041 :: Word64 - offset' = 2139095041 :: Int32 +-- | Exact embedding up to the largest representable 'Int32'. +i32f32 :: Conn (Nan Int32) Float +i32f32 = Conn (nan' g) (liftNan f) where + f x | abs x <= 2**24-1 = P.floor x + | otherwise = if x >= 0 then maximal else -2^24 - f x@(Ulp32 y) | ulp32Nan x = Nan - | negative y = Def $ fromIntegral (y + offset') - | otherwise = Def $ (fromIntegral y) + offset - where fromIntegral = connl conn + g i | abs i <= 2^24-1 = fromIntegral i + | otherwise = if i >= 0 then 2**24 else -1/0 - g x = case x of - Nan -> Ulp32 offset' - Def y | y < offset -> Ulp32 $ (fromIntegral y) - offset' - | otherwise -> Ulp32 $ fromIntegral ((min 4278190081 y) - offset) - where fromIntegral = connr conn +--------------------------------------------------------------------- +-- Double +--------------------------------------------------------------------- --- ---TODO handle neg case, get # of nans/denormals, collect constants +-- | All 'Int8' values are exactly representable in a 'Double'. +f64i08 :: Trip Double (Extended Int8) +f64i08 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling x -abs' :: (Eq a, Bound a, Num a) => a -> a -abs' x = if x == minimal then abs (x+1) else abs x + g = bounded ninf P.fromIntegral pinf ---TODO f32i64? -f32i32 :: Conn Float (Nan Int32) -f32i32 = Conn (liftNan f) (nan (0/0) g) where - f x | abs x <~ 2**24-1 = ceiling x - | otherwise = if x >~ 0 then 2^24 else minimal + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor x - g i | abs' i <~ 2^24-1 = fromIntegral i - | otherwise = if i >~ 0 then 1/0 else -2**24 - -i32f32 :: Conn (Nan Int32) Float -i32f32 = Conn (nan (0/0) f) (liftNan g) where - f i | abs i <~ 2^24-1 = fromIntegral i - | otherwise = if i >~ 0 then 2**24 else -1/0 + imax = 127 - g x | abs x <~ 2**24-1 = floor x - | otherwise = if x >~ 0 then maximal else -2^24 + imin = -128 -f64i64 :: Conn Double (Nan Int64) -f64i64 = Conn (liftNan f) (nan (0/0) g) where - f x | abs x <~ 2**53-1 = ceiling x - | otherwise = if x >~ 0 then 2^53 else minimal +-- | All 'Int16' values are exactly representable in a 'Double'. +f64i16 :: Trip Double (Extended Int16) +f64i16 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling x - g i | abs' i <~ 2^53-1 = fromIntegral i - | otherwise = if i >~ 0 then 1/0 else -2**53 - -i64f64 :: Conn (Nan Int64) Double -i64f64 = Conn (nan (0/0) f) (liftNan g) where - f i | abs i <~ 2^53-1 = fromIntegral i - | otherwise = if i >~ 0 then 2**53 else -1/0 + g = bounded ninf P.fromIntegral pinf - g x | abs x <~ 2**53-1 = floor x - | otherwise = if x >~ 0 then maximal else -2^53 + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor x -float_word8 :: Trip Float (Nan Word8) -float_word8 = Trip (liftNan f) (nan (0/0) g) (liftNan h) where - h x = if x > 0 then 0 else connr w08w32 $ B.shift (floatWord32 x) (-23) - g = word32Float . flip B.shift 23 . connl w08w32 - f x = 1 + min 254 (h x) + imax = 32767 --- | Shift by /Int32/ units of least precision. -shift :: Int32 -> Float -> Float -shift n = int32Float . (+ n) . floatInt32 + imin = -32768 --- internal +-- | All 'Int32' values are exactly representable in a 'Double'. +f64i32 :: Trip Double (Extended Int32) +f64i32 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling x --- Non-monotonic function -signed32 :: Word32 -> Int32 -signed32 x | x < 0x80000000 = fromIntegral x - | otherwise = fromIntegral (maximal - (x - 0x80000000)) + g = bounded ninf P.fromIntegral pinf --- Non-monotonic function converting from 2s-complement format. -unsigned32 :: Int32 -> Word32 -unsigned32 x | x >= 0 = fromIntegral x - | otherwise = 0x80000000 + (maximal - (fromIntegral x)) + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor x -int32Float :: Int32 -> Float -int32Float = word32Float . unsigned32 + imax = 2147483647 -floatInt32 :: Float -> Int32 -floatInt32 = signed32 . floatWord32 + imin = -2147483648 --- Bit-for-bit conversion. -word32Float :: Word32 -> Float -word32Float = F.castWord32ToFloat +-- | Exact embedding up to the largest representable 'Int64'. +f64i64 :: Conn Double (Nan Int64) +f64i64 = Conn (liftNan f) (nan' g) where + f x | abs x <= 2**53-1 = P.ceiling x + | otherwise = if x >= 0 then 2^53 else minimal --- TODO force to positive representation? --- Bit-for-bit conversion. -floatWord32 :: Float -> Word32 -floatWord32 = (+0) . F.castFloatToWord32 + g i | abs' i <= 2^53-1 = fromIntegral i + | otherwise = if i >= 0 then 1/0 else -2**53 + +-- | Exact embedding up to the largest representable 'Int64'. +i64f64 :: Conn (Nan Int64) Double +i64f64 = Conn (nan' g) (liftNan f) where + f x | abs x <= 2**53-1 = P.floor x + | otherwise = if x >= 0 then maximal else -2^53 + + g i | abs i <= 2^53-1 = fromIntegral i + | otherwise = if i >= 0 then 2**53 else -1/0 + +abs' :: Ord a => Minimal a => Ring a => a -> a +abs' x = if x =~ minimal then abs (x+one) else abs x + +{- slightly broken +f32w08 :: Trip Float (Nan Word8) +f32w08 = Trip (liftNan f) (nan (0/0) g) (liftNan h) where + h x = if x > 0 then 0 else connr w08w32 $ B.shift (floatWord32 x) (-23) + g = word32Float . flip B.shift 23 . connl w08w32 + f x = 1 + min 254 (h x) +-} diff --git a/src/Data/Connection/Int.hs b/src/Data/Connection/Int.hs --- a/src/Data/Connection/Int.hs +++ b/src/Data/Connection/Int.hs @@ -6,26 +6,35 @@ -- @ -- module Data.Connection.Int ( + ConnInteger(..) + , fromInteger -- * Int8 - i08w08 + , i08w08 , i08w08' , i08i16 , i08i32 , i08i64 + , i08int -- * Int16 , i16w16 , i16w16' , i16i32 , i16i64 + , i16int -- * Int32 , i32w32 , i32w32' , i32i64 + , i32int -- * Int64 , i64w64 , i64w64' + , i64int + -- * Int + , ixxwxx -- * Integer , intnat + , natint ) where import Control.Category ((>>>)) @@ -33,55 +42,120 @@ import Data.Connection.Word import Data.Int import Data.Prd +import Data.Semilattice.Top import Data.Word - import Numeric.Natural -unsigned :: (Bounded a, Integral a, Integral b) => Conn a b -unsigned = Conn (\y -> fromIntegral (y + maxBound + 1)) - (\x -> fromIntegral x - minBound) +import Prelude hiding (Num(..), (^), Bounded) +import qualified Prelude as P -i08w08 :: Conn Int8 Word8 -i08w08 = unsigned +class Prd a => ConnInteger a where + intxxx :: Conn (Bounded Integer) a +instance ConnInteger Int8 where + intxxx = tripr i08int + +instance ConnInteger Int16 where + intxxx = tripr i16int + +instance ConnInteger Int32 where + intxxx = tripr i32int + +instance ConnInteger Int64 where + intxxx = tripr i64int + +instance ConnInteger Word8 where + intxxx = tripr i08int >>> i08w08 + +instance ConnInteger Word16 where + intxxx = tripr i16int >>> i16w16 + +instance ConnInteger Word32 where + intxxx = tripr i32int >>> i32w32 + +instance ConnInteger Word64 where + intxxx = tripr i64int >>> i64w64 + +-- | Lawful replacement for the version in base. +-- +fromInteger :: ConnInteger a => Integer -> a +fromInteger = connl intxxx . Just . Fin + +unsigned :: (Bound a, Integral a, Integral b) => Conn a b +unsigned = Conn (\y -> fromIntegral (y P.+ maximal P.+ 1)) + (\x -> fromIntegral x P.- minimal) + i08w08' :: Conn Int8 Word8 -i08w08' = Conn (fromIntegral . max 0) (fromIntegral . min 127) +i08w08' = unsigned +i08w08 :: Conn Int8 Word8 +i08w08 = Conn (fromIntegral . max 0) (fromIntegral . min 127) + i08i16 :: Conn Int8 Int16 -i08i16 = i08w08 >>> w08w16 >>> w16i16 +i08i16 = i08w08' >>> w08w16 >>> w16i16 i08i32 :: Conn Int8 Int32 -i08i32 = i08w08 >>> w08w32 >>> w32i32 +i08i32 = i08w08' >>> w08w32 >>> w32i32 i08i64 :: Conn Int8 Int64 -i08i64 = i08w08 >>> w08w64 >>> w64i64 +i08i64 = i08w08' >>> w08w64 >>> w64i64 -i16w16 :: Conn Int16 Word16 -i16w16 = unsigned +i08int :: Trip Int8 (Bounded Integer) +i08int = Trip (liftBottom' fromIntegral) + (bounded' $ P.fromInteger . min 127 . max (-128)) + (liftTop' fromIntegral) i16w16' :: Conn Int16 Word16 -i16w16' = Conn (fromIntegral . max 0) (fromIntegral . min 32767) +i16w16' = unsigned +i16w16 :: Conn Int16 Word16 +i16w16 = Conn (fromIntegral . max 0) (fromIntegral . min 32767) + i16i32 :: Conn Int16 Int32 -i16i32 = i16w16 >>> w16w32 >>> w32i32 +i16i32 = i16w16' >>> w16w32 >>> w32i32 i16i64 :: Conn Int16 Int64 -i16i64 = i16w16 >>> w16w64 >>> w64i64 +i16i64 = i16w16' >>> w16w64 >>> w64i64 -i32w32 :: Conn Int32 Word32 -i32w32 = unsigned +i16int :: Trip Int16 (Bounded Integer) +i16int = Trip (liftBottom' fromIntegral) + (bounded' $ P.fromInteger . min 32767 . max (-32768)) + (liftTop' fromIntegral) i32w32' :: Conn Int32 Word32 -i32w32' = Conn (fromIntegral . max 0) (fromIntegral . min 2147483647) +i32w32' = unsigned +i32w32 :: Conn Int32 Word32 +i32w32 = Conn (fromIntegral . max 0) (fromIntegral . min 2147483647) + i32i64 :: Conn Int32 Int64 -i32i64 = i32w32 >>> w32w64 >>> w64i64 +i32i64 = i32w32' >>> w32w64 >>> w64i64 -i64w64 :: Conn Int64 Word64 -i64w64 = unsigned +i32int :: Trip Int32 (Bounded Integer) +i32int = Trip (liftBottom' fromIntegral) + (bounded' $ P.fromInteger . min 2147483647 . max (-2147483648)) + (liftTop' fromIntegral) i64w64' :: Conn Int64 Word64 -i64w64' = Conn (fromIntegral . max 0) (fromIntegral . min 9223372036854775807) +i64w64' = unsigned +i64w64 :: Conn Int64 Word64 +i64w64 = Conn (fromIntegral . max 0) (fromIntegral . min 9223372036854775807) + +i64int :: Trip Int64 (Bounded Integer) +i64int = Trip (liftBottom' fromIntegral) + (bounded' $ P.fromInteger . min 9223372036854775807 . max (-9223372036854775808)) + (liftTop' fromIntegral) + +ixxwxx :: Conn Int Word +ixxwxx = unsigned + intnat :: Conn Integer Natural intnat = Conn (fromIntegral . max 0) fromIntegral + +natint :: Conn Natural (Maybe Integer) +natint = Conn f (maybe minimal g) where + f i | i == 0 = Nothing + | otherwise = Just $ fromIntegral i + + g = P.fromInteger . max 0 diff --git a/src/Data/Connection/Property.hs b/src/Data/Connection/Property.hs --- a/src/Data/Connection/Property.hs +++ b/src/Data/Connection/Property.hs @@ -2,31 +2,27 @@ {-# Language TypeApplications #-} module Data.Connection.Property where -import Data.Proxy import Data.Prd import Data.Connection +import Prelude hiding (Num(..),Ord(..)) import qualified Test.Function.Idempotent as Prop import qualified Test.Function.Invertible as Prop import qualified Test.Function.Monotone as Prop -import Test.Util -import Prelude hiding (Ord(..)) - - -- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \) -- --- A monotone Galois connection. +-- A Galois connection. This is a required property. -- connection :: Prd a => Prd b => Conn a b -> a -> b -> Bool -connection (Conn f g) = Prop.adjoint_on (<~) (<~) f g +connection (Conn f g) = Prop.adjoint_on (<=) (<=) f g -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property. -- closed :: Prd a => Prd b => Conn a b -> a -> Bool -closed (Conn f g) = Prop.invertible_on (>~) f g +closed (Conn f g) = Prop.invertible_on (>=) f g -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- @@ -40,7 +36,7 @@ -- This is a required property. -- kernel :: Prd a => Prd b => Conn a b -> b -> Bool -kernel (Conn f g) = Prop.invertible_on (<~) g f +kernel (Conn f g) = Prop.invertible_on (<=) g f -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- @@ -53,23 +49,27 @@ -- -- This is a required property. -- -monotone :: Prd a => Prd b => Conn a b -> b -> b -> Bool -monotone (Conn _ g) = Prop.monotone_on (<~) (<~) g +monotoner :: Prd a => Prd b => Conn a b -> b -> b -> Bool +monotoner (Conn _ g) = Prop.monotone_on (<=) (<=) g -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \) -- -- This is a required property. -- -monotone' :: Prd a => Prd b => Conn a b -> a -> a -> Bool -monotone' (Conn f _) = Prop.monotone_on (<~) (<~) f +monotonel :: Prd a => Prd b => Conn a b -> a -> a -> Bool +monotonel (Conn f _) = Prop.monotone_on (<=) (<=) f -- | \( \forall x : f \dashv g \Rightarrow unit \circ unit (x) \sim unit (x) \) -- +-- This is a required property. +-- idempotent_unit :: Prd a => Prd b => Conn a b -> a -> Bool idempotent_unit conn = Prop.idempotent_on (=~) $ unit conn -- | \( \forall x : f \dashv g \Rightarrow counit \circ counit (x) \sim counit (x) \) -- +-- This is a required property. +-- idempotent_counit :: Prd a => Prd b => Conn a b -> b -> Bool idempotent_counit conn = Prop.idempotent_on (=~) $ counit conn @@ -77,13 +77,12 @@ -- -- See -- -projective_l :: Prd a => Prd b => Conn a b -> a -> Bool -projective_l conn@(Conn f _) = Prop.projective_on (=~) f $ counit conn +projectivel :: Prd a => Prd b => Conn a b -> a -> Bool +projectivel conn@(Conn f _) = Prop.projective_on (=~) f $ counit conn -- | \( \forall x: f \dashv g \Rightarrow unit \circ g (x) \sim g (x) \) -- -- See -- -projective_r :: Prd a => Prd b => Conn a b -> b -> Bool -projective_r conn@(Conn _ g) = Prop.projective_on (=~) g $ unit conn - +projectiver :: Prd a => Prd b => Conn a b -> b -> Bool +projectiver conn@(Conn _ g) = Prop.projective_on (=~) g $ unit conn diff --git a/src/Data/Connection/Ratio.hs b/src/Data/Connection/Ratio.hs new file mode 100644 --- /dev/null +++ b/src/Data/Connection/Ratio.hs @@ -0,0 +1,292 @@ +{-# Language AllowAmbiguousTypes #-} +{-# Language FunctionalDependencies #-} + +module Data.Connection.Ratio where + +import Data.Connection +import Data.Float +import Data.Int +import Data.Prd +import Data.Prd.Nan +import Data.Ratio +import Data.Semifield +import Data.Semilattice +import Data.Semilattice.Top +import Data.Semiring +import Data.Word +import GHC.Real hiding ((/), (^)) +import Numeric.Natural +import Prelude hiding (until, Ord(..), Num(..), Fractional(..), (^), Bounded) +import qualified Control.Category as C +import qualified Prelude as P + +reduce :: Integral a => a -> a -> Ratio a +reduce x 0 = x :% 0 +reduce x y = (x `quot` d) :% (y `quot` d) where d = gcd x y + +-- x % y = reduce (x * signum y) (abs y) +cancel :: Prd a => (Additive-Group) a => Ratio a -> Ratio a +cancel (x :% y) = if x < zero && y < zero then (pabs x) :% (pabs y) else x :% y + +-- TODO replace w/ Yoneda / Index / Graded +-- shift by n 'units of least precision' where the ULP is +-- determined by the denominator +shiftd :: (Additive-Semigroup) a => a -> Ratio a -> Ratio a +shiftd n (x :% y) = (n + x) :% y + +class (Prd (Ratio a), Prd b) => TripRatio a b | b -> a where + ratxxx :: Trip (Ratio a) b + +-- | Lawful replacement for the version in base. +-- +-- >>> fromRational @Float 1.3 +-- 1.3000001 +-- >>> fromRational @Float (1/0) +-- Infinity +-- >>> fromRational @Float (0/0) +-- NaN +-- +-- >>> fromRational @(Extended Int8) 4.9 +-- Def (fin 5) +-- >>> fromRational @(Extended Int8) (-1.2) +-- Def (fin (-1)) +-- >>> fromRational @(Extended Int8) (1/0) +-- Def Just Top +-- >>> fromRational @(Extended Int8) (0/0) +-- Nan +-- >>> fromRational @(Extended Int8) (-1/0) +-- Def Nothing +-- +fromRational :: TripRatio a b => Ratio a -> b +fromRational = connl . tripl $ ratxxx + +ratf32 :: Trip (Ratio Integer) Float +ratf32 = Trip (extend' f) (extend' g) (extend' h) where + f x = let est = P.fromRational x in --F.fromRat' + if extend' g est >= x + then est + else ascendf est (extend' g) x + + g = flip approxRational 0 + + h x = let est = P.fromRational x in + if extend' g est <= x + then est + else descendf est (extend' g) x + + ascendf z g1 y = until (\x -> g1 x >= y) (<=) (shiftf 1) z + + descendf z f1 x = until (\y -> f1 y <= x) (>=) (shiftf (-1)) z + +ratf64 :: Trip (Ratio Integer) Double +ratf64 = Trip (extend' f) (extend' g) (extend' h) where + f x = let est = P.fromRational x in + if extend' g est >= x + then est + else ascendf est (extend' g) x + + g = flip approxRational 0 + + h x = let est = P.fromRational x in + if extend' g est <= x + then est + else descendf est (extend' g) x + + ascendf z g1 y = until (\x -> g1 x >= y) (<=) (shift 1) z + + descendf z f1 x = until (\y -> f1 y <= x) (>=) (shift (-1)) z + +rati08 :: Trip (Ratio Integer) (Extended Int8) +rati08 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling $ cancel x + + g = bounded ninf P.fromIntegral pinf + + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor $ cancel x + + imax = 127 + + imin = -128 + +rati16 :: Trip (Ratio Integer) (Extended Int16) +rati16 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling $ cancel x + + g = bounded ninf P.fromIntegral pinf + + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor $ cancel x + + imax = 32767 + + imin = -32768 + +rati32 :: Trip (Ratio Integer) (Extended Int32) +rati32 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling $ cancel x + + g = bounded ninf P.fromIntegral pinf + + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor $ cancel x + + imax = 2147483647 + + imin = -2147483648 + +rati64 :: Trip (Ratio Integer) (Extended Int64) +rati64 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Just Top + | x =~ ninf = Nothing + | x < imin = fin bottom + | otherwise = fin $ P.ceiling $ cancel x + + g = bounded ninf P.fromIntegral pinf + + h x | x =~ pinf = Just Top + | x > imax = fin top + | x < imin = Nothing + | otherwise = fin $ P.floor $ cancel x + + imax = 9223372036854775807 + + imin = -9223372036854775808 + +ratint :: Trip (Ratio Integer) (Extended Integer) +ratint = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x =~ pinf = Just Top + | x =~ ninf = Nothing + | otherwise = fin $ P.ceiling $ cancel x + + g = bounded ninf P.fromIntegral pinf + + h x | x =~ pinf = Just Top + | x =~ ninf = Nothing + | otherwise = fin $ P.floor $ cancel x + +ratw08 :: Trip (Ratio Natural) (Lifted Word8) +ratw08 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Top + | otherwise = Fin $ P.ceiling x + + g = topped P.fromIntegral pinf + + h x | x =~ pinf = Top + | x > imax = Fin top + | otherwise = Fin $ P.floor x + + imax = 255 + +ratw16 :: Trip (Ratio Natural) (Lifted Word16) +ratw16 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Top + | otherwise = Fin $ P.ceiling x + + g = topped P.fromIntegral pinf + + h x | x =~ pinf = Top + | x > imax = Fin top + | otherwise = Fin $ P.floor x + + imax = 65535 + +ratw32 :: Trip (Ratio Natural) (Lifted Word32) +ratw32 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Top + | otherwise = Fin $ P.ceiling x + + g = topped P.fromIntegral pinf + + h x | x =~ pinf = Top + | x > imax = Fin top + | otherwise = Fin $ P.floor x + + imax = 4294967295 + +ratw64 :: Trip (Ratio Natural) (Lifted Word64) +ratw64 = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x > imax = Top + | otherwise = Fin $ P.ceiling x + + g = topped P.fromIntegral pinf + + h x | x =~ pinf = Top + | x > imax = Fin top + | otherwise = Fin $ P.floor x + + imax = 18446744073709551615 + +ratnat :: Trip (Ratio Natural) (Lifted Natural) +ratnat = Trip (liftNan f) (nan' g) (liftNan h) where + f x | x =~ pinf = Top + | otherwise = Fin $ P.ceiling x + + g = topped P.fromIntegral pinf + + h x | x =~ pinf = Top + | otherwise = Fin $ P.floor x + +--------------------------------------------------------------------- +-- Instances +--------------------------------------------------------------------- + +instance TripRatio Integer Float where + ratxxx = ratf32 + +instance TripRatio Integer Double where + ratxxx = ratf64 + +instance TripRatio Integer (Ratio Integer) where + ratxxx = C.id + +instance TripRatio Integer (Nan Ordering) where + ratxxx = fldord + +instance TripRatio Integer (Extended Int8) where + ratxxx = rati08 + +instance TripRatio Integer (Extended Int16) where + ratxxx = rati16 + +instance TripRatio Integer (Extended Int32) where + ratxxx = rati32 + +instance TripRatio Integer (Extended Int64) where + ratxxx = rati64 + +instance TripRatio Integer (Extended Integer) where + ratxxx = ratint + +instance TripRatio Natural (Ratio Natural) where + ratxxx = C.id + +instance TripRatio Natural (Lifted Word8) where + ratxxx = ratw08 + +instance TripRatio Natural (Lifted Word16) where + ratxxx = ratw16 + +instance TripRatio Natural (Lifted Word32) where + ratxxx = ratw32 + +instance TripRatio Natural (Lifted Word64) where + ratxxx = ratw64 + +instance TripRatio Natural (Lifted Natural) where + ratxxx = ratnat diff --git a/src/Data/Connection/Round.hs b/src/Data/Connection/Round.hs new file mode 100644 --- /dev/null +++ b/src/Data/Connection/Round.hs @@ -0,0 +1,249 @@ +{-# Language AllowAmbiguousTypes #-} + +module Data.Connection.Round ( + -- * Rounding Classes + TripInt16(..) + , ceil16 + , floor16 + , trunc16 + , round16 + , TripInt32(..) + , ceil32 + , floor32 + , trunc32 + , round32 + -- * Rounding Utils + , Mode(..) + , half + , tied + , above + , below + , addWith + , negWith + , subWith + , mulWith + , fmaWith + , remWith + , divWith + , divWith' +) where + +import Data.Bool +import Data.Connection +import Data.Connection.Float +import Data.Connection.Ratio +import Data.Float +import Data.Int +import Data.Prd +import Data.Ratio +import Data.Semifield +import Data.Semilattice +import Data.Semilattice.Top +import Data.Semiring +import Prelude hiding (until, Ord(..), Num(..), Fractional(..), (^), Bounded) +import Test.Logic (xor) + +class Prd a => TripInt16 a where + xxxi16 :: Trip a (Extended Int16) + +ceil16 :: TripInt16 a => a -> a +ceil16 = unitl xxxi16 + +floor16 :: TripInt16 a => a -> a +floor16 = counitr xxxi16 + +trunc16 :: (Additive-Monoid) a => TripInt16 a => a -> a +trunc16 x = bool (ceil16 x) (floor16 x) $ x >= zero + +round16 :: (Additive-Group) a => TripInt16 a => a -> a +round16 x | above xxxi16 x = ceil16 x -- upper half interval + | below xxxi16 x = floor16 x -- lower half interval + | otherwise = trunc16 x + +class Prd a => TripInt32 a where + xxxi32 :: Trip a (Extended Int32) + +ceil32 :: TripInt32 a => a -> a +ceil32 = unitl xxxi32 + +floor32 :: TripInt32 a => a -> a +floor32 = counitr xxxi32 + +trunc32 :: (Additive-Monoid) a => TripInt32 a => a -> a +trunc32 x = bool (ceil32 x) (floor32 x) $ x >= zero + +round32 :: (Additive-Group) a => TripInt32 a => a -> a +round32 x | above xxxi32 x = ceil32 x -- upper half interval + | below xxxi32 x = floor32 x -- lower half interval + | otherwise = trunc32 x + +--------------------------------------------------------------------- +-- Rounding +--------------------------------------------------------------------- + +-- | The four primary IEEE rounding modes. +-- +-- See . +-- +data Mode = + RNZ -- ^ round to nearest with ties towards zero + | RTP -- ^ round towards pos infinity + | RTN -- ^ round towards neg infinity + | RTZ -- ^ round towards zero + deriving (Eq, Show) + +-- | Determine which half of the interval between two representations of /a/ a particular value lies. +-- +half :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Maybe Ordering +half t x = pcompare (x - unitl t x) (counitr t x - x) + +-- | Determine whether /x/ lies above the halfway point between two representations. +-- +-- @ 'above' t x '==' (x '-' 'unitl' t x) '`gt`' ('counitr' t x '-' x) @ +-- +above :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool +above t = maybe False (== GT) . half t + +-- | Determine whether /x/ lies below the halfway point between two representations. +-- +-- @ 'below' t x '==' (x '-' 'unitl' t x) '`lt`' ('counitr' t x '-' x) @ +-- +below :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool +below t = maybe False (== LT) . half t + +-- | Determine whether /x/ lies exactly halfway between two representations. +-- +-- @ 'tied' t x '==' (x '-' 'unitl' t x) '=~' ('counitr' t x '-' x) @ +-- +tied :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool +tied t = maybe False (== EQ) . half t + +-- >>> addWith ratf32 RTN 1 2 +-- 3.0 +-- minSubf +addWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> b +addWith t@(Trip _ f _) rm x y = rnd t rm (addSgn t rm x y) (f x + f y) + +negWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b +negWith t@(Trip _ f _) rm x = rnd t rm (neg' t rm x) (zero - f x) + +subWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> b +subWith t@(Trip _ f _) rm x y = rnd t rm (subSgn t rm x y) (f x - f y) + +mulWith :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b +mulWith t@(Trip _ f _) rm x y = rnd t rm (xorSgn t rm x y) (f x * f y) + +{- +big = shiftf (-1) maximal +λ> fmaWith ratf32 RTN big 2 (-big) +3.4028235e38 +λ> big * 2 - big +Infinity +-} +fmaWith :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b -> b +fmaWith t@(Trip _ f _) rm x y z = rnd t rm (fmaSgn t rm x y z) $ f x * f y + f z + +{- +λ> remWith @Int RTP 17 5 +-3 +λ> remWith @Int RNZ 17 5 +2 +-} +remWith :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b +remWith t rm x y = fmaWith t rm (negWith t rm $ divWith t rm x y) y x + +{- +λ> divWith @Int RNZ 17 5 +3 +λ> divWith @Int RTP 17 5 +4 +-} +-- when pos numbers are divided by −0 we return minus infinity rather than pos: +-- >>> divWith C.id RNZ 1 (shiftf (-1) 0) +-- -Infinity +divWith :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b +divWith t@(Trip _ f _) rm x y = rnd t rm (xorSgn t rm x y) (f x / f y) + +-- requires that sign be flipped back in /a/. +divWith' :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b +divWith' t@(Trip _ f _) rm x y | xorSgn t rm x y = rnd t rm True (negate $ f x / f y) + | otherwise = rnd t rm False (f x / f y) + +--------------------------------------------------------------------- +-- Internal +--------------------------------------------------------------------- + +-- @ truncateWith C.id == id @ +truncateWith :: (Prd a, Prd b, (Additive-Monoid) a) => Trip a b -> a -> b +truncateWith t x = bool (ceilingWith t x) (floorWith t x) $ x >= zero + +-- @ ceilingWith C.id == id @ +ceilingWith :: Prd a => Prd b => Trip a b -> a -> b +ceilingWith = connl . tripl + +-- @ floorWith C.id == id @ +floorWith :: Prd a => Prd b => Trip a b -> a -> b +floorWith = connr . tripr + +-- @ roundWith C.id == id @ +roundWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> a -> b +roundWith t x | above t x = ceilingWith t x -- upper half interval + | below t x = floorWith t x -- lower half interval + | otherwise = truncateWith t x + +{- + +rndWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b +rndWith t@(Trip f g h) rm x = rnd t rm (neg' t rm x) (g x) + +-} + +-- Determine the sign of 0 when /a/ contains signed 0s +rsz :: (Prd a, Prd b) => Trip a b -> Bool -> a -> b +rsz t = bool (floorWith t) (ceilingWith t) + +rnd :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> Bool -> a -> b +rnd t RNZ s x = bool (roundWith t x) (rsz t s x) $ x =~ zero +rnd t RTP s x = bool (ceilingWith t x) (rsz t s x) $ x =~ zero +rnd t RTN s x = bool (floorWith t x) (rsz t s x) $ x =~ zero +rnd t RTZ s x = bool (truncateWith t x) (rsz t s x) $ x =~ zero + +neg' :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> Bool +neg' t rm x = x < rnd t rm False zero + +--pos' :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> Bool +--pos' t rm x = x > rnd t rm False zero + +-- | Determine signed-0 behavior under addition. +addSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool +addSgn t rm x y | rm == RTN = neg' t rm x || neg' t rm y + | otherwise = neg' t rm x && neg' t rm y + +subSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool +subSgn t rm x y = not (addSgn t rm x y) + +-- | Determine signed-0 behavior under multiplication and division. +xorSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool +xorSgn t rm x y = neg' t rm x `xor` neg' t rm y + +fmaSgn :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b -> Bool +fmaSgn t rm x y z = addSgn t rm (mulWith t rm x y) z + +--------------------------------------------------------------------- +-- Instances +--------------------------------------------------------------------- + +instance TripInt16 Float where + xxxi16 = f32i16 + +instance TripInt16 Double where + xxxi16 = f64i16 + +instance TripInt16 (Ratio Integer) where + xxxi16 = rati16 + +instance TripInt32 Double where + xxxi32 = f64i32 + +instance TripInt32 (Ratio Integer) where + xxxi32 = rati32 diff --git a/src/Data/Connection/Word.hs b/src/Data/Connection/Word.hs --- a/src/Data/Connection/Word.hs +++ b/src/Data/Connection/Word.hs @@ -19,12 +19,9 @@ , w64nat ) where -import Control.Category ((>>>)) import Data.Connection import Data.Int -import Data.Prd import Data.Word - import Numeric.Natural signed :: (Bounded b, Integral a, Integral b) => Conn a b diff --git a/src/Data/Connection/Yoneda.hs b/src/Data/Connection/Yoneda.hs deleted file mode 100644 --- a/src/Data/Connection/Yoneda.hs +++ /dev/null @@ -1,95 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE Rank2Types #-} - -module Data.Connection.Yoneda where - -import Data.Int -import Data.Word -import Data.Prd -import Data.Prd.Nan -import Data.Prd.Lattice -import Data.Bifunctor -import Data.Function -import Data.Functor.Identity -import Data.Functor.Product -import Data.Functor.Sum -import Data.Connection -import Data.Connection.Int -import Data.Connection.Word -import Data.Connection.Float -import Data.Foldable -import Data.List (unfoldr) -import GHC.Num (subtract) -import Numeric.Natural -import Data.Bool -import Prelude hiding (Enum(..), Ord(..), until, filter) - -import qualified Control.Category as C - - -type family Rep a :: * - -type instance Rep (Down a) = Down (Rep a) -type instance Rep Bool = Bool - --- | Yoneda representation for lattice ideals & filters. --- --- A subset /I/ of a lattice is an ideal if and only if it is a lower set --- that is closed under finite joins, i.e., it is nonempty and for all --- /x/, /y/ in /I/, the element /x \vee y/ is also in /I/. --- --- /upper/ and /lower/ commute with /Down/: --- --- * @lower x y == upper (Down x) (Down y)@ --- --- * @lower (Down x) (Down y) == upper x y@ --- --- /Rep a/ is upward-closed: --- --- * @'upper' x s && x '<~' y ==> 'upper' y s@ --- --- * @'upper' x s && 'upper' y s ==> 'connl' 'filter' x '/\' 'connl' 'filter' y '>~' s@ --- --- /Rep a/ is downward-closed: --- --- * @'lower' x s && x '>~' y ==> 'lower' y s@ --- --- * @'lower' x s && 'lower' y s ==> 'connl' 'ideal' x '\/' 'connl' 'ideal' y '~<' s@ --- --- Finally /filter >>> ideal/ and /ideal >>> filter/ are both connections --- on /a/ and /Rep a/ respectively. --- --- See: --- --- * --- * --- -class (Prd a, Lattice (Rep a)) => Yoneda a where - - -- | Principal ideal generated by an element of /a/. - ideal :: Conn (Rep a) a - - -- | Lower set in /a/ generated by an element in /Rep a/. - lower :: Rep a -> a -> Bool - - -- | Principal filter generated by an element of /a/. - filter :: Conn a (Rep a) - - -- | Upper set in /a/ generated by an element in /Rep a/. - upper :: Rep a -> a -> Bool - - -instance Yoneda a => Yoneda (Down a) where - ideal = dual filter - lower (Down r) (Down a) = upper @a r a - filter = dual ideal - upper (Down r) (Down a) = lower @a r a - -instance Yoneda Bool where - ideal = C.id - lower = (>~) - filter = C.id - upper = (<~) diff --git a/src/Data/Float.hs b/src/Data/Float.hs deleted file mode 100644 --- a/src/Data/Float.hs +++ /dev/null @@ -1,420 +0,0 @@ -{-# LANGUAGE CPP, ForeignFunctionInterface #-} -{-# LANGUAGE FlexibleContexts #-} -module Data.Float ( - Float - , module Data.Float - , module Data.Connection.Float -) where - -import Prelude hiding (Floating(..), RealFloat(..), Real(..), Enum(..)) - -import Foreign.C -import Data.Word -import Data.Prd.Nan -import Data.Connection.Float -import Data.Int (Int32) -import Data.Prd -import Data.Function (on) -import Data.Connection - ---import Data.Numbers.CrackNum (floatToFP) -import Data.Bits ((.&.)) - -import qualified Prelude as P -import qualified Data.Bits as B -import qualified GHC.Float as F - ---disp x = floatToFP x - - -split :: Float -> Either Float Float -split x = case signBit x of - True -> Left x - _ -> Right x - -lsbMask :: Float -> Word32 -lsbMask x = 0x00000001 .&. floatWord32 x - -msbMask :: Float -> Word32 -msbMask x = 0x80000000 .&. floatWord32 x - --- floatWord32 maximal == exponent maximal -expMask :: Float -> Word32 -expMask x = 0x7f800000 .&. floatWord32 x - --- chk f = f >= 0 ==> f == word32Float $ exponent f + significand f -sigMask :: Float -> Word32 -sigMask x = 0x007FFFFF .&. floatWord32 x - -signBit :: Float -> Bool -signBit x = if isNan x then False else msbMask x /= 0 - -evenBit :: Float -> Bool -evenBit x = lsbMask x == 0 - --- | maximal (positive) finite value. -maxNorm :: Float -maxNorm = shift (-1) pInf - --- | minimal (positive) normalized value. -minNorm :: Float -minNorm = word32Float 0x00800000 - --- | maximal representable odd integer. --- --- @ maxOdd = 2**24 - 1@ --- -maxOdd :: Float -maxOdd = 16777215 - --- | minimal (positive) value. -minSub :: Float -minSub = shift 0 1 - --- | difference between 1 and the smallest representable value greater than 1. -epsilon :: Float -epsilon = shift 1 1 - 1 - --- | first /NaN/ value. -aNan :: Float -aNan = 0/0 -- inc pInf - --- | Positive infinity --- --- @nInf = 1/0@ --- -pInf :: Float -pInf = word32Float 0x7f800000 - --- | Negative infinity --- --- @nInf = -1/0@ --- -nInf :: Float -nInf = word32Float 0xff800000 - --- Bitwise equality -eq' :: Float -> Float -> Bool -eq' = (==) `on` floatWord32 - -{- -instance Num Float where - Float x + Float y = Float $ F.plusFloat x y - Float x * Float y = Float $ F.timesFloat x y - Float x - Float y = Float $ F.minusFloat x y - negate x = Float $ F.negateFloat x - abs x = Float $ F.fabsFloat x - signum x = Float $ signum x - fromInteger = Float . fromInteger -- TODO dont use fromInteger - -f32i64 :: Conn Float Int -f32i64 = Conn (liftFloat' F.float2Int) (Float . F.int2Float) - -λ> unit f32i64 nan -Float (-9.223372e18) -λ> F.float2Int (3.0252336e+35) --9223372036854775808 -λ> F.float2Int (3.0252336e+25) --9223372036854775808 - -TODO: -different Conns for embedding a Float in the lower portion of a Double, -versus middle / higher - --} - --- | --- --- @nan x == indeterminate x@ --- -isNan :: Float -> Bool -isNan x = F.isFloatNaN x == 1 - -pinf :: Float -> Bool -pinf x = infinite x && positive x - -ninf :: Float -> Bool -ninf x = infinite x && negative x - -infinite :: Float -> Bool -infinite x = F.isFloatInfinite x == 1 - -denormalized :: Float -> Bool -denormalized x = F.isFloatDenormalized x == 1 - -finite :: Float -> Bool -finite x = F.isFloatFinite x == 1 - -nzero :: Float -> Bool -nzero x = F.isFloatNegativeZero x == 1 - - ----------------------------------------------------------------- --- Ulps-based comparison ----------------------------------------------------------------- - -{- - --- | --- Calculate relative error of two numbers: --- --- \[ \frac{|a - b|}{\max(|a|,|b|)} \] --- --- It lies in [0,1) interval for numbers with same sign and (1,2] for --- numbers with different sign. If both arguments are zero or negative --- zero function returns 0. If at least one argument is transfinite it --- returns NaN -relativeError :: Float -> Float -> Float -relativeError a b - | a == 0 && b == 0 = 0 - | otherwise = abs (a - b) / fmax (abs a) (abs b) -- TODO need / - --- | Check that relative error between two numbers @a@ and @b@. If --- 'relativeError' returns Nan it returns @False@. -eqRelErr :: Float -- ^ /eps/ relative error should be in [0,1) range - -> Float -- ^ /a/ - -> Float -- ^ /b/ - -> Bool -eqRelErr eps a b = relativeError a b < eps - --} - ----------------------------------------------------------------- --- Ulps-based comparison ----------------------------------------------------------------- - -ulps :: Float -> Float -> (Bool, Word32) -ulps x y = o - where x' = floatInt32 x - y' = floatInt32 y - o | x' >~ y' = (False, fromIntegral . abs $ x' - y') - | otherwise = (True, fromIntegral . abs $ y' - x') - -ulpDistance :: Float -> Float -> Word32 -ulpDistance x y = snd $ ulps x y - -ulpDelta :: Float -> Float -> Int -ulpDelta x y = if lesser then d' else (-1) * d' - where (lesser, d) = ulps x y - d' = fromIntegral d - -ulpDelta' :: Float -> Float -> Int32 -ulpDelta' x y = if lesser then d' else (-1) * d' - where (lesser, d) = ulps x y - d' = fromIntegral d - --- | Compare two 'Float' values for approximate equality, using --- Dawson's method. --- --- required accuracy is specified in ULPs (units of least --- precision). If the two numbers differ by the given number of ULPs --- or less, this function returns @True@. -within :: Word32 -> Float -> Float -> Bool -within tol a b = ulpDistance a b <~ tol - -{- - -foreign import ccall unsafe "fdimf" fdim :: Float -> Float -> Float - -foreign import ccall unsafe "fmaxf" fmax :: Float -> Float -> Float - -foreign import ccall unsafe "fminf" fmin :: Float -> Float -> Float - - --- Arithmetic functions - -mul :: Float -> Float -> Float -mul = liftFloat2 F.timesFloat - --- | 'pow' returns the value of x to the exponent y. --- -pow :: Float -> Float -> Float -pow = liftFloat2 F.powerFloat - -add :: Float -> Float -> Float -add = liftFloat2 F.plusFloat - -sub :: Float -> Float -> Float -sub = liftFloat2 F.minusFloat - -neg :: Float -> Float -neg = liftFloat F.negateFloat - -div :: Float -> Float -> Float -div = liftFloat2 F.divideFloat - --- | 'sqrt' returns the non-negative square root of x. --- -sqrt :: Float -> Float -sqrt = liftFloat F.sqrtFloat - --- | 'fabs' returns the absolute value of a floating-point number x. --- -fabs :: Float -> Float -fabs = liftFloat F.fabsFloat - --- | 'fma a x b' returns /a*x + b/ -foreign import ccall unsafe "fmaf" fma :: Float -> Float -> Float -> Float - --- | 'cbrt' returns the cube root of x. --- -foreign import ccall unsafe "cbrtf" cbrt :: Float -> Float - - --- Exponential and logarithmic functions - --- | 'exp' returns /e/ raised to the value of the given argument /x/. --- -exp :: Float -> Float -exp = liftFloat F.expFloat - --- | 'exp2' returns 2 raised to the value of the given argument /x/. --- -foreign import ccall unsafe "exp2f" exp2 :: Float -> Float - --- | 'exmp1' returns the exponential of /x-1/. --- -expm1 :: Float -> Float -expm1 = liftFloat F.expm1Float - --- | 'log' returns the value of the natural logarithm of argument x. --- -log :: Float -> Float -log = liftFloat F.logFloat - --- | 'log1pf' returns the log of 1+x. --- -log1p :: Float -> Float -log1p = liftFloat F.log1pFloat - --- | 'ilogb' returns x's exponent n, in integer format. --- ilogb(+-Infinity) re- turns INT_MAX and ilogb(0) returns INT_MIN. --- -foreign import ccall unsafe "ilogbf" ilogb :: Float -> CInt - --- | ldexp function multiplies a floating-point number by an integral power of 2. --- ldexp is not defined in the Haskell 98 report. --- -foreign import ccall unsafe "ldexpf" ldexp :: Float -> CInt -> Float - --- | 'log10' returns the value of the logarithm of argument x to base 10. --- log10 is not defined in the Haskell 98 report. --- -foreign import ccall unsafe "log10f" log10 :: Float -> Float - --- | 'log1pf' returns the log of 1+x. --- ---foreign import ccall unsafe "log1pf" log1p :: Float -> Float - -foreign import ccall unsafe "log2f" log2 :: Float -> Float - --- | 'logb' returns x's exponent n, a signed integer converted to floating-point. --- --- > logb(+-Infinity) = +Infinity; --- > logb(0) = -Infinity with a division by zero exception. --- -foreign import ccall unsafe "logbf" logb :: Float -> Float - --- | scalbn(x, n) returns x*(2**n) computed by exponent manipulation. -foreign import ccall unsafe "scalbnf" scalbn :: Float -> CInt -> Float - --- | scalbln(x, n) returns x*(2**n) computed by exponent manipulation. -foreign import ccall unsafe "scalblnf" scalbln :: Float -> CLong -> Float - - - --- Trigonometric functions - --- | 'hypot' returns the sqrt(x*x+y*y) in such a way that --- underflow will not happen, and overflow occurs only if the final result --- deserves it. --- --- > hypot(Infinity, v) = hypot(v, Infinity) = +Infinity for all v, including NaN. --- -foreign import ccall unsafe "hypotf" hypot :: Float -> Float -> Float - --- | 'tan' returns the tangent of x (measured in radians). --- A large magnitude argument may yield a result with little or no --- significance. --- -tan :: Float -> Float -tan = liftFloat F.tanFloat - --- | 'sin' returns the sine of x (measured in radians). --- A large magnitude argument may yield a result with little or no --- significance. --- -sin :: Float -> Float -sin = liftFloat F.sinFloat - --- | 'cos' returns the cosine of x (measured in radians). --- --- A large magnitude argument may yield a result with little or no significance. --- -cos :: Float -> Float -cos = liftFloat F.cosFloat - --- | 'atan' returns the principal value of the arc tangent of x --- in the range [-pi/2, +pi/2]. --- -atan :: Float -> Float -atan = liftFloat F.atanFloat - --- | 'atan2' returns the principal value of the arc tangent of --- y/x, using the signs of both arguments to determine the quadrant of the --- return value. --- -foreign import ccall unsafe "atan2f" atan2 :: Float -> Float -> Float - --- | 'asin' returns the principal value of the arc sine of x in the range [-pi/2, +pi/2]. --- -asin :: Float -> Float -asin = liftFloat F.asinFloat - --- | 'acos' returns the principal value of the arc cosine of x in the range [0, pi] --- -acos :: Float -> Float -acos = liftFloat F.acosFloat - --- | 'tanh' returns the hyperbolic tangent of x. --- -tanh :: Float -> Float -tanh = liftFloat F.tanhFloat - --- | 'sinh' returns the hyperbolic sine of x. --- -sinh :: Float -> Float -sinh = liftFloat F.sinhFloat - --- | 'cosh' returns the hyperbolic cosine of x. --- -cosh :: Float -> Float -cosh = liftFloat F.coshFloat - --- | 'atanh' returns the inverse hyperbolic tangent of x. --- -atanh :: Float -> Float -atanh = liftFloat F.atanh - --- | 'asinh' returns the inverse hyperbolic sine of x. --- -asinh :: Float -> Float -asinh = liftFloat F.asinh - --- | 'acosh' returns the inverse hyperbolic cosine of x. --- -acosh :: Float -> Float -acosh = liftFloat F.acosh - -liftFloat :: (F.Float -> F.Float) -> Float -> Float -liftFloat f x = Float $ f x - -liftFloat' :: (F.Float -> a) -> Float -> a -liftFloat' f x = f x - -liftFloat2 :: (F.Float -> F.Float -> F.Float) -> Float -> Float -> Float -liftFloat2 f x (Float y) = Float $ f x y - -liftFloat2' :: (F.Float -> F.Float -> a) -> Float -> Float -> a -liftFloat2' f x (Float y) = f x y --} diff --git a/src/Data/Float.hsc b/src/Data/Float.hsc new file mode 100644 --- /dev/null +++ b/src/Data/Float.hsc @@ -0,0 +1,875 @@ +{-# LANGUAGE CPP, ForeignFunctionInterface #-} +{-# LANGUAGE FlexibleContexts #-} +module Data.Float ( + Float + , Double + , module Data.Float +) where + +import Data.Bits ((.&.)) +import Data.Connection +import Data.Function (on) +import Data.Int +import Data.Prd +import Data.Semifield +import Data.Semigroup.Join +import Data.Semigroup.Meet +import Data.Semiring +import Data.Word +import Foreign hiding (shift) +import Foreign.C +import GHC.Float as F +import Prelude (Double,realToFrac,fromIntegral,($),return,IO) +import Prelude hiding (Ord(..), Num(..), Fractional(..), Floating(..), (^^), (^), RealFloat(..), Real(..), Enum(..)) +import System.IO.Unsafe (unsafePerformIO) +import qualified Prelude as P + + +{-# LINE 28 "Foreign/C/Math/Double.hsc" #-} + + +-- | The acos function computes the principal value of the arc cosine of x +-- in the range [0, pi] +-- +acos :: Double -> Double +acos x = realToFrac (c_acos (realToFrac x)) +{-# INLINE acos #-} + +foreign import ccall unsafe "math.h acos" + c_acos :: CDouble -> CDouble + +-- | The asin function computes the principal value of the arc sine of x in +-- the range [-pi/2, +pi/2]. +-- +asin :: Double -> Double +asin x = realToFrac (c_asin (realToFrac x)) +{-# INLINE asin #-} + +foreign import ccall unsafe "math.h asin" + c_asin :: CDouble -> CDouble + +-- | The atan function computes the principal value of the arc tangent of x +-- in the range [-pi/2, +pi/2]. +-- +atan :: Double -> Double +atan x = realToFrac (c_atan (realToFrac x)) +{-# INLINE atan #-} + +foreign import ccall unsafe "math.h atan" + c_atan :: CDouble -> CDouble + +-- | The atan2 function computes the principal value of the arc tangent of +-- y/x, using the signs of both arguments to determine the quadrant of the +-- return value. +-- +atan2 :: Double -> Double -> Double +atan2 x y = realToFrac (c_atan2 (realToFrac x) (realToFrac y)) +{-# INLINE atan2 #-} + +foreign import ccall unsafe "math.h atan2" + c_atan2 :: CDouble -> CDouble -> CDouble + +-- | The cos function computes the cosine of x (measured in radians). +-- A large magnitude argument may yield a result with little or no significance. For a +-- discussion of error due to roundoff, see math(3). +-- +cos :: Double -> Double +cos x = realToFrac (c_cos (realToFrac x)) +{-# INLINE cos #-} + +foreign import ccall unsafe "math.h cos" + c_cos :: CDouble -> CDouble + +-- | The sin function computes the sine of x (measured in radians). +-- A large magnitude argument may yield a result with little or no +-- significance. For a discussion of error due to roundoff, see math(3). +-- +sin :: Double -> Double +sin x = realToFrac (c_sin (realToFrac x)) +{-# INLINE sin #-} + +foreign import ccall unsafe "math.h sin" + c_sin :: CDouble -> CDouble + +-- | The tan function computes the tangent of x (measured in radians). +-- A large magnitude argument may yield a result with little or no +-- significance. For a discussion of error due to roundoff, see math(3). +-- +tan :: Double -> Double +tan x = realToFrac (c_tan (realToFrac x)) +{-# INLINE tan #-} + +foreign import ccall unsafe "math.h tan" + c_tan :: CDouble -> CDouble + +-- | The cosh function computes the hyperbolic cosine of x. +-- +cosh :: Double -> Double +cosh x = realToFrac (c_cosh (realToFrac x)) +{-# INLINE cosh #-} + +foreign import ccall unsafe "math.h cosh" + c_cosh :: CDouble -> CDouble + +-- | The sinh function computes the hyperbolic sine of x. +-- +sinh :: Double -> Double +sinh x = realToFrac (c_sinh (realToFrac x)) +{-# INLINE sinh #-} + +foreign import ccall unsafe "math.h sinh" + c_sinh :: CDouble -> CDouble + +-- | The tanh function computes the hyperbolic tangent of x. +-- +tanh :: Double -> Double +tanh x = realToFrac (c_tanh (realToFrac x)) +{-# INLINE tanh #-} + +foreign import ccall unsafe "math.h tanh" + c_tanh :: CDouble -> CDouble + +------------------------------------------------------------------------ + +-- | The exp() function computes the exponential value of the given argument x. +-- +exp :: Double -> Double +exp x = realToFrac (c_exp (realToFrac x)) +{-# INLINE exp #-} + +foreign import ccall unsafe "math.h exp" + c_exp :: CDouble -> CDouble + +-- | frexp convert floating-point number to fractional and integral components +-- frexp is not defined in the Haskell 98 report. +-- +frexp :: Double -> (Double,Int) +frexp x = unsafePerformIO $ + alloca $ \p -> do + d <- c_frexp (realToFrac x) p + i <- peek p + return (realToFrac d, fromIntegral i) + +foreign import ccall unsafe "math.h frexp" + c_frexp :: CDouble -> Ptr CInt -> IO Double + +-- | The ldexp function multiplies a floating-point number by an integral power of 2. +-- ldexp is not defined in the Haskell 98 report. +-- +ldexp :: Double -> Int -> Double +ldexp x i = realToFrac (c_ldexp (realToFrac x) (fromIntegral i)) +{-# INLINE ldexp #-} + +foreign import ccall unsafe "math.h ldexp" + c_ldexp :: CDouble -> CInt -> Double + +-- | The log() function computes the value of the natural logarithm of argument x. +-- +log :: Double -> Double +log x = realToFrac (c_log (realToFrac x)) +{-# INLINE log #-} + +foreign import ccall unsafe "math.h log" + c_log :: CDouble -> CDouble + +-- | The log10 function computes the value of the logarithm of argument x to base 10. +-- log10 is not defined in the Haskell 98 report. +log10 :: Double -> Double +log10 x = realToFrac (c_log10 (realToFrac x)) +{-# INLINE log10 #-} + +foreign import ccall unsafe "math.h log10" + c_log10 :: CDouble -> CDouble + +-- | The modf function breaks the argument value into integral and fractional +-- parts, each of which has the same sign as the argument. +-- modf is not defined in the Haskell 98 report. +-- +modf :: Double -> (Double,Double) +modf x = unsafePerformIO $ + alloca $ \p -> do + d <- c_modf (realToFrac x) p + i <- peek p + return (realToFrac d, realToFrac i) + +foreign import ccall unsafe "math.h modf" + c_modf :: CDouble -> Ptr CDouble -> IO CDouble + +-- | The pow function computes the value of x to the exponent y. +-- +pow :: Double -> Double -> Double +pow x y = realToFrac (c_pow (realToFrac x) (realToFrac y)) +{-# INLINE pow #-} + +foreign import ccall unsafe "math.h pow" + c_pow :: CDouble -> CDouble -> CDouble + +-- | The sqrt function computes the non-negative square root of x. +-- +sqrt :: Double -> Double +sqrt x = realToFrac (c_sqrt (realToFrac x)) +{-# INLINE sqrt #-} + +foreign import ccall unsafe "math.h sqrt" + c_sqrt :: CDouble -> CDouble + +-- | The ceil function returns the smallest integral value greater than or equal to x. +-- +ceil :: Double -> Double +ceil x = realToFrac (c_ceil (realToFrac x)) +{-# INLINE ceil #-} + +foreign import ccall unsafe "math.h ceil" + c_ceil :: CDouble -> CDouble + +-- | The fabs function computes the absolute value of a floating-point number x. +-- +fabs :: Double -> Double +fabs x = realToFrac (c_fabs (realToFrac x)) +{-# INLINE fabs #-} + +foreign import ccall unsafe "math.h fabs" + c_fabs :: CDouble -> CDouble + +-- | The floor function returns the largest integral value less than or equal to x. +-- +floor :: Double -> Double +floor x = realToFrac (c_floor (realToFrac x)) +{-# INLINE floor #-} + +foreign import ccall unsafe "math.h floor" + c_floor :: CDouble -> CDouble + +-- | The fmod function computes the floating-point remainder of x \/ y. +-- +fmod :: Double -> Double -> Double +fmod x y = realToFrac (c_fmod (realToFrac x) (realToFrac y)) +{-# INLINE fmod #-} + +foreign import ccall unsafe "math.h fmod" + c_fmod :: CDouble -> CDouble -> CDouble + +-- | The round function returns the nearest integral value to x; if x lies +-- halfway between two integral values, then these functions return the integral +-- value with the larger absolute value (i.e., it rounds away from zero). +-- +round :: Double -> Double +round x = realToFrac (c_round (realToFrac x)) +{-# INLINE round #-} + +foreign import ccall unsafe "math.h round" + c_round :: CDouble -> CDouble + +-- | The fmod function computes the floating-point remainder of x \/ y. +-- +trunc :: Double -> Double +trunc x = realToFrac (c_trunc (realToFrac x)) +{-# INLINE trunc #-} + +foreign import ccall unsafe "math.h trunc" + c_trunc :: CDouble -> CDouble + +-- | The erf calculates the error function of x. The error function is defined as: +-- +-- > erf(x) = 2/sqrt(pi)*integral from 0 to x of exp(-t*t) dt. +-- +erf :: Double -> Double +erf x = realToFrac (c_erf (realToFrac x)) +{-# INLINE erf #-} + +foreign import ccall unsafe "math.h erf" + c_erf :: CDouble -> CDouble + +-- | The erfc function calculates the complementary error function of x; +-- that is erfc() subtracts the result of the error function erf(x) from +-- 1.0. This is useful, since for large x places disappear. +-- +erfc :: Double -> Double +erfc x = realToFrac (c_erfc (realToFrac x)) +{-# INLINE erfc #-} + +foreign import ccall unsafe "math.h erfc" + c_erfc :: CDouble -> CDouble + +-- | The gamma function. +-- +gamma :: Double -> Double +gamma x = realToFrac (c_gamma (realToFrac x)) +{-# INLINE gamma #-} + +foreign import ccall unsafe "math.h gamma" + c_gamma :: CDouble -> CDouble + +-- | The hypot function function computes the sqrt(x*x+y*y) in such a way that +-- underflow will not happen, and overflow occurs only if the final result +-- deserves it. +-- +-- > hypot(Infinity, v) = hypot(v, Infinity) = +Infinity for all v, including NaN. +-- +hypot :: Double -> Double -> Double +hypot x y = realToFrac (c_hypot (realToFrac x) (realToFrac y)) +{-# INLINE hypot #-} + +foreign import ccall unsafe "math.h hypot" + c_hypot :: CDouble -> CDouble -> CDouble + +-- | The isinf function returns 1 if the number n is Infinity, otherwise 0. +-- +isinf :: Double -> Int +isinf x = fromIntegral (c_isinf (realToFrac x)) +{-# INLINE isinf #-} + +foreign import ccall unsafe "math.h isinf" + c_isinf :: CDouble -> CInt + +-- | The isnan function returns 1 if the number n is ``not-a-number'', +-- otherwise 0. +-- +isnan :: Double -> Int +isnan x = fromIntegral (c_isnan (realToFrac x)) +{-# INLINE isnan #-} + +foreign import ccall unsafe "math.h isnan" + c_isnan :: CDouble -> CInt + +-- | finite returns the value 1 just when -Infinity < x < +Infinity; otherwise +-- a zero is returned (when |x| = Infinity or x is NaN. +-- +finite :: Double -> Int +finite x = fromIntegral (c_finite (realToFrac x)) +{-# INLINE finite #-} + +foreign import ccall unsafe "math.h finite" + c_finite :: CDouble -> CInt + +-- | The functions j0() and j1() compute the Bessel function of the +-- first kind of the order 0 and the order 1, respectively, for the real +-- value x +-- +j0 :: Double -> Double +j0 x = realToFrac (c_j0 (realToFrac x)) +{-# INLINE j0 #-} + +foreign import ccall unsafe "math.h j0" + c_j0 :: CDouble -> CDouble + +-- | The functions j0() and j1() compute the Bessel function of the +-- first kind of the order 0 and the order 1, respectively, for the real +-- value x +-- +j1 :: Double -> Double +j1 x = realToFrac (c_j1 (realToFrac x)) +{-# INLINE j1 #-} + +foreign import ccall unsafe "math.h j1" + c_j1 :: CDouble -> CDouble + +-- | The functions y0() and y1() compute the linearly independent Bessel +-- function of the second kind of the order 0 and the order 1, +-- respectively, for the positive integer value x (expressed as a double) +-- +y0 :: Double -> Double +y0 x = realToFrac (c_y0 (realToFrac x)) +{-# INLINE y0 #-} + +foreign import ccall unsafe "math.h y0" + c_y0 :: CDouble -> CDouble + +-- | The functions y0() and y1() compute the linearly independent Bessel +-- function of the second kind of the order 0 and the order 1, +-- respectively, for the positive integer value x (expressed as a double) +-- +y1 :: Double -> Double +y1 x = realToFrac (c_y1 (realToFrac x)) +{-# INLINE y1 #-} + +foreign import ccall unsafe "math.h y1" + c_y1 :: CDouble -> CDouble + +-- | yn() computes the Bessel function of the second kind for the +-- integer Bessel0 n for the positive integer value x (expressed as a +-- double). +-- +yn :: Int -> Double -> Double +yn x y = realToFrac (c_yn (fromIntegral x) (realToFrac y)) +{-# INLINE yn #-} + +foreign import ccall unsafe "math.h yn" + c_yn :: CInt -> CDouble -> CDouble + +-- | lgamma(x) returns ln|| (x)|. +-- +lgamma :: Double -> Double +lgamma x = realToFrac (c_lgamma (realToFrac x)) +{-# INLINE lgamma #-} + +foreign import ccall unsafe "math.h lgamma" + c_lgamma :: CDouble -> CDouble + + +-- | The acosh function computes the inverse hyperbolic cosine of the real argument x. +-- +acosh :: Double -> Double +acosh x = realToFrac (c_acosh (realToFrac x)) +{-# INLINE acosh #-} + +foreign import ccall unsafe "math.h acosh" + c_acosh :: CDouble -> CDouble + +-- | The asinh function computes the inverse hyperbolic sine of the real argument. +-- +asinh :: Double -> Double +asinh x = realToFrac (c_asinh (realToFrac x)) +{-# INLINE asinh #-} + +foreign import ccall unsafe "math.h asinh" + c_asinh :: CDouble -> CDouble + +-- | The atanh function computes the inverse hyperbolic tangent of the real argument x. +-- +atanh :: Double -> Double +atanh x = realToFrac (c_atanh (realToFrac x)) +{-# INLINE atanh #-} + +foreign import ccall unsafe "math.h atanh" + c_atanh :: CDouble -> CDouble + +-- | The cbrt function computes the cube root of x. +-- +cbrt :: Double -> Double +cbrt x = realToFrac (c_cbrt (realToFrac x)) +{-# INLINE cbrt #-} + +foreign import ccall unsafe "math.h cbrt" + c_cbrt :: CDouble -> CDouble + +-- | logb x returns x's exponent n, a signed integer converted to +-- double-precision floating-point. +-- +-- > logb(+-Infinity) = +Infinity; +-- > logb(0) = -Infinity with a division by zero exception. +-- +logb :: Double -> Double +logb x = realToFrac (c_logb (realToFrac x)) +{-# INLINE logb #-} + +foreign import ccall unsafe "math.h logb" + c_logb :: CDouble -> CDouble + + +-- | nextafter returns the next machine representable number from x in direction y. +-- +nextafter :: Double -> Double -> Double +nextafter x y = realToFrac (c_nextafter (realToFrac x) (realToFrac y)) +{-# INLINE nextafter #-} + +foreign import ccall unsafe "math.h nextafter" + c_nextafter :: CDouble -> CDouble -> CDouble + +-- | remainder returns the remainder r := x - n*y where n is the integer +-- nearest the exact value of x/y; moreover if |n - x/y| = 1/2 then n is even. +-- Consequently, the remainder is computed exactly and |r| <= |y|/2. But +-- remainder(x, 0) and remainder(Infinity, 0) are invalid operations that produce +-- a NaN. -- +remainder :: Double -> Double -> Double +remainder x y = realToFrac (c_remainder (realToFrac x) (realToFrac y)) +{-# INLINE remainder #-} + +foreign import ccall unsafe "math.h remainder" + c_remainder :: CDouble -> CDouble -> CDouble + +-- | scalb(x, n) returns x*(2**n) computed by exponent manipulation. +scalb :: Double -> Double -> Double +scalb x y = realToFrac (c_scalb (realToFrac x) (realToFrac y)) +{-# INLINE scalb #-} + +foreign import ccall unsafe "math.h scalb" + c_scalb :: CDouble -> CDouble -> CDouble + +-- | significand(x) returns sig, where x := sig * 2**n with 1 <= sig < 2. +-- significand(x) is not defined when x is 0, +-Infinity, or NaN. +-- +significand :: Double -> Double +significand x = realToFrac (c_significand (realToFrac x)) +{-# INLINE significand #-} + +foreign import ccall unsafe "math.h significand" + c_significand :: CDouble -> CDouble + + +-- | copysign x y returns x with its sign changed to y's. +copysign :: Double -> Double -> Double +copysign x y = realToFrac (c_copysign (realToFrac x) (realToFrac y)) +{-# INLINE copysign #-} + +foreign import ccall unsafe "math.h copysign" + c_copysign :: CDouble -> CDouble -> CDouble + +-- | ilogb() returns x's exponent n, in integer format. +-- ilogb(+-Infinity) re- turns INT_MAX and ilogb(0) returns INT_MIN. +-- +ilogb :: Double -> Int +ilogb x = fromIntegral (c_ilogb (realToFrac x)) +{-# INLINE ilogb #-} + +foreign import ccall unsafe "math.h ilogb" + c_ilogb :: CDouble -> CInt + +-- | The rint() function returns the integral value (represented as a +-- double precision number) nearest to x according to the prevailing +-- rounding mode. +-- +rint :: Double -> Double +rint x = realToFrac (c_rint (realToFrac x)) +{-# INLINE rint #-} + +foreign import ccall unsafe "math.h rint" + c_rint :: CDouble -> CDouble + + +-- | Determine bitwise equality. +-- +eq :: Double -> Double -> Bool +eq = (==) `on` doubleWord64 + +eqf :: Float -> Float -> Bool +eqf = (==) `on` floatWord32 + +-- | Maximum finite value. +-- +-- >>> shift 1 maxNorm +-- Infinity +-- +maxNorm :: Double +maxNorm = shift (-1) maximal + +maxNormf :: Float +maxNormf = shiftf (-1) maximal + +-- | Minimum normalized value. +-- +-- >>> shift (-1) minNorm +-- 0 +-- +minNorm :: Double +minNorm = word64Double 0x0080000000000000 + +minNormf :: Float +minNormf = word32Float 0x00800000 + +-- | Maximum representable odd integer. +-- +-- @ maxOdd = 2**53 - 1@ +-- +maxOdd :: Double +maxOdd = 9.007199254740991e15 + +-- | Maximum representable odd integer. +-- +-- @ maxOddf = 2**24 - 1@ +-- +maxOddf :: Float +maxOddf = 1.6777215e7 + +-- | Minimum (pos) value. +-- +-- >>> shift (-1) minSub +-- 0.0 +-- +minSub :: Double +minSub = shift 1 0 + +minSubf :: Float +minSubf = shiftf 1 0 + +-- | Difference between 1 and the smallest representable value greater than 1. +epsilon :: Double +epsilon = shift 1 1 - 1 + +epsilonf :: Float +epsilonf = shiftf 1 1 - 1 + +-- | Split a 'Double' symmetrically along the sign bit. +-- +-- >>> split 0 +-- Right 0.0 +-- >>> split (shift (-1) 0) +-- Left (-0.0) +-- +split :: Double -> Either Double Double +split x = case signBit x of + True -> Left x + _ -> Right x + +splitf :: Float -> Either Float Float +splitf x = case signBitf x of + True -> Left x + _ -> Right x + + +-- TODO replace w/ Yoneda / Index / Graded +-- | Shift by /Int64/ units of least precision. +-- +shift :: Int64 -> Double -> Double +shift n = int64Double . (+ n) . doubleInt64 + +shiftf :: Int32 -> Float -> Float +shiftf n = int32Float . (+ n) . floatInt32 + +-- | Compute signed distance in units of least precision. +-- +-- @ 'ulps' x ('shift' ('abs' n) x) '==' ('True', 'abs' n) @ +-- +ulps :: Double -> Double -> (Bool, Word64) +ulps x y = o + where x' = doubleInt64 x + y' = doubleInt64 y + o | x' >= y' = (False, fromIntegral . abs $ x' - y') + | otherwise = (True, fromIntegral . abs $ y' - x') + +ulpsf :: Float -> Float -> (Bool, Word32) +ulpsf x y = o + where x' = floatInt32 x + y' = floatInt32 y + o | x' >= y' = (False, fromIntegral . abs $ x' - y') + | otherwise = (True, fromIntegral . abs $ y' - x') + +-- | Compute distance in units of least precision. +-- +-- @ 'ulps'' x ('shift' n x) '==' 'abs' n @ +-- +ulps' :: Double -> Double -> Word64 +ulps' x y = snd $ ulps x y + +ulpsf' :: Float -> Float -> Word32 +ulpsf' x y = snd $ ulpsf x y + +-- | Compare two values for approximate equality. +-- +-- Required accuracy is specified in units of least precision. +-- +-- See also . +-- +within :: Word64 -> Double -> Double -> Bool +within tol a b = ulps' a b <= tol + +withinf :: Word32 -> Float -> Float -> Bool +withinf tol a b = ulpsf' a b <= tol + + + +{- +ulpDelta :: Float -> Float -> Int +ulpDelta x y = if lesser then d' else (-1) * d' + where (lesser, d) = ulps x y + d' = fromIntegral d + +ulpDelta' :: Float -> Float -> Int32 +ulpDelta' x y = if lesser then d' else (-1) * d' + where (lesser, d) = ulps x y + d' = fromIntegral d +-} + +---------------------------------------------------------------- +-- Ulp32 +---------------------------------------------------------------- + +-- | 32 bit unit of least precision type. +-- +newtype Ulp32 = Ulp32 { unUlp32 :: Int32 } deriving Show + +ulp32Nan :: Ulp32 -> Bool +ulp32Nan (Ulp32 x) = x /= (min 2139095040 . max (- 2139095041)) x + +instance Eq Ulp32 where + x == y | ulp32Nan x && ulp32Nan y = True + | ulp32Nan x || ulp32Nan y = False + | otherwise = on (==) unUlp32 x y + +instance Prd Ulp32 where + x <= y | ulp32Nan x && ulp32Nan y = True + | ulp32Nan x || ulp32Nan y = False + | otherwise = on (<=) unUlp32 x y + +instance Minimal Ulp32 where + minimal = Ulp32 $ -2139095041 + +instance Maximal Ulp32 where + maximal = Ulp32 $ 2139095040 + +instance Semigroup (Additive Ulp32) where + Additive (Ulp32 x) <> Additive (Ulp32 y) = Additive . Ulp32 $ x + y + +instance Monoid (Additive Ulp32) where + mempty = Additive $ Ulp32 0 + +instance Semigroup (Multiplicative Ulp32) where + Multiplicative (Ulp32 x) <> Multiplicative (Ulp32 y) = Multiplicative . Ulp32 $ x * y + +instance Monoid (Multiplicative Ulp32) where + mempty = Multiplicative $ Ulp32 1 + +instance Presemiring Ulp32 +instance Semiring Ulp32 + +instance Semigroup (Join Ulp32) where + Join (Ulp32 x) <> Join (Ulp32 y) = Join . Ulp32 $ P.max x y + +instance Semigroup (Meet Ulp32) where + Meet (Ulp32 x) <> Meet (Ulp32 y) = Meet . Ulp32 $ P.min x y + +f32u32 :: Conn Float Ulp32 +f32u32 = Conn (Ulp32 . floatInt32) (int32Float . unUlp32) + +u32f32 :: Conn Ulp32 Float +u32f32 = Conn (int32Float . unUlp32) (Ulp32 . floatInt32) + +-- fromIntegral (maxBound :: Ulp32) + 1 , image of aNan + + +--newtype Ulp a = Ulp { unUlp :: a } +-- instance +{- correct but should replace w/ Graded / Yoneda / Indexed etc +u32w64 :: Conn Ulp32 (Nan Word64) +u32w64 = Conn f g where + conn = i32w32 >>> w32w64 + + offset = 2139095041 :: Word64 + offset' = 2139095041 :: Int32 + + f x@(Ulp32 y) | ulp32Nan x = Nan + | neg y = Def $ fromIntegral (y + offset') + | otherwise = Def $ (fromIntegral y) + offset + where fromIntegral = connl conn + + g x = case x of + Nan -> Ulp32 offset' + Def y | y < offset -> Ulp32 $ (fromIntegral y) P.- offset' + | otherwise -> Ulp32 $ fromIntegral ((min 4278190081 y) P.- offset) + where fromIntegral = connr conn +-} + + +-- internal + +-- +--TODO handle neg case, get # of nans/denormals, collect constants + +--abs' :: Eq a => Ord a => Bound a => Ring a => a -> a +--abs' x = if x == minimal then abs (x+one) else abs x + +signBit :: Double -> Bool +signBit x = if x =~ anan then False else msbMask x /= 0 + +evenBit :: Double -> Bool +evenBit x = lsbMask x == 0 + +lsbMask :: Double -> Word64 +lsbMask x = 0x0000000000000001 .&. doubleWord64 x + +msbMask :: Double -> Word64 +msbMask x = 0x8000000000000000 .&. doubleWord64 x + +-- loatWord64 maximal == exponent maximal +--expMask :: Double -> Word64 +--expMask x = 0x7F80000000000000 .&. doubleWord64 x + +-- chk = >= 0 ==> == word64Double $ exponent + signiicand +sigMask :: Double -> Word64 +sigMask x = 0x007FFFFFFFFFFFFF .&. doubleWord64 x + + + +signBitf :: Float -> Bool +signBitf x = if x =~ anan then False else msbMaskf x /= 0 + +evenBitf :: Float -> Bool +evenBitf x = lsbMaskf x == 0 + +lsbMaskf :: Float -> Word32 +lsbMaskf x = 0x00000001 .&. floatWord32 x + +msbMaskf :: Float -> Word32 +msbMaskf x = 0x80000000 .&. floatWord32 x + +-- floatWord32 maximal == exponent maximal +expMaskf :: Float -> Word32 +expMaskf x = 0x7f800000 .&. floatWord32 x + +-- chk f = f >= 0 ==> f == word32Float $ exponent f + significand f +sigMaskf :: Float -> Word32 +sigMaskf x = 0x007FFFFF .&. floatWord32 x + + + +{- +-- | first /NaN/ value. +--naN :: Float +--naN = 0/0 -- inc pInf + +-- | Positive infinity +-- +-- @nInf = 1/0@ +-- +pInf :: Float +pInf = word32Float 0x7f800000 + +-- | Negative infinity +-- +-- @nInf = -1/0@ +-- +nInf :: Float +nInf = word32Float 0xff800000 +-} + + +-- Non-monotonic function +signed64 :: Word64 -> Int64 +signed64 x | x < 0x8000000000000000 = fromIntegral x + | otherwise = fromIntegral (maximal P.- (x P.- 0x8000000000000000)) + +-- Non-monotonic function converting from 2s-complement format. +unsigned64 :: Int64 -> Word64 +unsigned64 x | x >= 0 = fromIntegral x + | otherwise = 0x8000000000000000 + (maximal P.- (fromIntegral x)) + +int64Double :: Int64 -> Double +int64Double = word64Double . unsigned64 + +doubleInt64 :: Double -> Int64 +doubleInt64 = signed64 . doubleWord64 + +-- Bit-for-bit conversion. +word64Double :: Word64 -> Double +word64Double = F.castWord64ToDouble + +-- TODO force to pos representation? +-- Bit-for-bit conversion. +doubleWord64 :: Double -> Word64 +doubleWord64 = (+0) . F.castDoubleToWord64 + +-- Non-monotonic function +signed32 :: Word32 -> Int32 +signed32 x | x < 0x80000000 = fromIntegral x + | otherwise = fromIntegral (maximal P.- (x P.- 0x80000000)) + +-- Non-monotonic function converting from 2s-complement format. +unsigned32 :: Int32 -> Word32 +unsigned32 x | x >= 0 = fromIntegral x + | otherwise = 0x80000000 + (maximal P.- (fromIntegral x)) + +int32Float :: Int32 -> Float +int32Float = word32Float . unsigned32 + +floatInt32 :: Float -> Int32 +floatInt32 = signed32 . floatWord32 + +-- Bit-for-bit conversion. +word32Float :: Word32 -> Float +word32Float = F.castWord32ToFloat + +-- TODO force to pos representation? +-- Bit-for-bit conversion. +floatWord32 :: Float -> Word32 +floatWord32 = (+0) . F.castFloatToWord32 + diff --git a/src/Data/Prd.hs b/src/Data/Prd.hs --- a/src/Data/Prd.hs +++ b/src/Data/Prd.hs @@ -6,41 +6,45 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE CPP #-} module Data.Prd ( - module Data.Prd - , Down(..) + Down(..) + , Ord(min, max, compare) + , module Data.Prd ) where -import Control.Applicative -import Control.Monad -import Data.Data (Data, Typeable) import Data.Function import Data.Int as Int (Int, Int8, Int16, Int32, Int64) import Data.List.NonEmpty (NonEmpty(..)) import Data.Maybe import Data.Monoid hiding (First, Last) -import Data.Ord (Down(..)) +import Data.Ord (Ord, Down(..), compare, min, max) import Data.Ratio import Data.Word (Word, Word8, Word16, Word32, Word64) -import GHC.Generics (Generic, Generic1) -import GHC.Real +import GHC.Real hiding (Fractional(..), div, (^^), (^), (%)) import Numeric.Natural - +--import Data.Semigroup +import Data.Semigroup.Additive +import Data.Semigroup.Multiplicative +import Data.Semiring +import Data.Semifield (Field, Semifield, anan, pinf, ninf) +import Data.Fixed import qualified Data.Semigroup as S import qualified Data.Set as Set import qualified Data.Map as Map import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet -import qualified Data.Sequence as Seq +import qualified Prelude as P -infix 4 <~, >~, /~, ~~, =~, ?~, `pgt`, `pge`, `peq`, `pne`, `ple`, `plt` -infix 4 `lt`, `gt`, `le`, `ge`, `eq`, `ne`, `pmax`, `pmin` +import Prelude hiding (Ord(..), Fractional(..),Num(..)) +infix 4 <=, >=, <, >, =~, ~~, !~, /~, ?~, `pgt`, `pge`, `peq`, `pne`, `ple`, `plt` --- | A partial order on the set /a/. +-- | A partial order on /a/. -- --- A poset relation '<~' must satisfy the following three partial order axioms: +-- A poset relation '<=' must satisfy the following three partial order axioms: -- -- \( \forall x: x \leq x \) (reflexivity) -- @@ -51,11 +55,10 @@ -- If a prior equality relation is available, then a valid @Prd a@ instance may be derived from a semiorder relation 'lt' as: -- -- @ --- x '<~' y = 'lt' x y '||' x '==' y +-- x '<=' y '==' 'lt' x y '||' x '==' y -- @ -- --- If /a/ is derived from a semiorder then the definition of 'lt' must satisfy --- the three semiorder axioms: +-- If /a/ is derived from a semiorder then the definition of 'lt' must satisfy the three semiorder axioms: -- -- \( \forall x, y: x \lt y \Rightarrow \neg y \lt x \) (asymmetry) -- @@ -63,7 +66,7 @@ -- -- \( \forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w) \) (3-1 chain) -- --- The poset axioms on '<~' then follow from the first & second axioms on 'lt', +-- The poset axioms on '<=' then follow from the first & second axioms on 'lt', -- however the converse is not true. While the first semiorder axiom on 'lt' follows, the second -- and third semiorder axioms forbid partial orders of four items forming two disjoint chains: -- @@ -74,175 +77,232 @@ -- and . -- class Prd a where - {-# MINIMAL (<~) | (>~) #-} + {-# MINIMAL (<=) | pcompare #-} -- | Non-strict partial order relation on /a/. -- - -- '<~' is reflexive, anti-symmetric, and transitive. + -- '<=' is reflexive, anti-symmetric, and transitive. -- - (<~) :: a -> a -> Bool - (<~) = flip (>~) + -- Furthermore we have: + -- + -- @ + -- x '<=' y ≡ 'maybe' 'False' ('<=' 'EQ') ('pcompare' x y) + -- x '<=' y ≡ x '<' y '||' x '=~' y + -- @ + -- for all /x/, /y/ in /a/. + -- + (<=) :: a -> a -> Bool + x <= y = maybe False (P.<= EQ) $ pcompare x y -- | Converse non-strict partial order relation on /a/. -- - -- '>~' is reflexive, anti-symmetric, and transitive. + -- '>=' is reflexive, anti-symmetric, and transitive. -- - (>~) :: a -> a -> Bool - (>~) = flip (<~) + -- Furthermore we have: + -- + -- @ + -- x '>=' y ≡ 'maybe' 'False' ('>=' 'EQ') ('pcompare' x y) + -- x '>=' y ≡ x '>' y '||' x '=~' y + -- @ + -- for all /x/, /y/ in /a/. + -- + (>=) :: a -> a -> Bool + (>=) = flip (<=) - -- | Equivalence relation on /a/. + -- | Strict partial order relation on /a/. -- - -- '=~' is reflexive, symmetric, and transitive. + -- '<' is irreflexive, asymmetric, and transitive. -- - -- @ x =~ y = maybe False (== EQ) (pcomparePrd x y) + -- Furthermore we have: -- - -- If /a/ implements 'Eq' then (ideally) @x =~ y = x == y@. + -- @ + -- x '<' y ≡ 'maybe' 'False' ('<' 'EQ') ('pcompare' x y) + -- x '<' y ≡ x '?~' y '==>' x '<=' y '&&' x '\~' y + -- @ + -- for all /x/, /y/ in /a/. -- - (=~) :: a -> a -> Bool - x =~ y = x <~ y && x >~ y + (<) :: a -> a -> Bool + x < y = maybe False (P.< EQ) $ pcompare x y + -- | Converse strict partial order relation on /a/. + -- + -- '>' is irreflexive, asymmetric, and transitive. + -- + -- Furthermore we have: + -- + -- @ + -- x '>' y ≡ 'maybe' 'False' ('>' 'EQ') ('pcompare' x y) + -- x '>' y ≡ x '?~' y '==>' x '>=' y '&&' x '\~' y + -- @ + -- for all /x/, /y/ in /a/. + -- + (>) :: Prd a => a -> a -> Bool + x > y = maybe False (P.> EQ) $ pcompare x y + -- | Comparability relation on /a/. -- -- '?~' is reflexive, symmetric, and transitive. -- - -- @ x ?~ y = maybe False (const True) (pcomparePrd x y) @ + -- Furthermore we have: -- - -- If /a/ implements 'Ord' then (ideally) @x ?~ y = True@. + -- @ + -- x '=~' y ≡ 'maybe' 'False' ('const' 'True') ('pcompare' x y) + -- x '=~' y ≡ x '<=' y '||' x '>=' y + -- @ + -- for all /x/, /y/ in /a/. -- + -- If /a/ implements 'Ord' then we must have: + -- + -- @x '?~' y ≡ 'True'@ + -- for all /x/, /y/ in /a/. + -- (?~) :: a -> a -> Bool - x ?~ y = x <~ y || x >~ y + x ?~ y = maybe False (const True) $ pcompare x y - -- | Partial version of 'Data.Ord.compare'. + -- | Equivalence relation on /a/. -- - pcompare :: Eq a => a -> a -> Maybe Ordering - pcompare x y - | x `lt` y = Just LT - | x == y = Just EQ - | x `gt` y = Just GT - | otherwise = Nothing + -- '=~' is reflexive, symmetric, and transitive: + -- + -- Furthermore we have: + -- + -- @ + -- x '=~' y ≡ 'maybe' 'False' ('=~' 'EQ') ('pcompare' x y) + -- x '=~' y ≡ x '<=' y '&&' x '>=' y + -- @ + -- for all /x/, /y/ in /a/. + -- + -- If /a/ implements 'Eq' then it is recommended to use the + -- same definitions for '==' and '=~'. + -- + (=~) :: a -> a -> Bool + x =~ y = maybe False (== EQ) $ pcompare x y + -- | Negation of '=~'. + -- + (/~) :: a -> a -> Bool + x /~ y = not $ x =~ y --- | Similarity relation on /a/. --- --- '~~' is reflexive and symmetric, but not necessarily transitive. --- --- Note this is only equivalent to '==' in a total (i.e. linear) order. --- -(~~) :: Eq a => Prd a => a -> a -> Bool -x ~~ y = not (x `lt` y) && not (x `gt` y) + -- | Similarity relation on /a/. + -- + -- '~~' is reflexive and symmetric, but not necessarily transitive. + -- + -- Furthermore we have: + -- + -- @ + -- x '>=' y ≡ 'maybe' 'True' ('=~' 'EQ') ('pcompare' x y) + -- x '~~' y ≡ 'not' (x '<' y) '&&' 'not' (x '<' y) + -- @ + -- for all /x/, /y/ in /a/. + -- + -- If /a/ implements 'Ord' then we must have: + -- + -- @x '~~' y ≡ x '=~' y @ + -- for all /x/, /y/ in /a/. + -- + (~~) :: a -> a -> Bool + x ~~ y = not (x < y) && not (x > y) --- | Negation of '~~'. --- -(/~) :: Eq a => Prd a => a -> a -> Bool -x /~ y = not $ x ~~ y + -- | Negation of '~~'. + -- + (!~) :: a -> a -> Bool + x !~ y = not $ x ~~ y --- | Version of 'pcompare' that uses the derived equivalence relation. --- --- This can be useful if there is no 'Eq' instance or if it is --- suspect, for example when /a/ is a floating point number. --- -pcomparePrd :: Prd a => a -> a -> Maybe Ordering -pcomparePrd x y - | x <~ y = Just $ if y <~ x then EQ else LT - | y <~ x = Just GT - | otherwise = Nothing + -- | Partial version of 'compare'. + -- + pcompare :: a -> a -> Maybe Ordering + pcompare x y + | x <= y = Just $ if y <= x then EQ else LT + | y <= x = Just GT + | otherwise = Nothing --- | Version of 'pcompare' that uses 'compare'. --- -pcompareOrd :: Ord a => a -> a -> Maybe Ordering -pcompareOrd x y = Just $ x `compare` y --- | Prefix version of '=~'. --- --- @ eq x y = maybe False (== EQ) (pcomparePrd x y) --- -eq :: Prd a => a -> a -> Bool -x `eq` y = x <~ y && x >~ y - --- | Negation of 'eq'. --- --- @ ne x y = maybe False (/= EQ) (pcomparePrd x y) --- -ne :: Prd a => a -> a -> Bool -x `ne` y = not $ x `eq` y +type Bound a = (Minimal a, Maximal a) --- | Prefix version of '<~'. +-- | A minimal element of a partially ordered set. +-- +-- @ 'minimal' '?~' a '==>' 'minimal' '<=' a @ -- --- @ le x y = maybe False (<= EQ) (pcomparePrd x y) +-- Note that 'minimal' needn't be comparable to all values in /a/. -- -le :: Prd a => a -> a -> Bool -x `le` y = x <~ y - --- | Prefix version of '>~'. +-- When /a/ is a 'Field' we should have: @ 'minimal' '==' 'ninf' @. -- --- @ ge x y = maybe False (>= EQ) (pcomparePrd x y) +-- See < https://en.wikipedia.org/wiki/Maximal_and_minimal_elements >. -- -ge :: Prd a => a -> a -> Bool -x `ge` y = x >~ y +class Prd a => Minimal a where + minimal :: a --- | Strict partial order relation on /a/. +-- | A maximal element of a partially ordered set. +-- +-- @ 'maximal' '?~' a '==>' 'maximal' '>=' a @ -- --- 'lt' is irreflexive, asymmetric, and transitive. +-- Note that 'maximal' needn't be comparable to all values in /a/. -- --- @ lt x y = maybe False (< EQ) (pcompare x y) @ +-- When /a/ is a 'Semifield' we should have @ 'maximal' = 'pinf' @. -- --- If /a/ implements 'Ord' then (ideally) @x `lt` y = x < y@. +-- See < https://en.wikipedia.org/wiki/Maximal_and_minimal_elements >. -- -lt :: Eq a => Prd a => a -> a -> Bool -x `lt` y | x /= x || y /= y = False -- guard on lawless 0/0 cases - | otherwise = x <~ y && x /= y +class Prd a => Maximal a where + maximal :: a --- | Converse strict partial order relation on /a/. --- --- 'gt' is irreflexive, asymmetric, and transitive. +-- | Version of 'pcompare' that uses a semiorder relation and '=='. -- --- @ gt x y = maybe False (> EQ) (pcompare x y) @ +-- See . -- --- If /a/ implements 'Ord' then (ideally) @x `gt` y = x > y@. +pcompareEq :: Eq a => (a -> a -> Bool) -> a -> a -> Maybe Ordering +pcompareEq lt x y + | lt x y = Just LT + | x == y = Just EQ + | lt y x = Just GT + | otherwise = Nothing + +-- | Version of 'pcompare' that uses 'compare'. -- -gt :: Eq a => Prd a => a -> a -> Bool -x `gt` y | x /= x || y /= y = False - | otherwise = x >~ y && x /= y +pcompareOrd :: Ord a => a -> a -> Maybe Ordering +pcompareOrd x y = Just $ x `compare` y -- | A partial version of ('=~') -- -- Returns 'Nothing' instead of 'False' when the two values are not comparable. -- -peq :: Eq a => Prd a => a -> a -> Maybe Bool -peq x y = case x `pcompare` y of - Just EQ -> Just True - Just _ -> Just False - Nothing -> Nothing +peq :: Prd a => a -> a -> Maybe Bool +peq x y = do + o <- pcompare x y + case o of + EQ -> Just True + _ -> Just False -- | A partial version of ('/~') -- -- Returns 'Nothing' instead of 'False' when the two values are not comparable. -- -pne :: Eq a => Prd a => a -> a -> Maybe Bool -pne x y = case x `pcompare` y of - Just EQ -> Just False - Just _ -> Just True - Nothing -> Nothing +pne :: Prd a => a -> a -> Maybe Bool +pne x y = do + o <- pcompare x y + case o of + EQ -> Just False + _ -> Just True --- | A partial version of ('<~') +-- | A partial version of ('<=') -- -- Returns 'Nothing' instead of 'False' when the two values are not comparable. -- -ple :: Eq a => Prd a => a -> a -> Maybe Bool -ple x y = case x `pcompare` y of - Just GT -> Just False - Just _ -> Just True - Nothing -> Nothing +ple :: Prd a => a -> a -> Maybe Bool +ple x y = do + o <- pcompare x y + case o of + GT -> Just False + _ -> Just True --- | A partial version of ('>~') +-- | A partial version of ('>=') -- -- Returns 'Nothing' instead of 'False' when the two values are not comparable. -- -pge :: Eq a => Prd a => a -> a -> Maybe Bool -pge x y = case x `pcompare` y of - Just LT -> Just False - Just _ -> Just True - Nothing -> Nothing +pge :: Prd a => a -> a -> Maybe Bool +pge x y = do + o <- pcompare x y + case o of + LT -> Just False + _ -> Just True -- | A partial version of ('<') -- @@ -250,11 +310,12 @@ -- -- @lt x y == maybe False id $ plt x y@ -- -plt :: Eq a => Prd a => a -> a -> Maybe Bool -plt x y = case x `pcompare` y of - Just LT -> Just True - Just _ -> Just False - Nothing -> Nothing +plt :: Prd a => a -> a -> Maybe Bool +plt x y = do + o <- pcompare x y + case o of + LT -> Just True + _ -> Just False -- | A partial version of ('>') -- @@ -262,127 +323,65 @@ -- -- @gt x y == maybe False id $ pgt x y@ -- -pgt :: Eq a => Prd a => a -> a -> Maybe Bool -pgt x y = case x `pcompare` y of - Just GT -> Just True - Just _ -> Just False - Nothing -> Nothing +pgt :: Prd a => a -> a -> Maybe Bool +pgt x y = do + o <- pcompare x y + case o of + GT -> Just True + _ -> Just False -- | A partial version of 'Data.Ord.max'. -- -- Returns the right argument in the case of equality. -- -pmax :: Eq a => Prd a => a -> a -> Maybe a +pmax :: Prd a => a -> a -> Maybe a pmax x y = do o <- pcompare x y case o of GT -> Just x - EQ -> Just y - LT -> Just y - -pjoin :: Eq a => Minimal a => Foldable f => f a -> Maybe a -pjoin = foldM pmax minimal + _ -> Just y -- | A partial version of 'Data.Ord.min'. -- -- Returns the right argument in the case of equality. -- -pmin :: Eq a => Prd a => a -> a -> Maybe a +pmin :: Prd a => a -> a -> Maybe a pmin x y = do o <- pcompare x y case o of GT -> Just y - EQ -> Just x - LT -> Just x - -pmeet :: Eq a => Maximal a => Foldable f => f a -> Maybe a -pmeet = foldM pmin maximal + _ -> Just x -sign :: Eq a => Num a => Prd a => a -> Maybe Ordering -sign x = pcompare x 0 +pabs :: (Additive-Group) a => Prd a => a -> a +pabs x = if zero <= x then x else negate x -zero :: Eq a => Num a => Prd a => a -> Bool -zero x = sign x == Just EQ +sign :: (Additive-Monoid) a => Prd a => a -> Maybe Ordering +sign x = pcompare x zero -positive :: Eq a => Num a => Prd a => a -> Bool -positive x = sign x == Just GT +finite :: Prd a => Semifield a => a -> Bool +finite = (/~ anan) * (/~ pinf) -negative :: Eq a => Num a => Prd a => a -> Bool -negative x = sign x == Just LT +finite' :: Prd a => Field a => a -> Bool +finite' = finite * (/~ ninf) -indeterminate :: Eq a => Num a => Prd a => a -> Bool -indeterminate x = sign x == Nothing +extend :: (Prd a, Semifield a, Semifield b) => (a -> b) -> a -> b +extend f x | x =~ anan = anan + | x =~ pinf = pinf + | otherwise = f x +extend' :: (Prd a, Field a, Field b) => (a -> b) -> a -> b +extend' f x | x =~ ninf = ninf + | otherwise = extend f x --------------------------------------------------------------------- -- Instances --------------------------------------------------------------------- -instance Prd Bool where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Char where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Integer where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Int where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Int8 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Int16 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Int32 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Int64 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Natural where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Word where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Word8 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Word16 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Word32 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Word64 where - (<~) = (<=) - pcompare = pcompareOrd - -instance Prd Ordering where - (<~) = (<=) - pcompare = pcompareOrd - instance Prd a => Prd [a] where {-# SPECIALISE instance Prd [Char] #-} - [] <~ _ = True - (_:_) <~ [] = False - (x:xs) <~ (y:ys) = x <~ y && xs <~ ys + [] <= _ = True + (_:_) <= [] = False + (x:xs) <= (y:ys) = x <= y && xs <= ys {- pcompare [] [] = Just EQ @@ -394,156 +393,178 @@ -} instance Prd a => Prd (NonEmpty a) where - (x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys + (x :| xs) <= (y :| ys) = x <= y && xs <= ys instance Prd a => Prd (Down a) where - x <~ y = y <~ x + (Down x) <= (Down y) = y <= x + pcompare (Down x) (Down y) = pcompare y x -- Canonically ordered. instance Prd a => Prd (Dual a) where - x <~ y = y <~ x - -instance Prd Any where - Any x <~ Any y = x <~ y - -instance Prd All where - All x <~ All y = y <~ x - -{- + (Dual x) <= (Dual y) = y <= x + pcompare (Dual x) (Dual y) = pcompare y x --- | 'First a' forms a pre-dioid for any semigroup @a@. -instance (Eq a, Semigroup a) => Prd (S.First a) where - (<~) = (==) +instance Prd a => Prd (S.Max a) where + S.Max a <= S.Max b = a <= b -instance Ord a => Prd (S.Maximal a) where - pcompare (S.Maximal x) (S.Maximal y) = Just $ compare x y +instance Prd a => Prd (S.Min a) where + S.Min a <= S.Min b = a <= b -instance Ord a => Prd (S.Minimal a) where - pcompare (S.Minimal x) (S.Minimal y) = Just $ compare y x +instance Prd Any where + Any x <= Any y = x <= y --} +instance Prd All where + All x <= All y = y <= x instance Prd Float where - x <~ y | x /= x && y /= y = True + x <= y | x /= x && y /= y = True | x /= x || y /= y = False - | otherwise = x <= y -{- + | otherwise = x P.<= y + + x =~ y | x /= x && y /= y = True + | x /= x || y /= y = False + | otherwise = x == y + + x ?~ y | x /= x && y /= y = True + | x /= x || y /= y = False + | otherwise = True + pcompare x y | x /= x && y /= y = Just EQ | x /= x || y /= y = Nothing | otherwise = pcompareOrd x y - x `eq` y | x /= x && y /= y = True - | x /= x || y /= y = False - | otherwise = x == y +instance Prd Double where + x <= y | x /= x && y /= y = True + | x /= x || y /= y = False + | otherwise = x P.<= y - x `lt` y | x /= x || y /= y = False - | otherwise = shift 2 x P.< y --} + x =~ y | x /= x && y /= y = True + | x /= x || y /= y = False + | otherwise = x == y + x ?~ y | x /= x && y /= y = True + | x /= x || y /= y = False + | otherwise = True + pcompare x y | x /= x && y /= y = Just EQ + | x /= x || y /= y = Nothing + | otherwise = pcompareOrd x y -instance Prd Double where - x <~ y | x /= x && y /= y = True - | x /= x || y /= y = False - | otherwise = x <= y +instance Prd (Ratio Integer) where + pcompare (x:%y) (x':%y') | (x == 0 && y == 0) && (x' == 0 && y' == 0) = Just EQ + | (x == 0 && y == 0) || (x' == 0 && y' == 0) = Nothing + | y == 0 && y' == 0 = Just $ compare (signum x) (signum x') + | y == 0 = pcompareOrd x 0 + | y' == 0 = pcompareOrd 0 x' + | otherwise = pcompareOrd (x%y) (x'%y') -instance (Prd a, Integral a) => Prd (Ratio a) where - {-# SPECIALIZE instance Prd Rational #-} - (x:%y) <~ (x':%y') | (x `eq` 0 && y `eq` 0) || (x' `eq` 0 && y' `eq` 0) = False - | otherwise = x * y' <~ x' * y +--TODO add prop tests +instance Prd (Ratio Natural) where + pcompare (x:%y) (x':%y') | (x == 0 && y == 0) && (x' == 0 && y' == 0) = Just EQ + | (x == 0 && y == 0) || (x' == 0 && y' == 0) = Nothing + | y == 0 && y' == 0 = Just EQ + | y == 0 = Just GT + | y' == 0 = Just LT + | otherwise = pcompareOrd (x*y') (x'*y) -- Canonical semigroup ordering instance Prd a => Prd (Maybe a) where - Just a <~ Just b = a <~ b - x@Just{} <~ Nothing = False - Nothing <~ _ = True + Just a <= Just b = a <= b + Just{} <= Nothing = False + Nothing <= _ = True -- Canonical semigroup ordering instance (Prd a, Prd b) => Prd (Either a b) where - Right a <~ Right b = a <~ b - Right _ <~ _ = False + Right a <= Right b = a <= b + Right _ <= _ = False - Left e <~ Left f = e <~ f - Left _ <~ _ = True + Left e <= Left f = e <= f + Left _ <= _ = True -instance Prd () where - pcompare _ _ = Just EQ - _ <~ _ = True - -- Canonical semigroup ordering instance (Prd a, Prd b) => Prd (a, b) where - (a,b) <~ (i,j) = a <~ i && b <~ j + (a,b) <= (i,j) = a <= i && b <= j instance (Prd a, Prd b, Prd c) => Prd (a, b, c) where - (a,b,c) <~ (i,j,k) = a <~ i && b <~ j && c <~ k + (a,b,c) <= (i,j,k) = a <= i && b <= j && c <= k instance (Prd a, Prd b, Prd c, Prd d) => Prd (a, b, c, d) where - (a,b,c,d) <~ (i,j,k,l) = a <~ i && b <~ j && c <~ k && d <~ l + (a,b,c,d) <= (i,j,k,l) = a <= i && b <= j && c <= k && d <= l instance (Prd a, Prd b, Prd c, Prd d, Prd e) => Prd (a, b, c, d, e) where - (a,b,c,d,e) <~ (i,j,k,l,m) = a <~ i && b <~ j && c <~ k && d <~ l && e <~ m + (a,b,c,d,e) <= (i,j,k,l,m) = a <= i && b <= j && c <= k && d <= l && e <= m instance Ord a => Prd (Set.Set a) where - (<~) = Set.isSubsetOf + (<=) = Set.isSubsetOf instance (Ord k, Prd a) => Prd (Map.Map k a) where - (<~) = Map.isSubmapOfBy (<~) + (<=) = Map.isSubmapOfBy (<=) instance Prd a => Prd (IntMap.IntMap a) where - (<~) = IntMap.isSubmapOfBy (<~) + (<=) = IntMap.isSubmapOfBy (<=) instance Prd IntSet.IntSet where - (<~) = IntSet.isSubsetOf + (<=) = IntSet.isSubsetOf --- Helper type for 'DerivingVia' -newtype Ordered a = Ordered { getOrdered :: a } - deriving ( Eq, Ord, Show, Data, Typeable, Generic, Generic1, Functor, Foldable, Traversable) +#define derivePrd(ty) \ +instance Prd ty where { \ + (<=) = (P.<=) \ +; {-# INLINE (<=) #-} \ +; (>=) = (P.>=) \ +; {-# INLINE (>=) #-} \ +; (<) = (P.<) \ +; {-# INLINE (<) #-} \ +; (>) = (P.>) \ +; {-# INLINE (>) #-} \ +; (=~) = (P.==) \ +; {-# INLINE (=~) #-} \ +; (~~) = (P.==) \ +; {-# INLINE (~~) #-} \ +; pcompare = pcompareOrd \ +; {-# INLINE pcompare #-} \ +} -instance Ord a => Prd (Ordered a) where - (<~) = (<=) +derivePrd(()) +derivePrd(Bool) +derivePrd(Char) +derivePrd(Ordering) +derivePrd(Int) +derivePrd(Int8) +derivePrd(Int16) +derivePrd(Int32) +derivePrd(Int64) +derivePrd(Integer) + +derivePrd(Word) +derivePrd(Word8) +derivePrd(Word16) +derivePrd(Word32) +derivePrd(Word64) +derivePrd(Natural) + +derivePrd(Uni) +derivePrd(Deci) +derivePrd(Centi) +derivePrd(Milli) +derivePrd(Micro) +derivePrd(Nano) +derivePrd(Pico) + ------------------------------------------------------------------------------- -- Minimal ------------------------------------------------------------------------------- -type Bound a = (Minimal a, Maximal a) - --- | Minimal element of a partially ordered set. --- --- \( \forall x: x \ge minimal \) --- --- This means that 'minimal' must be comparable to all values in /a/. --- -class Prd a => Minimal a where - minimal :: a +instance Minimal Float where minimal = ninf -instance Minimal () where minimal = () +instance Minimal Double where minimal = ninf instance Minimal Natural where minimal = 0 -instance Minimal Bool where minimal = minBound - -instance Minimal Ordering where minimal = minBound - -instance Minimal Int where minimal = minBound - -instance Minimal Int8 where minimal = minBound - -instance Minimal Int16 where minimal = minBound - -instance Minimal Int32 where minimal = minBound - -instance Minimal Int64 where minimal = minBound - -instance Minimal Word where minimal = minBound - -instance Minimal Word8 where minimal = minBound - -instance Minimal Word16 where minimal = minBound - -instance Minimal Word32 where minimal = minBound +instance Minimal (Ratio Natural) where minimal = 0 -instance Minimal Word64 where minimal = minBound +instance Minimal IntSet.IntSet where + minimal = IntSet.empty instance Prd a => Minimal (IntMap.IntMap a) where minimal = IntMap.empty @@ -566,44 +587,62 @@ instance Maximal a => Minimal (Down a) where minimal = Down maximal -------------------------------------------------------------------------------- --- Maximal -------------------------------------------------------------------------------- +instance Maximal a => Minimal (Dual a) where + minimal = Dual maximal --- | Maximal element of a partially ordered set. --- --- \( \forall x: x \le maximal \) --- --- This means that 'maximal' must be comparable to all values in /a/. --- -class Prd a => Maximal a where - maximal :: a +#define deriveMinimal(ty) \ +instance Minimal ty where { \ + minimal = minBound \ +; {-# INLINE minimal #-} \ +} -instance Maximal () where maximal = () -instance Maximal Bool where maximal = maxBound +deriveMinimal(()) +deriveMinimal(Bool) +deriveMinimal(Ordering) -instance Maximal Ordering where maximal = maxBound +deriveMinimal(Int) +deriveMinimal(Int8) +deriveMinimal(Int16) +deriveMinimal(Int32) +deriveMinimal(Int64) -instance Maximal Int where maximal = maxBound +deriveMinimal(Word) +deriveMinimal(Word8) +deriveMinimal(Word16) +deriveMinimal(Word32) +deriveMinimal(Word64) -instance Maximal Int8 where maximal = maxBound +------------------------------------------------------------------------------- +-- Maximal +------------------------------------------------------------------------------- -instance Maximal Int16 where maximal = maxBound +#define deriveMaximal(ty) \ +instance Maximal ty where { \ + maximal = maxBound \ +; {-# INLINE maximal #-} \ +} -instance Maximal Int32 where maximal = maxBound -instance Maximal Int64 where maximal = maxBound - -instance Maximal Word where maximal = maxBound +deriveMaximal(()) +deriveMaximal(Bool) +deriveMaximal(Ordering) -instance Maximal Word8 where maximal = maxBound +deriveMaximal(Int) +deriveMaximal(Int8) +deriveMaximal(Int16) +deriveMaximal(Int32) +deriveMaximal(Int64) -instance Maximal Word16 where maximal = maxBound +deriveMaximal(Word) +deriveMaximal(Word8) +deriveMaximal(Word16) +deriveMaximal(Word32) +deriveMaximal(Word64) -instance Maximal Word32 where maximal = maxBound +instance Maximal Float where maximal = pinf -instance Maximal Word64 where maximal = maxBound +instance Maximal Double where maximal = pinf instance (Maximal a, Maximal b) => Maximal (a, b) where maximal = (maximal, maximal) @@ -614,6 +653,9 @@ instance Maximal a => Maximal (Maybe a) where maximal = Just maximal +instance Minimal a => Maximal (Dual a) where + maximal = Dual minimal + instance Minimal a => Maximal (Down a) where maximal = Down minimal @@ -623,29 +665,20 @@ {-# INLINE until #-} until :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a -until pred rel f seed = go seed +until pre rel f seed = go seed where go x | x' `rel` x = x - | pred x = x + | pre x = x | otherwise = go x' where x' = f x {-# INLINE while #-} while :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a -while pred rel f seed = go seed +while pre rel f seed = go seed where go x | x' `rel` x = x - | not (pred x') = x + | not (pre x') = x | otherwise = go x' where x' = f x -{- -while' :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a -while' pred rel f seed = go seed f - where go x | x' `rel` x = id - | not (pred x') = id - | otherwise = go x' . f - where x' = f x --} - -- | Greatest (resp. least) fixed point of a monitone (resp. antitone) function. -- -- Does not check that the function is monitone (resp. antitone). @@ -655,4 +688,3 @@ {-# INLINE fixed #-} fixed :: (a -> a -> Bool) -> (a -> a) -> a -> a fixed = while (\_ -> True) - diff --git a/src/Data/Prd/Lattice.hs b/src/Data/Prd/Lattice.hs deleted file mode 100644 --- a/src/Data/Prd/Lattice.hs +++ /dev/null @@ -1,290 +0,0 @@ -{-# LANGUAGE ConstrainedClassMethods #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Safe #-} - -module Data.Prd.Lattice where - -import Data.Data (Data, Typeable) -import Data.Foldable -import Data.Function -import Data.Int as Int (Int, Int8, Int16, Int32, Int64) -import Data.Maybe -import Data.Monoid hiding (First, Last) -import Data.Ord -import Data.Prd -import Data.Semigroup (Semigroup(..)) -import Data.Semigroup.Foldable -import Data.Set (Set) -import Data.Word (Word, Word8, Word16, Word32, Word64) -import GHC.Generics (Generic, Generic1) - -import Prelude - -import qualified Data.Map as Map -import qualified Data.Set as Set -import qualified Data.IntMap as IntMap -import qualified Data.IntSet as IntSet -import qualified Data.Sequence as Seq - - -{- - -A partially ordered set is a directed-complete partial order (dcpo) if each of its directed subsets has a supremum. A subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the subset. In the literature, dcpos sometimes also appear under the label up-complete poset. - - -distributivity: A join-semilattice is distributive if for all a, b, and x with x ≤ a ∨ b there exist a' ≤ a and b' ≤ b such that x = a' ∨ b' . Distributive meet-semilattices are defined dually. These definitions are justified by the fact that any distributive join-semilattice in which binary meets exist is a distributive lattice - -morphisms: Given two join-semilattices (S, ∨) and (T, ∨), a homomorphism of (join-) semilattices is a function f: S → T such that - -f(x ∨ y) = f(x) ∨ f(y). -Hence f is just a homomorphism of the two semigroups associated with each semilattice. If S and T both include a least element 0, then f should also be a monoid homomorphism, i.e. we additionally require that - -f(0) = 0. -In the order-theoretic formulation, these conditions just state that a homomorphism of join-semilattices is a function that preserves binary joins and least elements, if such there be. The obvious dual—replacing ∧ with ∨ and 0 with 1—transforms this definition of a join-semilattice homomorphism into its meet-semilattice equivalent. - -Note that any semilattice homomorphism is necessarily monotone with respect to the associated ordering relation. - --} - ---(a ∧ b) ⊗ c = (a ⊗ c) ∧ (b ⊗ c), c ⊗ (a ∧ b) = (c ⊗ a) ∧ (c ⊗ b) --- (meet x y) /\ z = x /\ z `meet` y /\ z - --- idempotent sup dioids ? complete (join-semi)lattices derived from <~? ---connr-distributivity (the group (E\{ε}, ⊗) is therefore reticulated) --- --- mon zero = const Nothing - --- bounded meet semilattice --- need the codistributive property & absorbtion & commutativity - -{- -If E is a distributive lattice, then (E, ∨, ∧) is a doublyidempotent dioid, the order relation (canonical) of the dioid being defined as: -a ≤ b ⇔ a ∨ b = b. -Conversely, let (E, ⊕, ⊗) be a doubly-idempotent dioid for which ≤, the canonical -order relation relative to the law ⊕ is also a canonical order relation for ⊗: -x ≤ y ⇔ x ⊗ y = x. -Then E is a distributive lattice. --} - -infixr 6 /\ -infixr 5 \/ - --- | Lattices. --- --- A lattice is a partially ordered set in which every two elements have a unique join --- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum). --- --- See and . --- --- --- /Laws/ --- --- @ --- x '\/' 'maximal' ≡ x --- @ --- --- /Corollary/ --- --- @ --- x '\/' 'maximal' --- ≡⟨ identity ⟩ --- (x '\/' 'maximal') '/\' 'maximal' --- ≡⟨ absorption ⟩ --- 'maximal' --- @ --- --- @ --- x '\/' 'minimal' ≡ x --- @ --- --- /Corollary/ --- --- @ --- x '/\' 'minimal' --- ≡⟨ identity ⟩ --- (x '/\' 'minimal') '\/' 'minimal' --- ≡⟨ absorption ⟩ --- 'minimal' --- @ --- --- /Associativity/ --- --- @ --- x '\/' (y '\/' z) ≡ (x '\/' y) '\/' z --- x '/\' (y '/\' z) ≡ (x '/\' y) '/\' z --- @ --- --- /Commutativity/ --- --- @ --- x '\/' y ≡ y '\/' x --- x '/\' y ≡ y '/\' x --- @ --- --- /Idempotency/ --- --- @ --- x '\/' x ≡ x --- x '/\' x ≡ x --- @ --- --- /Absorption/ --- --- @ --- (x '\/' y) '/\' y ≡ y --- (x '/\' y) '\/' y ≡ y --- @ --- -class Prd a => Lattice a where - - (\/) :: a -> a -> a - - (/\) :: a -> a -> a - - -- | Lattice morphism. - fromSubset :: Minimal a => Set a -> a - fromSubset = join - --- | The partial ordering induced by the join-semilattice structure -joinLeq :: Lattice a => a -> a -> Bool -joinLeq x y = x \/ y =~ y - -meetLeq :: Lattice a => a -> a -> Bool -meetLeq x y = x /\ y =~ x - -join :: (Minimal a, Lattice a, Foldable f) => f a -> a -join = foldr' (\/) minimal - -meet :: (Maximal a, Lattice a, Foldable f) => f a -> a -meet = foldr' (/\) maximal - --- | The join of at a list of join-semilattice elements (of length at least one) -join1 :: (Lattice a, Foldable1 f) => f a -> a -join1 = unJoin . foldMap1 Join - --- --- | The meet of at a list of meet-semilattice elements (of length at least one) -meet1 :: (Lattice a, Foldable1 f) => f a -> a -meet1 = unMeet . foldMap1 Meet - --- | Birkhoff's self-dual ternary median operation. --- --- @ median x x y ≡ x @ --- --- @ median x y z ≡ median z x y @ --- --- @ median x y z ≡ median x z y @ --- --- @ median (median x w y) w z ≡ median x w (median y w z) @ --- -median :: Lattice a => a -> a -> a -> a -median x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x) - ---------------------------------------------------------------------- --- Instances ---------------------------------------------------------------------- - -instance Lattice () where - _ \/ _ = () - _ /\ _ = () - -instance (Lattice a, Lattice b) => Lattice (a, b) where - (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2) - (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) - -instance (Lattice a, Lattice b) => Lattice (Either a b) where - Right x \/ Right y = Right $ x \/ y - x@Right{} \/ _ = x - Left x \/ Left y = Left $ x \/ y - x@Left{} \/ y = y - - Right x /\ Right y = Right $ x /\ y - x@Right{} /\ y = y - Left x /\ Left y = Left $ x /\ y - x@Left{} /\ _ = x - -instance Lattice a => Lattice (Maybe a) where - Just x \/ Just y = Just $ x \/ y - x@Just{} \/ _ = x - Nothing \/ Nothing = Nothing - Nothing \/ y = y - - Just x /\ Just y = Just $ x /\ y - x@Just{} /\ y = y - Nothing /\ _ = Nothing - -instance Lattice Bool where - (\/) = (||) - (/\) = (&&) - -instance Lattice All where - All a \/ All b = All $ a \/ b - All a /\ All b = All $ a /\ b - -instance Minimal All where - minimal = All False - -instance Maximal All where - maximal = All True - -instance Lattice Any where - Any a \/ Any b = Any $ a \/ b - Any a /\ Any b = Any $ a /\ b - -instance Minimal Any where - minimal = Any False - -instance Maximal Any where - maximal = Any True - -instance Lattice a => Lattice (Down a) where - Down x \/ Down y = Down (x /\ y) - Down x /\ Down y = Down (x \/ y) - -instance Ord a => Lattice (Ordered a) where - Ordered x \/ Ordered y = Ordered (max x y) - Ordered x /\ Ordered y = Ordered (min x y) - -instance Ord a => Lattice (Set.Set a) where - (\/) = Set.union - (/\) = Set.intersection - -instance (Ord k, Lattice a) => Lattice (Map.Map k a) where - (\/) = Map.unionWith (\/) - (/\) = Map.intersectionWith (/\) - -instance Lattice a => Lattice (IntMap.IntMap a) where - (\/) = IntMap.unionWith (\/) - (/\) = IntMap.intersectionWith (/\) - -instance Lattice IntSet.IntSet where - (\/) = IntSet.union - (/\) = IntSet.intersection - ---------------------------------------------------------------------- --- Newtypes ---------------------------------------------------------------------- - -newtype Join a = Join { unJoin :: a } - deriving (Eq, Ord, Show, Typeable, Data, Generic) - -instance Lattice a => Semigroup (Join a) where - Join a <> Join b = Join (a \/ b) - -instance (Lattice a, Minimal a) => Monoid (Join a) where - mempty = Join minimal - Join a `mappend` Join b = Join (a \/ b) - -instance (Eq a, Lattice a) => Prd (Join a) where - (Join a) <~ (Join b) = joinLeq a b - -newtype Meet a = Meet { unMeet :: a } - deriving (Eq, Ord, Show, Typeable, Data, Generic) - -instance Lattice a => Semigroup (Meet a) where - Meet a <> Meet b = Meet (a /\ b) - -instance (Lattice a, Maximal a) => Monoid (Meet a) where - mempty = Meet maximal - Meet a `mappend` Meet b = Meet (a /\ b) diff --git a/src/Data/Prd/Nan.hs b/src/Data/Prd/Nan.hs --- a/src/Data/Prd/Nan.hs +++ b/src/Data/Prd/Nan.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} @@ -6,54 +5,55 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE Rank2Types #-} module Data.Prd.Nan where import Control.Applicative -import Data.Data (Data, Typeable) import Data.Prd import Data.Connection +import Data.Semiring +import Data.Semifield import GHC.Generics (Generic, Generic1) --- A type with an additional element allowing for the possibility of undefined values. +import Prelude hiding (Ord(..), Num(..), Fractional(..)) + +-- | A type with an additional incomparable element allowing for the possibility of undefined values. -- Isomorphic to /Maybe a/ but with a different 'Prd' instance. -data Nan a = Nan | Def a - deriving ( Eq, Ord, Show, Data, Typeable, Generic, Generic1, Functor, Foldable, Traversable) +data Nan a = Nan | Def a deriving ( Show, Generic, Generic1, Functor, Foldable, Traversable) +{- + +instance Field a => Field (Nan a) where + +u + Nan = Nan + u = Nan − Nan = Nan +u · Nan = Nan · u = Nan Nan−1 = Nan +Nan u ⇔ u = Nan u Nan ⇔ u = Nan +-} + nan :: b -> (a -> b) -> Nan a -> b nan _ f (Def y) = f y nan x _ Nan = x -defined :: Nan a -> Bool -defined Nan = False -defined _ = True +nan' :: Semifield b => (a -> b) -> Nan a -> b +nan' f = nan anan f +isDef :: Nan a -> Bool +isDef Nan = False +isDef _ = True + mapNan :: (a -> b) -> Nan a -> Nan b mapNan f = nan Nan $ Def . f -maybeNan :: (forall a. a -> a) -> Maybe a -> Nan a -maybeNan _ Nothing = Nan -maybeNan f (Just x) = Def $ f x - -nanMaybe :: (forall a. a -> a) -> Nan a -> Maybe a -nanMaybe _ Nan = Nothing -nanMaybe f (Def x) = Just $ f x - -eitherNan :: Either a b -> Nan b -eitherNan = either (const Nan) Def - -nanEither :: a -> Nan b -> Either a b -nanEither x = nan (Left x) Right +joinNan :: Nan (Nan a) -> Nan a +joinNan Nan = Nan +joinNan (Def Nan) = Nan +joinNan (Def (Def a)) = Def a +-- collectNan = joinNan . liftNan id -liftNan :: (Prd a, Fractional a) => (a -> b) -> a -> Nan b -liftNan f x | x =~ (0/0) = Nan +liftNan :: Prd a => Semifield a => (a -> b) -> a -> Nan b +liftNan f x | x =~ anan = Nan | otherwise = Def (f x) -liftNan' :: RealFloat a => (a -> b) -> a -> Nan b -liftNan' f x | isNaN x = Nan - | otherwise = Def (f x) - -- Lift all exceptional values liftAll :: (RealFloat a, Prd a, Bound b) => (a -> b) -> a -> Nan b liftAll f x | isNaN x = Nan @@ -62,92 +62,65 @@ | otherwise = Def (f x) isInf :: (RealFloat a, Prd a) => a -> Bool -isInf x = isInfinite x && gt x 0 +isInf x = isInfinite x && x > 0 -floatOrdering :: (RealFloat a, Prd a) => Trip a (Nan Ordering) -floatOrdering = Trip f g h where +defnan :: Prd a => Prd b => Conn a b -> Conn (Nan a) (Nan b) +defnan (Conn f g) = Conn (fmap f) (fmap g) - g (Def GT) = 1/0 - g (Def LT) = - 1/0 - g (Def EQ) = 0 - g Nan = 0/0 +defnan' :: Prd a => Prd b => Trip a b -> Trip (Nan a) (Nan b) +defnan' (Trip f g h) = Trip (fmap f) (fmap g) (fmap h) + +--nanfld :: Prd a => Field a => Trip (Nan a) a +-- Field a => Field (Nan a) +-- /Caution/ this is only legal if (Nan a) has no nans. +{- +fldnan :: Prd a => Field a => Trip a (Nan a) +fldnan = Trip f g f where + f a = if a =~ zero / zero then Nan else Def a + g = nan (zero / zero) id +-} + +fldord :: Prd a => Field a => Trip a (Nan Ordering) +fldord = Trip f g h where + g (Def GT) = pinf + g (Def LT) = ninf + g (Def EQ) = zero + g Nan = anan - f x | isNaN x = Nan - f x | isInf (-x) = Def LT - f x | x <~ 0 = Def EQ - f x | otherwise = Def GT + f x | x =~ anan = Nan + | x =~ ninf = Def LT + | x <= zero = Def EQ + | otherwise = Def GT - h x | isNaN x = Nan - h x | isInf x = Def GT - h x | x >~ 0 = Def EQ - h x | otherwise = Def LT + h x | x =~ anan = Nan + | x =~ pinf = Def GT + | x >= zero = Def EQ + | otherwise = Def LT instance Prd a => Prd (Nan a) where - Nan <~ Nan = True - _ <~ Nan = False - Nan <~ _ = False - Def a <~ Def b = a <~ b + Nan <= Nan = True + _ <= Nan = False + Nan <= _ = False + Def a <= Def b = a <= b instance Applicative Nan where pure = Def Nan <*> _ = Nan Def f <*> x = f <$> x -instance Num a => Num (Nan a) where - negate = fmap negate - (+) = liftA2 (+) - (*) = liftA2 (*) - fromInteger = pure . fromInteger - abs = fmap abs - signum = fmap signum - -nanflt :: Prd a => Fractional a => Conn (Nan a) a -nanflt = Conn (nan (0/0) id) $ \y -> if y =~ (0/0) then Nan else Def y - -def :: Prd a => Prd b => Conn a b -> Conn (Nan a) (Nan b) -def conn = Conn f g where - Conn f' g' = right conn - f = eitherNan . f' . nanEither () - g = eitherNan . g' . nanEither () - -{- -floatOrdering :: Trip Float (Nan Ordering) -floatOrdering = Trip f g h where - h x | isNaN x = Nan - h x | posinf x = Def GT - h x | finite x && x >~ 0 = Def EQ - h x | otherwise = Def LT - - g (Def GT) = maxBound - g (Def LT) = minBound - g (Def EQ) = 0 - g Nan = aNan - - f x | isNaN x = Nan - f x | neginf x = Def LT - f x | finite x && x <~ 0 = Def EQ - f x | otherwise = Def GT - - -_Def' :: Prd a => Prd b => Trip a b -> Trip (Nan a) (Nan b) -_Def' trip = Trip f g h where - Trip f' g' h' = _R' trip - f = eitherNan . f' . nanEither () - g = eitherNan . g' . nanEither () - h = eitherNan . h' . nanEither () - - -instance Semigroup a => Semigroup (Nan a) where -instance Semiring a => Semiring (Nan a) where -instance Semifield a => Semifield (Nan a) where +instance (Additive-Semigroup) a => Semigroup (Additive (Nan a)) where + Additive a <> Additive b = Additive $ liftA2 (+) a b -instance Group a => Group (Nan a) where -instance Ring a => Ring (Nan a) where +-- MinPlus Dioid +instance (Additive-Monoid) a => Monoid (Additive (Nan a)) where + mempty = Additive $ pure zero -instance Field a => Field (Nan a) where +instance (Multiplicative-Semigroup) a => Semigroup (Multiplicative (Nan a)) where + Multiplicative a <> Multiplicative b = Multiplicative $ liftA2 (*) a b -u + Nan = Nan + u = Nan − Nan = Nan -u · Nan = Nan · u = Nan Nan−1 = Nan -Nan u ⇔ u = Nan u Nan ⇔ u = Nan --} +-- MinPlus Dioid +instance (Multiplicative-Monoid) a => Monoid (Multiplicative (Nan a)) where + mempty = Multiplicative $ pure one +-- Presemiring with a absorbing element. +instance Presemiring a => Presemiring (Nan a) diff --git a/src/Data/Prd/Property.hs b/src/Data/Prd/Property.hs --- a/src/Data/Prd/Property.hs +++ b/src/Data/Prd/Property.hs @@ -1,11 +1,11 @@ -- | See . module Data.Prd.Property ( + -- * Typeclass consistency + consistent -- * Equivalence relations - symmetric - , coreflexive + , symmetric , reflexive_eq , transitive_eq - -- * Partial orders -- ** Non-strict partial orders , antisymmetric @@ -26,34 +26,64 @@ ) where import Data.Prd -import Data.Prd.Lattice -import Test.Util +import Test.Logic import Prelude hiding (Ord(..)) import qualified Prelude as P import qualified Test.Relation as R --- | \( \forall a, b: (a \eq b) \Leftrightarrow (b \eq a) \) --- --- '=~' is a symmetric relation. +-- | Check that 'Prd' methods are internally consistent. -- -- This is a required property. -- -symmetric :: Prd r => r -> r -> Bool -symmetric = R.symmetric (=~) +consistent :: Prd r => r -> r -> Bool +consistent x y = + ((x <= y) == le x y) && + ((x >= y) == ge x y) && + ((x < y) == lt x y) && + ((x > y) == gt x y) && + ((x ?~ y) == cp x y) && + ((x =~ y) == eq x y) && + ((x /~ y) == ne x y) && + ((x ~~ y) == sm x y) && + ((x !~ y) == ns x y) && + (pcompare x y == pcmp x y) --- | \( \forall x, y: x \eq y \Leftrightarrow x == y \) --- --- '=~' is a coreflexive relation. + where + le x1 y1 = maybe False (P.<= EQ) $ pcompare x1 y1 + + ge x1 y1 = maybe False (P.>= EQ) $ pcompare x1 y1 + + lt x1 y1 = maybe False (P.< EQ) $ pcompare x1 y1 + + gt x1 y1 = maybe False (P.> EQ) $ pcompare x1 y1 + + cp x1 y1 = maybe False (const True) $ pcompare x1 y1 + + eq x1 y1 = maybe False (== EQ) $ pcompare x1 y1 + + ne x1 y1 = not $ x1 =~ y1 + + sm x1 y1 = not (x1 < y1) && not (x1 > y1) + + ns x1 y1 = not $ x1 ~~ y1 + + pcmp x1 y1 + | x1 <= y1 = Just $ if y1 <= x1 then EQ else LT + | y1 <= x1 = Just GT + | otherwise = Nothing + + +-- | \( \forall a, b: (a = b) \Leftrightarrow (b = a) \) -- --- See . +-- '=~' is a symmetric relation. -- -- This is a required property. -- -coreflexive :: (Eq r, Prd r) => r -> r -> Bool -coreflexive x y = x =~ y ==> x == y +symmetric :: Prd r => r -> r -> Bool +symmetric = R.symmetric (=~) --- | \( \forall a: (a \eq a) \) +-- | \( \forall a: (a = a) \) -- -- '=~' is a reflexive relation. -- @@ -62,7 +92,7 @@ reflexive_eq :: Prd r => r -> Bool reflexive_eq = R.reflexive (=~) --- | \( \forall a, b, c: ((a \eq b) \wedge (b \eq c)) \Rightarrow (a \eq c) \) +-- | \( \forall a, b, c: ((a = b) \wedge (b = c)) \Rightarrow (a = c) \) -- -- '=~' is a transitive relation. -- @@ -71,39 +101,39 @@ transitive_eq :: Prd r => r -> r -> r -> Bool transitive_eq = R.transitive (=~) --- | \( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a \eq b \) +-- | \( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a = b \) -- --- '<~' is an antisymmetric relation. +-- '<=' is an antisymmetric relation. -- -- This is a required property. -- antisymmetric :: Prd r => r -> r -> Bool -antisymmetric = R.antisymmetric_on (=~) (<~) +antisymmetric = R.antisymmetric_on (=~) (<=) -- | \( \forall a: (a \leq a) \) -- --- '<~' is a reflexive relation. +-- '<=' is a reflexive relation. -- -- This is a required property. -- reflexive_le :: Prd r => r -> Bool -reflexive_le = R.reflexive (<~) +reflexive_le = R.reflexive (<=) -- | \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \) -- --- '<~' is an transitive relation. +-- '<=' is an transitive relation. -- -- This is a required property. -- transitive_le :: Prd r => r -> r -> r -> Bool -transitive_le = R.transitive (<~) +transitive_le = R.transitive (<=) -- | \( \forall a, b: ((a \leq b) \vee (b \leq a)) \) -- --- '<~' is a connex relation. +-- '<=' is a connex relation. -- connex :: Prd r => r -> r -> Bool -connex = R.connex (<~) +connex = R.connex (<=) -- | \( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \) -- @@ -112,7 +142,7 @@ -- This is a required property. -- asymmetric :: Eq r => Prd r => r -> r -> Bool -asymmetric = R.asymmetric lt +asymmetric = R.asymmetric (<) -- | \( \forall a: \neg (a \lt a) \) -- @@ -121,7 +151,7 @@ -- This is a required property. -- irreflexive_lt :: Eq r => Prd r => r -> Bool -irreflexive_lt = R.irreflexive lt +irreflexive_lt = R.irreflexive (<) -- | \( \forall a, b, c: ((a \lt b) \wedge (b \lt c)) \Rightarrow (a \lt c) \) -- @@ -130,34 +160,34 @@ -- This is a required property. -- transitive_lt :: Eq r => Prd r => r -> r -> r -> Bool -transitive_lt = R.transitive lt +transitive_lt = R.transitive (<) --- | \( \forall a, b: \neg (a \eq b) \Rightarrow ((a \lt b) \vee (b \lt a)) \) +-- | \( \forall a, b: \neg (a = b) \Rightarrow ((a \lt b) \vee (b \lt a)) \) -- -- 'lt' is a semiconnex relation. -- semiconnex :: Eq r => Prd r => r -> r -> Bool -semiconnex = R.semiconnex_on (=~) lt +semiconnex = R.semiconnex_on (=~) (<) --- | \( \forall a, b, c: ((a \lt b) \vee (a \eq b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a \eq b) \wedge (b \lt a)) \) +-- | \( \forall a, b, c: ((a \lt b) \vee (a = b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a = b) \wedge (b \lt a)) \) -- --- In other words, exactly one of \(a \lt b\), \(a \eq b\), or \(b \lt a\) holds. +-- In other words, exactly one of \(a \lt b\), \(a = b\), or \(b \lt a\) holds. -- -- If 'lt' is a trichotomous relation then the set is totally ordered. -- trichotomous :: Eq r => Prd r => r -> r -> Bool -trichotomous = R.trichotomous_on (=~) lt +trichotomous = R.trichotomous_on (=~) (<) -- | \( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \) -- -- A semiorder does not allow 2-2 chains. -- chain_22 :: Eq r => Prd r => r -> r -> r -> r -> Bool -chain_22 x y z w = x `lt` y && y ~~ z && z `lt` w ==> x `lt` w +chain_22 x y z w = x < y && y ~~ z && z < w ==> x < w -- \( \forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w) \) (3-1 chain) -- -- A semiorder does not allow 3-1 chains. -- chain_31 :: Eq r => Prd r => r -> r -> r -> r -> Bool -chain_31 x y z w = x `lt` y && y `lt` z && y ~~ w ==> not (x ~~ w && z ~~ w) +chain_31 x y z w = x < y && y < z && y ~~ w ==> not (x ~~ w && z ~~ w) diff --git a/src/Data/Semigroup/Join.hs b/src/Data/Semigroup/Join.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup/Join.hs @@ -0,0 +1,272 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Data.Semigroup.Join where + +import Control.Applicative +import Data.Bool +import Data.Maybe +import Data.Either +import Data.Prd +import Data.Semigroup +import Data.Semigroup.Additive +import Data.Semigroup.Meet +import GHC.Generics (Generic) + +import Numeric.Natural +import Data.Word +import Data.Int +import Data.Fixed + +import Prelude ( Eq(..), Ord(..), Show, Ordering(..), Applicative(..), Functor(..), Monoid(..), Semigroup(..), (.), ($), (<$>), Integer) +import qualified Prelude as P + +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.IntMap as IntMap +import qualified Data.IntSet as IntSet + +infixr 5 ∨ + +-- | Join operation on a semilattice. +-- +-- >>> (> (0::Int)) ∧ ((< 10) ∨ (== 15)) $ 10 +-- False +-- +-- >>> IntSet.fromList [1..5] ∧ IntSet.fromList [2..5] +-- fromList [2,3,4,5] +(∨) :: (Join-Semigroup) a => a -> a -> a +a ∨ b = unJoin (Join a <> Join b) +{-# INLINE (∨) #-} + +bottom :: (Join-Monoid) a => a +bottom = unJoin mempty +{-# INLINE bottom #-} + +type JoinSemilattice a = (Prd a, (Join-Semigroup) a) + +-- | The partial ordering induced by the join-semilattice structure. +-- +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'joinLeq' x y ≡ x '<=' y @ +-- +joinLeq :: Eq a => (Join-Semigroup) a => a -> a -> Bool +joinLeq x y = x ∨ y == y + +-- | The partial ordering induced by the join-semilattice structure. +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'joinGeq' x y ≡ x '>=' y @ +-- +joinGeq :: Eq a => (Join-Semigroup) a => a -> a -> Bool +joinGeq x y = x ∨ y == x + +-- | Partial version of 'Data.Ord.compare'. +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'pcompareJoin' x y ≡ 'pcompare' x y @ +-- +pcompareJoin :: Eq a => (Join-Semigroup) a => a -> a -> Maybe Ordering +pcompareJoin x y + | x == y = Just EQ + | x ∨ y == y && x /= y = Just LT + | x ∨ y == x && x /= y = Just GT + | otherwise = Nothing + +-- | A commutative 'Semigroup' under '∨'. +newtype Join a = Join { unJoin :: a } deriving (Eq, Generic, Ord, Show, Functor) + +instance Applicative Join where + pure = Join + Join f <*> Join a = Join (f a) + +-- >>> Down True ∨ Down False +-- Down False +instance (Meet-Semigroup) a => Semigroup (Join (Down a)) where + (<>) = liftA2 . liftA2 $ (∧) + +-- >>> bottom :: Down Bool +-- Down True +instance (Meet-Monoid) a => Monoid (Join (Down a)) where + mempty = pure . pure $ top + +-- >>> Down True ∧ Down False +-- Down True +instance (Join-Semigroup) a => Semigroup (Meet (Down a)) where + (<>) = liftA2 . liftA2 $ (∨) + +-- >>> top :: Down Bool +-- Down False +instance (Join-Monoid) a => Monoid (Meet (Down a)) where + mempty = pure . pure $ bottom + + +instance Semigroup (Max a) => Semigroup (Join (Max a)) where + (<>) = liftA2 (<>) + +instance (Join-Semigroup) (Max a) => Semigroup (Additive (Max a)) where + (<>) = liftA2 (∨) + +instance (Join-Monoid) (Max a) => Monoid (Additive (Max a)) where + mempty = pure bottom + +-- workaround for poorly specified entailment: instance (Ord a, Bounded a) => Monoid (Max a) +instance (Minimal a, Semigroup (Max a)) => Monoid (Join (Max a)) where + mempty = pure $ Max minimal + +--------------------------------------------------------------------- +-- Idempotent and selective instances +--------------------------------------------------------------------- + +{- +instance Ord a => Semigroup (Join (Down a)) where + (<>) = liftA2 . liftA2 $ (∨) + +instance (Join-Monoid) a => Monoid (Join (Down a)) where + mempty = pure . pure $ bottom +-} + + +{- +instance (Join-Semigroup) a => Semigroup (Join (Dual a)) where + (<>) = liftA2 . liftA2 $ flip (∨) + +instance (Join-Monoid) a => Monoid (Join (Dual a)) where + mempty = pure . pure $ bottom + + + +instance (Join-Semigroup) a => Semigroup (Join (Down a)) where + (<>) = liftA2 . liftA2 $ (∨) + +instance (Join-Monoid) a => Monoid (Join (Down a)) where + --Join (Down a) <> Join (Down b) + mempty = pure . pure $ bottom + +instance Semigroup (Max a) => Semigroup (Join (Max a)) where + (<>) = liftA2 (<>) + +-- MinPlus Predioid +-- >>> Min 1 `mul` Min 2 :: Min Int +-- Min {getMin = 3} +instance (Join-Semigroup) a => Semigroup (Multiplicative (Min a)) where + Multiplicative a <> Multiplicative b = Multiplicative $ liftA2 (∨) a b + +-- MinPlus Dioid +instance (Join-Monoid) a => Monoid (Multiplicative (Min a)) where + mempty = Multiplicative $ pure bottom +-} + + +--instance ((Join-Semigroup) a, Minimal a) => Monoid (Join a) where +-- mempty = Join minimal + +-- instance (Meet-Monoid) (Down a) => Monoid (Meet (Down a)) where mempty = Down <$> mempty + +instance ((Join-Semigroup) a, (Join-Semigroup) b) => Semigroup (Join (a, b)) where + Join (x1, y1) <> Join (x2, y2) = Join (x1 ∨ x2, y1 ∨ y2) + +instance (Join-Semigroup) a => Semigroup (Join (Maybe a)) where + Join (Just x) <> Join (Just y) = Join . Just $ x ∨ y + Join (x@Just{}) <> _ = Join x + Join Nothing <> y = y + +instance (Join-Semigroup) a => Monoid (Join (Maybe a)) where + mempty = Join Nothing + +instance ((Join-Semigroup) a, (Join-Semigroup) b) => Semigroup (Join (Either a b)) where + Join (Right x) <> Join (Right y) = Join . Right $ x ∨ y + + Join(x@Right{}) <> _ = Join x + Join (Left x) <> Join (Left y) = Join . Left $ x ∨ y + Join (Left _) <> y = y + +instance Ord a => Semigroup (Join (Set.Set a)) where + (<>) = liftA2 Set.union + +instance (Ord k, (Join-Semigroup) a) => Semigroup (Join (Map.Map k a)) where + (<>) = liftA2 (Map.unionWith (∨)) + +instance (Join-Semigroup) a => Semigroup (Join (IntMap.IntMap a)) where + (<>) = liftA2 (IntMap.unionWith (∨)) + +instance Semigroup (Join IntSet.IntSet) where + (<>) = liftA2 IntSet.union + +instance Monoid (Join IntSet.IntSet) where + mempty = Join IntSet.empty + +instance (Join-Semigroup) a => Monoid (Join (IntMap.IntMap a)) where + mempty = Join IntMap.empty + +instance Ord a => Monoid (Join (Set.Set a)) where + mempty = Join Set.empty + +instance (Ord k, (Join-Semigroup) a) => Monoid (Join (Map.Map k a)) where + mempty = Join Map.empty + + +#define deriveJoinSemigroup(ty) \ +instance Semigroup (Join ty) where { \ + a <> b = (P.max) <$> a <*> b \ +; {-# INLINE (<>) #-} \ +} + +deriveJoinSemigroup(()) +deriveJoinSemigroup(Bool) + +deriveJoinSemigroup(Int) +deriveJoinSemigroup(Int8) +deriveJoinSemigroup(Int16) +deriveJoinSemigroup(Int32) +deriveJoinSemigroup(Int64) +deriveJoinSemigroup(Integer) + +deriveJoinSemigroup(Word) +deriveJoinSemigroup(Word8) +deriveJoinSemigroup(Word16) +deriveJoinSemigroup(Word32) +deriveJoinSemigroup(Word64) +deriveJoinSemigroup(Natural) + +deriveJoinSemigroup(Uni) +deriveJoinSemigroup(Deci) +deriveJoinSemigroup(Centi) +deriveJoinSemigroup(Milli) +deriveJoinSemigroup(Micro) +deriveJoinSemigroup(Nano) +deriveJoinSemigroup(Pico) + + +#define deriveJoinMonoid(ty) \ +instance Monoid (Join ty) where { \ + mempty = pure minimal \ +; {-# INLINE mempty #-} \ +} + +deriveJoinMonoid(()) +deriveJoinMonoid(Bool) + +deriveJoinMonoid(Int) +deriveJoinMonoid(Int8) +deriveJoinMonoid(Int16) +deriveJoinMonoid(Int32) +deriveJoinMonoid(Int64) + +deriveJoinMonoid(Word) +deriveJoinMonoid(Word8) +deriveJoinMonoid(Word16) +deriveJoinMonoid(Word32) +deriveJoinMonoid(Word64) +deriveJoinMonoid(Natural) diff --git a/src/Data/Semigroup/Meet.hs b/src/Data/Semigroup/Meet.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup/Meet.hs @@ -0,0 +1,267 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Data.Semigroup.Meet ( + type (-) + , module Data.Semigroup.Meet +) where + +import Control.Applicative +import Data.Bool +import Data.Either +import Data.Fixed +import Data.Int +import Data.Maybe +import Data.Prd +import Data.Ratio +import Data.Semigroup +import Data.Semigroup.Additive +import Data.Semigroup.Multiplicative +import Data.Word +import GHC.Generics (Generic) +import Numeric.Natural +import Prelude + ( Eq(..), Ord, Show, Ordering(..), Applicative(..), Functor(..) + , Monoid(..), Semigroup(..), (.), ($), (<$>), Integer) + +import qualified Data.IntMap as IntMap +import qualified Data.IntSet as IntSet +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Prelude as P + +infixr 6 ∧ + +-- | Meet operation on a semilattice. +-- +-- >>> (> (0::Int)) ∧ ((< 10) ∨ (== 15)) $ 15 +-- True +-- +(∧) :: (Meet-Semigroup) a => a -> a -> a +a ∧ b = unMeet (Meet a <> Meet b) +{-# INLINE (∧) #-} + +top :: (Meet-Monoid) a => a +top = unMeet mempty +{-# INLINE top #-} + +-- | The partial ordering induced by the meet-semilattice structure. +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'meetLeq' x y ≡ x '<=' y @ +-- +meetLeq :: Eq a => (Meet-Semigroup) a => a -> a -> Bool +meetLeq x y = x ∧ y == x + +-- | The partial ordering induced by the meet-semilattice structure. +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'meetGeq' x y ≡ x '>=' y @ +-- +meetGeq :: Eq a => (Meet-Semigroup) a => a -> a -> Bool +meetGeq x y = x ∧ y == y + +-- | Partial version of 'Data.Ord.compare'. +-- +-- Normally when /a/ implements 'Prd' we should have: +-- @ 'pcompareJoin' x y ≡ 'pcompare' x y @ +-- +pcompareMeet :: Eq a => (Meet-Semigroup) a => a -> a -> Maybe Ordering +pcompareMeet x y + | x == y = Just EQ + | x ∧ y == x && x /= y = Just LT + | x ∧ y == y && x /= y = Just GT + | otherwise = Nothing + +type MeetSemilattice a = (Prd a, (Meet-Semigroup) a) + +newtype Meet a = Meet { unMeet :: a } deriving (Eq, Generic, Ord, Show, Functor) + +instance Applicative Meet where + pure = Meet + Meet f <*> Meet a = Meet (f a) + +-- >>> Min 1 ∧ Min 2 :: Min Int +-- Min {getMin = 1} +instance Semigroup (Min a) => Semigroup (Meet (Min a)) where + (<>) = liftA2 (<>) + +instance (Meet-Semigroup) (Min a) => Semigroup (Additive (Min a)) where + (<>) = liftA2 (∧) + +instance (Meet-Monoid) (Min a) => Monoid (Additive (Min a)) where + mempty = pure top + +-- workaround for poorly specified entailment: instance (Ord a, Bounded a) => Monoid (Min a) +-- >>> zero :: Min Natural +-- Min {getMin = 0} +instance (Maximal a, Semigroup (Min a)) => Monoid (Meet (Min a)) where + mempty = pure $ Min maximal + +--------------------------------------------------------------------- +-- Semigroup Instances +--------------------------------------------------------------------- + +--instance ((Meet-Semigroup) a, Maximal a) => Monoid (Meet a) where +-- mempty = Meet maximal + + +-- MaxTimes Predioid + +instance (Meet-Semigroup) a => Semigroup (Meet (Max a)) where + Meet a <> Meet b = Meet $ liftA2 (∧) a b + +-- MaxTimes Dioid +instance (Meet-Monoid) a => Monoid (Meet (Max a)) where + mempty = Meet $ pure top + +instance ((Meet-Semigroup) a, (Meet-Semigroup) b) => Semigroup (Meet (a, b)) where + Meet (x1, y1) <> Meet (x2, y2) = Meet (x1 ∧ x2, y1 ∧ y2) + +instance (Meet-Semigroup) b => Semigroup (Meet (a -> b)) where + (<>) = liftA2 . liftA2 $ (∧) + {-# INLINE (<>) #-} + +instance (Meet-Monoid) b => Monoid (Meet (a -> b)) where + mempty = pure . pure $ top + +instance (Meet-Semigroup) a => Semigroup (Meet (Maybe a)) where + Meet Nothing <> _ = Meet Nothing + Meet (Just{}) <> Meet Nothing = Meet Nothing + Meet (Just x) <> Meet (Just y) = Meet . Just $ x ∧ y + + -- Mul a <> Mul b = Mul $ liftA2 (∧) a b + +instance (Meet-Monoid) a => Monoid (Meet (Maybe a)) where + mempty = Meet $ pure top + +instance ((Meet-Semigroup) a, (Meet-Semigroup) b) => Semigroup (Meet (Either a b)) where + Meet (Right x) <> Meet (Right y) = Meet . Right $ x ∧ y + Meet (Right{}) <> y = y + Meet (Left x) <> Meet (Left y) = Meet . Left $ x ∧ y + Meet (x@Left{}) <> _ = Meet x + +instance Ord a => Semigroup (Meet (Set.Set a)) where + (<>) = liftA2 Set.intersection + +instance (Ord k, (Meet-Semigroup) a) => Semigroup (Meet (Map.Map k a)) where + (<>) = liftA2 (Map.intersectionWith (∧)) + +instance (Meet-Semigroup) a => Semigroup (Meet (IntMap.IntMap a)) where + (<>) = liftA2 (IntMap.intersectionWith (∧)) + +instance Semigroup (Meet IntSet.IntSet) where + (<>) = liftA2 IntSet.intersection + +{- +instance (Ord k, (Meet-Monoid) k, (Meet-Monoid) a) => Monoid (Meet (Map.Map k a)) where + mempty = Meet $ Map.singleton top top + +instance (Meet-Monoid) a => Monoid (Meet (IntMap.IntMap a)) where + mempty = Meet $ IntMap.singleton 0 top --TODO check +-} + +{- + + +instance Monoid a => Semiring (Seq.Seq a) where + (*) = liftA2 (<>) + {-# INLINE (*) #-} + + fromBoolean = fromBooleanDef $ Seq.singleton mempty + +instance (Ord k, Monoid k, Monoid a) => Semiring (Map.Map k a) where + xs * ys = foldMap (flip Map.map xs . (<>)) ys + {-# INLINE (*) #-} + + fromBoolean = fromBooleanDef $ Map.singleton mempty mempty + +instance Monoid a => Semiring (IntMap.IntMap a) where + xs * ys = foldMap (flip IntMap.map xs . (<>)) ys + {-# INLINE (*) #-} + + fromBoolean = fromBooleanDef $ IntMap.singleton 0 mempty +-} + +{- +instance Semigroup (Meet ()) where + _ <> _ = pure () + {-# INLINE (<>) #-} + +instance Monoid (Meet ()) where + mempty = pure () + {-# INLINE mempty #-} + +instance Semigroup (Meet Bool) where + a <> b = (P.&&) <$> a <*> b + {-# INLINE (<>) #-} + +instance Monoid (Meet Bool) where + mempty = pure True + {-# INLINE mempty #-} +-} + +#define deriveMeetSemigroup(ty) \ +instance Semigroup (Meet ty) where { \ + a <> b = (P.min) <$> a <*> b \ +; {-# INLINE (<>) #-} \ +} + +deriveMeetSemigroup(()) +deriveMeetSemigroup(Bool) + +deriveMeetSemigroup(Int) +deriveMeetSemigroup(Int8) +deriveMeetSemigroup(Int16) +deriveMeetSemigroup(Int32) +deriveMeetSemigroup(Int64) +deriveMeetSemigroup(Integer) + +deriveMeetSemigroup(Word) +deriveMeetSemigroup(Word8) +deriveMeetSemigroup(Word16) +deriveMeetSemigroup(Word32) +deriveMeetSemigroup(Word64) +deriveMeetSemigroup(Natural) + +deriveMeetSemigroup(Uni) +deriveMeetSemigroup(Deci) +deriveMeetSemigroup(Centi) +deriveMeetSemigroup(Milli) +deriveMeetSemigroup(Micro) +deriveMeetSemigroup(Nano) +deriveMeetSemigroup(Pico) + +deriveMeetSemigroup(Rational) +deriveMeetSemigroup((Ratio Natural)) + +#define deriveMeetMonoid(ty) \ +instance Monoid (Meet ty) where { \ + mempty = pure maximal \ +; {-# INLINE mempty #-} \ +} + +deriveMeetMonoid(()) +deriveMeetMonoid(Bool) + +deriveMeetMonoid(Int) +deriveMeetMonoid(Int8) +deriveMeetMonoid(Int16) +deriveMeetMonoid(Int32) +deriveMeetMonoid(Int64) + +deriveMeetMonoid(Word) +deriveMeetMonoid(Word8) +deriveMeetMonoid(Word16) +deriveMeetMonoid(Word32) +deriveMeetMonoid(Word64) diff --git a/src/Data/Semilattice.hs b/src/Data/Semilattice.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semilattice.hs @@ -0,0 +1,347 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} + +module Data.Semilattice ( + type (-) + -- * Join semilattices + , JoinSemilattice + , BoundedJoinSemilattice + , Join(..) + , bottom + , (∨) + , join + , joinWith + , join1 + , joinWith1 + -- * Meet semilattices + , MeetSemilattice + , BoundedMeetSemilattice + , Meet(..) + , top + , (∧) + , meet + , meetWith + , meet1 + , meetWith1 + -- * Lattices + , LatticeLaw + , BoundedLatticeLaw + , BoundedLattice + , LowerBoundedLattice + , UpperBoundedLattice + , Lattice + , glb + , glbWith + , lub + , lubWith + , eval + , evalWith + , eval1 + , evalWith1 + , cross + , cross1 +) where + +import Control.Applicative +import Data.Bool +import Data.Either +import Data.Fixed +import Data.Foldable +import Data.Functor.Apply +import Data.Int +import Data.Maybe +import Data.Ord (Ord) +import Data.Prd +import Data.Semigroup.Foldable +import Data.Semigroup.Join +import Data.Semigroup.Meet +import Data.Word +import Numeric.Natural +import Prelude hiding (Ord(..), Fractional(..),Num(..)) +import qualified Data.IntMap as IntMap +import qualified Data.IntSet as IntSet +import qualified Data.Map as Map +import qualified Data.Set as Set + + + + +{- +--(a ∧ b) ⊗ c = (a ⊗ c) ∧ (b ⊗ c), c ⊗ (a ∧ b) = (c ⊗ a) ∧ (c ⊗ b) +-- (meet x y) ∧ z = x ∧ z `meet` y ∧ z + +-- idempotent sup dioids ? complete (join-semi)lattices derived from <=? +--connr-distributivity (the group (E\{ε}, ⊗) is therefore reticulated) +-- +-- mon zero = const Nothing + +-- bounded meet semilattice +-- need the codistributive property & absorbtion & commutativity + +If E is a distributive lattice, then (E, ∨, ∧) is a doublyidempotent dioid, the order relation (canonical) of the dioid being defined as: +a ≤ b ⇔ a ∨ b = b. +Conversely, let (E, ⊕, ⊗) be a doubly-idempotent dioid for which ≤, the canonical +order relation relative to the law ⊕ is also a canonical order relation for ⊗: +x ≤ y ⇔ x ⊗ y = x. +Then E is a distributive lattice. +-} + + +-- Lattice types + + +type LatticeLaw a = (JoinSemilattice a, MeetSemilattice a) + +type BoundedLatticeLaw a = (BoundedJoinSemilattice a, BoundedMeetSemilattice a) + +type BoundedLattice a = (Lattice a, BoundedLatticeLaw a) + +type LowerBoundedLattice a = (Lattice a, (Join-Monoid) a) + +type UpperBoundedLattice a = (Lattice a, (Meet-Monoid) a) + +type BoundedJoinSemilattice a = (JoinSemilattice a, (Join-Monoid) a) + +type BoundedMeetSemilattice a = (MeetSemilattice a, (Meet-Monoid) a) + + +-- | Lattices. +-- +-- A lattice is a partially ordered set in which every two elements have a unique join +-- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum). +-- +-- /Neutrality/ +-- +-- @ +-- x '∨' 'minimal' = x +-- x '∧' 'maximal' = x +-- @ +-- +-- /Associativity/ +-- +-- @ +-- x '∨' (y '∨' z) = (x '∨' y) '∨' z +-- x '∧' (y '∧' z) = (x '∧' y) '∧' z +-- @ +-- +-- /Commutativity/ +-- +-- @ +-- x '∨' y = y '∨' x +-- x '∧' y = y '∧' x +-- @ +-- +-- /Idempotency/ +-- +-- @ +-- x '∨' x = x +-- x '∧' x = x +-- @ +-- +-- /Absorption/ +-- +-- @ +-- (x '∨' y) '∧' y = y +-- (x '∧' y) '∨' y = y +-- @ +-- +-- See and . +-- +-- Note that distributivity is _not_ a requirement for a lattice, +-- however distributive lattices are idempotent, commutative dioids. +-- +class LatticeLaw a => Lattice a + + +-- | Birkhoff's self-dual < https://en.wikipedia.org/wiki/Median_algebra ternary median > operation. +-- +-- If the lattice is distributive then 'glb' has the following properties. +-- +-- @ +-- 'glb' x y y = y +-- 'glb' x y z = 'glb' z x y +-- 'glb' x y z = 'glb' x z y +-- 'glb' ('glb' x w y) w z = 'glb' x w ('glb' y w z) +-- @ +-- +-- >>> glb 1 2 3 :: Int +-- 2 +-- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int +-- fromList [3,5] +-- +-- See 'Data.Semilattice.Property'. +-- +glb :: Lattice a => a -> a -> a -> a +glb = glbWith id + +-- | +-- >>> glbWith N5 1 9 7 +-- N5 {fromN5 = 7.0} +-- >>> glbWith N5 1 9 (0/0) +-- N5 {fromN5 = 9.0} +glbWith :: Lattice r => (a -> r) -> a -> a -> a -> r +glbWith f x y z = (f x ∨ f y) ∧ (f y ∨ f z) ∧ (f z ∨ f x) + +-- | The order dual of 'glb'. +-- +lub :: Lattice a => a -> a -> a -> a +lub = lubWith id + +-- | +-- >>> lubWith N5 1 9 7 +-- N5 {fromN5 = 7.0} +-- >>> lubWith N5 1 9 (0/0) +-- N5 {fromN5 = 1.0} +lubWith :: Lattice r => (a -> r) -> a -> a -> a -> r +lubWith f x y z = (f x ∧ f y) ∨ (f y ∧ f z) ∨ (f z ∧ f x) + +-- @ 'join' :: 'Lattice' a => 'Minimal' a => 'Set' a -> a @ +-- +join :: (Join-Monoid) a => Lattice a => Foldable f => f a -> a +join = joinWith id + +-- >>> joinWith Just [1..5 :: Int] +-- Just 5 +-- >>> joinWith N5 [1,5,0/0] +-- N5 {fromN5 = Infinity} +-- >>> joinWith MaxMin $ [IntSet.fromList [1..5], IntSet.fromList [2..4]] +-- MaxMin {unMaxMin = fromList [2,3,4]} +joinWith :: (Join-Monoid) a => Foldable t => (b -> a) -> t b -> a +joinWith f = foldr' ((∨) . f) bottom +{-# INLINE joinWith #-} + +meet :: (Meet-Monoid) a => Lattice a => Foldable f => f a -> a +meet = meetWith id + +-- | Fold over a collection using the multiplicative operation of an arbitrary semiring. +-- +-- @ +-- 'meet' f = 'Data.foldr'' ((*) . f) 'top' +-- @ +-- +-- +-- >>> meetWith Just [1..5 :: Int] +-- Just 1 +-- >>> meetWith N5 [1,5,0/0] +-- N5 {fromN5 = -Infinity} +meetWith :: (Meet-Monoid) a => Foldable t => (b -> a) -> t b -> a +meetWith f = foldr' ((∧) . f) top +{-# INLINE meetWith #-} + +-- | The join of a list of join-semilattice elements (of length at least top) +join1 :: Lattice a => Foldable1 f => f a -> a +join1 = joinWith1 id + +-- | Fold over a non-empty collection using the join operation of an arbitrary join semilattice. +-- +joinWith1 :: Foldable1 t => Lattice a => (b -> a) -> t b -> a +joinWith1 f = unJoin . foldMap1 (Join . f) +{-# INLINE joinWith1 #-} + +-- | The meet of a list of meet-semilattice elements (of length at least top) +meet1 :: Lattice a => Foldable1 f => f a -> a +meet1 = meetWith1 id + +-- | Fold over a non-empty collection using the multiplicative operation of a semiring. +-- +-- As the collection is non-empty this does not require a distinct multiplicative unit: +-- +-- >>> meetWith1 Just $ 1 :| [2..5 :: Int] +-- Just 120 +-- >>> meetWith1 First $ 1 :| [2..(5 :: Int)] +-- First {getFirst = 15} +-- >>> meetWith1 First $ Nothing :| [Just (5 :: Int), Just 6, Nothing] +-- First {getFirst = Just 11} +-- +meetWith1 :: Foldable1 t => Lattice a => (b -> a) -> t b -> a +meetWith1 f = unMeet . foldMap1 (Meet . f) +{-# INLINE meetWith1 #-} + +-- | Evaluate a lattice expression. +-- +-- @ (a11 ∧ .. ∧ a1m) ∨ (a21 ∧ .. ∧ a2n) ∨ ... @ +-- +-- >>> eval [[1, 2], [3, 4, 5], [6, 7 :: Int]] -- 1 * 2 + 3 * 4 +-- 14 +-- >>> eval $ sequence [[1, 2], [3, 4 :: Int]] -- 1 + 2 * 3 + 4 +-- 21 +-- +eval :: BoundedLattice a => Functor f => Foldable f => Foldable g => f (g a) -> a +eval = join . fmap meet + +-- >>> evalWith Max [[1..4 :: Int], [0..2 :: Int]] +-- Max {getMax = 24} +evalWith :: BoundedLattice r => Functor f => Functor g => Foldable f => Foldable g => (a -> r) -> f (g a) -> r +evalWith f = join . fmap meet . (fmap . fmap) f + +eval1 :: Lattice a => Functor f => Foldable1 f => Foldable1 g => f (g a) -> a +eval1 = join1 . fmap meet1 + +-- >>> evalWith1 (Max . Down) $ (1 :| [2..5 :: Int]) :| [-5 :| [2..5 :: Int]] +-- Max {getMax = Down 9} +-- >>> evalWith1 Max $ (1 :| [2..5 :: Int]) :| [-5 :| [2..5 :: Int]] +-- Max {getMax = 15} +-- +evalWith1 :: Lattice r => Functor f => Functor g => Foldable1 f => Foldable1 g => (a -> r) -> f (g a) -> r +evalWith1 f = join1 . fmap meet1 . (fmap . fmap) f + +-- | Cross-multiply two collections. +-- +-- >>> cross [1,3,5 :: Int] [2,4] +-- 4 +-- +-- >>> cross [1,2,3 :: Int] [] +-- -9223372036854775808 +-- +cross :: Foldable f => Applicative f => LowerBoundedLattice a => f a -> f a -> a +cross a b = join $ liftA2 (∧) a b +{-# INLINE cross #-} + +-- | Cross-multiply two non-empty collections. +-- +cross1 :: Foldable1 f => Apply f => Lattice a => f a -> f a -> a +cross1 a b = join1 $ liftF2 (∧) a b +{-# INLINE cross1 #-} + + + +-- Lattices +instance Lattice () +instance Lattice Bool +instance Lattice Word +instance Lattice Word8 +instance Lattice Word16 +instance Lattice Word32 +instance Lattice Word64 +instance Lattice Natural + +instance Lattice Int +instance Lattice Int8 +instance Lattice Int16 +instance Lattice Int32 +instance Lattice Int64 +instance Lattice Integer + +instance Lattice Uni +instance Lattice Deci +instance Lattice Centi +instance Lattice Milli +instance Lattice Micro +instance Lattice Nano +instance Lattice Pico + +instance Lattice a => Lattice (Down a) +instance (Lattice a, Lattice b) => Lattice (Either a b) +instance Lattice a => Lattice (Maybe a) +instance Lattice a => Lattice (IntMap.IntMap a) +instance Lattice IntSet.IntSet +instance Ord a => Lattice (Set.Set a) +instance (Ord k, Lattice a) => Lattice (Map.Map k a) diff --git a/src/Data/Semilattice/MaxMin.hs b/src/Data/Semilattice/MaxMin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semilattice/MaxMin.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DeriveFunctor #-} +module Data.Semilattice.MaxMin where + +import Control.Applicative +import Data.Prd +import Data.Semilattice + +import Prelude hiding ((<=)) + +newtype MaxMin a = MaxMin { unMaxMin :: a } deriving (Show, Functor) + +instance Applicative MaxMin where + pure = MaxMin + MaxMin f <*> MaxMin a = MaxMin (f a) + +instance Prd a => Prd (MaxMin a) where + MaxMin a <= MaxMin b = a <= b + +instance Prd a => Eq (MaxMin a) where + (==) = (=~) + +instance Ord a => Semigroup (Join (MaxMin a)) where + (<>) = liftA2 . liftA2 $ max + +instance (Ord a, Minimal a) => Monoid (Join (MaxMin a)) where + mempty = pure . pure $ minimal + +instance Ord a => Semigroup (Meet (MaxMin a)) where + (<>) = liftA2 . liftA2 $ min + +instance (Ord a, Maximal a) => Monoid (Meet (MaxMin a)) where + mempty = pure . pure $ maximal + +instance (Ord a, Bound a) => Lattice (MaxMin a) diff --git a/src/Data/Semilattice/N5.hs b/src/Data/Semilattice/N5.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semilattice/N5.hs @@ -0,0 +1,135 @@ +{-# LANGUAGE DeriveFunctor #-} +module Data.Semilattice.N5 where + +import Control.Applicative +import Data.Prd +import Data.Prd.Nan +import Data.Connection +import Data.Semilattice +import Data.Semiring +import Data.Semifield + +import Prelude hiding (Num(..), Ord(..), Fractional(..), Bounded) + +-- | Lift a 'Semifield' into a non-modular lattice. +-- +-- See +-- +newtype N5 a = N5 { unN5 :: a } deriving (Show, Functor) + +n5 :: (Minimal a, Semifield a, Minimal b, Semifield b) => Conn a b -> Conn (N5 a) (N5 b) +n5 (Conn f g) = Conn (fmap f) (fmap g) + +n5' :: Semifield a => Minimal a => Bound b => Trip a (Nan b) -> Trip (N5 a) b +n5' t = Trip f g h where + Conn f g = n5l . tripl $ t + Conn _ h = n5r . tripr $ t + +n5l :: Semifield a => Minimal a => Maximal b => Conn a (Nan b) -> Conn (N5 a) b +n5l (Conn f g) = Conn f' g' where + f' (N5 x) = nan maximal id $ f x + g' = N5 . g . Def + +n5r :: Semifield b => Minimal a => Minimal b => Conn (Nan a) b -> Conn a (N5 b) +n5r (Conn f g) = Conn f' g' where + f' = N5 . f . Def + g' (N5 x) = nan minimal id $ g x + +{- +untf64 :: Conn (Bottom Unit) (N5 Double) +untf64 = Conn f g where + f = maybe (N5 ninf) (N5 . unUnit) + g (N5 x) | x >= 0 = Just . Unit $ min 1 x + | otherwise = Nothing + +nan :: b -> (a -> b) -> Nan a -> b + +extended :: Field b => (a -> b) -> Extended a -> b +extended f = nan' $ bounded ninf f pinf + +liftNan :: Prd a => Semifield a => (a -> b) -> a -> Nan b +liftNan f x | x =~ anan = Nan + | otherwise = Def (f x) +-} + +joinN5 :: Minimal a => Semifield a => N5 a -> N5 a -> N5 a +joinN5 (N5 x) (N5 y) = case pcompare x y of + Just LT -> N5 y + Just EQ -> N5 x + Just GT -> N5 x + Nothing -> N5 pinf + +meetN5 :: Minimal a => Semifield a => N5 a -> N5 a -> N5 a +meetN5 (N5 x) (N5 y) = case pcompare x y of + Just LT -> N5 x + Just EQ -> N5 x + Just GT -> N5 y + Nothing -> N5 minimal + + +instance (Minimal a, Semifield a) => Prd (N5 a) where + + -- | + -- @ 'anan' '<=' 'pinf' @ + -- @ 'anan' '>=' 'ninf' @ + pcompare (N5 x) (N5 y) | x =~ y = Just EQ + | x =~ minimal = Just LT + | y =~ minimal = Just GT + | x =~ pinf = Just GT + | y =~ pinf = Just LT + | otherwise = pcompare x y + +instance (Minimal a, Semifield a) => Eq (N5 a) where + (==) = (=~) + +instance (Minimal a, Semifield a) => Minimal (N5 a) where + minimal = N5 minimal + +instance (Bound a, Semifield a) => Maximal (N5 a) where + maximal = N5 maximal + +instance (Minimal a, Semifield a) => Semigroup (Meet (N5 a)) where + (<>) = liftA2 meetN5 + +instance (Minimal a, Semifield a) => Monoid (Meet (N5 a)) where + mempty = Meet $ N5 pinf + +instance (Minimal a, Semifield a) => Semigroup (Join (N5 a)) where + (<>) = liftA2 joinN5 + +instance (Minimal a, Semifield a) => Monoid (Join (N5 a)) where + mempty = Join $ N5 minimal + +instance (Minimal a, Semifield a) => Lattice (N5 a) + +instance (Additive-Semigroup) a => Semigroup (Additive (N5 a)) where + (<>) = liftA2 (+) + +instance (Additive-Monoid) a => Monoid (Additive (N5 a)) where + mempty = pure zero + +instance (Additive-Group) a => Magma (Additive (N5 a)) where + (<<) = liftA2 (-) + +instance (Additive-Group) a => Quasigroup (Additive (N5 a)) +instance (Additive-Group) a => Loop (Additive (N5 a)) +instance (Additive-Group) a => Group (Additive (N5 a)) + +instance (Multiplicative-Semigroup) a => Semigroup (Multiplicative (N5 a)) where + (<>) = liftA2 (*) + +instance (Multiplicative-Monoid) a => Monoid (Multiplicative (N5 a)) where + mempty = pure one + +instance (Multiplicative-Group) a => Magma (Multiplicative (N5 a)) where + (<<) = liftA2 (/) + +instance (Multiplicative-Group) a => Quasigroup (Multiplicative (N5 a)) +instance (Multiplicative-Group) a => Loop (Multiplicative (N5 a)) +instance (Multiplicative-Group) a => Group (Multiplicative (N5 a)) + +instance Presemiring a => Presemiring (N5 a) +instance Semiring a => Semiring (N5 a) +instance Ring a => Ring (N5 a) +instance Semifield a => Semifield (N5 a) +instance Field a => Field (N5 a) diff --git a/src/Data/Semilattice/Property.hs b/src/Data/Semilattice/Property.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semilattice/Property.hs @@ -0,0 +1,348 @@ +{-# Language AllowAmbiguousTypes #-} + +module Data.Semilattice.Property ( + -- * Properties of join lattices + monotone_join + , idempotent_join + , idempotent_join_on + , associative_join + , associative_join_on + , commutative_join + , commutative_join_on + , neutral_join + , neutral_join_on + , distributive_join + -- * Properties of meet semilattices + , monotone_meet + , idempotent_meet + , idempotent_meet_on + , associative_meet + , associative_meet_on + , commutative_meet + , commutative_meet_on + , neutral_meet + , neutral_meet_on + , distributive_meet + -- * Properties of lattices + , absorbative + , absorbative' + , annihilative_join + , annihilative_meet + , distributive + , codistributive + , majority_glb + , commutative_glb + , commutative_glb' + , associative_glb + --, distributive_finite_on + --, distributive_finite1_on + --, distributive_cross_on + --, distributive_cross1_on + -- * Properties of semilattice & lattice morphisms + , morphism_join + , morphism_join_on + , morphism_join' + , morphism_join_on' + , morphism_meet + , morphism_meet_on + , morphism_meet' + , morphism_meet_on' + , morphism_distributive +) where + +--import Data.Semigroup.Property as Prop +import Data.Prd hiding ((~~)) +import Data.Semigroup +import Data.Semigroup.Join +import Data.Semigroup.Meet +import Data.Semilattice +import Test.Function as Prop +import Test.Logic (Rel, (==>)) +import qualified Test.Operation as Prop + +import Prelude hiding (Ord(..), Num(..), sum) + +------------------------------------------------------------------------------------ +-- Properties of join semilattices + +-- | \( \forall a, b, c: b \leq c \Rightarrow b ∨ a \leq c ∨ a \) +-- +-- This is a required property. +-- +monotone_join :: JoinSemilattice r => r -> r -> r -> Bool +monotone_join x = Prop.monotone_on (<=) (<=) (∨ x) + +-- | \( \forall a \in R: a ∨ a = a \) +-- +-- @ 'idempotent_join' = 'absorbative' 'top' @ +-- +-- See < https://en.wikipedia.org/wiki/Band_(mathematics) >. +-- +-- This is a required property. +-- +idempotent_join :: JoinSemilattice r => r -> Bool +idempotent_join = idempotent_join_on (=~) + +idempotent_join_on :: (Join-Semigroup) r => Rel r b -> r -> b +idempotent_join_on (~~) r = (∨) r r ~~ r + +-- | \( \forall a, b, c \in R: (a ∨ b) ∨ c = a ∨ (b ∨ c) \) +-- +-- This is a required property. +-- +associative_join :: JoinSemilattice r => r -> r -> r -> Bool +associative_join = Prop.associative_on (=~) (∨) + +associative_join_on :: (Join-Semigroup) r => Rel r b -> r -> r -> r -> b +associative_join_on (~~) = Prop.associative_on (~~) (∨) + +-- | \( \forall a, b \in R: a ∨ b = b ∨ a \) +-- +-- This is a required property. +-- +commutative_join :: JoinSemilattice r => r -> r -> Bool +commutative_join = commutative_join_on (=~) + +commutative_join_on :: (Join-Semigroup) r => Rel r b -> r -> r -> b +commutative_join_on (~~) = Prop.commutative_on (~~) (∨) + +-- | \( \forall a \in R: (bottom ∨ a) = a \) +-- +-- This is a required property for bounded join semilattices. +-- +neutral_join :: BoundedJoinSemilattice r => r -> Bool +neutral_join = neutral_join_on (=~) + +neutral_join_on :: (Join-Monoid) r => Rel r b -> r -> b +neutral_join_on (~~) = Prop.neutral_on (~~) (∨) bottom + +-- | \( \forall a, b, c: c \leq a ∨ b \Rightarrow \exists a',b': c = a' ∨ b' \) +-- +-- See < https://en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices > +-- +-- This is a required property for distributive join semilattices. +-- +distributive_join :: JoinSemilattice r => r -> r -> r -> r -> r -> Bool +distributive_join c a b a' b' = c <= a ∨ b ==> a' <= a && b' <= b && c <= a' ∨ b' + +------------------------------------------------------------------------------------ +-- Properties of meet semilattices + +-- | \( \forall a, b, c: b \leq c \Rightarrow b ∧ a \leq c ∧ a \) +-- +-- This is a required property. +-- +monotone_meet :: MeetSemilattice r => r -> r -> r -> Bool +monotone_meet x = Prop.monotone_on (<=) (<=) (∧ x) + +-- | \( \forall a, b, c \in R: (a * b) * c = a * (b * c) \) +-- +-- This is a required property. +-- +associative_meet :: MeetSemilattice r => r -> r -> r -> Bool +associative_meet = associative_meet_on (=~) + +associative_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> r -> r -> b +associative_meet_on (~~) = Prop.associative_on (~~) (∧) + +-- | \( \forall a, b \in R: a ∧ b = b ∧ a \) +-- +-- This is a required property. +-- +commutative_meet :: MeetSemilattice r => r -> r -> Bool +commutative_meet = commutative_meet_on (=~) + +commutative_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> r -> b +commutative_meet_on (~~) = Prop.commutative_on (~~) (∧) + +-- | \( \forall a \in R: a ∧ a = a \) +-- +-- @ 'idempotent_meet' = 'absorbative' 'bottom' @ +-- +-- See < https://en.wikipedia.org/wiki/Band_(mathematics) >. +-- +-- This is a required property. +-- +idempotent_meet :: MeetSemilattice r => r -> Bool +idempotent_meet = idempotent_meet_on (=~) + +idempotent_meet_on :: (Meet-Semigroup) r => Rel r b -> r -> b +idempotent_meet_on (~~) r = (∧) r r ~~ r + +-- | \( \forall a \in R: (bottom ∧ a) = a \) +-- +-- This is a required property for bounded meet semilattices. +-- +neutral_meet :: BoundedMeetSemilattice r => r -> Bool +neutral_meet = neutral_meet_on (=~) + +neutral_meet_on :: (Meet-Monoid) r => Rel r b -> r -> b +neutral_meet_on (~~) = Prop.neutral_on (~~) (∧) top + +-- | \( \forall a, b, c: c \leq a ∨ b \Rightarrow \exists a',b': c = a' ∧ b' \) +-- +-- See < https://en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices > +-- +-- This is a required property for distributive meet semilattices. +-- +distributive_meet :: MeetSemilattice r => r -> r -> r -> r -> r -> Bool +distributive_meet c a b a' b' = c >= a ∧ b ==> a' >= a && b' >= b && c >= a' ∧ b' + +------------------------------------------------------------------------------------ +-- Properties of lattices + +-- | \( \forall a, b \in R: a ∧ b ∨ b = b \) +-- +-- Absorbativity is a generalized form of idempotency: +-- +-- @ +-- 'absorbative' 'top' a = a ∨ a = a +-- @ +-- +-- This is a required property. +-- +absorbative :: Lattice r => r -> r -> Bool +absorbative x y = (x ∧ y ∨ y) =~ y + +-- | \( \forall a, b \in R: a ∨ b ∧ b = b \) +-- +-- Absorbativity is a generalized form of idempotency: +-- +-- @ +-- 'absorbative'' 'bottom' a = a ∨ a = a +-- @ +-- +-- This is a required property. +-- +absorbative' :: Lattice r => r -> r -> Bool +absorbative' x y = (x ∨ y ∧ y) =~ y + +-- | \( \forall a \in R: (top ∨ a) = top \) +-- +-- If /R/ is a lattice then its top element must be annihilative. +-- +-- This is a required property. +-- +annihilative_join :: UpperBoundedLattice r => r -> Bool +annihilative_join r = Prop.annihilative_on (=~) (∨) top r + +-- | \( \forall a \in R: (bottom ∧ a) = bottom \) +-- +-- If /R/ is a lattice then its bottom element must be annihilative. +-- +-- For 'Semiring' instances this property translates to: +-- +-- @ +-- 'zero' '*' a = 'zero' +-- @ +-- +-- For 'Alternative' instances this property translates to: +-- +-- @ +-- 'empty' '*>' a = 'empty' +-- @ +-- +-- This is a required property. +-- +annihilative_meet :: LowerBoundedLattice r => r -> Bool +annihilative_meet r = Prop.annihilative_on (=~) (∧) bottom r + +------------------------------------------------------------------------------------ +-- Properties of distributive lattices + +distributive :: Lattice r => r -> r -> r -> Bool +distributive = Prop.distributive_on (=~) (∧) (∨) + +-- | \( \forall a, b, c \in R: c ∨ (a ∧ b) \equiv (c ∨ a) ∧ (c ∨ b) \) +-- +-- A right-codistributive semiring has a right-annihilative meet: +-- +-- @ 'codistributive' 'top' a 'bottom' = 'top' '=~' 'top' '∨' a @ +-- +-- idempotent mulitiplication: +-- +-- @ 'codistributive' 'bottom' 'bottom' a = a '=~' a '∧' a @ +-- +-- and idempotent addition: +-- +-- @ 'codistributive' a 'bottom' a = a '=~' a '∨' a @ +-- +-- Furthermore if /R/ is commutative then it is a right-distributive lattice. +-- +codistributive :: Lattice r => r -> r -> r -> Bool +codistributive = Prop.distributive_on' (=~) (∧) (∨) + +-- | @ 'glb' x x y = x @ +-- +majority_glb :: Lattice r => r -> r -> Bool +majority_glb x y = glb x y y =~ y + +-- | @ 'glb' x y z = 'glb' z x y @ +-- +commutative_glb :: Lattice r => r -> r -> r -> Bool +commutative_glb x y z = glb x y z =~ glb z x y + +-- | @ 'glb' x y z = 'glb' x z y @ +-- +commutative_glb' :: Lattice r => r -> r -> r -> Bool +commutative_glb' x y z = glb x y z =~ glb x z y + +-- | @ 'glb' ('glb' x w y) w z = 'glb' x w ('glb' y w z) @ +-- +associative_glb :: Lattice r => r -> r -> r -> r -> Bool +associative_glb x y z w = glb (glb x w y) w z =~ glb x w (glb y w z) + +------------------------------------------------------------------------------------ +-- Properties of semilattice & lattice morphisms + +-- | \( \forall a, b: f(a ∨ b) = f(a) ∨ f(b) \) +-- +-- Given two join-semilattices (S, ∨) and (T, ∨), a homomorphism is a monotone function /f: S → T/ such that +-- +-- @ f (x '∨' y) '=~' f x '∨' f y @ +-- +-- This is a required property for join semilattice morphisms. +-- +morphism_join :: JoinSemilattice r => JoinSemilattice s => (r -> s) -> r -> r -> Bool +morphism_join = morphism_join_on (=~) + +morphism_join_on :: (Join-Semigroup) r => (Join-Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b +morphism_join_on (~~) f x y = (f $ x ∨ y) ~~ (f x ∨ f y) + +-- | \( \forall a, b: f(bottom) = bottom \) +-- +-- This is a required property for bounded join semilattice morphisms. +-- +morphism_join' :: BoundedJoinSemilattice r => BoundedJoinSemilattice s => (r -> s) -> Bool +morphism_join' = morphism_join_on' (=~) + +morphism_join_on' :: (Join-Monoid) r => (Join-Monoid) s => Rel s b -> (r -> s) -> b +morphism_join_on' (~~) f = (f bottom) ~~ bottom + +-- | \( \forall a, b: f(a ∧ b) = f(a) ∧ f(b) \) +-- +-- The obvious dual replacing '∧' with '∨' and 'bottom' with 'top' transforms this +-- definition of a join-semilattice homomorphism into its meet-semilattice equivalent. +-- +-- This is a required property for meet semilattice morphisms. +-- +morphism_meet :: MeetSemilattice r => MeetSemilattice s => (r -> s) -> r -> r -> Bool +morphism_meet = morphism_meet_on (=~) + +morphism_meet_on :: (Meet-Semigroup) r => (Meet-Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b +morphism_meet_on (~~) f x y = (f $ x ∧ y) ~~ (f x ∧ f y) + +-- | \( \forall a, b: f(top) = top \) +-- +-- This is a required property for bounded meet semilattice morphisms. +-- +morphism_meet' :: BoundedMeetSemilattice r => BoundedMeetSemilattice s => (r -> s) -> Bool +morphism_meet' = morphism_meet_on' (=~) + +morphism_meet_on' :: (Meet-Monoid) r => (Meet-Monoid) s => Rel s b -> (r -> s) -> b +morphism_meet_on' (~~) f = (f top) ~~ top + +-- | Distributive lattice morphisms are compatible with 'glb'. +-- +morphism_distributive :: Prd r => Prd s => Lattice r => Lattice s => (r -> s) -> r -> r -> r -> Bool +morphism_distributive f x y z = f (glb x y z) =~ glb (f x) (f y) (f z) diff --git a/src/Data/Semilattice/Top.hs b/src/Data/Semilattice/Top.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semilattice/Top.hs @@ -0,0 +1,148 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.Semilattice.Top where + +import Data.Prd +import Data.Prd.Nan +import Data.Semilattice +import Data.Semifield +import GHC.Generics (Generic, Generic1) + +import Prelude hiding (Ord(..), Bounded) + +type Bottom a = Maybe a +type Bounded a = Bottom (Top a) +type Lifted a = Nan (Top a) +type Lowered a = Nan (Bottom a) +type Extended a = Nan (Bounded a) + +data Top a = Fin a | Top + deriving (Show, Generic, Generic1, Functor, Foldable, Traversable) + +-- analagous to Maybe Semigroup instance +instance Semigroup a => Semigroup (Top a) where + Top <> _ = Top + _ <> Top = Top + Fin x <> Fin y = Fin $ x <> y + +instance Monoid a => Monoid (Top a) where + mempty = Fin mempty + +instance Prd a => Prd (Top a) where + _ <= Top = True + Top <= _ = False + Fin a <= Fin b = a <= b + +instance Minimal a => Minimal (Top a) where + minimal = Fin minimal + +instance Prd a => Maximal (Top a) where + maximal = Top + +-- analagous to Maybe (Meet-Semigroup) instance +instance (Join-Semigroup) a => Semigroup (Join (Top a)) where + Join Top <> _ = Join Top + Join (Fin{}) <> Join Top = Join Top + Join (Fin x) <> Join (Fin y) = Join . Fin $ x ∨ y + +-- analagous to Maybe (Meet-Monoid) instance +instance (Join-Monoid) a => Monoid (Join (Top a)) where + mempty = Join $ Fin bottom + +instance (Meet-Semigroup) a => Semigroup (Meet (Top a)) where + Meet (Fin x) <> Meet (Fin y) = Meet . Fin $ x ∧ y + Meet (x@Fin{}) <> _ = Meet x + Meet Top <> y = y + +instance (Meet-Semigroup) a => Monoid (Meet (Top a)) where + mempty = Meet Top + +instance Lattice a => Lattice (Top a) + +{- + +instance Covered (Top Float) where + Bounded x <. Bounded y = shiftf 1 x == y + +instance Graded (Top Float) where + rank (Bounded x) | ind x = 0 + | otherwise = r where + x' = floatInt32 x + y' = floatInt32 ninf + r = fromIntegral . abs $ x' - y' +-} + + +isTop :: Bounded a -> Bool +isTop = bounded False (const False) True + +isBottom :: Bounded a -> Bool +isBottom = bounded True (const False) False + +isFin :: Bounded a -> Bool +isFin = bounded False (const True) False + +fin :: a -> Bounded a +fin = Just . Fin + +toTop :: Prd a => LowerBoundedLattice b => (a -> b) -> Bounded a -> Top b +toTop f = bounded (Fin bottom) (Fin . f) Top + +toBottom :: Prd a => UpperBoundedLattice b => (a -> b) -> Bounded a -> Bottom b +toBottom f = bounded Nothing (Just . f) (Just top) + +topped :: (a -> b) -> b -> Top a -> b +topped f _ (Fin a) = f a +topped _ b Top = b + +lifted :: Semifield b => (a -> b) -> Lifted a -> b +lifted f = nan' $ topped f pinf + +bounded :: b -> (a -> b) -> b -> Bounded a -> b +bounded b _ _ Nothing = b +bounded _ f _ (Just (Fin a)) = f a +bounded _ _ b (Just Top) = b + +-- | Interpret @'Bounded' a@ using the 'BoundedLattice' of @a@. +-- +-- This map is monotone when /f/ is. +-- +bounded' :: BoundedLattice b => (a -> b) -> Bounded a -> b +bounded' f = bounded bottom f top + +extended :: b -> b -> (a -> b) -> b -> Extended a -> b +extended x y f z = nan x $ bounded y f z + +extended' :: Field b => (a -> b) -> Extended a -> b +extended' f = extended anan ninf f pinf + +-- this is a monotone map +liftTop :: Maximal a => (a -> b) -> a -> Top b +liftTop f = g where + g i | i =~ maximal = Top + | otherwise = Fin $ f i + +liftTop' :: Maximal a => (a -> b) -> a -> Bounded b +liftTop' f a = Just $ liftTop f a + +-- This map is a lattice morphism when /f/ is. +liftBottom :: Minimal a => (a -> b) -> a -> Bottom b +liftBottom f = g where + g i | i =~ minimal = Nothing + | otherwise = Just $ f i + +liftBottom' :: Minimal a => (a -> b) -> a -> Bounded b +liftBottom' f = liftBottom (Fin . f) + +-- this is a monotone map +liftBounded :: Bound a => (a -> b) -> a -> Bounded b +liftBounded f = liftBottom (liftTop f) + +-- Lift all exceptional values +liftExtended :: Bound a => Field a => (a -> b) -> a -> Extended b +liftExtended f = liftNan (liftBounded f) diff --git a/src/Numeric/Prelude.hs b/src/Numeric/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Prelude.hs @@ -0,0 +1,182 @@ +{-# LANGUAGE RebindableSyntax #-} +module Numeric.Prelude + ( -- * Combinators + id, + (.), + ($), + ($!), + (&), + const, + flip, + on, + seq, + -- * Primitive types + -- ** Bool + Bool (..), + bool, + (&&), + (||), + not, + otherwise, + ifThenElse, + -- ** Char + Char, + -- ** Int + Integer, + Int, + Int8, + Int16, + Int32, + Int64, + -- ** Word + Natural, + Word, + Word8, + Word16, + Word32, + Word64, + -- ** Rational + Ratio(..), + -- ** Floating + Float, + Double, + fmod, floor, ceil, trunc, round, + sqrt, cbrt, pow, log, exp, ldexp, + pi, sin, cos, tan, + asin, acos, atan, atan2, + sinh, cosh, tanh, + asinh, acosh, atanh, + -- * Numerical Typeclasses + -- ** Eq + Eq (..), + -- ** Orders + Prd (..), + Ordering (..), + min, max, + compare, + comparing, + -- ** Connections + TripRatio(..), + ConnInteger(..), + fromRational, + fromInteger, + floor16, ceil16, round16, trunc16, + floor32, ceil32, round32, trunc32, + -- ** Magmas + Semigroup (..), + Monoid (..), + mreplicate, + Magma(..), + Quasigroup, + Loop, + Group(..), + -- ** Semirings + Semiring, + Ring, + (+), (-), (*), (^), + zero, one, + abs, + negate, + signum, + sum, + product, + -- ** Semifields + Semifield, + Field, + (/), (^^), + pinf, ninf, anan, + recip, + -- * Data structures + -- ** Either + Either (..), + either, + -- ** Maybe + Maybe (..), + fromMaybe, + maybe, + -- ** Tuple + fst, + snd, + curry, + uncurry, + -- * Algebraic structures + -- ** Functor + Functor (..), + (<$>), + ($>), + void, + -- ** Bifunctor + Bifunctor (..), + -- ** Applicative + Applicative (..), + (<**>), + liftA3, + -- ** Alternative + Alternative (..), + asum, + -- ** Traversable + Traversable (..), + for, + -- ** Monad + Monad ((>>=), (>>), return), + (=<<), + forM, + forM_, + mapM_, + when, + -- ** MonadPlus + MonadPlus (..), + guard, + msum, + -- ** Foldable + Foldable (foldMap, fold), + foldl', foldr', + for_, + traverse_, + -- ** Show + Show (..), + -- *** ShowS + ShowS, + showString, + ) where + +import Control.Applicative ((<**>), Alternative (..), Applicative (..), empty, liftA3) +import Control.Monad ((=<<), Monad (..), MonadPlus (..), forM, forM_, guard, mapM_, msum, when) +import Data.Bifunctor (Bifunctor (..), first, second) +import Data.Bool ((&&), Bool (..), bool, not, otherwise, (||)) +import Data.Char (Char) +import Data.Connection.Int (ConnInteger(..), fromInteger) +import Data.Connection.Ratio (TripRatio(..), fromRational) +import Data.Connection.Round (floor16, ceil16, trunc16, round16, floor32, ceil32, trunc32, round32) +import Data.Either (Either (..), either) +import Data.Eq (Eq (..)) +import Data.Float (fmod, floor, ceil, trunc, round, sqrt, cbrt, pow, log, exp, ldexp, sin, cos, tan + , asin, acos, atan, atan2, sinh, cosh, tanh, asinh, acosh, atanh) +import Data.Foldable (Foldable (), asum, fold, foldMap, foldl', foldr', for_, traverse_) +import Data.Function (($), (&), (.), const, flip, id, on) +import Data.Functor (($>), (<$>), Functor (..), void) +import Data.Int (Int, Int16, Int32, Int64, Int8) +import Data.Maybe (Maybe (..), fromMaybe, maybe) +import Data.Monoid (Monoid (..)) +import Data.Ord (Ordering (..), min, max, compare, comparing) +import Data.Prd (Prd (..)) +import Data.Semifield (Semifield, Field, (/), (^^), anan, pinf, ninf, recip) +import Data.Semigroup (Semigroup (..)) +import Data.Semiring (Semiring, Ring, (+), (-), (*), (^), zero, one, abs, negate, signum, sum, product) +import Data.Semiring (Magma(..), Quasigroup, Loop, Group(..), mreplicate) +import Data.Traversable (Traversable (..), for) +import Data.Tuple (curry, fst, snd, uncurry) +import Data.Word (Word, Word16, Word32, Word64, Word8) +import GHC.Real (Ratio(..)) +import Numeric.Natural (Natural) +import Text.Show (Show (..), ShowS, showString) + +import Prelude (($!), Double, Float, Integer, seq) + +pi :: TripRatio Integer b => b +pi = 3.141592653589793238 + +-- Used in conjunction with RebindableSyntax. +ifThenElse :: Bool -> a -> a -> a +ifThenElse b x y = bool y x b +{-# INLINE ifThenElse #-} diff --git a/test/Test/Data/Connection.hs b/test/Test/Data/Connection.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Connection.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE TemplateHaskell #-} +module Test.Data.Connection where + +import Control.Applicative +import Data.Float +import Data.Ord +import Data.Prd +import Data.Prd.Nan +import Data.Ratio +import Data.Semifield +import Data.Semilattice.N5 +import Data.Semilattice.Top +import GHC.Real hiding (Fractional(..), (^^), (^), div) +import Hedgehog +import Numeric.Natural +import Prelude hiding (Bounded) +import qualified Data.Connection.Property as Prop +import qualified Hedgehog.Gen as G +import qualified Hedgehog.Range as R + +ri :: (Integral a, Bound a) => Range a +ri = R.linearFrom 0 minimal maximal + +ri' :: Range Integer +ri' = R.linearFrom 0 (- 2^127) (2^127) + +ri'' :: Range Integer +ri'' = R.exponentialFrom 0 (-340282366920938463463374607431768211456) 340282366920938463463374607431768211456 + +rn :: Range Natural +rn = R.linear 0 (2^128) + +rf :: Range Float +rf = R.exponentialFloatFrom 0 (-3.4028235e38) 3.4028235e38 + +rd :: Range Double +rd = R.exponentialFloatFrom 0 (-1.7976931348623157e308) 1.7976931348623157e308 + +ord :: Gen Ordering +ord = G.element [LT, EQ, GT] + +f32 :: Gen Float +f32 = gen_fld $ G.float rf + +f64 :: Gen Double +f64 = gen_fld $ G.double rd + +rat :: Gen (Ratio Integer) +rat = gen_fld $ G.realFrac_ (R.linearFracFrom 0 (- 2^127) (2^127)) + +pos :: Gen (Ratio Natural) +pos = G.frequency [(49, gen), (1, G.element [pinf, anan])] + where gen = G.realFrac_ (R.linearFracFrom 0 0 (2^127)) + +gen_dwn :: Gen a -> Gen (Down a) +gen_dwn gen = Down <$> gen + +gen_nan :: Gen a -> Gen (Nan a) +gen_nan gen = G.frequency [(9, Def <$> gen), (1, pure Nan)] + +gen_pn5 :: Gen a -> Gen (N5 a) +gen_pn5 gen = N5 <$> gen + +gen_bot :: Gen a -> Gen (Bottom a) +gen_bot gen = G.frequency [(9, Just <$> gen), (1, pure Nothing)] + +gen_top :: Gen a -> Gen (Top a) +gen_top gen = G.frequency [(9, Fin <$> gen), (1, pure Top)] + +gen_bnd :: Gen a -> Gen (Bounded a) +gen_bnd gen = G.frequency [(18, (Just . Fin) <$> gen), (1, pure Nothing), (1, pure $ Just Top)] + +gen_lft :: Gen a -> Gen (Lifted a) +gen_lft = gen_nan . gen_top + +gen_ext :: Gen a -> Gen (Extended a) +gen_ext = gen_nan . gen_bnd + +gen_fld :: Field a => Gen a -> Gen a +gen_fld gen = G.frequency [(49, gen), (1, G.element [ninf, pinf, anan])] + + + +tests :: IO Bool +tests = checkParallel $$(discover) diff --git a/test/Test/Data/Connection/Float.hs b/test/Test/Data/Connection/Float.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Connection/Float.hs @@ -0,0 +1,531 @@ +{-# LANGUAGE TemplateHaskell #-} +module Test.Data.Connection.Float where + +import Data.Connection +import Data.Connection.Float +import Data.Float +import Data.Int +import Data.Ord +import Data.Prd.Nan +import Data.Semilattice.N5 +import Data.Semilattice.Top +import Hedgehog +import Prelude hiding (Bounded) +import Test.Data.Connection +import qualified Data.Connection.Property as Prop +import qualified Hedgehog.Gen as G + +prop_connection_f32ord :: Property +prop_connection_f32ord = withTests 100 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_nan ord + y' <- forAll $ gen_nan ord + + let f32ord = fldord :: Trip Float (Nan Ordering) + + assert $ Prop.connection (tripl f32ord) x y + assert $ Prop.connection (tripr f32ord) y x + assert $ Prop.closed (tripl f32ord) x + assert $ Prop.closed (tripr f32ord) y + assert $ Prop.kernel (tripl f32ord) y + assert $ Prop.kernel (tripr f32ord) x + assert $ Prop.monotonel (tripl f32ord) x x' + assert $ Prop.monotonel (tripr f32ord) y y' + assert $ Prop.monotoner (tripl f32ord) y y' + assert $ Prop.monotoner (tripr f32ord) x x' + assert $ Prop.projectivel (tripl f32ord) x + assert $ Prop.projectivel (tripr f32ord) y + assert $ Prop.projectiver (tripl f32ord) y + assert $ Prop.projectiver (tripr f32ord) x + +prop_connection_n5ford :: Property +prop_connection_n5ford = withTests 100 . property $ do + x <- forAll $ gen_pn5 f32 + x' <- forAll $ gen_pn5 f32 + y <- forAll ord + y' <- forAll ord + + let n5ford = n5' fldord :: Trip (N5 Float) Ordering + + assert $ Prop.connection (tripl n5ford) x y + assert $ Prop.connection (tripr n5ford) y x + assert $ Prop.closed (tripl n5ford) x + assert $ Prop.closed (tripr n5ford) y + assert $ Prop.kernel (tripl n5ford) y + assert $ Prop.kernel (tripr n5ford) x + assert $ Prop.monotonel (tripl n5ford) x x' + assert $ Prop.monotonel (tripr n5ford) y y' + assert $ Prop.monotoner (tripl n5ford) y y' + assert $ Prop.monotoner (tripr n5ford) x x' + assert $ Prop.projectivel (tripl n5ford) x + assert $ Prop.projectivel (tripr n5ford) y + assert $ Prop.projectiver (tripl n5ford) y + assert $ Prop.projectiver (tripr n5ford) x + +prop_connection_f32i08 :: Property +prop_connection_f32i08 = withTests 1000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_ext $ G.integral (ri @Int8) + y' <- forAll $ gen_ext $ G.integral (ri @Int8) + + assert $ Prop.connection (tripl f32i08) x y + assert $ Prop.connection (tripr f32i08) y x + assert $ Prop.closed (tripl f32i08) x + assert $ Prop.closed (tripr f32i08) y + assert $ Prop.kernel (tripl f32i08) y + assert $ Prop.kernel (tripr f32i08) x + assert $ Prop.monotonel (tripl f32i08) x x' + assert $ Prop.monotonel (tripr f32i08) y y' + assert $ Prop.monotoner (tripl f32i08) y y' + assert $ Prop.monotoner (tripr f32i08) x x' + assert $ Prop.projectivel (tripl f32i08) x + assert $ Prop.projectivel (tripr f32i08) y + assert $ Prop.projectiver (tripl f32i08) y + assert $ Prop.projectiver (tripr f32i08) x + +prop_connection_n5fi08 :: Property +prop_connection_n5fi08 = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f32 + x' <- forAll $ gen_pn5 f32 + y <- forAll $ gen_bnd $ G.integral (ri @Int8) + y' <- forAll $ gen_bnd $ G.integral (ri @Int8) + + let n5fi08 = n5' f32i08 :: Trip (N5 Float) (Bounded Int8) + + assert $ Prop.connection (tripl n5fi08) x y + assert $ Prop.connection (tripr n5fi08) y x + assert $ Prop.closed (tripl n5fi08) x + assert $ Prop.closed (tripr n5fi08) y + assert $ Prop.kernel (tripl n5fi08) y + assert $ Prop.kernel (tripr n5fi08) x + assert $ Prop.monotonel (tripl n5fi08) x x' + assert $ Prop.monotonel (tripr n5fi08) y y' + assert $ Prop.monotoner (tripl n5fi08) y y' + assert $ Prop.monotoner (tripr n5fi08) x x' + assert $ Prop.projectivel (tripl n5fi08) x + assert $ Prop.projectivel (tripr n5fi08) y + assert $ Prop.projectiver (tripl n5fi08) y + assert $ Prop.projectiver (tripr n5fi08) x + +prop_connection_f32i16 :: Property +prop_connection_f32i16 = withTests 1000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_ext $ G.integral (ri @Int16) + y' <- forAll $ gen_ext $ G.integral (ri @Int16) + + assert $ Prop.connection (tripl f32i16) x y + assert $ Prop.connection (tripr f32i16) y x + assert $ Prop.closed (tripl f32i16) x + assert $ Prop.closed (tripr f32i16) y + assert $ Prop.kernel (tripl f32i16) y + assert $ Prop.kernel (tripr f32i16) x + assert $ Prop.monotonel (tripl f32i16) x x' + assert $ Prop.monotonel (tripr f32i16) y y' + assert $ Prop.monotoner (tripl f32i16) y y' + assert $ Prop.monotoner (tripr f32i16) x x' + assert $ Prop.projectivel (tripl f32i16) x + assert $ Prop.projectivel (tripr f32i16) y + assert $ Prop.projectiver (tripl f32i16) y + assert $ Prop.projectiver (tripr f32i16) x + +prop_connection_n5fi16 :: Property +prop_connection_n5fi16 = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f32 + x' <- forAll $ gen_pn5 f32 + y <- forAll $ gen_bnd $ G.integral (ri @Int16) + y' <- forAll $ gen_bnd $ G.integral (ri @Int16) + + let n5fi16 = n5' f32i16 :: Trip (N5 Float) (Bounded Int16) + + assert $ Prop.connection (tripl n5fi16) x y + assert $ Prop.connection (tripr n5fi16) y x + assert $ Prop.closed (tripl n5fi16) x + assert $ Prop.closed (tripr n5fi16) y + assert $ Prop.kernel (tripl n5fi16) y + assert $ Prop.kernel (tripr n5fi16) x + assert $ Prop.monotonel (tripl n5fi16) x x' + assert $ Prop.monotonel (tripr n5fi16) y y' + assert $ Prop.monotoner (tripl n5fi16) y y' + assert $ Prop.monotoner (tripr n5fi16) x x' + assert $ Prop.projectivel (tripl n5fi16) x + assert $ Prop.projectivel (tripr n5fi16) y + assert $ Prop.projectiver (tripl n5fi16) y + assert $ Prop.projectiver (tripr n5fi16) x + +prop_connections_f32 :: Property +prop_connections_f32 = withTests 1000 . property $ do + x <- forAll f32 + y <- forAll (gen_nan $ G.integral ri) + x' <- forAll f32 + y' <- forAll (gen_nan $ G.integral ri) + + assert $ Prop.connection f32i32 x y + assert $ Prop.connection i32f32 y x + assert $ Prop.closed f32i32 x + assert $ Prop.closed i32f32 y + assert $ Prop.kernel i32f32 x + assert $ Prop.kernel f32i32 y + assert $ Prop.monotonel f32i32 x x' + assert $ Prop.monotonel i32f32 y y' + assert $ Prop.monotoner f32i32 y y' + assert $ Prop.monotoner i32f32 x x' + assert $ Prop.projectivel f32i32 x + assert $ Prop.projectivel i32f32 y + assert $ Prop.projectiver i32f32 x + assert $ Prop.projectiver f32i32 y + +prop_connection_f64ord :: Property +prop_connection_f64ord = withTests 100 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_nan ord + y' <- forAll $ gen_nan ord + + let f64ord = fldord :: Trip Double (Nan Ordering) + + assert $ Prop.connection (tripl f64ord) x y + assert $ Prop.connection (tripr f64ord) y x + assert $ Prop.closed (tripl f64ord) x + assert $ Prop.closed (tripr f64ord) y + assert $ Prop.kernel (tripl f64ord) y + assert $ Prop.kernel (tripr f64ord) x + assert $ Prop.monotonel (tripl f64ord) x x' + assert $ Prop.monotonel (tripr f64ord) y y' + assert $ Prop.monotoner (tripl f64ord) y y' + assert $ Prop.monotoner (tripr f64ord) x x' + assert $ Prop.projectivel (tripl f64ord) x + assert $ Prop.projectivel (tripr f64ord) y + assert $ Prop.projectiver (tripl f64ord) y + assert $ Prop.projectiver (tripr f64ord) x + +prop_connection_n5dord :: Property +prop_connection_n5dord = withTests 100 . property $ do + x <- forAll $ gen_pn5 f64 + x' <- forAll $ gen_pn5 f64 + y <- forAll ord + y' <- forAll ord + + let n5dord = n5' fldord :: Trip (N5 Double) Ordering + + assert $ Prop.connection (tripl n5dord) x y + assert $ Prop.connection (tripr n5dord) y x + assert $ Prop.closed (tripl n5dord) x + assert $ Prop.closed (tripr n5dord) y + assert $ Prop.kernel (tripl n5dord) y + assert $ Prop.kernel (tripr n5dord) x + assert $ Prop.monotonel (tripl n5dord) x x' + assert $ Prop.monotonel (tripr n5dord) y y' + assert $ Prop.monotoner (tripl n5dord) y y' + assert $ Prop.monotoner (tripr n5dord) x x' + assert $ Prop.projectivel (tripl n5dord) x + assert $ Prop.projectivel (tripr n5dord) y + assert $ Prop.projectiver (tripl n5dord) y + assert $ Prop.projectiver (tripr n5dord) x + +prop_connection_f64i08 :: Property +prop_connection_f64i08 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_ext $ G.integral (ri @Int8) + y' <- forAll $ gen_ext $ G.integral (ri @Int8) + + assert $ Prop.connection (tripl f64i08) x y + assert $ Prop.connection (tripr f64i08) y x + assert $ Prop.closed (tripl f64i08) x + assert $ Prop.closed (tripr f64i08) y + assert $ Prop.kernel (tripl f64i08) y + assert $ Prop.kernel (tripr f64i08) x + assert $ Prop.monotonel (tripl f64i08) x x' + assert $ Prop.monotonel (tripr f64i08) y y' + assert $ Prop.monotoner (tripl f64i08) y y' + assert $ Prop.monotoner (tripr f64i08) x x' + assert $ Prop.projectivel (tripl f64i08) x + assert $ Prop.projectivel (tripr f64i08) y + assert $ Prop.projectiver (tripl f64i08) y + assert $ Prop.projectiver (tripr f64i08) x + +prop_connection_n5di08 :: Property +prop_connection_n5di08 = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f64 + x' <- forAll $ gen_pn5 f64 + y <- forAll $ gen_bnd $ G.integral (ri @Int8) + y' <- forAll $ gen_bnd $ G.integral (ri @Int8) + + let n5di08 = n5' f64i08 :: Trip (N5 Double) (Bounded Int8) + + assert $ Prop.connection (tripl n5di08) x y + assert $ Prop.connection (tripr n5di08) y x + assert $ Prop.closed (tripl n5di08) x + assert $ Prop.closed (tripr n5di08) y + assert $ Prop.kernel (tripl n5di08) y + assert $ Prop.kernel (tripr n5di08) x + assert $ Prop.monotonel (tripl n5di08) x x' + assert $ Prop.monotonel (tripr n5di08) y y' + assert $ Prop.monotoner (tripl n5di08) y y' + assert $ Prop.monotoner (tripr n5di08) x x' + assert $ Prop.projectivel (tripl n5di08) x + assert $ Prop.projectivel (tripr n5di08) y + assert $ Prop.projectiver (tripl n5di08) y + assert $ Prop.projectiver (tripr n5di08) x + +prop_connection_f64i16 :: Property +prop_connection_f64i16 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_ext $ G.integral (ri @Int16) + y' <- forAll $ gen_ext $ G.integral (ri @Int16) + + assert $ Prop.connection (tripl f64i16) x y + assert $ Prop.connection (tripr f64i16) y x + assert $ Prop.closed (tripl f64i16) x + assert $ Prop.closed (tripr f64i16) y + assert $ Prop.kernel (tripl f64i16) y + assert $ Prop.kernel (tripr f64i16) x + assert $ Prop.monotonel (tripl f64i16) x x' + assert $ Prop.monotonel (tripr f64i16) y y' + assert $ Prop.monotoner (tripl f64i16) y y' + assert $ Prop.monotoner (tripr f64i16) x x' + assert $ Prop.projectivel (tripl f64i16) x + assert $ Prop.projectivel (tripr f64i16) y + assert $ Prop.projectiver (tripl f64i16) y + assert $ Prop.projectiver (tripr f64i16) x + +prop_connection_n5di16 :: Property +prop_connection_n5di16 = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f64 + x' <- forAll $ gen_pn5 f64 + y <- forAll $ gen_bnd $ G.integral (ri @Int16) + y' <- forAll $ gen_bnd $ G.integral (ri @Int16) + + let n5di16 = n5' f64i16 :: Trip (N5 Double) (Bounded Int16) + + assert $ Prop.connection (tripl n5di16) x y + assert $ Prop.connection (tripr n5di16) y x + assert $ Prop.closed (tripl n5di16) x + assert $ Prop.closed (tripr n5di16) y + assert $ Prop.kernel (tripl n5di16) y + assert $ Prop.kernel (tripr n5di16) x + assert $ Prop.monotonel (tripl n5di16) x x' + assert $ Prop.monotonel (tripr n5di16) y y' + assert $ Prop.monotoner (tripl n5di16) y y' + assert $ Prop.monotoner (tripr n5di16) x x' + assert $ Prop.projectivel (tripl n5di16) x + assert $ Prop.projectivel (tripr n5di16) y + assert $ Prop.projectiver (tripl n5di16) y + assert $ Prop.projectiver (tripr n5di16) x + +prop_connection_f64i32 :: Property +prop_connection_f64i32 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_ext $ G.integral (ri @Int32) + y' <- forAll $ gen_ext $ G.integral (ri @Int32) + + assert $ Prop.connection (tripl f64i32) x y + assert $ Prop.connection (tripr f64i32) y x + assert $ Prop.closed (tripl f64i32) x + assert $ Prop.closed (tripr f64i32) y + assert $ Prop.kernel (tripl f64i32) y + assert $ Prop.kernel (tripr f64i32) x + assert $ Prop.monotonel (tripl f64i32) x x' + assert $ Prop.monotonel (tripr f64i32) y y' + assert $ Prop.monotoner (tripl f64i32) y y' + assert $ Prop.monotoner (tripr f64i32) x x' + assert $ Prop.projectivel (tripl f64i32) x + assert $ Prop.projectivel (tripr f64i32) y + assert $ Prop.projectiver (tripl f64i32) y + assert $ Prop.projectiver (tripr f64i32) x + +prop_connection_n5di32 :: Property +prop_connection_n5di32 = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f64 + x' <- forAll $ gen_pn5 f64 + y <- forAll $ gen_bnd $ G.integral (ri @Int32) + y' <- forAll $ gen_bnd $ G.integral (ri @Int32) + + let n5di32 = n5' f64i32 :: Trip (N5 Double) (Bounded Int32) + + assert $ Prop.connection (tripl n5di32) x y + assert $ Prop.connection (tripr n5di32) y x + assert $ Prop.closed (tripl n5di32) x + assert $ Prop.closed (tripr n5di32) y + assert $ Prop.kernel (tripl n5di32) y + assert $ Prop.kernel (tripr n5di32) x + assert $ Prop.monotonel (tripl n5di32) x x' + assert $ Prop.monotonel (tripr n5di32) y y' + assert $ Prop.monotoner (tripl n5di32) y y' + assert $ Prop.monotoner (tripr n5di32) x x' + assert $ Prop.projectivel (tripl n5di32) x + assert $ Prop.projectivel (tripr n5di32) y + assert $ Prop.projectiver (tripl n5di32) y + assert $ Prop.projectiver (tripr n5di32) x + +prop_connections_f64 :: Property +prop_connections_f64 = withTests 1000 . property $ do + x <- forAll f64 + y <- forAll (gen_nan $ G.integral ri) + x' <- forAll f64 + y' <- forAll (gen_nan $ G.integral ri) + + assert $ Prop.connection f64i64 x y + assert $ Prop.connection i64f64 y x + assert $ Prop.closed f64i64 x + assert $ Prop.closed i64f64 y + assert $ Prop.kernel i64f64 x + assert $ Prop.kernel f64i64 y + assert $ Prop.monotonel f64i64 x x' + assert $ Prop.monotonel i64f64 y y' + assert $ Prop.monotoner f64i64 y y' + assert $ Prop.monotoner i64f64 x x' + assert $ Prop.projectivel f64i64 x + assert $ Prop.projectivel i64f64 y + assert $ Prop.projectiver i64f64 x + assert $ Prop.projectiver f64i64 y + + + +{- +prop_connections_n5d :: Property +prop_connections_n5d = withTests 1000 . property $ do + x <- forAll $ gen_pn5 f64 + y <- forAll (gen_bnd $ G.integral ri) + x' <- forAll $ gen_pn5 f64 + y' <- forAll (gen_bnd $ G.integral ri) + + assert $ Prop.connection f64i64 x y + assert $ Prop.connection i64f64 y x + assert $ Prop.closed f64i64 x + assert $ Prop.closed i64f64 y + assert $ Prop.kernel i64f64 x + assert $ Prop.kernel f64i64 y + assert $ Prop.monotonel f64i64 x x' + assert $ Prop.monotonel i64f64 y y' + assert $ Prop.monotoner f64i64 y y' + assert $ Prop.monotoner i64f64 x x' + assert $ Prop.projectivel f64i64 x + assert $ Prop.projectivel i64f64 y + assert $ Prop.projectiver i64f64 x + assert $ Prop.projectiver f64i64 y + +prop_prd_u32 :: Property +prop_prd_u32 = withTests 1000 . property $ do + x <- connl f32u32 <$> forAll f32 + y <- connl f32u32 <$> forAll f32 + z <- connl f32u32 <$> forAll f32 + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + +-} + +{- + +gen_sgn :: Gen Signed +gen_sgn = Signed <$> f32 + +gen_ugn :: Gen Unsigned +gen_ugn = (Unsigned . abs) <$> f32 + +prop_connections_f32u32 :: Property +prop_connections_f32u32 = withTests 1000 . property $ do + x <- forAll f32 + y <- Ulp32 <$> forAll (G.integral ri) + x' <- forAll f32 + y' <- Ulp32 <$> forAll (G.integral ri) + + assert $ Prop.connection f32u32 x y + assert $ Prop.connection u32f32 y x + assert $ Prop.monotonel f32u32 x x' + assert $ Prop.monotonel u32f32 y y' + assert $ Prop.monotoner f32u32 y y' + assert $ Prop.monotoner u32f32 x x' + assert $ Prop.closed f32u32 x + assert $ Prop.closed u32f32 y + assert $ Prop.kernel u32f32 x + assert $ Prop.kernel f32u32 y + +prop_connections_f32sgn :: Property +prop_connections_f32sgn = withTests 10000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_sgn + y' <- forAll $ gen_sgn + + assert $ Prop.connection f32sgn x y + assert $ Prop.monotonel f32sgn x x' + assert $ Prop.monotoner f32sgn y y' + assert $ Prop.closed f32sgn x + assert $ Prop.kernel f32sgn y + + + +prop_connections_f32w08 :: Property +prop_connections_f32w08 = withTests 10000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_nan $ G.integral (ri @Word8) + y' <- forAll $ gen_nan $ G.integral (ri @Word8) + + assert $ Prop.connection (tripl f32w08) x y + assert $ Prop.connection (tripr f32w08) y x + assert $ Prop.monotonel (tripl f32w08) x x' + assert $ Prop.monotonel (tripr f32w08) y y' + assert $ Prop.monotoner (tripl f32w08) y y' + assert $ Prop.monotoner (tripr f32w08) x x' + assert $ Prop.closed (tripl f32w08) x + assert $ Prop.closed (tripr f32w08) y + assert $ Prop.kernel (tripl f32w08) y + assert $ Prop.kernel (tripr f32w08) x +-} + + + +{- +prop_connections_f32w64 :: Property +prop_connections_f32w64 = withTests 1000 . property $ do + x <- forAll f32 + y <- forAll f32 + x' <- forAll f32 + y' <- forAll f32 + z <- forAll (gen_nan $ G.integral @_ @Word64 ri) + w <- forAll (gen_nan $ G.integral @_ @Word64 ri) + z' <- forAll (gen_nan $ G.integral @_ @Word64 ri) + w' <- forAll (gen_nan $ G.integral @_ @Word64 ri) + exy <- forAll $ G.element [Left x, Right y] + exy' <- forAll $ G.element [Left x', Right y'] + ezw <- forAll $ G.element [Left z, Right w] + ezw' <- forAll $ G.element [Left z', Right w'] + + assert $ Prop.closed (idx @Float) x --TODO in Index.hs + assert $ Prop.kernel (idx @Float) z + assert $ Prop.monotonel (idx @Float) x x' + assert $ Prop.monotoner (idx @Float) z z' + assert $ Prop.connection (idx @Float) x z + + assert $ Prop.closed (idx @(Float,Float)) (x,y) + assert $ Prop.kernel (idx @(Float,Float)) (z,w) + assert $ Prop.monotonel (idx @(Float,Float)) (x,y) (x',y') + assert $ Prop.monotoner (idx @(Float,Float)) (z,w) (z',w') + assert $ Prop.connection (idx @(Float,Float)) (x,y)(z,w) + + assert $ Prop.closed (idx @(Either Float Float)) exy + assert $ Prop.kernel (idx @(Either Float Float)) ezw + assert $ Prop.monotonel (idx @(Either Float Float)) exy exy' + assert $ Prop.monotoner (idx @(Either Float Float)) ezw ezw' + assert $ Prop.connection (idx @(Either Float Float)) exy ezw +-} + + + + +tests :: IO Bool +tests = checkParallel $$(discover) diff --git a/test/Test/Data/Connection/Int.hs b/test/Test/Data/Connection/Int.hs --- a/test/Test/Data/Connection/Int.hs +++ b/test/Test/Data/Connection/Int.hs @@ -1,28 +1,18 @@ {-# LANGUAGE TemplateHaskell #-} module Test.Data.Connection.Int where -import Data.Int -import Data.Word import Data.Connection import Data.Connection.Int -import Numeric.Natural -import qualified Data.Connection.Property as Prop - +import Data.Int +import Data.Word import Hedgehog +import Prelude hiding (Bounded) +import Test.Data.Connection +import qualified Data.Connection.Property as Prop import qualified Hedgehog.Gen as G -import qualified Hedgehog.Range as R -ri :: (Integral a, Bounded a) => Range a -ri = R.linearFrom 0 minBound maxBound - -rint :: Range Integer -rint = R.linearFrom 0 (- 2^127) (2^127) - -rnat :: Range Natural -rnat = R.linear 0 (2^128) - -prop_connections_int_wrd :: Property -prop_connections_int_wrd = withTests 1000 . property $ do +prop_connections :: Property +prop_connections = withTests 1000 . property $ do i08 <- forAll $ G.integral (ri @Int8) w08 <- forAll $ G.integral (ri @Word8) @@ -32,8 +22,12 @@ w32 <- forAll $ G.integral (ri @Word32) i64 <- forAll $ G.integral (ri @Int64) w64 <- forAll $ G.integral (ri @Word64) - int <- forAll $ G.integral rint - nat <- forAll $ G.integral rnat + ixx <- forAll $ G.integral (ri @Int) + wxx <- forAll $ G.integral (ri @Word) + int <- forAll $ G.integral ri' + nat <- forAll $ G.integral rn + mnt <- forAll $ gen_bot (G.integral ri') + inf <- forAll $ gen_bnd (G.integral ri') i08' <- forAll $ G.integral (ri @Int8) w08' <- forAll $ G.integral (ri @Word8) @@ -43,10 +37,16 @@ w32' <- forAll $ G.integral (ri @Word32) i64' <- forAll $ G.integral (ri @Int64) w64' <- forAll $ G.integral (ri @Word64) - int' <- forAll $ G.integral rint - nat' <- forAll $ G.integral rnat + ixx' <- forAll $ G.integral (ri @Int) + wxx' <- forAll $ G.integral (ri @Word) + int' <- forAll $ G.integral ri' + nat' <- forAll $ G.integral rn + mnt' <- forAll $ gen_bot (G.integral ri') + inf' <- forAll $ gen_bnd (G.integral ri') assert $ Prop.connection intnat int nat + assert $ Prop.connection natint nat mnt + assert $ Prop.connection ixxwxx ixx wxx assert $ Prop.connection i64w64 i64 w64 assert $ Prop.connection i64w64' i64 w64 assert $ Prop.connection i32i64 i32 i64 @@ -61,40 +61,18 @@ assert $ Prop.connection i08i16 i08 i16 assert $ Prop.connection i08w08 i08 w08 assert $ Prop.connection i08w08' i08 w08 - - assert $ Prop.monotone' intnat int int' - assert $ Prop.monotone' i64w64 i64 i64' - assert $ Prop.monotone' i64w64' i64 i64' - assert $ Prop.monotone' i32i64 i32 i32' - assert $ Prop.monotone' i32w32 i32 i32' - assert $ Prop.monotone' i32w32' i32 i32' - assert $ Prop.monotone' i16i64 i16 i16' - assert $ Prop.monotone' i16i32 i16 i16' - assert $ Prop.monotone' i16w16 i16 i16' - assert $ Prop.monotone' i16w16' i16 i16' - assert $ Prop.monotone' i08i64 i08 i08' - assert $ Prop.monotone' i08i32 i08 i08' - assert $ Prop.monotone' i08i16 i08 i08' - assert $ Prop.monotone' i08w08 i08 i08' - assert $ Prop.monotone' i08w08' i08 i08' - - assert $ Prop.monotone intnat nat nat' - assert $ Prop.monotone i64w64 w64 w64' - assert $ Prop.monotone i64w64' w64 w64' - assert $ Prop.monotone i32i64 i64 i64' - assert $ Prop.monotone i32w32 w32 w32' - assert $ Prop.monotone i32w32' w32 w32' - assert $ Prop.monotone i16i64 i64 i64' - assert $ Prop.monotone i16i32 i32 i32' - assert $ Prop.monotone i16w16 w16 w16' - assert $ Prop.monotone i16w16' w16 w16' - assert $ Prop.monotone i08i64 i64 i64' - assert $ Prop.monotone i08i32 i32 i32' - assert $ Prop.monotone i08i16 i16 i16' - assert $ Prop.monotone i08w08 w08 w08' - assert $ Prop.monotone i08w08' w08 w08' + assert $ Prop.connection (tripl i64int) i64 inf + assert $ Prop.connection (tripr i64int) inf i64 + assert $ Prop.connection (tripl i32int) i32 inf + assert $ Prop.connection (tripr i32int) inf i32 + assert $ Prop.connection (tripl i16int) i16 inf + assert $ Prop.connection (tripr i16int) inf i16 + assert $ Prop.connection (tripl i08int) i08 inf + assert $ Prop.connection (tripr i08int) inf i08 assert $ Prop.closed intnat int + assert $ Prop.closed natint nat + assert $ Prop.closed ixxwxx ixx assert $ Prop.closed i64w64 i64 assert $ Prop.closed i64w64' i64 assert $ Prop.closed i32i64 i32 @@ -109,8 +87,18 @@ assert $ Prop.closed i08i16 i08 assert $ Prop.closed i08w08 i08 assert $ Prop.closed i08w08' i08 + assert $ Prop.closed (tripl i64int) i64 + assert $ Prop.closed (tripr i64int) inf + assert $ Prop.closed (tripl i32int) i32 + assert $ Prop.closed (tripr i32int) inf + assert $ Prop.closed (tripl i16int) i16 + assert $ Prop.closed (tripr i16int) inf + assert $ Prop.closed (tripl i08int) i08 + assert $ Prop.closed (tripr i08int) inf assert $ Prop.kernel intnat nat + assert $ Prop.kernel natint mnt + assert $ Prop.kernel ixxwxx wxx assert $ Prop.kernel i64w64' w64 assert $ Prop.kernel i64w64 w64 assert $ Prop.kernel i32i64 i64 @@ -125,6 +113,118 @@ assert $ Prop.kernel i08i16 i16 assert $ Prop.kernel i08w08' w08 assert $ Prop.kernel i08w08 w08 + assert $ Prop.kernel (tripl i64int) inf + assert $ Prop.kernel (tripr i64int) i64 + assert $ Prop.kernel (tripl i32int) inf + assert $ Prop.kernel (tripr i32int) i32 + assert $ Prop.kernel (tripl i16int) inf + assert $ Prop.kernel (tripr i16int) i16 + assert $ Prop.kernel (tripl i08int) inf + assert $ Prop.kernel (tripr i08int) i08 + + assert $ Prop.monotonel intnat int int' + assert $ Prop.monotonel natint nat nat' + assert $ Prop.monotonel ixxwxx ixx ixx' + assert $ Prop.monotonel i64w64 i64 i64' + assert $ Prop.monotonel i64w64' i64 i64' + assert $ Prop.monotonel i32i64 i32 i32' + assert $ Prop.monotonel i32w32 i32 i32' + assert $ Prop.monotonel i32w32' i32 i32' + assert $ Prop.monotonel i16i64 i16 i16' + assert $ Prop.monotonel i16i32 i16 i16' + assert $ Prop.monotonel i16w16 i16 i16' + assert $ Prop.monotonel i16w16' i16 i16' + assert $ Prop.monotonel i08i64 i08 i08' + assert $ Prop.monotonel i08i32 i08 i08' + assert $ Prop.monotonel i08i16 i08 i08' + assert $ Prop.monotonel i08w08 i08 i08' + assert $ Prop.monotonel i08w08' i08 i08' + assert $ Prop.monotonel (tripl i64int) i64 i64' + assert $ Prop.monotonel (tripr i64int) inf inf' + assert $ Prop.monotonel (tripl i32int) i32 i32' + assert $ Prop.monotonel (tripr i32int) inf inf' + assert $ Prop.monotonel (tripl i16int) i16 i16' + assert $ Prop.monotonel (tripr i16int) inf inf' + assert $ Prop.monotonel (tripl i08int) i08 i08' + assert $ Prop.monotonel (tripr i08int) inf inf' + + assert $ Prop.monotoner intnat nat nat' + assert $ Prop.monotoner natint mnt mnt' + assert $ Prop.monotoner ixxwxx wxx wxx' + assert $ Prop.monotoner i64w64 w64 w64' + assert $ Prop.monotoner i64w64' w64 w64' + assert $ Prop.monotoner i32i64 i64 i64' + assert $ Prop.monotoner i32w32 w32 w32' + assert $ Prop.monotoner i32w32' w32 w32' + assert $ Prop.monotoner i16i64 i64 i64' + assert $ Prop.monotoner i16i32 i32 i32' + assert $ Prop.monotoner i16w16 w16 w16' + assert $ Prop.monotoner i16w16' w16 w16' + assert $ Prop.monotoner i08i64 i64 i64' + assert $ Prop.monotoner i08i32 i32 i32' + assert $ Prop.monotoner i08i16 i16 i16' + assert $ Prop.monotoner i08w08 w08 w08' + assert $ Prop.monotoner i08w08' w08 w08' + assert $ Prop.monotoner (tripl i64int) inf inf' + assert $ Prop.monotoner (tripr i64int) i64 i64' + assert $ Prop.monotoner (tripl i32int) inf inf' + assert $ Prop.monotoner (tripr i32int) i32 i32' + assert $ Prop.monotoner (tripl i16int) inf inf' + assert $ Prop.monotoner (tripr i16int) i16 i16' + assert $ Prop.monotoner (tripl i08int) inf inf' + assert $ Prop.monotoner (tripr i08int) i08 i08' + + assert $ Prop.projectivel intnat int + assert $ Prop.projectivel natint nat + assert $ Prop.projectivel ixxwxx ixx + assert $ Prop.projectivel i64w64 i64 + assert $ Prop.projectivel i64w64' i64 + assert $ Prop.projectivel i32i64 i32 + assert $ Prop.projectivel i32w32 i32 + assert $ Prop.projectivel i32w32' i32 + assert $ Prop.projectivel i16i64 i16 + assert $ Prop.projectivel i16i32 i16 + assert $ Prop.projectivel i16w16 i16 + assert $ Prop.projectivel i16w16' i16 + assert $ Prop.projectivel i08i64 i08 + assert $ Prop.projectivel i08i32 i08 + assert $ Prop.projectivel i08i16 i08 + assert $ Prop.projectivel i08w08 i08 + assert $ Prop.projectivel i08w08' i08 + assert $ Prop.projectivel (tripl i64int) i64 + assert $ Prop.projectivel (tripr i64int) inf + assert $ Prop.projectivel (tripl i32int) i32 + assert $ Prop.projectivel (tripr i32int) inf + assert $ Prop.projectivel (tripl i16int) i16 + assert $ Prop.projectivel (tripr i16int) inf + assert $ Prop.projectivel (tripl i08int) i08 + assert $ Prop.projectivel (tripr i08int) inf + + assert $ Prop.projectiver intnat nat + assert $ Prop.projectiver natint mnt + assert $ Prop.projectiver ixxwxx wxx + assert $ Prop.projectiver i64w64' w64 + assert $ Prop.projectiver i64w64 w64 + assert $ Prop.projectiver i32i64 i64 + assert $ Prop.projectiver i32w32' w32 + assert $ Prop.projectiver i32w32 w32 + assert $ Prop.projectiver i16i64 i64 + assert $ Prop.projectiver i16i32 i32 + assert $ Prop.projectiver i16w16' w16 + assert $ Prop.projectiver i16w16 w16 + assert $ Prop.projectiver i08i64 i64 + assert $ Prop.projectiver i08i32 i32 + assert $ Prop.projectiver i08i16 i16 + assert $ Prop.projectiver i08w08' w08 + assert $ Prop.projectiver i08w08 w08 + assert $ Prop.projectiver (tripl i64int) inf + assert $ Prop.projectiver (tripr i64int) i64 + assert $ Prop.projectiver (tripl i32int) inf + assert $ Prop.projectiver (tripr i32int) i32 + assert $ Prop.projectiver (tripl i16int) inf + assert $ Prop.projectiver (tripr i16int) i16 + assert $ Prop.projectiver (tripl i08int) inf + assert $ Prop.projectiver (tripr i08int) i08 tests :: IO Bool tests = checkParallel $$(discover) diff --git a/test/Test/Data/Connection/Ratio.hs b/test/Test/Data/Connection/Ratio.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Connection/Ratio.hs @@ -0,0 +1,303 @@ +{-# LANGUAGE TemplateHaskell #-} +module Test.Data.Connection.Ratio where + +import Data.Connection +import Data.Connection.Ratio +import Data.Int +import Data.Prd.Nan +import Data.Word +import Hedgehog +import Test.Data.Connection +import qualified Data.Connection.Property as Prop +import qualified Hedgehog.Gen as G + +prop_connection_ratord :: Property +prop_connection_ratord = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_nan ord + y' <- forAll $ gen_nan ord + + let ratord = fldord :: Trip Rational (Nan Ordering) + + assert $ Prop.connection (tripl ratord) x y + assert $ Prop.connection (tripr ratord) y x + assert $ Prop.closed (tripl ratord) x + assert $ Prop.closed (tripr ratord) y + assert $ Prop.kernel (tripl ratord) y + assert $ Prop.kernel (tripr ratord) x + assert $ Prop.monotonel (tripl ratord) x x' + assert $ Prop.monotonel (tripr ratord) y y' + assert $ Prop.monotoner (tripl ratord) y y' + assert $ Prop.monotoner (tripr ratord) x x' + assert $ Prop.projectivel (tripl ratord) x + assert $ Prop.projectivel (tripr ratord) y + assert $ Prop.projectiver (tripl ratord) y + assert $ Prop.projectiver (tripr ratord) x + +prop_connection_ratf32 :: Property +prop_connection_ratf32 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll f32 + y' <- forAll f32 + + assert $ Prop.connection (tripl ratf32) x y + assert $ Prop.connection (tripr ratf32) y x + assert $ Prop.closed (tripl ratf32) x + assert $ Prop.closed (tripr ratf32) y + assert $ Prop.kernel (tripl ratf32) y + assert $ Prop.kernel (tripr ratf32) x + assert $ Prop.monotoner (tripl ratf32) y y' + assert $ Prop.monotoner (tripr ratf32) x x' + assert $ Prop.monotonel (tripl ratf32) x x' + assert $ Prop.monotonel (tripr ratf32) y y' + assert $ Prop.projectivel (tripl ratf32) x + assert $ Prop.projectivel (tripr ratf32) y + assert $ Prop.projectiver (tripl ratf32) y + assert $ Prop.projectiver (tripr ratf32) x + +prop_connection_ratf64 :: Property +prop_connection_ratf64 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll f64 + y' <- forAll f64 + + assert $ Prop.connection (tripl ratf64) x y + assert $ Prop.connection (tripr ratf64) y x + assert $ Prop.closed (tripl ratf64) x + assert $ Prop.closed (tripr ratf64) y + assert $ Prop.kernel (tripl ratf64) y + assert $ Prop.kernel (tripr ratf64) x + assert $ Prop.monotoner (tripl ratf64) y y' + assert $ Prop.monotoner (tripr ratf64) x x' + assert $ Prop.monotonel (tripl ratf64) x x' + assert $ Prop.monotonel (tripr ratf64) y y' + assert $ Prop.projectivel (tripl ratf64) x + assert $ Prop.projectivel (tripr ratf64) y + assert $ Prop.projectiver (tripl ratf64) y + assert $ Prop.projectiver (tripr ratf64) x + +prop_connection_rati08 :: Property +prop_connection_rati08 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_ext $ G.integral (ri @Int8) + y' <- forAll $ gen_ext $ G.integral (ri @Int8) + + assert $ Prop.connection (tripl rati08) x y + assert $ Prop.connection (tripr rati08) y x + assert $ Prop.closed (tripl rati08) x + assert $ Prop.closed (tripr rati08) y + assert $ Prop.kernel (tripl rati08) y + assert $ Prop.kernel (tripr rati08) x + assert $ Prop.monotonel (tripl rati08) x x' + assert $ Prop.monotonel (tripr rati08) y y' + assert $ Prop.monotoner (tripl rati08) y y' + assert $ Prop.monotoner (tripr rati08) x x' + assert $ Prop.projectivel (tripl rati08) x + assert $ Prop.projectivel (tripr rati08) y + assert $ Prop.projectiver (tripl rati08) y + assert $ Prop.projectiver (tripr rati08) x + +prop_connection_rati16 :: Property +prop_connection_rati16 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_ext $ G.integral (ri @Int16) + y' <- forAll $ gen_ext $ G.integral (ri @Int16) + + assert $ Prop.connection (tripl rati16) x y + assert $ Prop.connection (tripr rati16) y x + assert $ Prop.closed (tripl rati16) x + assert $ Prop.closed (tripr rati16) y + assert $ Prop.kernel (tripl rati16) y + assert $ Prop.kernel (tripr rati16) x + assert $ Prop.monotonel (tripl rati16) x x' + assert $ Prop.monotonel (tripr rati16) y y' + assert $ Prop.monotoner (tripl rati16) y y' + assert $ Prop.monotoner (tripr rati16) x x' + assert $ Prop.projectivel (tripl rati16) x + assert $ Prop.projectivel (tripr rati16) y + assert $ Prop.projectiver (tripl rati16) y + assert $ Prop.projectiver (tripr rati16) x + +prop_connection_rati32 :: Property +prop_connection_rati32 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_ext $ G.integral (ri @Int32) + y' <- forAll $ gen_ext $ G.integral (ri @Int32) + + assert $ Prop.connection (tripl rati32) x y + assert $ Prop.connection (tripr rati32) y x + assert $ Prop.closed (tripl rati32) x + assert $ Prop.closed (tripr rati32) y + assert $ Prop.kernel (tripl rati32) y + assert $ Prop.kernel (tripr rati32) x + assert $ Prop.monotonel (tripl rati32) x x' + assert $ Prop.monotonel (tripr rati32) y y' + assert $ Prop.monotoner (tripl rati32) y y' + assert $ Prop.monotoner (tripr rati32) x x' + assert $ Prop.projectivel (tripl rati32) x + assert $ Prop.projectivel (tripr rati32) y + assert $ Prop.projectiver (tripl rati32) y + assert $ Prop.projectiver (tripr rati32) x + +prop_connection_rati64 :: Property +prop_connection_rati64 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_ext $ G.integral (ri @Int64) + y' <- forAll $ gen_ext $ G.integral (ri @Int64) + + assert $ Prop.connection (tripl rati64) x y + assert $ Prop.connection (tripr rati64) y x + assert $ Prop.closed (tripl rati64) x + assert $ Prop.closed (tripr rati64) y + assert $ Prop.kernel (tripl rati64) y + assert $ Prop.kernel (tripr rati64) x + assert $ Prop.monotonel (tripl rati64) x x' + assert $ Prop.monotonel (tripr rati64) y y' + assert $ Prop.monotoner (tripl rati64) y y' + assert $ Prop.monotoner (tripr rati64) x x' + assert $ Prop.projectivel (tripl rati64) x + assert $ Prop.projectivel (tripr rati64) y + assert $ Prop.projectiver (tripl rati64) y + assert $ Prop.projectiver (tripr rati64) x + +prop_connection_ratint :: Property +prop_connection_ratint = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_ext $ G.integral ri' + y' <- forAll $ gen_ext $ G.integral ri' + + assert $ Prop.connection (tripl ratint) x y + assert $ Prop.connection (tripr ratint) y x + assert $ Prop.closed (tripl ratint) x + assert $ Prop.closed (tripr ratint) y + assert $ Prop.kernel (tripl ratint) y + assert $ Prop.kernel (tripr ratint) x + assert $ Prop.monotonel (tripl ratint) x x' + assert $ Prop.monotonel (tripr ratint) y y' + assert $ Prop.monotoner (tripl ratint) y y' + assert $ Prop.monotoner (tripr ratint) x x' + assert $ Prop.projectivel (tripl ratint) x + assert $ Prop.projectivel (tripr ratint) y + assert $ Prop.projectiver (tripl ratint) y + assert $ Prop.projectiver (tripr ratint) x + +prop_connection_ratw08 :: Property +prop_connection_ratw08 = withTests 1000 . property $ do + x <- forAll pos + x' <- forAll pos + y <- forAll $ gen_lft $ G.integral (ri @Word8) + y' <- forAll $ gen_lft $ G.integral (ri @Word8) + + assert $ Prop.connection (tripl ratw08) x y + assert $ Prop.connection (tripr ratw08) y x + assert $ Prop.closed (tripl ratw08) x + assert $ Prop.closed (tripr ratw08) y + assert $ Prop.kernel (tripl ratw08) y + assert $ Prop.kernel (tripr ratw08) x + assert $ Prop.monotonel (tripl ratw08) x x' + assert $ Prop.monotonel (tripr ratw08) y y' + assert $ Prop.monotoner (tripl ratw08) y y' + assert $ Prop.monotoner (tripr ratw08) x x' + assert $ Prop.projectivel (tripl ratw08) x + assert $ Prop.projectivel (tripr ratw08) y + assert $ Prop.projectiver (tripl ratw08) y + assert $ Prop.projectiver (tripr ratw08) x + +prop_connection_ratw16 :: Property +prop_connection_ratw16 = withTests 1000 . property $ do + x <- forAll pos + x' <- forAll pos + y <- forAll $ gen_lft $ G.integral (ri @Word16) + y' <- forAll $ gen_lft $ G.integral (ri @Word16) + + assert $ Prop.connection (tripl ratw16) x y + assert $ Prop.connection (tripr ratw16) y x + assert $ Prop.closed (tripl ratw16) x + assert $ Prop.closed (tripr ratw16) y + assert $ Prop.kernel (tripl ratw16) y + assert $ Prop.kernel (tripr ratw16) x + assert $ Prop.monotonel (tripl ratw16) x x' + assert $ Prop.monotonel (tripr ratw16) y y' + assert $ Prop.monotoner (tripl ratw16) y y' + assert $ Prop.monotoner (tripr ratw16) x x' + assert $ Prop.projectivel (tripl ratw16) x + assert $ Prop.projectivel (tripr ratw16) y + assert $ Prop.projectiver (tripl ratw16) y + assert $ Prop.projectiver (tripr ratw16) x + +prop_connection_ratw32 :: Property +prop_connection_ratw32 = withTests 1000 . property $ do + x <- forAll pos + x' <- forAll pos + y <- forAll $ gen_lft $ G.integral (ri @Word32) + y' <- forAll $ gen_lft $ G.integral (ri @Word32) + + assert $ Prop.connection (tripl ratw32) x y + assert $ Prop.connection (tripr ratw32) y x + assert $ Prop.closed (tripl ratw32) x + assert $ Prop.closed (tripr ratw32) y + assert $ Prop.kernel (tripl ratw32) y + assert $ Prop.kernel (tripr ratw32) x + assert $ Prop.monotonel (tripl ratw32) x x' + assert $ Prop.monotonel (tripr ratw32) y y' + assert $ Prop.monotoner (tripl ratw32) y y' + assert $ Prop.monotoner (tripr ratw32) x x' + assert $ Prop.projectivel (tripl ratw32) x + assert $ Prop.projectivel (tripr ratw32) y + assert $ Prop.projectiver (tripl ratw32) y + assert $ Prop.projectiver (tripr ratw32) x + +prop_connection_ratw64 :: Property +prop_connection_ratw64 = withTests 1000 . property $ do + x <- forAll pos + x' <- forAll pos + y <- forAll $ gen_lft $ G.integral (ri @Word64) + y' <- forAll $ gen_lft $ G.integral (ri @Word64) + + assert $ Prop.connection (tripl ratw64) x y + assert $ Prop.connection (tripr ratw64) y x + assert $ Prop.closed (tripl ratw64) x + assert $ Prop.closed (tripr ratw64) y + assert $ Prop.kernel (tripl ratw64) y + assert $ Prop.kernel (tripr ratw64) x + assert $ Prop.monotonel (tripl ratw64) x x' + assert $ Prop.monotonel (tripr ratw64) y y' + assert $ Prop.monotoner (tripl ratw64) y y' + assert $ Prop.monotoner (tripr ratw64) x x' + assert $ Prop.projectivel (tripl ratw64) x + assert $ Prop.projectivel (tripr ratw64) y + assert $ Prop.projectiver (tripl ratw64) y + assert $ Prop.projectiver (tripr ratw64) x + +prop_connection_ratnat :: Property +prop_connection_ratnat = withTests 1000 . property $ do + x <- forAll pos + x' <- forAll pos + y <- forAll $ gen_lft $ G.integral rn + y' <- forAll $ gen_lft $ G.integral rn + + assert $ Prop.connection (tripl ratnat) x y + assert $ Prop.connection (tripr ratnat) y x + assert $ Prop.closed (tripl ratnat) x + assert $ Prop.closed (tripr ratnat) y + assert $ Prop.kernel (tripl ratnat) y + assert $ Prop.kernel (tripr ratnat) x + assert $ Prop.monotonel (tripl ratnat) x x' + assert $ Prop.monotonel (tripr ratnat) y y' + assert $ Prop.monotoner (tripl ratnat) y y' + assert $ Prop.monotoner (tripr ratnat) x x' + assert $ Prop.projectivel (tripl ratnat) x + assert $ Prop.projectivel (tripr ratnat) y + assert $ Prop.projectiver (tripl ratnat) y + assert $ Prop.projectiver (tripr ratnat) x + +tests :: IO Bool +tests = checkParallel $$(discover) diff --git a/test/Test/Data/Connection/Word.hs b/test/Test/Data/Connection/Word.hs --- a/test/Test/Data/Connection/Word.hs +++ b/test/Test/Data/Connection/Word.hs @@ -3,23 +3,17 @@ import Data.Int import Data.Word -import Data.Connection import Data.Connection.Word -import Numeric.Natural +import Test.Data.Connection import qualified Data.Connection.Property as Prop import Hedgehog import qualified Hedgehog.Gen as G import qualified Hedgehog.Range as R -ri :: (Integral a, Bounded a) => Range a -ri = R.linearFrom 0 minBound maxBound -rnat :: Range Natural -rnat = R.linear 0 (2^128) - -prop_connections_wrd_int :: Property -prop_connections_wrd_int = withTests 1000 . property $ do +prop_connections :: Property +prop_connections = withTests 1000 . property $ do i08 <- forAll $ G.integral (ri @Int8) w08 <- forAll $ G.integral (ri @Word8) @@ -29,7 +23,7 @@ w32 <- forAll $ G.integral (ri @Word32) i64 <- forAll $ G.integral (ri @Int64) w64 <- forAll $ G.integral (ri @Word64) - nat <- forAll $ G.integral rnat + nat <- forAll $ G.integral rn i08' <- forAll $ G.integral (ri @Int8) w08' <- forAll $ G.integral (ri @Word8) @@ -39,7 +33,7 @@ w32' <- forAll $ G.integral (ri @Word32) i64' <- forAll $ G.integral (ri @Int64) w64' <- forAll $ G.integral (ri @Word64) - nat' <- forAll $ G.integral rnat + nat' <- forAll $ G.integral rn assert $ Prop.connection w64nat w64 nat assert $ Prop.connection w64i64 w64 i64 @@ -56,36 +50,6 @@ assert $ Prop.connection w08w16 w08 w16 assert $ Prop.connection w08i08 w08 i08 - assert $ Prop.monotone' w64nat w64 w64' - assert $ Prop.monotone' w64i64 w64 w64' - assert $ Prop.monotone' w32nat w32 w32' - assert $ Prop.monotone' w32w64 w32 w32' - assert $ Prop.monotone' w32i32 w32 w32' - assert $ Prop.monotone' w16nat w16 w16' - assert $ Prop.monotone' w16w64 w16 w16' - assert $ Prop.monotone' w16w32 w16 w16' - assert $ Prop.monotone' w16i16 w16 w16' - assert $ Prop.monotone' w08nat w08 w08' - assert $ Prop.monotone' w08w64 w08 w08' - assert $ Prop.monotone' w08w32 w08 w08' - assert $ Prop.monotone' w08w16 w08 w08' - assert $ Prop.monotone' w08i08 w08 w08' - - assert $ Prop.monotone w64nat nat nat' - assert $ Prop.monotone w64i64 i64 i64' - assert $ Prop.monotone w32nat nat nat' - assert $ Prop.monotone w32w64 w64 w64' - assert $ Prop.monotone w32i32 i32 i32' - assert $ Prop.monotone w16nat nat nat' - assert $ Prop.monotone w16w64 w64 w64' - assert $ Prop.monotone w16w32 w32 w32' - assert $ Prop.monotone w16i16 i16 i16' - assert $ Prop.monotone w08nat nat nat' - assert $ Prop.monotone w08w64 w64 w64' - assert $ Prop.monotone w08w32 w32 w32' - assert $ Prop.monotone w08w16 w16 w16' - assert $ Prop.monotone w08i08 i08 i08' - assert $ Prop.closed w64nat w64 assert $ Prop.closed w64i64 w64 assert $ Prop.closed w32nat w32 @@ -115,6 +79,66 @@ assert $ Prop.kernel w08w32 w32 assert $ Prop.kernel w08w16 w16 assert $ Prop.kernel w08i08 i08 + + assert $ Prop.monotonel w64nat w64 w64' + assert $ Prop.monotonel w64i64 w64 w64' + assert $ Prop.monotonel w32nat w32 w32' + assert $ Prop.monotonel w32w64 w32 w32' + assert $ Prop.monotonel w32i32 w32 w32' + assert $ Prop.monotonel w16nat w16 w16' + assert $ Prop.monotonel w16w64 w16 w16' + assert $ Prop.monotonel w16w32 w16 w16' + assert $ Prop.monotonel w16i16 w16 w16' + assert $ Prop.monotonel w08nat w08 w08' + assert $ Prop.monotonel w08w64 w08 w08' + assert $ Prop.monotonel w08w32 w08 w08' + assert $ Prop.monotonel w08w16 w08 w08' + assert $ Prop.monotonel w08i08 w08 w08' + + assert $ Prop.monotoner w64nat nat nat' + assert $ Prop.monotoner w64i64 i64 i64' + assert $ Prop.monotoner w32nat nat nat' + assert $ Prop.monotoner w32w64 w64 w64' + assert $ Prop.monotoner w32i32 i32 i32' + assert $ Prop.monotoner w16nat nat nat' + assert $ Prop.monotoner w16w64 w64 w64' + assert $ Prop.monotoner w16w32 w32 w32' + assert $ Prop.monotoner w16i16 i16 i16' + assert $ Prop.monotoner w08nat nat nat' + assert $ Prop.monotoner w08w64 w64 w64' + assert $ Prop.monotoner w08w32 w32 w32' + assert $ Prop.monotoner w08w16 w16 w16' + assert $ Prop.monotoner w08i08 i08 i08' + + assert $ Prop.projectivel w64nat w64 + assert $ Prop.projectivel w64i64 w64 + assert $ Prop.projectivel w32nat w32 + assert $ Prop.projectivel w32w64 w32 + assert $ Prop.projectivel w32i32 w32 + assert $ Prop.projectivel w16nat w16 + assert $ Prop.projectivel w16w64 w16 + assert $ Prop.projectivel w16w32 w16 + assert $ Prop.projectivel w16i16 w16 + assert $ Prop.projectivel w08nat w08 + assert $ Prop.projectivel w08w64 w08 + assert $ Prop.projectivel w08w32 w08 + assert $ Prop.projectivel w08w16 w08 + assert $ Prop.projectivel w08i08 w08 + + assert $ Prop.projectiver w64nat nat + assert $ Prop.projectiver w64i64 i64 + assert $ Prop.projectiver w32nat nat + assert $ Prop.projectiver w32w64 w64 + assert $ Prop.projectiver w32i32 i32 + assert $ Prop.projectiver w16nat nat + assert $ Prop.projectiver w16w64 w64 + assert $ Prop.projectiver w16w32 w32 + assert $ Prop.projectiver w16i16 i16 + assert $ Prop.projectiver w08nat nat + assert $ Prop.projectiver w08w64 w64 + assert $ Prop.projectiver w08w32 w32 + assert $ Prop.projectiver w08w16 w16 + assert $ Prop.projectiver w08i08 i08 tests :: IO Bool tests = checkParallel $$(discover) diff --git a/test/Test/Data/Float.hs b/test/Test/Data/Float.hs deleted file mode 100644 --- a/test/Test/Data/Float.hs +++ /dev/null @@ -1,157 +0,0 @@ -{-# LANGUAGE TemplateHaskell #-} -module Test.Data.Float where - -import Data.Prd.Nan -import Data.Int -import Data.Word -import Data.Float -import Data.Prd -import Data.Connection ---import Data.Connection.Filter -import Data.Connection.Float - -import qualified Data.Prd.Property as Prop -import qualified Data.Connection.Property as Prop - -import Hedgehog -import qualified Hedgehog.Gen as G -import qualified Hedgehog.Range as R - -ri :: (Integral a, Bounded a) => Range a -ri = R.exponentialFrom 0 minBound maxBound - -rf :: Range Float -rf = R.exponentialFloatFrom 0 (-3.4028235e38) 3.4028235e38 - -gen_flt32' :: Gen Float -gen_flt32' = G.frequency [(99, gen_flt32), (1, G.element [nInf, pInf, aNan])] - -gen_flt32 :: Gen Float -gen_flt32 = G.float rf - -gen_nan :: Gen a -> Gen (Nan a) -gen_nan gen = G.frequency [(9, Def <$> gen), (1, pure Nan)] - -prop_prd_ulp32 :: Property -prop_prd_ulp32 = withTests 1000 . property $ do - x <- connl f32u32 <$> forAll gen_flt32' - y <- connl f32u32 <$> forAll gen_flt32' - z <- connl f32u32 <$> forAll gen_flt32' - assert $ Prop.reflexive_eq x - assert $ Prop.reflexive_le x - assert $ Prop.irreflexive_lt x - assert $ Prop.symmetric x y - assert $ Prop.asymmetric x y - assert $ Prop.antisymmetric x y - assert $ Prop.transitive_lt x y z - assert $ Prop.transitive_le x y z - assert $ Prop.transitive_eq x y z - -prop_prd_flt32 :: Property -prop_prd_flt32 = withTests 1000 . property $ do - x <- forAll gen_flt32' - y <- forAll gen_flt32' - z <- forAll gen_flt32' - w <- forAll gen_flt32' - assert $ Prop.reflexive_eq x - assert $ Prop.reflexive_le x - assert $ Prop.irreflexive_lt x - assert $ Prop.symmetric x y - assert $ Prop.asymmetric x y - assert $ Prop.antisymmetric x y - assert $ Prop.transitive_lt x y z - assert $ Prop.transitive_le x y z - assert $ Prop.transitive_eq x y z - assert $ Prop.chain_22 x y z w - --assert $ Prop.chain_31 x y z w - -{- -prop_semigroup_float :: Property -prop_semigroup_float = withTests 20000 $ property $ do - x <- forAll gen_flt32' - y <- forAll gen_flt32' - z <- forAll gen_flt32' - - assert $ Prop.neutral_addition' x - assert $ Prop.associative_addition (abs x) (abs y) (abs z) - -prop_connections_flt32_wrd64 :: Property -prop_connections_flt32_wrd64 = withTests 1000 . property $ do - x <- forAll gen_flt32' - y <- forAll gen_flt32' - x' <- forAll gen_flt32' - y' <- forAll gen_flt32' - z <- forAll (gen_nan $ G.integral @_ @Word64 ri) - w <- forAll (gen_nan $ G.integral @_ @Word64 ri) - z' <- forAll (gen_nan $ G.integral @_ @Word64 ri) - w' <- forAll (gen_nan $ G.integral @_ @Word64 ri) - exy <- forAll $ G.element [Left x, Right y] - exy' <- forAll $ G.element [Left x', Right y'] - ezw <- forAll $ G.element [Left z, Right w] - ezw' <- forAll $ G.element [Left z', Right w'] - - assert $ Prop.closed (idx @Float) x --TODO in Index.hs - assert $ Prop.kernel (idx @Float) z - assert $ Prop.monotone' (idx @Float) x x' - assert $ Prop.monotone (idx @Float) z z' - assert $ Prop.connection (idx @Float) x z - - assert $ Prop.closed (idx @(Float,Float)) (x,y) - assert $ Prop.kernel (idx @(Float,Float)) (z,w) - assert $ Prop.monotone' (idx @(Float,Float)) (x,y) (x',y') - assert $ Prop.monotone (idx @(Float,Float)) (z,w) (z',w') - assert $ Prop.connection (idx @(Float,Float)) (x,y)(z,w) - - assert $ Prop.closed (idx @(Either Float Float)) exy - assert $ Prop.kernel (idx @(Either Float Float)) ezw - assert $ Prop.monotone' (idx @(Either Float Float)) exy exy' - assert $ Prop.monotone (idx @(Either Float Float)) ezw ezw' - assert $ Prop.connection (idx @(Either Float Float)) exy ezw --} - -prop_connections_flt32_ulp32 :: Property -prop_connections_flt32_ulp32 = withTests 1000 . property $ do - x <- forAll gen_flt32' - y <- Ulp32 <$> forAll (G.integral ri) - x' <- forAll gen_flt32' - y' <- Ulp32 <$> forAll (G.integral ri) - - assert $ Prop.connection f32u32 x y - assert $ Prop.connection u32f32 y x - - assert $ Prop.monotone' f32u32 x x' - assert $ Prop.monotone' u32f32 y y' - - assert $ Prop.monotone f32u32 y y' - assert $ Prop.monotone u32f32 x x' - - assert $ Prop.closed f32u32 x - assert $ Prop.closed u32f32 y - - assert $ Prop.kernel u32f32 x - assert $ Prop.kernel f32u32 y - -prop_connections_flt32_int64 :: Property -prop_connections_flt32_int64 = withTests 1000 . property $ do - x <- forAll gen_flt32' - y <- forAll (gen_nan $ G.integral ri) - x' <- forAll gen_flt32' - y' <- forAll (gen_nan $ G.integral ri) - - assert $ Prop.connection f32i32 x y - assert $ Prop.connection i32f32 y x - - assert $ Prop.monotone' f32i32 x x' - assert $ Prop.monotone' i32f32 y y' - - assert $ Prop.monotone f32i32 y y' - assert $ Prop.monotone i32f32 x x' - - assert $ Prop.closed f32i32 x - assert $ Prop.closed i32f32 y - - assert $ Prop.kernel i32f32 x - assert $ Prop.kernel f32i32 y - -tests :: IO Bool -tests = checkParallel $$(discover) diff --git a/test/Test/Data/Prd.hs b/test/Test/Data/Prd.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Prd.hs @@ -0,0 +1,337 @@ +{-# LANGUAGE TemplateHaskell #-} +module Test.Data.Prd where + +import Data.Int +import Data.Word +import Test.Data.Connection +import Hedgehog + +import qualified Data.Prd.Property as Prop +import qualified Hedgehog.Gen as G + +prop_prd_i08 :: Property +prop_prd_i08 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Int8) + y <- forAll $ G.integral (ri @Int8) + z <- forAll $ G.integral (ri @Int8) + w <- forAll $ G.integral (ri @Int8) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_i16 :: Property +prop_prd_i16 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Int16) + y <- forAll $ G.integral (ri @Int16) + z <- forAll $ G.integral (ri @Int16) + w <- forAll $ G.integral (ri @Int16) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_i32 :: Property +prop_prd_i32 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Int32) + y <- forAll $ G.integral (ri @Int32) + z <- forAll $ G.integral (ri @Int32) + w <- forAll $ G.integral (ri @Int32) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_i64 :: Property +prop_prd_i64 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Int64) + y <- forAll $ G.integral (ri @Int64) + z <- forAll $ G.integral (ri @Int64) + w <- forAll $ G.integral (ri @Int64) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_ixx :: Property +prop_prd_ixx = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Int) + y <- forAll $ G.integral (ri @Int) + z <- forAll $ G.integral (ri @Int) + w <- forAll $ G.integral (ri @Int) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_int :: Property +prop_prd_int = withTests 1000 . property $ do + x <- forAll $ G.integral ri' + y <- forAll $ G.integral ri' + z <- forAll $ G.integral ri' + w <- forAll $ G.integral ri' + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_w08 :: Property +prop_prd_w08 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Word8) + y <- forAll $ G.integral (ri @Word8) + z <- forAll $ G.integral (ri @Word8) + w <- forAll $ G.integral (ri @Word8) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_w16 :: Property +prop_prd_w16 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Word16) + y <- forAll $ G.integral (ri @Word16) + z <- forAll $ G.integral (ri @Word16) + w <- forAll $ G.integral (ri @Word16) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_w32 :: Property +prop_prd_w32 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Word32) + y <- forAll $ G.integral (ri @Word32) + z <- forAll $ G.integral (ri @Word32) + w <- forAll $ G.integral (ri @Word32) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_w64 :: Property +prop_prd_w64 = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Word64) + y <- forAll $ G.integral (ri @Word64) + z <- forAll $ G.integral (ri @Word64) + w <- forAll $ G.integral (ri @Word64) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_wxx :: Property +prop_prd_wxx = withTests 1000 . property $ do + x <- forAll $ G.integral (ri @Word) + y <- forAll $ G.integral (ri @Word) + z <- forAll $ G.integral (ri @Word) + w <- forAll $ G.integral (ri @Word) + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +prop_prd_nat :: Property +prop_prd_nat = withTests 1000 . property $ do + x <- forAll $ G.integral rn + y <- forAll $ G.integral rn + z <- forAll $ G.integral rn + w <- forAll $ G.integral rn + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + assert $ Prop.chain_31 x y z w + +{- +w = (-61190296498818470224935979790417002496) % 1 +y = 784675940593409576367211913280487424 % 1 +z = 44351588178463768880997328738947432448 % 1 +w = 0 % 0 +Prop.chain_31 x y z w +-} + +prop_prd_rat :: Property +prop_prd_rat = withTests 1000 . property $ do + x <- forAll rat + y <- forAll rat + z <- forAll rat + w <- forAll rat + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + +prop_prd_pos :: Property +prop_prd_pos = withTests 1000 . property $ do + x <- forAll pos + y <- forAll pos + z <- forAll pos + w <- forAll pos + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + +prop_prd_f32 :: Property +prop_prd_f32 = withTests 1000 . property $ do + x <- forAll f32 + y <- forAll f32 + z <- forAll f32 + w <- forAll f32 + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + +prop_prd_f64 :: Property +prop_prd_f64 = withTests 1000 . property $ do + x <- forAll f64 + y <- forAll f64 + z <- forAll f64 + w <- forAll f64 + assert $ Prop.consistent x y + assert $ Prop.consistent z w + assert $ Prop.reflexive_eq x + assert $ Prop.reflexive_le x + assert $ Prop.irreflexive_lt x + assert $ Prop.symmetric x y + assert $ Prop.asymmetric x y + assert $ Prop.antisymmetric x y + assert $ Prop.transitive_lt x y z + assert $ Prop.transitive_le x y z + assert $ Prop.transitive_eq x y z + assert $ Prop.chain_22 x y z w + +tests :: IO Bool +tests = checkParallel $$(discover) diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -2,14 +2,22 @@ import System.Exit (exitFailure) import System.IO (BufferMode(..), hSetBuffering, stdout, stderr) - -import qualified Test.Data.Float as F +import qualified Test.Data.Prd as P +import qualified Test.Data.Connection as C import qualified Test.Data.Connection.Int as CI import qualified Test.Data.Connection.Word as CW - +import qualified Test.Data.Connection.Float as CF +import qualified Test.Data.Connection.Ratio as CR tests :: IO [Bool] -tests = sequence [CI.tests, CW.tests, F.tests] +tests = sequence + [ P.tests + , C.tests + , CI.tests + , CW.tests + , CF.tests + , CR.tests + ] main :: IO () main = do