Add fromInt and fromInt# to Arithmetic.Fin

CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for natural-arithmetic
 
+## 0.2.1.0 -- 2024-??-??
+
+* Add `fromInt` and `fromInt#` to `Arithmetic.Fin`.
+
 ## 0.2.0.0 -- 2024-01-09
 
 * Change the types of `with#` and `construct#` (both in `Arithmetic.Fin`)

natural-arithmetic.cabal

@@ -1,6 +1,6 @@
 cabal-version: 2.2
 name: natural-arithmetic
-version: 0.2.0.0
+version: 0.2.1.0
 synopsis: Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals

src/Arithmetic/Fin.hs

@@ -55,6 +55,8 @@ module Arithmetic.Fin
   , construct#
   , remInt#
   , remWord#
+  , fromInt
+  , fromInt#
     -- * Lift and Unlift
   , lift
   , unlift
@@ -466,6 +468,32 @@ succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of
   where
   !ix' = ix +# 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.
+fromInt ::
+     Nat n -- ^ exclusive upper bound
+  -> Int
+  -> Maybe (Fin n)
+{-# inline fromInt #-}
+fromInt bound i
+  | i < 0 = errorWithoutStackTrace "Arithmetic.Fin.fromInt: negative argument"
+  | otherwise = Nat.with i $ \number -> case number <? bound of
+      Just lt -> Just (Fin number lt)
+      Nothing -> Nothing
+
+-- | Unboxed variant of 'fromInt'.
+fromInt# ::
+     Nat# n -- ^ exclusive upper bound
+  -> Int#
+  -> MaybeFin# n
+{-# inline fromInt# #-}
+fromInt# (Nat# n) i
+  | Exts.isTrue# (i Exts.<# 0#) =
+      errorWithoutStackTrace "Arithmetic.Fin.fromInt#: negative argument"
+  | Exts.isTrue# (i Exts.<# n) = MaybeFinJust# (Fin# i)
+  | otherwise = MaybeFinNothing#
+
 -- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
 -- the remainder.
 remInt# :: Int# -> Nat# n -> Fin# n