natural-arithmetic 0.2.3.0 → 0.2.4.0

raw patch · 6 files changed

+99/−7 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• natural-arithmetic.cabal +2/−2
• src/Arithmetic/Fin.hs +39/−2
• src/Arithmetic/Nat.hs +21/−2
• src/Arithmetic/Types.hs +27/−1
• src/Arithmetic/Unsafe.hs +4/−0

@@ -1,5 +1,11 @@ # Revision history for natural-arithmetic +## 0.2.4.0 -- 2026-07-14++* Add more stuff for Fin32#+* Add withPred#+* Correct implementation of testLessThanEqual#+ ## 0.2.3.0 -- 2025-06-12  * Add Fin.greatest#

@@ -1,6 +1,6 @@ cabal-version:   2.2 name:            natural-arithmetic-version:         0.2.3.0+version:         0.2.4.0 synopsis:        Arithmetic of natural numbers description:   A search for terms like `arithmetic` and `natural` on hackage reveals@@ -91,4 +91,4 @@  source-repository head   type:     git-  location: git://github.com/byteverse/natural-arithmetic.git+  location: ssh://github.com/byteverse/natural-arithmetic.git

@@ -22,8 +22,11 @@   , weakenL#   , weakenR   , weakenR#+  , weaken32R#   , succ   , succ#+  , succ32#+  , pred32#      -- * Traverse @@ -65,6 +68,7 @@      -- * Construct   , construct#+  , construct32#   , nativeTo32#   , nativeFrom32#   , remInt#@@ -73,6 +77,7 @@   , fromInt#   , constant#   , greatest#+  , greatest32#      -- * Compare   , equals#@@ -88,9 +93,9 @@ import Prelude hiding (last, succ)  import Arithmetic.Nat ((<?),(<?#))-import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=), (:=:#))+import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, pattern MaybeFin32Nothing#, pattern MaybeFin32Just#, type (:=:), type (<), type (<#), type (<=), (:=:#)) import Arithmetic.Types (type (<=#))-import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))+import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#), MaybeFin32#(MaybeFin32#)) import Data.Maybe.Void (pattern JustVoid#) import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#)) import GHC.TypeNats (CmpNat, type (+))@@ -158,6 +163,12 @@ {-# INLINE weakenR# #-} weakenR# (Fin# i) = Fin# i +{- | Unboxed variant of 'weakenR'.+-}+weaken32R# :: forall n m. Fin32# n -> Fin32# (n + m)+{-# INLINE weaken32R# #-}+weaken32R# (Fin32# i) = Fin32# i+ {- | Weaken the bound, replacing it by another number greater than or equal to itself. This does not change the index. -}@@ -595,6 +606,10 @@ {-# INLINE construct# #-} construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x +construct32# :: (n <=# 2147483648) -> (i <# n) -> Nat# i -> Fin32# n+{-# INLINE construct32# #-}+construct32# _ _ (Unsafe.Nat# x) = Unsafe.Fin32# (Exts.intToInt32# x)+ {- | Return the successor of the Fin or return nothing if the argument is the greatest inhabitant. -}@@ -615,6 +630,25 @@  where   !ix' = ix +# 1# +-- | Variant of 'succ' for unlifted 32-bit finite numbers.+--+-- The implementation of this is kind of weird because we have to+-- worry about overflow.+succ32# :: (n <=# 2147483648) -> Nat# n -> Fin32# n -> MaybeFin32# n+{-# INLINE succ32# #-}+succ32# _ (Nat# n) (Fin32# ix) =+  case ix' Exts.<# n of+    0# -> MaybeFin32Nothing#+    _ -> MaybeFin32Just# (Fin32# (Exts.intToInt32# ix'))+ where+  !ix' = Exts.int32ToInt# ix +# 1#++pred32# :: Fin32# n -> MaybeFin32# n+{-# inline pred32# #-}+pred32# (Fin32# x) = case Exts.int32ToInt# x of+  0# -> MaybeFin32Nothing#+  _ -> MaybeFin32# (Exts.subInt32# x (Exts.intToInt32# 1# ))+ {- | Convert an Int to a finite number, testing that it is less than the upper bound. This crashes with an uncatchable exception when given a negative number.@@ -685,3 +719,6 @@  greatest# :: Nat# n -> Fin# (n + 1) greatest# (Nat# i) = Fin# i++greatest32# :: (n <# 2147483648) -> Nat# n -> Fin32# (n + 1)+greatest32# _ (Nat# i) = Fin32# (Exts.intToInt32# i)

