Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add Fin.constant# #7

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Add Fin.constant# #7

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a873702
Add Fin.constant#
andrewthad Jun 18, 2024
f999770
Add documentation
andrewthad Jun 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion src/Arithmetic/Fin.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ module Arithmetic.Fin
, remWord#
, fromInt
, fromInt#
, constant#

-- * Lift and Unlift
, lift
Expand All @@ -75,7 +76,7 @@ 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 GHC.TypeNats (CmpNat, type (+))

import qualified Arithmetic.Equal as Eq
import qualified Arithmetic.Lt as Lt
Expand All @@ -84,6 +85,7 @@ import qualified Arithmetic.Nat as Nat
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@.
Expand Down Expand Up @@ -599,3 +601,12 @@ remWord# :: Word# -> Nat# n -> Fin# n
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