natural-arithmetic 0.1.4.0 → 0.2.0.0

raw patch · 9 files changed

+461/−14 lines, 9 filesdep +unliftedPVP ok

version bump matches the API change (PVP)

Dependencies added: unlifted

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• natural-arithmetic.cabal +4/−2
• src/Arithmetic/Equal.hs +18/−1
• src/Arithmetic/Fin.hs +67/−6
• src/Arithmetic/Lt.hs +90/−0
• src/Arithmetic/Lte.hs +80/−0
• src/Arithmetic/Nat.hs +132/−3
• src/Arithmetic/Types.hs +30/−1
• src/Arithmetic/Unsafe.hs +30/−1

@@ -1,5 +1,15 @@ # Revision history for natural-arithmetic +## 0.2.0.0 -- 2024-01-09++* Change the types of `with#` and `construct#` (both in `Arithmetic.Fin`)+  to use an unboxed "less than" instead of a boxed one. This is a breaking+  change.+* Add patterns for the natural numbers 5, 6, 7.+* Add a lot of primitives for working with unboxed natural and inequalities.+  GHC is unable to eliminate the boxed `Fin` type in a suprisingly large+  number of cases, and `Fin#` helps a lot with this.+ ## 0.1.4.0 -- 2023-05-31  * Add unboxed Nat type

@@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic-version: 0.1.4.0+version: 0.2.0.0 synopsis: Arithmetic of natural numbers description:   A search for terms like `arithmetic` and `natural` on hackage reveals@@ -74,7 +74,9 @@     Arithmetic.Types     Arithmetic.Unsafe     Arithmetic.Plus-  build-depends: base>=4.14 && <5+  build-depends:+    , base>=4.14 && <5+    , unlifted >=0.2.1   hs-source-dirs: src   default-language: Haskell2010   ghc-options: -Wall -O2

