finite-typelits 0.2.0.1 → 0.2.1.0

raw patch · 4 files changed

+103/−106 lines, 4 filesdep ~QuickCheckdep ~basedep ~taggedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: QuickCheck, base, tagged, template-haskell

API changes (from Hackage documentation)

Files

• finite-typelits.cabal +1/−1
• src/Data/Finite/Integral.hs +8/−0
• src/Data/Finite/Internal/Integral.hs +18/−4
• test/Main.hs +76/−101

@@ -1,5 +1,5 @@ name:                finite-typelits-version:             0.2.0.1+version:             0.2.1.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

@@ -33,6 +33,7 @@         combineSum, combineZero, combineProduct, combineOne, combineExponential,         separateSum, separateZero, separateProduct, separateOne,         separateExponential,+        castFinite,         isValidFinite     )     where@@ -344,6 +345,13 @@             where n' = n `div` m         m = intVal (Proxy :: Proxy m) {-# INLINABLE separateExponential #-}++-- | Convert a 'Finite' between different 'SaneIntegral' numeric types.+castFinite+    :: forall b a n. (SaneIntegral a, SaneIntegral b, Limited b n)+    => Finite a n -> Finite b n+castFinite (Finite x) = Finite $ fromIntegral x+{-# INLINABLE castFinite #-}  -- | Verifies that a given 'Finite' is valid. Should always return 'True' unless -- you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or

