finite-typelits 0.1.5.0 → 0.1.6.0

raw patch · 4 files changed

+17/−21 lines, 4 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

• LICENSE +1/−1
• finite-typelits.cabal +3/−3
• src/Data/Finite.hs +3/−3
• test/Main.hs +10/−14

@@ -1,4 +1,4 @@-Copyright (c) 2015, mniip+Copyright (c) 2015-2022, mniip  All rights reserved. 

@@ -1,5 +1,5 @@ name:                finite-typelits-version:             0.1.5.0+version:             0.1.6.0 synopsis:            A type inhabited by finitely many values, indexed by type-level naturals description:         A type inhabited by finitely many values, indexed by type-level naturals. homepage:            https://github.com/mniip/finite-typelits@@ -14,7 +14,7 @@ library   exposed-modules:     Data.Finite                      , Data.Finite.Internal-  build-depends:       base >= 4.7 && <= 4.17+  build-depends:       base >= 4.7 && < 4.18                      , deepseq >= 1.4   hs-source-dirs:      src   default-language:    Haskell2010@@ -24,7 +24,7 @@   type:                exitcode-stdio-1.0   main-is:             test/Main.hs   build-depends:       finite-typelits-                     , base >= 4.9 && <= 4.17+                     , base >= 4.9 && < 4.18                      , deepseq >= 1.4                      , QuickCheck   default-language:    Haskell2010

@@ -117,14 +117,14 @@  -- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input -- was one of the removed inhabitants.-strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)+strengthenN :: KnownNat n => Finite m -> Maybe (Finite n) strengthenN (Finite x) = result     where         result = if x < natVal (fromJust result)             then Just $ Finite x             else Nothing --- | Add multiple inhabitant in the beginning, shifting everything up by the+-- | Add multiple inhabitants in the beginning, shifting everything up by the -- amount of inhabitants added. shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m shiftN fx@(Finite x) = result@@ -134,7 +134,7 @@ -- | Remove multiple inhabitants from the beginning, shifting everything down by -- the amount of inhabitants removed. Returns 'Nothing' if the input was one of -- the removed inhabitants.-unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n)+unshiftN :: (KnownNat n, KnownNat m) => Finite m -> Maybe (Finite n) unshiftN fx@(Finite x) = result     where         result = if x < natVal fx - natVal (fromJust result)

@@ -320,15 +320,13 @@         n <= m ==> unsafeWithInequality @n @m @Property $             map (weakenN @n @m) finites === take n finites -prop_valid_strengthenN = withNat $ \n (_ :: Proxy n) ->-    withNatPos $ \m (_ :: Proxy m) ->-        n <= m ==> unsafeWithInequality @n @m @Property $-            property $ \x ->-                maybe True isValidFinite $ strengthenN @n @m x+prop_valid_strengthenN = withNat $ \_ (_ :: Proxy n) ->+    withNatPos $ \_ (_ :: Proxy m) ->+        property $ \x ->+            maybe True isValidFinite $ strengthenN @n @m x prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->     withNat $ \m (_ :: Proxy m) ->-        n <= m ==> unsafeWithInequality @m @n @Property $-            map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing+        map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing  prop_valid_shiftN = withNatPos $ \n (_ :: Proxy n) ->     withNatPos $ \m (_ :: Proxy m) ->@@ -340,15 +338,13 @@         n <= m ==> unsafeWithInequality @n @m @Property $             map (shiftN @n @m) finites === drop (m - n) finites -prop_valid_unshiftN = withNatPos $ \n (_ :: Proxy n) ->-    withNat $ \m (_ :: Proxy m) ->-        n <= m ==> unsafeWithInequality @n @m @Property $-            property $ \x ->-                maybe True isValidFinite $ unshiftN @n @m x+prop_valid_unshiftN = withNatPos $ \_ (_ :: Proxy n) ->+    withNat $ \_ (_ :: Proxy m) ->+        property $ \x ->+            maybe True isValidFinite $ unshiftN @n @m x prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->     withNat $ \m (_ :: Proxy m) ->-        m <= n ==> unsafeWithInequality @m @n @Property $-            map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)+        map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)  prop_valid_weakenProxy = withNatPos $ \n (_ :: Proxy n) ->     withNat $ \k (_ :: Proxy k) ->