natural-arithmetic 0.1.1.0 → 0.1.2.0

raw patch · 4 files changed

+34/−2 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• natural-arithmetic.cabal +1/−1
• src/Arithmetic/Fin.hs +21/−0
• src/Arithmetic/Types.hs +4/−1

@@ -1,5 +1,13 @@ # Revision history for natural-arithmetic +## 0.1.2.0 -- 2019-01-20++* Add strict variant of descend.++## 0.1.1.0 -- 2019-11-22++* Undocumented+ ## 0.1.0.0 -- 2019-09-04  * Initial release.

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

@@ -24,6 +24,7 @@   , ascendM   , ascendM_   , descend+  , descend'   , descendM   , descendM_   , ascending@@ -98,6 +99,26 @@   go !m = case m <? n of     Nothing -> b0     Just lt -> f (Fin m lt) (go (Nat.succ m))++-- | 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.+--+-- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))+descend' :: forall a n.+     Nat n -- ^ Upper bound+  -> a -- ^ Initial accumulator+  -> (Fin n -> a -> a) -- ^ Update accumulator+  -> a+{-# inline descend' #-}+descend' !n !b0 f = go n Lte.reflexive b0+  where+    go :: Nat p -> p <= n -> a -> a+    go !m pLteEn !b = case Nat.monus m Nat.one of+      Nothing -> b+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+        let !cLtEn = descendLemma cPlusOneEqP pLteEn+        in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b)  -- | Fold over the numbers bounded by @n@ in ascending order. This -- is lazy in the accumulator.

@@ -23,7 +23,10 @@ import qualified GHC.TypeNats as GHC  data WithNat :: (GHC.Nat -> Type) -> Type where-  WithNat :: Nat n -> f n -> WithNat f+  WithNat ::+       {-# UNPACK #-} !(Nat n)+    -> f n+    -> WithNat f  -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }' data Fin :: GHC.Nat -> Type where