natural-arithmetic 0.2.2.0 → 0.2.3.0
raw patch · 7 files changed
+114/−3 lines, 7 files
Files
- CHANGELOG.md +14/−0
- natural-arithmetic.cabal +1/−1
- src/Arithmetic/Equal.hs +10/−0
- src/Arithmetic/Fin.hs +52/−2
- src/Arithmetic/Lte.hs +11/−0
- src/Arithmetic/Nat.hs +19/−0
- src/Arithmetic/Plus.hs +7/−0
CHANGELOG.md view
@@ -1,5 +1,19 @@ # Revision history for natural-arithmetic +## 0.2.3.0 -- 2025-06-12++* Add Fin.greatest#+* Add Plus.commutative#+* Add substitution functions for unlifted less-than-or-equal-to+* Add Nat.substitute#+* Add Eq.symmetric#+* Add nativeFrom32#+* Add incrementL#+* Add testLessThanEqual#+* Add nativeTo32#+* Add Fin.ascendFromToM_#+* Add Fin.weaken#+ ## 0.2.2.0 -- 2025-04-07 * Add Fin.weakenL#
natural-arithmetic.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic-version: 0.2.2.0+version: 0.2.3.0 synopsis: Arithmetic of natural numbers description: A search for terms like `arithmetic` and `natural` on hackage reveals
src/Arithmetic/Equal.hs view
@@ -7,11 +7,13 @@ module Arithmetic.Equal ( symmetric+ , symmetric# , plusR , plusL , plusR# , plusL# , lift+ , unlift ) where import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#))@@ -21,6 +23,10 @@ {-# INLINE symmetric #-} symmetric Eq = Eq +symmetric# :: (m :=:# n) -> (n :=:# m)+{-# INLINE symmetric# #-}+symmetric# _ = Eq# (# #)+ plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n) {-# INLINE plusL #-} plusL Eq = Eq@@ -40,3 +46,7 @@ lift :: (m :=:# n) -> (m :=: n) {-# INLINE lift #-} lift _ = Eq++unlift :: (m :=: n) -> (m :=:# n)+{-# INLINE unlift #-}+unlift _ = Eq# (# #)
src/Arithmetic/Fin.hs view
@@ -13,9 +13,11 @@ module Arithmetic.Fin ( -- * Modification incrementL+ , incrementL# , incrementR , incrementR# , weaken+ , weaken# , weakenL , weakenL# , weakenR@@ -38,6 +40,7 @@ , ascendM# , ascendM_ , ascendM_#+ , ascendFromToM_# , descend , descend# , descend'@@ -62,15 +65,21 @@ -- * Construct , construct#+ , nativeTo32#+ , nativeFrom32# , remInt# , remWord# , fromInt , fromInt# , constant#+ , greatest# -- * Compare , equals# + -- * Substitute Bound+ , substitute#+ -- * Lift and Unlift , lift , unlift@@ -78,9 +87,11 @@ 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.Nat ((<?),(<?#))+import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=), (:=:#))+import Arithmetic.Types (type (<=#)) import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))+import Data.Maybe.Void (pattern JustVoid#) import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#)) import GHC.TypeNats (CmpNat, type (+)) @@ -111,6 +122,10 @@ {-# INLINE incrementL #-} incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf) +incrementL# :: forall n m. Nat# m -> Fin# n -> Fin# (m + n)+{-# INLINE incrementL# #-}+incrementL# (Nat# n) (Fin# i) = Fin# (n +# i)+ {- | Weaken the bound by @m@, adding it to the left-hand side of the existing bound. This does not change the index. -}@@ -150,6 +165,10 @@ {-# INLINE weaken #-} weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt) +weaken# :: forall n m. (n <=# m) -> Fin# n -> Fin# m+{-# INLINE weaken# #-}+weaken# _ (Fin# x) = Fin# x+ -- | A finite set of no values is impossible. absurd :: Fin 0 -> void {-# INLINE absurd #-}@@ -362,6 +381,23 @@ Nothing -> pure () Just lt -> f (Fin m lt) *> go (Nat.succ m) +ascendFromToM_# ::+ forall m a i n.+ (Monad m) =>+ -- | Index to start at (inclusive)+ Nat# i ->+ -- | Upper bound (exclusive)+ Nat# n ->+ -- | Update accumulator+ (Fin# n -> m a) ->+ m ()+ascendFromToM_# m0 end f = go m0+ where+ go :: forall k. Nat# k -> m ()+ go m = case m <?# end of+ JustVoid# lt -> f (construct# lt m) *> go (Nat.succ# m)+ _ -> pure ()+ {- | Variant of @ascendM_@ that takes an unboxed Nat and provides an unboxed Fin to the callback. -}@@ -624,6 +660,14 @@ 0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero" _ -> Fin# (Exts.word2Int# (Exts.remWord# w (Exts.int2Word# n))) +nativeTo32# :: (n <=# 2147483648) -> Fin# n -> Fin32# n+{-# inline nativeTo32# #-}+nativeTo32# _ (Fin# x) = Fin32# (Exts.intToInt32# x)++nativeFrom32# :: Fin32# n -> Fin# n+{-# inline nativeFrom32# #-}+nativeFrom32# (Fin32# x) = Fin# (Exts.int32ToInt# x)+ {- | Create an unlifted finite number from an unlifted natural number. The upper bound is the first type argument so that user can use type applications to clarify when it is helpful. For example:@@ -635,3 +679,9 @@ equals# :: Fin# n -> Fin# n -> Bool equals# (Fin# a) (Fin# b) = Exts.isTrue# (a ==# b)++substitute# :: (m :=:# n) -> Fin# m -> Fin# n+substitute# _ (Fin# x) = Fin# x++greatest# :: Nat# n -> Fin# (n + 1)+greatest# (Nat# i) = Fin# i
src/Arithmetic/Lte.hs view
@@ -13,7 +13,9 @@ -- * Substitution , substituteL+ , substituteL# , substituteR+ , substituteR# -- * Increment , incrementL@@ -54,6 +56,7 @@ ) where import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#))+import Arithmetic.Unsafe (type (:=:#)) import GHC.TypeNats (CmpNat, type (+)) import qualified GHC.TypeNats as GHC@@ -71,6 +74,14 @@ substituteR :: (b :=: c) -> (a <= b) -> (a <= c) {-# INLINE substituteR #-} substituteR Eq Lte = Lte++substituteL# :: (b :=:# c) -> (b <=# a) -> (c <=# a)+{-# INLINE substituteL# #-}+substituteL# _ _ = Lte# (# #)++substituteR# :: (b :=:# c) -> (a <=# b) -> (a <=# c)+{-# INLINE substituteR# #-}+substituteR# _ _ = Lte# (# #) -- | Add two inequalities. plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
src/Arithmetic/Nat.hs view
@@ -32,12 +32,14 @@ , testLessThan , testLessThan# , testLessThanEqual+ , testLessThanEqual# , testZero , testZero# , (=?) , (<?) , (<?#) , (<=?)+ , (<=?#) -- * Constants , zero@@ -80,12 +82,16 @@ , lift , with , with#++ -- * Substitute+ , substitute# ) where import Prelude hiding (succ) import Arithmetic.Types import Arithmetic.Unsafe (Nat (Nat), Nat# (Nat#), (:=:) (Eq), (:=:#) (Eq#), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte))+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#, (+#), (<#), (==#))@@ -113,6 +119,10 @@ {-# INLINE (<?#) #-} (<?#) = testLessThan# +(<=?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)+{-# INLINE (<=?#) #-}+(<=?#) = testLessThanEqual#+ {- | Is the first argument strictly less than the second argument? -}@@ -139,6 +149,12 @@ then Just Lte else Nothing +testLessThanEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)+{-# INLINE testLessThanEqual# #-}+testLessThanEqual# (Nat# x) (Nat# y) = case x <# y of+ 0# -> NothingVoid#+ _ -> JustVoid# (Lte# (# #))+ -- | Are the two arguments equal to one another? testEqual :: Nat a -> Nat b -> Maybe (a :=: b) {-# INLINE testEqual #-}@@ -345,3 +361,6 @@ pattern N16384# :: Nat# 16384 pattern N16384# = Nat# 16384#++substitute# :: (m :=:# n) -> Nat# m -> Nat# n+substitute# _ (Nat# x) = Nat# x
src/Arithmetic/Plus.hs view
@@ -2,16 +2,20 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-} module Arithmetic.Plus ( zeroL , zeroR , commutative+ , commutative# , associative ) where import Arithmetic.Unsafe (type (:=:) (Eq))+import Arithmetic.Unsafe (type (:=:#) (Eq#)) import GHC.TypeNats (type (+)) -- | Any number plus zero is equal to the original number.@@ -25,6 +29,9 @@ -- | Addition is commutative. commutative :: forall a b. a + b :=: b + a commutative = Eq++commutative# :: forall a b. (# #) -> a + b :=:# b + a+commutative# _ = Eq# (# #) -- | Addition is associative. associative :: forall a b c. (a + b) + c :=: a + (b + c)