@@ -10,6 +10,7 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}@@ -106,6 +107,17 @@     modMul n a b = fromInteger         (modMul (toInteger n) (toInteger a) (toInteger b) :: Integer) +    -- | Unsafely obtain evidence that @n <= Limit a@. When 'Limit' is 'Nothing'+    -- there is no evidence to obtain, and @\\_ _ k -> k@ is a valid+    -- implementation. When 'Limit' is a 'Just', the default implementation+    -- should work.+    unsafeWithLimited :: proxy1 a -> proxy2 n -> (Limited a n => r) -> r+    default unsafeWithLimited+        :: forall n r lim proxy1 proxy2. (Limit a ~ 'Just lim)+        => proxy1 a -> proxy2 n -> (Limited a n => r) -> r+    unsafeWithLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of+        Refl -> k+ instance SaneIntegral Integer where     type Limit Integer = 'Nothing     modAdd n a b = case a + b of@@ -113,6 +125,7 @@         r -> r     modSub n a b = if a >= b then a - b else n - b + a     modMul n a b = (a * b) `mod` n+    unsafeWithLimited _ _ k = k  #if MIN_VERSION_base(4,8,0) instance SaneIntegral Natural where@@ -122,6 +135,7 @@         r -> r     modSub n a b = if a >= b then a - b else n - b + a     modMul n a b = (a * b) `mod` n+    unsafeWithLimited _ _ k = k #endif  instance SaneIntegral Word where@@ -252,7 +266,7 @@     :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)     => proxy1 a -> proxy2 n -> (KnownNat n => r) -> r withIntegral _ _ k = case someNatVal n of-    Nothing -> error $ "withIntegral: got KnowIntegral instance dictionary "+    Nothing -> error $ "withIntegral: got KnownIntegral instance dictionary "         ++ " for which toInteger returns " ++ show n     Just (SomeNat (_ :: Proxy m)) -> case unsafeCoerce Refl :: n :~: m of         Refl -> k@@ -261,10 +275,10 @@  -- | Recover a 'Limited' constraint from a 'KnownIntegral' constraint. withLimited-    :: forall a n r lim proxy1 proxy2. (Limit a ~ 'Just lim, KnownIntegral a n)+    :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)     => proxy1 a -> proxy2 n -> (Limited a n => r) -> r-withLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of-    Refl -> k+withLimited = unsafeWithLimited+  where _n = intVal_ :: Tagged n a {-# INLINABLE withLimited #-}  -- | Finite number type. The type @'Finite' a n@ is inhabited by exactly @n@

@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -11,6 +12,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} module Main where  import Control.Exception@@ -96,23 +98,26 @@ data SLimited a where     SLimited :: (Limited a n, KnownNat n) => Proxy n -> SLimited a -mkLimited-    :: forall a lim. (Limit a ~ 'Just lim, KnownNat lim)-    => Integer -> Maybe (SLimited a)-mkLimited n = case someNatVal n of-    Just (SomeNat (p :: Proxy b))-        | n <= natVal @lim Proxy-        , Refl :: (b <=? lim) :~: 'True <- unsafeCoerce Refl-        -> Just $ SLimited p-    _ -> Nothing+class MkSLimited (lim :: Maybe Nat) where+    mkSLimited+        :: forall a. (SaneIntegral a, Limit a ~ lim)+        => Integer -> Maybe (SLimited a) -mkUnlimited-    :: forall a. Limit a ~ 'Nothing-    => Integer -> Maybe (SLimited a)-mkUnlimited n = case someNatVal n of-    Just (SomeNat p) -> Just $ SLimited p-    _ -> Nothing+instance KnownNat lim => MkSLimited ('Just lim) where+    mkSLimited+        :: forall a. (SaneIntegral a, Limit a ~ 'Just lim)+        => Integer -> Maybe (SLimited a)+    mkSLimited n = case someNatVal n of+        Just (SomeNat p)+            | n <= natVal @lim Proxy+            -> Just $ unsafeWithLimited (Proxy @a) p $ SLimited p+        _ -> Nothing +instance MkSLimited 'Nothing where+    mkSLimited n = case someNatVal n of+        Just (SomeNat p) -> Just $ SLimited p+        _ -> Nothing+ genSmall, genOver7, genOver8, genOver15, genOver16, genOver31, genOver32,     genOver63, genOver64, genOverI, genOverW, genUnder7, genUnder8, genUnder15,     genUnder16, genUnder32, genUnder63, genUnder64, genUnderI, genUnderW@@ -139,14 +144,19 @@ genUnderI = ((toInteger (maxBound @Int) -) <$> genSmall) `suchThat` (>= 0) genUnderW = ((toInteger (maxBound @Word) -) <$> genSmall) `suchThat` (>= 0) +shrinkSLimited+    :: (SaneIntegral a, MkSLimited (Limit a), Arbitrary a)+    => SLimited a -> [SLimited a]+shrinkSLimited (SLimited p) = mapMaybe mkSLimited $ shrink $ natVal p+ instance Arbitrary (SLimited Integer) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI         , genOverI, genUnderW, genOverW ]-        `suchThatMap` mkUnlimited-    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Natural) where     arbitrary = oneof@@ -154,8 +164,8 @@         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI         , genOverI, genUnderW, genOverW ]-        `suchThatMap` mkUnlimited-    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Word) where     arbitrary = oneof@@ -163,55 +173,55 @@         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI         , genOverI, genUnderW ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Int) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Word8) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Int8) where     arbitrary = oneof         [ genSmall, genUnder7 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Word16) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Int16) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Word32) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Int32) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16, genOver16, genUnder31 ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Word64) where     arbitrary = oneof@@ -219,65 +229,22 @@         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genOver63, genUnder64, genOverI, genUnderW         , genOverW ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  instance Arbitrary (SLimited Int64) where     arbitrary = oneof         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32         , genOver32, genUnder63, genUnderI, genOverI, genUnderW, genOverW ]-        `suchThatMap` mkLimited-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p+        `suchThatMap` mkSLimited+    shrink = shrinkSLimited  newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a } -instance Arbitrary (SmallLimited Integer) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Natural) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Word) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Int) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Word8) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Int8) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Word16) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Int16) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Word32) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Int32) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Word64) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited-    shrink = map SmallLimited . shrink . getSmallLimited--instance Arbitrary (SmallLimited Int64) where-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+instance (SaneIntegral a, MkSLimited (Limit a), Arbitrary (SLimited a))+    => Arbitrary (SmallLimited a) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkSLimited     shrink = map SmallLimited . shrink . getSmallLimited  type Good a =@@ -288,7 +255,7 @@     , SaneIntegral a     , Arbitrary a     , Arbitrary (SLimited a)-    , Arbitrary (SmallLimited a)+    , MkSLimited (Limit a)     , CoArbitrary a     ) @@ -357,23 +324,10 @@     (map getSmallLimited . shrink . SmallLimited)  unsafeWithKnownIntegral-    :: forall n a. (SaneIntegral a, Typeable a)+    :: forall n a. (SaneIntegral a, MkSLimited (Limit a), Typeable a)     => Integer -> ((KnownNat n, Limited a n) => Property) -> Property unsafeWithKnownIntegral n prop-    | Just (Refl :: a :~: Integer) <- cast (Refl @a)-    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n-    , Refl <- unsafeCoerce Refl :: n :~: n'-    = prop-    | Just (Refl :: a :~: Natural) <- cast (Refl @a)-    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n-    , Refl <- unsafeCoerce Refl :: n :~: n'-    = prop-    | Just (Refl :: a :~: Word) <- cast (Refl @a)-    , Just (SLimited (_ :: Proxy n')) <- mkLimited @a n-    , Refl <- unsafeCoerce Refl :: n :~: n'-    = prop-    | Just (Refl :: a :~: Int) <- cast (Refl @a)-    , Just (SLimited (_ :: Proxy n')) <- mkLimited @a n+    | Just (SLimited (_ :: Proxy n')) <- mkSLimited @_ @a n     , Refl <- unsafeCoerce Refl :: n :~: n'     = prop     | otherwise = discard@@ -1113,6 +1067,27 @@     property $ \(Big f :: Big a (m ^ n)) ->     f `seq` -- could be discard         combineExponential (separateExponential @n @m @a f) === f++prop_valid_castFinite = forType $ \(_ :: Proxy b) ->+    forType $ \(_ :: Proxy a) ->+    forPositiveLimit @b $ \n (_ :: Proxy n) ->+    unsafeWithKnownIntegral @n @a n $+    property $ \(Edgy x :: Edgy a n) ->+        isValidFinite $ castFinite @b x+prop_sym_castFinite = forType $ \(_ :: Proxy a) ->+    forType $ \(_ :: Proxy b) ->+    forPositiveLimit @a $ \n (_ :: Proxy n) ->+    unsafeWithKnownIntegral @n @b n $+    property $ \(Edgy x :: Edgy b n) ->+        castFinite @b (castFinite @a x) === x+prop_trans_castFinite = forType $ \(_ :: Proxy a) ->+    forType $ \(_ :: Proxy b) ->+    forType $ \(_ :: Proxy c) ->+    forPositiveLimit @a $ \n (_ :: Proxy n) ->+    unsafeWithKnownIntegral @n @b n $+    unsafeWithKnownIntegral @n @c n $+    property $ \(Edgy x :: Edgy a n) ->+        castFinite @c (castFinite @b x) === castFinite @c x  return [] main = $quickCheckAll >>= \case