@@ -1,15 +1,20 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-}+{-# language MagicHash #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-}  module Arithmetic.Equal   ( symmetric   , plusR   , plusL+  , plusR#+  , plusL#+  , lift   ) where -import Arithmetic.Unsafe (type (:=:)(Eq))+import Arithmetic.Unsafe (type (:=:)(Eq), type (:=:#)(Eq#)) import GHC.TypeNats (type (+))  symmetric :: (m :=: n) -> (n :=: m)@@ -23,3 +28,15 @@ plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c) {-# inline plusR #-} plusR Eq = Eq++plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n)+{-# inline plusL# #-}+plusL# _ = Eq# (# #)++plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c)+{-# inline plusR# #-}+plusR# _ = Eq# (# #)++lift :: (m :=:# n) -> (m :=: n)+{-# inline lift #-}+lift _ = Eq

@@ -4,17 +4,22 @@ {-# language GADTs #-} {-# language KindSignatures #-} {-# language MagicHash #-}+{-# language PatternSynonyms #-} {-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeApplications #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-} module Arithmetic.Fin   ( -- * Modification     incrementL   , incrementR+  , incrementR#   , weaken   , weakenL   , weakenR+  , succ+  , succ#     -- * Traverse     -- | These use the terms @ascend@ and @descend@ rather than the     -- more popular @l@ (left) and @r@ (right) that pervade the Haskell@@ -30,6 +35,7 @@   , ascendM_   , ascendM_#   , descend+  , descend#   , descend'   , descendM   , descendM_@@ -41,21 +47,26 @@   , absurd     -- * Demote   , demote+  , demote#     -- * Deconstruct   , with   , with#     -- * Construct   , construct#+  , remInt#+  , remWord#     -- * Lift and Unlift   , lift   , unlift   ) where -import Prelude hiding (last)+import Prelude hiding (last,succ)  import Arithmetic.Nat ((<?))-import Arithmetic.Types (Fin(..),Fin#,Difference(..),Nat,Nat#,type (<), type (<=), type (:=:))-import GHC.Exts (Int(I#))+import Arithmetic.Types (Fin(..),Difference(..),Nat,Nat#,type (<), type (<#), type (<=), type (:=:))+import Arithmetic.Types (pattern MaybeFinNothing#, pattern MaybeFinJust#)+import Arithmetic.Unsafe (Nat#(Nat#),Fin#(Fin#),MaybeFin#)+import GHC.Exts (Int(I#),(+#),Int#,Word#) import GHC.TypeNats (type (+))  import qualified Arithmetic.Lt as Lt@@ -64,6 +75,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  -- | Raise the index by @m@ and weaken the bound by @m@, adding -- @m@ to the right-hand side of @n@.@@ -71,6 +83,10 @@ {-# inline incrementR #-} incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf) +incrementR# :: forall n m. Nat# m -> Fin# n -> Fin# (n + m)+{-# inline incrementR# #-}+incrementR# (Nat# n) (Fin# i) = Fin# (n +# i)+ -- | Raise the index by @m@ and weaken the bound by @m@, adding -- @m@ to the left-hand side of @n@. incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)@@ -122,6 +138,14 @@     Nothing -> b0     Just lt -> f (Fin m lt) (go (Nat.succ m)) +descend# :: forall a n.+     Nat# n -- ^ Upper bound+  -> a -- ^ Initial accumulator+  -> (Fin# n -> a -> a) -- ^ Update accumulator+  -> a+{-# inline descend# #-}+descend# !n b0 f = descend (Nat.lift n) b0 (\ix a -> f (unlift ix) a)+ -- | Fold over the numbers bounded by @n@ in descending -- order. This is strict in the accumulator. For convenince, -- this differs from @foldr'@ in the order of the parameters.@@ -397,6 +421,10 @@ {-# inline demote #-} demote (Fin i _) = Nat.demote i +demote# :: Fin# n -> Int#+{-# inline demote# #-}+demote# (Fin# i) = i+ lift :: Unsafe.Fin# n -> Fin n {-# inline lift #-} lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt@@ -411,10 +439,43 @@ with (Fin i lt) f = f lt i  -- | Variant of 'with' for unboxed argument and result types.-with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a+with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a {-# inline with# #-}-with# (Unsafe.Fin# i) f = f Unsafe.Lt (Unsafe.Nat# i)+with# (Unsafe.Fin# i) f = f (Unsafe.Lt# (# #)) (Unsafe.Nat# i) -construct# :: (i < n) -> Nat# i -> Fin# n+construct# :: (i <# n) -> Nat# i -> Fin# n {-# inline construct# #-} construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x++-- | Return the successor of the Fin or return nothing if the+-- argument is the greatest inhabitant.+succ :: Nat n -> Fin n -> Maybe (Fin n)+{-# inline succ #-}+succ n (Fin ix _) = case ix' <? n of+  Nothing -> Nothing+  Just lt -> Just (Fin ix' lt)+  where+  ix' = Nat.succ ix++-- | Variant of 'succ' for unlifted finite numbers.+succ# :: Nat# n -> Fin# n -> MaybeFin# n+{-# inline succ# #-}+succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of+  0# -> MaybeFinNothing#+  _ -> MaybeFinJust# (Fin# ix')+  where+  !ix' = ix +# 1#++-- | This crashes if @n = 0@. Divides @i@ by @n@ and takes+-- the remainder.+remInt# :: Int# -> Nat# n -> Fin# n+remInt# i (Nat# n) = case n of+  0# -> errorWithoutStackTrace "Arithmetic.Fin.remInt#: cannot divide by zero"+  _ -> Fin# (Exts.remInt# i n)++-- | This crashes if @n = 0@. Divides @i@ by @n@ and takes+-- the remainder.+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)))

@@ -2,29 +2,44 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-}+{-# language MagicHash #-}+{-# language UnboxedTuples #-} {-# language TypeFamilies #-} {-# language TypeOperators #-}  module Arithmetic.Lt   ( -- * Special Inequalities     zero+  , zero#     -- * Substitution   , substituteL   , substituteR     -- * Increment   , incrementL+  , incrementL#   , incrementR+  , incrementR#     -- * Decrement   , decrementL+  , decrementL#   , decrementR+  , decrementR#     -- * Weaken   , weakenL+  , weakenL#   , weakenR+  , weakenR#+  , weakenLhsL#+  , weakenLhsR#     -- * Composition   , plus+  , plus#   , transitive+  , transitive#   , transitiveNonstrictL+  , transitiveNonstrictL#   , transitiveNonstrictR+  , transitiveNonstrictR#     -- * Multiplication and Division   , reciprocalA   , reciprocalB@@ -35,10 +50,15 @@   , absurd     -- * Integration with GHC solver   , constant+  , constant#+    -- * Lift and Unlift+  , lift+  , unlift   ) where  import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) import Arithmetic.Unsafe (type (<=)(Lte))+import Arithmetic.Unsafe (type (<#)(Lt#),type (<=#)) import GHC.TypeNats (CmpNat,type (+))  import qualified GHC.TypeNats as GHC@@ -68,6 +88,10 @@ {-# inline plus #-} plus Lt Lte = Lt +plus# :: (a <# b) -> (c <=# d) -> (a + c <# b + d)+{-# inline plus# #-}+plus# _ _ = Lt# (# #)+ -- | Add a constant to the left-hand side of both sides of -- the strict inequality. incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -75,6 +99,11 @@ {-# inline incrementL #-} incrementL Lt = Lt +incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) -> (c + a <# c + b)+{-# inline incrementL# #-}+incrementL# _ = Lt# (# #)+ -- | Add a constant to the right-hand side of both sides of -- the strict inequality. incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -82,6 +111,11 @@ {-# inline incrementR #-} incrementR Lt = Lt +incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) -> (a + c <# b + c)+{-# inline incrementR# #-}+incrementR# _ = Lt# (# #)+ -- | Subtract a constant from the left-hand side of both sides of -- the inequality. This is the opposite of 'incrementL'. decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -89,6 +123,11 @@ {-# inline decrementL #-} decrementL Lt = Lt +decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  ((c + a) <# (c + b)) -> (a <# b)+{-# inline decrementL# #-}+decrementL# _ = Lt# (# #)+ -- | Subtract a constant from the right-hand side of both sides of -- the inequality. This is the opposite of 'incrementR'. decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -96,6 +135,11 @@ {-# inline decrementR #-} decrementR Lt = Lt +decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <# b + c) -> (a <# b)+{-# inline decrementR# #-}+decrementR# _ = Lt# (# #)+ -- | Add a constant to the left-hand side of the right-hand side of -- the strict inequality. weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -103,6 +147,21 @@ {-# inline weakenL #-} weakenL Lt = Lt +weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) -> (a <# c + b)+{-# inline weakenL# #-}+weakenL# _ = Lt# (# #)++weakenLhsL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a <# b) -> (a <# b)+{-# inline weakenLhsL# #-}+weakenLhsL# _ = Lt# (# #)++weakenLhsR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <# b) -> (a <# b)+{-# inline weakenLhsR# #-}+weakenLhsR# _ = Lt# (# #)+ -- | Add a constant to the right-hand side of the right-hand side of -- the strict inequality. weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -110,26 +169,47 @@ {-# inline weakenR #-} weakenR Lt = Lt +weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) -> (a <# b + c)+{-# inline weakenR# #-}+weakenR# _ = Lt# (# #)+ -- | Compose two strict inequalities using transitivity. transitive :: (a < b) -> (b < c) -> (a < c) {-# inline transitive #-} transitive Lt Lt = Lt +transitive# :: (a <# b) -> (b <# c) -> (a <# c)+{-# inline transitive# #-}+transitive# _ _ = Lt# (# #)+ -- | Compose a strict inequality (the first argument) with a nonstrict -- inequality (the second argument). transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c) {-# inline transitiveNonstrictR #-} transitiveNonstrictR Lt Lte = Lt +transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> (a <# c)+{-# inline transitiveNonstrictR# #-}+transitiveNonstrictR# _ _ = Lt# (# #)+ transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c) {-# inline transitiveNonstrictL #-} transitiveNonstrictL Lte Lt = Lt +transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> (a <# c)+{-# inline transitiveNonstrictL# #-}+transitiveNonstrictL# _ _ = Lt# (# #)+ -- | Zero is less than one. zero :: 0 < 1 {-# inline zero #-} zero = Lt +zero# :: (# #) -> 0 <# 1+{-# inline zero# #-}+zero# _ = Lt# (# #)+ -- | Nothing is less than zero. absurd :: n < 0 -> void {-# inline absurd #-}@@ -142,6 +222,10 @@ {-# inline constant #-} constant = Lt +constant# :: forall a b. (CmpNat a b ~ 'LT) => (# #) -> (a <# b)+{-# inline constant# #-}+constant# _ = Lt# (# #)+ -- | Given that @m < n/p@, we know that @p*m < n@. reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).   (m < GHC.Div n p) -> (p GHC.* m) < n@@ -153,3 +237,9 @@   (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n {-# inline reciprocalB #-} reciprocalB _ = Lt++unlift :: (a < b) -> (a <# b)+unlift _ = Lt# (# #)++lift :: (a <# b) -> (a < b)+lift _ = Lt

@@ -1,36 +1,54 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-}+{-# language MagicHash #-} {-# language TypeFamilies #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-}  module Arithmetic.Lte   ( -- * Special Inequalities     zero   , reflexive+  , reflexive#     -- * Substitution   , substituteL   , substituteR     -- * Increment   , incrementL+  , incrementL#   , incrementR+  , incrementR#     -- * Decrement   , decrementL+  , decrementL#   , decrementR+  , decrementR#     -- * Weaken   , weakenL+  , weakenL#   , weakenR+  , weakenR#     -- * Composition   , transitive+  , transitive#   , plus+  , plus#     -- * Convert Strict Inequality   , fromStrict+  , fromStrict#+  , fromStrictSucc+  , fromStrictSucc#     -- * Integration with GHC solver   , constant+    -- * Lift and Unlift+  , lift+  , unlift   ) where  import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) import Arithmetic.Unsafe (type (<=)(Lte))+import Arithmetic.Unsafe (type (<=#)(Lte#),type (<#)) import GHC.TypeNats (CmpNat,type (+))  import qualified GHC.TypeNats as GHC@@ -52,16 +70,28 @@ {-# inline plus #-} plus Lte Lte = Lte +plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d)+{-# inline plus# #-}+plus# _ _ = Lte# (# #)+ -- | Compose two inequalities using transitivity. transitive :: (a <= b) -> (b <= c) -> (a <= c) {-# inline transitive #-} transitive Lte Lte = Lte +transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c)+{-# inline transitive# #-}+transitive# _ _ = Lte# (# #)+ -- | Any number is less-than-or-equal-to itself. reflexive :: a <= a {-# inline reflexive #-} reflexive = Lte +reflexive# :: (# #) -> a <=# a+{-# inline reflexive# #-}+reflexive# _ = Lte# (# #)+ -- | Add a constant to the left-hand side of both sides of -- the inequality. incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -69,6 +99,11 @@ {-# inline incrementL #-} incrementL Lte = Lte +incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) -> (c + a <=# c + b)+{-# inline incrementL# #-}+incrementL# _ = Lte# (# #)+ -- | Add a constant to the right-hand side of both sides of -- the inequality. incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -76,6 +111,11 @@ {-# inline incrementR #-} incrementR Lte = Lte +incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) -> (a + c <=# b + c)+{-# inline incrementR# #-}+incrementR# _ = Lte# (# #)+ -- | Add a constant to the left-hand side of the right-hand side of -- the inequality. weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -83,6 +123,11 @@ {-# inline weakenL #-} weakenL Lte = Lte +weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) -> (a <=# c + b)+{-# inline weakenL# #-}+weakenL# _ = Lte# (# #)+ -- | Add a constant to the right-hand side of the right-hand side of -- the inequality. weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -90,6 +135,11 @@ {-# inline weakenR #-} weakenR Lte = Lte +weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) -> (a <=# b + c)+{-# inline weakenR# #-}+weakenR# _ = Lte# (# #)+ -- | Subtract a constant from the left-hand side of both sides of -- the inequality. This is the opposite of 'incrementL'. decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -97,6 +147,11 @@ {-# inline decrementL #-} decrementL Lte = Lte +decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a <=# c + b) -> (a <=# b)+{-# inline decrementL# #-}+decrementL# _ = Lte# (# #)+ -- | Subtract a constant from the right-hand side of both sides of -- the inequality. This is the opposite of 'incrementR'. decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).@@ -104,11 +159,30 @@ {-# inline decrementR #-} decrementR Lte = Lte +decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <=# b + c) -> (a <=# b)+{-# inline decrementR# #-}+decrementR# _ = Lte# (# #)+ -- | Weaken a strict inequality to a non-strict inequality. fromStrict :: (a < b) -> (a <= b) {-# inline fromStrict #-} fromStrict Lt = Lte +fromStrict# :: (a <# b) -> (a <=# b)+{-# inline fromStrict# #-}+fromStrict# _ = Lte# (# #)++-- | Weaken a strict inequality to a non-strict inequality, incrementing+-- the right-hand argument by one.+fromStrictSucc :: (a < b) -> (a + 1 <= b)+{-# inline fromStrictSucc #-}+fromStrictSucc Lt = Lte++fromStrictSucc# :: (a <# b) -> (a + 1 <=# b)+{-# inline fromStrictSucc# #-}+fromStrictSucc# _ = Lte# (# #)+ -- | Zero is less-than-or-equal-to any number. zero :: 0 <= a {-# inline zero #-}@@ -125,3 +199,9 @@   IsLte 'GT = 'False   IsLte 'LT = 'True   IsLte 'EQ = 'True++unlift :: (a <= b) -> (a <=# b)+unlift _ = Lte# (# #)++lift :: (a <=# b) -> (a <= b)+lift _ = Lte

@@ -2,10 +2,12 @@ {-# language ExplicitForAll #-} {-# language KindSignatures #-} {-# language MagicHash #-}+{-# language PatternSynonyms #-} {-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeOperators #-} {-# language UnboxedTuples #-}+{-# language UnboxedSums #-}  module Arithmetic.Nat   ( -- * Addition@@ -20,13 +22,18 @@   , times     -- * Successor   , succ+  , succ#     -- * Compare   , testEqual+  , testEqual#   , testLessThan+  , testLessThan#   , testLessThanEqual   , testZero+  , testZero#   , (=?)   , (<?)+  , (<?#)   , (<=?)     -- * Constants   , zero@@ -34,23 +41,48 @@   , two   , three   , constant+  , constant#     -- * Unboxed Constants   , zero#+  , one#+    -- * Unboxed Pattern Synonyms+  , pattern N0#+  , pattern N1#+  , pattern N2#+  , pattern N3#+  , pattern N4#+  , pattern N5#+  , pattern N6#+  , pattern N7#+  , pattern N8#+  , pattern N16#+  , pattern N32#+  , pattern N64#+  , pattern N128#+  , pattern N256#+  , pattern N512#+  , pattern N1024#+  , pattern N2048#+  , pattern N4096#     -- * Convert   , demote+  , demote#   , unlift   , lift   , with+  , with#   ) where  import Prelude hiding (succ)  import Arithmetic.Types-import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))-import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt))-import GHC.Exts (Proxy#,proxy#,(+#))+import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte), (:=:#)(Eq#))+import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt),type (<#)(Lt#))+import GHC.Exts (Proxy#,proxy#,(+#),(<#),Int#,(==#)) import GHC.TypeNats (type (+),type (-),Div,KnownNat,natVal') import GHC.Int (Int(I#))+import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)+import Data.Either.Void (EitherVoid#, pattern LeftVoid#, pattern RightVoid#)  import qualified GHC.TypeNats as GHC @@ -69,6 +101,10 @@ {-# inline (=?) #-} (=?) = testEqual +(<?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)+{-# inline (<?#) #-}+(<?#) = testLessThan#+ -- | Is the first argument strictly less than the second -- argument? testLessThan :: Nat a -> Nat b -> Maybe (a < b)@@ -77,6 +113,12 @@   then Just Lt   else Nothing +testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)+{-# inline testLessThan# #-}+testLessThan# (Nat# x) (Nat# y) = case x <# y of+  0# -> NothingVoid#+  _ -> JustVoid# (Lt# (# #))+ -- | Is the first argument less-than-or-equal-to the second -- argument? testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)@@ -92,6 +134,12 @@   then Just Eq   else Nothing +testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b)+{-# inline testEqual# #-}+testEqual# (Nat# x) (Nat# y) = case x ==# y of+  0# -> NothingVoid#+  _ -> JustVoid# (Eq# (# #))+ -- | Is zero equal to this number or less than it? testZero :: Nat a -> Either (0 :=: a) (0 < a) {-# inline testZero #-}@@ -99,6 +147,11 @@   0 -> Left Eq   _ -> Right Lt +testZero# :: Nat# a -> EitherVoid# (0 :=:# a) (0 <# a)+testZero# (Nat# x) = case x of+  0# -> LeftVoid# (Eq# (# #))+  _ -> RightVoid# (Lt# (# #))+ -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b) {-# inline plus #-}@@ -132,6 +185,11 @@ {-# inline succ #-} succ n = plus n one +-- | Unlifted variant of 'succ'.+succ# :: Nat# a -> Nat# (a + 1)+{-# inline succ# #-}+succ# n = plus# n (one# (# #))+ -- | Subtract the second argument from the first argument. monus :: Nat a -> Nat b -> Maybe (Difference a b) {-# inline monus #-}@@ -166,10 +224,19 @@ {-# inline constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n))) +constant# :: forall n. KnownNat n => (# #) -> Nat# n+{-# inline constant# #-}+constant# _ = case fromIntegral (natVal' (proxy# :: Proxy# n)) of+  I# i -> Nat# i+ -- | The number zero. Unboxed. zero# :: (# #) -> Nat# 0 zero# _ = Nat# 0# +-- | The number one. Unboxed.+one# :: (# #) -> Nat# 1+one# _ = Nat# 1#+ -- | Extract the 'Int' from a 'Nat'. This is intended to be used -- at a boundary where a safe interface meets the unsafe primitives -- on top of which it is built.@@ -177,6 +244,10 @@ {-# inline demote #-} demote (Nat n) = n +demote# :: Nat# n -> Int#+{-# inline demote# #-}+demote# (Nat# n) = n+ -- | Run a computation on a witness of a type-level number. The -- argument 'Int' must be greater than or equal to zero. This is -- not checked. Failure to upload this invariant will lead to a@@ -185,6 +256,10 @@ {-# inline with #-} with i f = f (Nat i) +with# :: Int# -> (forall n. Nat# n -> a) -> a+{-# inline with# #-}+with# i f = f (Nat# i)+ unlift :: Nat n -> Nat# n {-# inline unlift #-} unlift (Nat (I# i)) = Nat# i@@ -192,3 +267,57 @@ lift :: Nat# n -> Nat n {-# inline lift #-} lift (Nat# i) = Nat (I# i)++pattern N0# :: Nat# 0+pattern N0# = Nat# 0#++pattern N1# :: Nat# 1+pattern N1# = Nat# 1#++pattern N2# :: Nat# 2+pattern N2# = Nat# 2#++pattern N3# :: Nat# 3+pattern N3# = Nat# 3#++pattern N4# :: Nat# 4+pattern N4# = Nat# 4#++pattern N5# :: Nat# 5+pattern N5# = Nat# 5#++pattern N6# :: Nat# 6+pattern N6# = Nat# 6#++pattern N7# :: Nat# 7+pattern N7# = Nat# 7#++pattern N8# :: Nat# 8+pattern N8# = Nat# 8#++pattern N16# :: Nat# 16+pattern N16# = Nat# 16#++pattern N32# :: Nat# 32+pattern N32# = Nat# 32#++pattern N64# :: Nat# 64+pattern N64# = Nat# 64#++pattern N128# :: Nat# 128+pattern N128# = Nat# 128#++pattern N256# :: Nat# 256+pattern N256# = Nat# 256#++pattern N512# :: Nat# 512+pattern N512# = Nat# 512#++pattern N1024# :: Nat# 1024+pattern N1024# = Nat# 1024#++pattern N2048# :: Nat# 2048+pattern N2048# = Nat# 2048#++pattern N4096# :: Nat# 4096+pattern N4096# = Nat# 4096#

@@ -1,10 +1,14 @@ {-# language DataKinds #-} {-# language MagicHash #-} {-# language ExplicitNamespaces #-}+{-# language PatternSynonyms #-}+{-# language ViewPatterns #-} {-# language GADTs #-} {-# language KindSignatures #-} {-# language RankNTypes #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-}+{-# language UnboxedSums #-}  module Arithmetic.Types   ( Nat@@ -13,13 +17,25 @@   , Difference(..)   , Fin(..)   , Fin#+  , Fin32#+    -- * Maybe Fin+  , MaybeFin#+  , pattern MaybeFinJust#+  , pattern MaybeFinNothing#+    -- * Infix Operators   , type (<)   , type (<=)+  , type (<#)+  , type (<=#)   , type (:=:)+  , type (:=:#)   ) where -import Arithmetic.Unsafe (Fin#,Nat#,Nat(getNat), type (<=))+import Arithmetic.Unsafe (Fin#(Fin#),Nat#,Nat(getNat), type (<=))+import Arithmetic.Unsafe (Fin32#)+import Arithmetic.Unsafe (MaybeFin#(..)) import Arithmetic.Unsafe (type (<), type (:=:))+import Arithmetic.Unsafe (type (<#), type (<=#), (:=:#)) import Data.Kind (type Type) import GHC.TypeNats (type (+)) @@ -54,3 +70,16 @@  instance Ord (Fin n) where   Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)++pattern MaybeFinJust# :: Fin# n -> MaybeFin# n+pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) where+  MaybeFinJust# (Fin# i) = MaybeFin# i++pattern MaybeFinNothing# :: MaybeFin# n+pattern MaybeFinNothing# = MaybeFin# (-1#)++maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #)+{-# inline maybeFinToFin# #-}+maybeFinToFin# (MaybeFin# i) = case i of+  -1# -> (# (# #) | #)+  _ -> (# | Fin# i #)

@@ -8,22 +8,28 @@ {-# language RoleAnnotations #-} {-# language StandaloneDeriving #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-} {-# language UnliftedNewtypes #-}  module Arithmetic.Unsafe   ( Nat(..)   , Nat#(..)   , Fin#(..)+  , MaybeFin#(..)+  , Fin32#(..)+  , type (<#)(Lt#)+  , type (<=#)(Lte#)   , type (<)(Lt)   , type (<=)(Lte)   , type (:=:)(Eq)+  , type (:=:#)(Eq#)   ) where  import Prelude hiding ((>=),(<=))  import Control.Category (Category) import Data.Kind (Type)-import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))+import GHC.Exts (Int#,Int32#,TYPE,RuntimeRep(IntRep,Int32Rep,TupleRep))  import qualified Control.Category import qualified GHC.TypeNats as GHC@@ -36,7 +42,10 @@  infix 4 < infix 4 <=+infix 4 <#+infix 4 <=# infix 4 :=:+infix 4 :=:#  -- | A value-level representation of a natural number @n@. newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }@@ -54,19 +63,39 @@   Fin# :: Int# -> Fin# n type role Fin# nominal +-- | Either a @Fin#@ or Nothing. Internally, this uses negative+-- one to mean Nothing.+newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where+  MaybeFin# :: Int# -> MaybeFin# n+type role MaybeFin# nominal++-- | Variant of 'Fin#' that only allows 32-bit integers.+newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where+  Fin32# :: Int32# -> Fin32# n+type role Fin32# nominal+ -- | Proof that the first argument is strictly less than the -- second argument. data (<) :: GHC.Nat -> GHC.Nat -> Type where   Lt :: a < b +newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Lt# :: (# #) -> a <# b+ -- | Proof that the first argument is less than or equal to the -- second argument. data (<=) :: GHC.Nat -> GHC.Nat -> Type where   Lte :: a <= b +newtype (<=#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Lte# :: (# #) -> a <=# b+ -- | Proof that the first argument is equal to the second argument. data (:=:) :: GHC.Nat -> GHC.Nat -> Type where   Eq :: a :=: b++newtype (:=:#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Eq# :: (# #) -> a :=:# b  instance Category (<=) where   id = Lte