constraints 0.14.1 → 0.14.2

raw patch · 4 files changed

+59/−22 lines, 4 filesdep +integer-gmpdep ~hashablePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: integer-gmp

Dependency ranges changed: hashable

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +5/−0
• constraints.cabal +4/−1
• src/Data/Constraint/Nat.hs +47/−18
• src/Data/Constraint/Symbol.hs +3/−3

@@ -1,3 +1,8 @@+0.14.2 [2024.05.12]+-------------------+* Re-export `Log2` from `Data.Constraint.Nat`.+* Add `log2Nat` and `log2Pow` to `Data.Constraint.Nat`.+ 0.14.1 [2024.04.29] ------------------- * Remove an unused dependency on the `type-equality` library.

@@ -1,7 +1,7 @@ cabal-version: 2.4 name:          constraints category:      Constraints-version:       0.14.1+version:       0.14.2 license:       BSD-2-Clause license-file:  LICENSE author:        Edward A. Kmett@@ -60,6 +60,9 @@     , hashable       >= 1.2   && < 1.5     , mtl            >= 2.2   && < 2.4     , transformers   >= 0.5   && < 0.7+  if !impl(ghc >= 9.0)+    build-depends:+      integer-gmp    exposed-modules:     Data.Constraint

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-}@@ -15,8 +16,8 @@ -- -- This module is only available on GHC 8.0 or later. module Data.Constraint.Nat-  ( Min, Max, Lcm, Gcd, Divides, Div, Mod-  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat+  ( Min, Max, Lcm, Gcd, Divides, Div, Mod, Log2+  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat, log2Nat   , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne   , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates   , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes@@ -36,6 +37,7 @@   , euclideanNat   , plusMod, timesMod   , modBound+  , log2Pow   , dividesDef   , timesDiv   , eqLe, leEq, leId, leTrans@@ -47,10 +49,17 @@ import Data.Constraint.Unsafe import Data.Proxy import Data.Type.Bool-import GHC.TypeLits-#if MIN_VERSION_base(4,18,0)-import qualified GHC.TypeNats as TN+import GHC.TypeNats+import qualified Numeric.Natural as Nat++#if MIN_VERSION_base(4,15,0)+import GHC.Num.Natural (naturalLog2) #else+import GHC.Exts (Int(..))+import GHC.Integer.Logarithms (integerLog2#)+#endif++#if !MIN_VERSION_base(4,18,0) import Unsafe.Coerce #endif @@ -69,13 +78,20 @@ newtype Magic n = Magic (KnownNat n => Dict (KnownNat n)) #endif -magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o+magicNNN :: forall n m o. (Nat.Natural -> Nat.Natural -> Nat.Natural) -> (KnownNat n, KnownNat m) :- KnownNat o #if MIN_VERSION_base(4,18,0)-magic f = Sub $ TN.withKnownNat @o (unsafeSNat (fromInteger (natVal (Proxy @n) `f` natVal (Proxy @m)))) Dict+magicNNN f = Sub $ withKnownNat @o (unsafeSNat (natVal (Proxy @n) `f` natVal (Proxy @m))) Dict #else-magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))+magicNNN f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m)) #endif +magicNN :: forall n m. (Nat.Natural -> Nat.Natural) -> KnownNat n :- KnownNat m+#if MIN_VERSION_base(4,18,0)+magicNN f = Sub $ withKnownNat @m (unsafeSNat (f (natVal (Proxy @n)))) Dict+#else+magicNN f = Sub $ unsafeCoerce (Magic Dict) (f (natVal (Proxy :: Proxy n)))+#endif+ axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b) axiomLe = unsafeAxiom @@ -107,35 +123,45 @@ lcmOne = unsafeAxiom  gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)-gcdNat = magic gcd+gcdNat = magicNNN gcd  lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)-lcmNat = magic lcm+lcmNat = magicNNN lcm  plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)-plusNat = magic (+)+plusNat = magicNNN (+)  minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)-minusNat = Sub $ case magic @n @m (-) of Sub r -> r+minusNat = Sub $ case magicNNN @n @m (-) of Sub r -> r  minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)-minNat = magic min+minNat = magicNNN min  maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)-maxNat = magic max+maxNat = magicNNN max  timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)-timesNat = magic (*)+timesNat = magicNNN (*)  powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)-powNat = magic (^)+powNat = magicNNN (^)  divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)-divNat = Sub $ case magic @n @m div of Sub r -> r+divNat = Sub $ case magicNNN @n @m div of Sub r -> r  modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)-modNat = Sub $ case magic @n @m mod of Sub r -> r+modNat = Sub $ case magicNNN @n @m mod of Sub r -> r +log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)+log2Nat = Sub $ case magicNN @n log2 of Sub r -> r+  where+    log2 :: Nat.Natural -> Nat.Natural+#if MIN_VERSION_base(4,15,0)+    log2 n = fromIntegral (naturalLog2 n)+#else+    log2 n = fromIntegral (I# (integerLog2# (toInteger n)))+#endif+ plusZero :: forall n. Dict ((n + 0) ~ n) plusZero = Dict @@ -231,6 +257,9 @@  modBound :: forall m n. (1 <= n) :- (Mod m n <= n) modBound = Sub unsafeAxiom++log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)+log2Pow = unsafeAxiom  euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c)) euclideanNat = Sub unsafeAxiom

@@ -64,21 +64,21 @@ #if MIN_VERSION_base(4,18,0) magicNSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))) Dict #else-magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m))+magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m)) #endif  magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o #if MIN_VERSION_base(4,18,0) magicSSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))) Dict #else-magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m))+magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy @n) `f` symbolVal (Proxy @m)) #endif  magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n #if MIN_VERSION_base(4,18,0) magicSN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (symbolVal (Proxy :: Proxy a))))) Dict #else-magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy :: Proxy a))))+magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy @a)))) #endif  -- operations