natural-arithmetic 0.2.1.0 → 0.2.2.0
raw patch · 6 files changed
+92/−5 lines, 6 files
Files
- CHANGELOG.md +10/−0
- natural-arithmetic.cabal +2/−1
- src/Arithmetic/Fin.hs +39/−3
- src/Arithmetic/Nat.hs +8/−0
- src/Arithmetic/Types.hs +22/−1
- src/Arithmetic/Unsafe.hs +11/−0
CHANGELOG.md view
@@ -1,5 +1,15 @@ # Revision history for natural-arithmetic +## 0.2.2.0 -- 2025-04-07++* Add Fin.weakenL#+* Add Fin.weakenR#+* Add Fin.demote32#+* Add Fin.constant#+* Add Fin.equals#+* Add more nat constants (N8192# and N16384#)+* Add EitherFin#+ ## 0.2.1.0 -- 2024-02-02 * Add `fromInt` and `fromInt#` to `Arithmetic.Fin`.
natural-arithmetic.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic-version: 0.2.1.0+version: 0.2.2.0 synopsis: Arithmetic of natural numbers description: A search for terms like `arithmetic` and `natural` on hackage reveals@@ -64,6 +64,7 @@ copyright: 2019 Andrew Martin category: Math extra-doc-files: CHANGELOG.md+tested-with: GHC ==9.4.8 || ==9.6.3 || ==9.8.1 common build-settings default-language: Haskell2010
src/Arithmetic/Fin.hs view
@@ -17,7 +17,9 @@ , incrementR# , weaken , weakenL+ , weakenL# , weakenR+ , weakenR# , succ , succ# @@ -52,6 +54,7 @@ -- * Demote , demote , demote#+ , demote32# -- * Deconstruct , with@@ -63,7 +66,11 @@ , remWord# , fromInt , fromInt#+ , constant# + -- * Compare+ , equals#+ -- * Lift and Unlift , lift , unlift@@ -73,9 +80,9 @@ import Arithmetic.Nat ((<?)) import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=))-import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#))-import GHC.Exts (Int (I#), Int#, Word#, (+#))-import GHC.TypeNats (type (+))+import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))+import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#))+import GHC.TypeNats (CmpNat, type (+)) import qualified Arithmetic.Equal as Eq import qualified Arithmetic.Lt as Lt@@ -84,6 +91,7 @@ import qualified Arithmetic.Plus as Plus import qualified Arithmetic.Unsafe as Unsafe import qualified GHC.Exts as Exts+import qualified GHC.TypeNats as GHC {- | Raise the index by @m@ and weaken the bound by @m@, adding @m@ to the right-hand side of @n@.@@ -116,6 +124,12 @@ (Lt.plus pf (Lte.zero @m)) ) +{- | Unboxed variant of 'weakenL'.+-}+weakenL# :: forall n m. Fin# n -> Fin# (m + n)+{-# INLINE weakenL# #-}+weakenL# (Fin# i) = Fin# i+ {- | Weaken the bound by @m@, adding it to the right-hand side of the existing bound. This does not change the index. -}@@ -123,6 +137,12 @@ {-# INLINE weakenR #-} weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero) +{- | Unboxed variant of 'weakenR'.+-}+weakenR# :: forall n m. Fin# n -> Fin# (n + m)+{-# INLINE weakenR# #-}+weakenR# (Fin# i) = Fin# i+ {- | Weaken the bound, replacing it by another number greater than or equal to itself. This does not change the index. -}@@ -513,6 +533,10 @@ {-# INLINE demote# #-} demote# (Fin# i) = i +demote32# :: Fin32# n -> Int32#+{-# INLINE demote32# #-}+demote32# (Fin32# i) = i+ lift :: Unsafe.Fin# n -> Fin n {-# INLINE lift #-} lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt@@ -599,3 +623,15 @@ remWord# w (Nat# n) = case n of 0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero" _ -> Fin# (Exts.word2Int# (Exts.remWord# w (Exts.int2Word# n)))++{- | 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:++>>> Fin.constant# @10 N4#+-}+constant# :: forall (b :: GHC.Nat) (a :: GHC.Nat). (CmpNat a b ~ 'LT) => Nat# a -> Fin# b+constant# (Nat# i) = Fin# i++equals# :: Fin# n -> Fin# n -> Bool+equals# (Fin# a) (Fin# b) = Exts.isTrue# (a ==# b)
src/Arithmetic/Nat.hs view
@@ -70,6 +70,8 @@ , pattern N1024# , pattern N2048# , pattern N4096#+ , pattern N8192#+ , pattern N16384# -- * Convert , demote@@ -337,3 +339,9 @@ pattern N4096# :: Nat# 4096 pattern N4096# = Nat# 4096#++pattern N8192# :: Nat# 8192+pattern N8192# = Nat# 8192#++pattern N16384# :: Nat# 16384+pattern N16384# = Nat# 16384#
src/Arithmetic/Types.hs view
@@ -22,6 +22,11 @@ , pattern MaybeFinJust# , pattern MaybeFinNothing# + -- * Either Fin+ , EitherFin#+ , pattern EitherFinLeft#+ , pattern EitherFinRight#+ -- * Infix Operators , type (<) , type (<=)@@ -31,8 +36,9 @@ , type (:=:#) ) where -import Arithmetic.Unsafe (Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))+import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32#, MaybeFin# (..), 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@@ -69,6 +75,21 @@ instance Ord (Fin n) where Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)++pattern EitherFinLeft# :: Fin# m -> EitherFin# m n+pattern EitherFinLeft# f <- (eitherFinToSum# -> (# f | #))+ where+ EitherFinLeft# (Fin# i) = EitherFin# ((-1#) -# i)++pattern EitherFinRight# :: Fin# n -> EitherFin# m n+pattern EitherFinRight# f <- (eitherFinToSum# -> (# | f #))+ where+ EitherFinRight# (Fin# i) = EitherFin# i++eitherFinToSum# :: EitherFin# m n -> (# Fin# m | Fin# n #)+eitherFinToSum# (EitherFin# i) = case i <# 0# of+ 1# -> (# Fin# ((-1#) -# i) | #)+ _ -> (# | Fin# i #) pattern MaybeFinJust# :: Fin# n -> MaybeFin# n pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #))
src/Arithmetic/Unsafe.hs view
@@ -15,6 +15,7 @@ , Nat# (..) , Fin# (..) , MaybeFin# (..)+ , EitherFin# (..) , Fin32# (..) , type (<#) (Lt#) , type (<=#) (Lte#)@@ -72,6 +73,16 @@ MaybeFin# :: Int# -> MaybeFin# n type role MaybeFin# nominal++{- | Either a @Fin#@ bounded by the left natural or one bounded+by the right natural.+-}+newtype EitherFin# :: GHC.Nat -> GHC.Nat -> TYPE 'IntRep where+ -- Implementation note: Left is represented by (-m + 1), and+ -- right is represented by n.+ EitherFin# :: Int# -> EitherFin# m n++type role EitherFin# nominal nominal -- | Variant of 'Fin#' that only allows 32-bit integers. newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where