natural-arithmetic 0.1.2.0 → 0.1.3.0

raw patch · 5 files changed

+52/−2 lines, 5 filesdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• natural-arithmetic.cabal +2/−2
• src/Arithmetic/Fin.hs +21/−0
• src/Arithmetic/Nat.hs +16/−0
• src/Arithmetic/Unsafe.hs +8/−0

@@ -1,5 +1,10 @@ # Revision history for natural-arithmetic +## 0.1.3.0 -- 2022-05-23++* Add strict variant of descend.+* Add unboxed Fin type+ ## 0.1.2.0 -- 2019-01-20  * Add strict variant of descend.

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

@@ -3,6 +3,7 @@ {-# language ExplicitNamespaces #-} {-# language GADTs #-} {-# language KindSignatures #-}+{-# language MagicHash #-} {-# language ScopedTypeVariables #-} {-# language TypeApplications #-} {-# language TypeOperators #-}@@ -35,12 +36,16 @@   , absurd     -- * Demote   , demote+    -- * Lift and Unlift+  , lift+  , unlift   ) where  import Prelude hiding (last)  import Arithmetic.Nat ((<?)) import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))+import GHC.Exts (Int(I#)) import GHC.TypeNats (type (+))  import qualified Arithmetic.Lt as Lt@@ -48,20 +53,24 @@ import qualified Arithmetic.Equal as Eq import qualified Arithmetic.Nat as Nat import qualified Arithmetic.Plus as Plus+import qualified Arithmetic.Unsafe as Unsafe  -- | Raise the index by @m@ and weaken the bound by @m@, adding -- @m@ to the right-hand side of @n@. incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)+{-# inline incrementR #-} incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf)  -- | 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)+{-# inline incrementL #-} incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)  -- | Weaken the bound by @m@, adding it to the left-hand side of -- the existing bound. This does not change the index. weakenL :: forall n m. Fin n -> Fin (m + n)+{-# inline weakenL #-} weakenL (Fin i pf) = Fin i   ( Lt.substituteR     (Plus.commutative @n @m)@@ -71,15 +80,18 @@ -- | Weaken the bound by @m@, adding it to the right-hand side of -- the existing bound. This does not change the index. weakenR :: forall n m. Fin n -> Fin (n + m)+{-# inline weakenR #-} weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero)  -- | Weaken the bound, replacing it by another number greater than -- or equal to itself. This does not change the index. weaken :: forall n m. (n <= m) -> Fin n -> Fin m+{-# inline weaken #-} weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)  -- | A finite set of no values is impossible. absurd :: Fin 0 -> void+{-# inline absurd #-} absurd (Fin _ pf) = Lt.absurd pf  -- | Fold over the numbers bounded by @n@ in descending@@ -325,4 +337,13 @@ -- at a boundary where a safe interface meets the unsafe primitives -- on top of which it is built. demote :: Fin n -> Int+{-# inline demote #-} demote (Fin i _) = Nat.demote i++lift :: Unsafe.Fin# n -> Fin n+{-# inline lift #-}+lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt++unlift :: Fin n -> Unsafe.Fin# n+{-# inline unlift #-}+unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i

@@ -42,19 +42,23 @@  -- | Infix synonym of 'testLessThan'. (<?) :: Nat a -> Nat b -> Maybe (a < b)+{-# inline (<?) #-} (<?) = testLessThan  -- | Infix synonym of 'testLessThanEqual'. (<=?) :: Nat a -> Nat b -> Maybe (a <= b)+{-# inline (<=?) #-} (<=?) = testLessThanEqual  -- | Infix synonym of 'testEqual'. (=?) :: Nat a -> Nat b -> Maybe (a :=: b)+{-# inline (=?) #-} (=?) = testEqual  -- | Is the first argument strictly less than the second -- argument? testLessThan :: Nat a -> Nat b -> Maybe (a < b)+{-# inline testLessThan #-} testLessThan (Nat x) (Nat y) = if x < y   then Just Lt   else Nothing@@ -62,28 +66,33 @@ -- | Is the first argument less-than-or-equal-to the second -- argument? testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)+{-# inline testLessThanEqual #-} testLessThanEqual (Nat x) (Nat y) = if x <= y   then Just Lte   else Nothing  -- | Are the two arguments equal to one another? testEqual :: Nat a -> Nat b -> Maybe (a :=: b)+{-# inline testEqual #-} testEqual (Nat x) (Nat y) = if x == y   then Just Eq   else Nothing  -- | Is zero equal to this number or less than it? testZero :: Nat a -> Either (0 :=: a) (0 < a)+{-# inline testZero #-} testZero (Nat x) = case x of   0 -> Left Eq   _ -> Right Lt  -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b)+{-# inline plus #-} plus (Nat x) (Nat y) = Nat (x + y)  -- | The successor of a number. succ :: Nat a -> Nat (a + 1)+{-# inline succ #-} succ n = plus n one  -- | Subtract the second argument from the first argument.@@ -95,30 +104,36 @@  -- | The number zero. zero :: Nat 0+{-# inline zero #-} zero = Nat 0  -- | The number one. one :: Nat 1+{-# inline one #-} one = Nat 1  -- | The number two. two :: Nat 2+{-# inline two #-} two = Nat 2  -- | The number three. three :: Nat 3+{-# inline three #-} three = Nat 3  -- | Use GHC's built-in type-level arithmetic to create a witness -- of a type-level number. This only reduces if the number is a -- constant. constant :: forall n. KnownNat n => Nat n+{-# inline constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))  -- | 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. demote :: Nat n -> Int+{-# inline demote #-} demote (Nat n) = n  -- | Run a computation on a witness of a type-level number. The@@ -126,4 +141,5 @@ -- not checked. Failure to upload this invariant will lead to a -- segfault. with :: Int -> (forall n. Nat n -> a) -> a+{-# inline with #-} with i f = f (Nat i)

@@ -4,12 +4,15 @@ {-# language GADTSyntax #-} {-# language GeneralizedNewtypeDeriving #-} {-# language KindSignatures #-}+{-# language MagicHash #-} {-# language RoleAnnotations #-} {-# language StandaloneDeriving #-} {-# language TypeOperators #-}+{-# language UnliftedNewtypes #-}  module Arithmetic.Unsafe   ( Nat(..)+  , Fin#(..)   , type (<)(Lt)   , type (<=)(Lte)   , type (:=:)(Eq)@@ -19,6 +22,7 @@  import Control.Category (Category) import Data.Kind (Type)+import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))  import qualified Control.Category import qualified GHC.TypeNats as GHC@@ -38,6 +42,10 @@ type role Nat nominal  deriving newtype instance Show (Nat n)++-- | Finite numbers without the overhead of carrying around a proof.+newtype Fin# :: GHC.Nat -> TYPE 'IntRep where+  Fin# :: Int# -> Fin# n  -- | Proof that the first argument is strictly less than the -- second argument.