@@ -25,6 +25,8 @@     -- * Successor   , succ   , succ#+    -- * Predecessor+  , withPred#      -- * Compare   , testEqual@@ -74,6 +76,8 @@   , pattern N4096#   , pattern N8192#   , pattern N16384#+  , pattern N32768#+  , pattern N65536#      -- * Convert   , demote@@ -94,7 +98,7 @@ import Arithmetic.Unsafe (type (<=#) (Lte#)) import Data.Either.Void (EitherVoid#, pattern LeftVoid#, pattern RightVoid#) import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)-import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#))+import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#), (-#), (<=#)) import GHC.Int (Int (I#)) import GHC.TypeNats (Div, KnownNat, natVal', type (+), type (-)) @@ -151,7 +155,7 @@  testLessThanEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b) {-# INLINE testLessThanEqual# #-}-testLessThanEqual# (Nat# x) (Nat# y) = case x <# y of+testLessThanEqual# (Nat# x) (Nat# y) = case x <=# y of   0# -> NothingVoid#   _ -> JustVoid# (Lte# (# #)) @@ -219,6 +223,15 @@ {-# INLINE succ# #-} succ# n = plus# n (one# (# #)) +-- | If a natural number is greater than zero, we can operate on its+-- predecessor.+withPred# ::+     Nat# a+  -> (0 <# a)+  -> (forall b. Nat# b -> (a :=:# b + 1) -> t)+  -> t+withPred# (Nat# i) _ f = f (Nat# (i -# 1#)) (Eq# (# #))+ -- | Subtract the second argument from the first argument. monus :: Nat a -> Nat b -> Maybe (Difference a b) {-# INLINE monus #-}@@ -361,6 +374,12 @@  pattern N16384# :: Nat# 16384 pattern N16384# = Nat# 16384#++pattern N32768# :: Nat# 32768+pattern N32768# = Nat# 32768#++pattern N65536# :: Nat# 65536+pattern N65536# = Nat# 65536#  substitute# :: (m :=:# n) -> Nat# m -> Nat# n substitute# _ (Nat# x) = Nat# x

@@ -21,6 +21,9 @@   , MaybeFin#   , pattern MaybeFinJust#   , pattern MaybeFinNothing#+  , MaybeFin32#+  , pattern MaybeFin32Just#+  , pattern MaybeFin32Nothing#      -- * Either Fin   , EitherFin#@@ -36,12 +39,13 @@   , type (:=:#)   ) where -import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))+import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32# (Fin32#), MaybeFin# (..), MaybeFin32# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#)) import Data.Kind (type Type) import GHC.Exts ((-#), (<#)) import GHC.TypeNats (type (+))  import qualified GHC.TypeNats as GHC+import qualified GHC.Exts as Exts  data WithNat :: (GHC.Nat -> Type) -> Type where   WithNat ::@@ -99,8 +103,30 @@ pattern MaybeFinNothing# :: MaybeFin# n pattern MaybeFinNothing# = MaybeFin# (-1#) +pattern MaybeFin32Just# :: Fin32# n -> MaybeFin32# n+pattern MaybeFin32Just# f <- (maybeFin32ToFin32# -> (# | f #))+  where+    MaybeFin32Just# (Fin32# i) = MaybeFin32# i++pattern MaybeFin32Nothing# :: MaybeFin32# n+pattern MaybeFin32Nothing# <- (isNegativeOne32 -> True)+  where+    MaybeFin32Nothing# = MaybeFin32# (Exts.intToInt32# (-1#))++isNegativeOne32 :: MaybeFin32# n -> Bool+{-# INLINE isNegativeOne32 #-}+isNegativeOne32 (MaybeFin32# x) = case Exts.int32ToInt# x of+  (-1#) -> True+  _ -> False+ maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #) {-# INLINE maybeFinToFin# #-} maybeFinToFin# (MaybeFin# i) = case i of   -1# -> (# (# #) | #)   _ -> (# | Fin# i #)++maybeFin32ToFin32# :: MaybeFin32# n -> (# (# #) | Fin32# n #)+{-# INLINE maybeFin32ToFin32# #-}+maybeFin32ToFin32# (MaybeFin32# i) = case Exts.int32ToInt# i of+  -1# -> (# (# #) | #)+  _ -> (# | Fin32# i #)

@@ -15,6 +15,7 @@   , Nat# (..)   , Fin# (..)   , MaybeFin# (..)+  , MaybeFin32# (..)   , EitherFin# (..)   , Fin32# (..)   , type (<#) (Lt#)@@ -71,6 +72,9 @@ -} newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where   MaybeFin# :: Int# -> MaybeFin# n++newtype MaybeFin32# :: GHC.Nat -> TYPE 'Int32Rep where+  MaybeFin32# :: Int32# -> MaybeFin32# n  type role MaybeFin# nominal