diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`. diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal --- a/natural-arithmetic.cabal +++ b/natural-arithmetic.cabal @@ -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 diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs --- a/src/Arithmetic/Fin.hs +++ b/src/Arithmetic/Fin.hs @@ -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 (( 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) diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs --- a/src/Arithmetic/Nat.hs +++ b/src/Arithmetic/Nat.hs @@ -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# diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs --- a/src/Arithmetic/Types.hs +++ b/src/Arithmetic/Types.hs @@ -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 #)) diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs --- a/src/Arithmetic/Unsafe.hs +++ b/src/Arithmetic/Unsafe.hs @@ -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