connections 0.0.2.2 → 0.0.3

raw patch · 32 files changed

+5543/−1807 lines, 32 filesdep +ringsdep −propertydep ~lawzdep ~semigroupoidsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: rings

Dependencies removed: property

Dependency ranges changed: lawz, semigroupoids

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−3
• connections.cabal +34/−17
• src/Data/Connection.hs +92/−83
• src/Data/Connection/Float.hs +137/−109
• src/Data/Connection/Int.hs +97/−23
• src/Data/Connection/Property.hs +17/−18
• src/Data/Connection/Ratio.hs +292/−0
• src/Data/Connection/Round.hs +249/−0
• src/Data/Connection/Word.hs +0/−3
• src/Data/Connection/Yoneda.hs +0/−95
• src/Data/Float.hs +0/−420
• src/Data/Float.hsc +875/−0
• src/Data/Prd.hs +385/−353
• src/Data/Prd/Lattice.hs +0/−290
• src/Data/Prd/Nan.hs +74/−101
• src/Data/Prd/Property.hs +67/−37
• src/Data/Semigroup/Join.hs +272/−0
• src/Data/Semigroup/Meet.hs +267/−0
• src/Data/Semilattice.hs +347/−0
• src/Data/Semilattice/MaxMin.hs +34/−0
• src/Data/Semilattice/N5.hs +135/−0
• src/Data/Semilattice/Property.hs +348/−0
• src/Data/Semilattice/Top.hs +148/−0
• src/Numeric/Prelude.hs +182/−0
• test/Test/Data/Connection.hs +85/−0
• test/Test/Data/Connection/Float.hs +531/−0
• test/Test/Data/Connection/Int.hs +153/−53
• test/Test/Data/Connection/Ratio.hs +303/−0
• test/Test/Data/Connection/Word.hs +65/−41
• test/Test/Data/Float.hs +0/−157
• test/Test/Data/Prd.hs +337/−0
• test/test.hs +12/−4

@@ -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

@@ -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

@@ -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 <https://ncatlab.org/nlab/show/adjoint+triple> -- 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

@@ -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)+-}

@@ -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

@@ -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 <https://ncatlab.org/nlab/show/idempotent+adjunction> ---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 <https://ncatlab.org/nlab/show/idempotent+adjunction> ---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

@@ -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

@@ -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 <https://en.wikipedia.org/wiki/Rounding>.+--+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

@@ -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

@@ -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:------ * <https://en.wikipedia.org/wiki/Filter_(mathematics)>--- * <https://en.wikipedia.org/wiki/Ideal_(order_theory)>----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 = (<~)

@@ -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--}

@@ -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 <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.+-- +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+

@@ -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 <https://en.wikipedia.org/wiki/Reflexive_relation reflexive> 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 <https://en.wikipedia.org/wiki/Semiorder semiorder>. -- 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 <https://en.wikipedia.org/wiki/Semiorder>. ----- 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)-

@@ -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 <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.--------- /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)

@@ -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)

@@ -1,11 +1,11 @@ -- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>. 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 <https://en.wikipedia.org/wiki/Reflexive_relation#Related_terms>.+-- '=~' 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)

@@ -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)

@@ -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)

@@ -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 <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.+--+-- 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)

@@ -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)

@@ -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 <https://en.wikipedia.org/wiki/Modular_lattice#Examples>+--+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)

@@ -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)

@@ -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)

@@ -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 #-}

@@ -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)

@@ -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)