packages feed

ghc-typelits-knownnat 0.2.4 → 0.3

raw patch · 5 files changed

+78/−35 lines, 5 filesdep ~basedep ~ghcdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, ghc, singletons

API changes (from Hackage documentation)

Files

CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.3 *May 15th 2017*+* GHC 8.2.1 support: Underlying representation for `KnownNat` in GHC 8.2 is `Natural`, meaning users of this plugin will need to update their code to use `Natural` for GHC 8.2 as well.+ ## 0.2.4 *April 10th 2017* * New features:   * Derive constraints for unary functions via a `KnownNat1` instance; thanks to @nshepperd [#11](https://github.com/clash-lang/ghc-typelits-knownnat/pull/11)
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name:                ghc-typelits-knownnat-version:             0.2.4+version:             0.3 synopsis:            Derive KnownNat constraints from other KnownNat constraints description:   A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -81,8 +81,8 @@                        TypeInType                        UndecidableInstances                        ViewPatterns-  build-depends:       base                      >= 4.9      && <4.10,-                       ghc                       >= 8.0.1    && <8.2,+  build-depends:       base                      >= 4.9      && <5,+                       ghc                       >= 8.0.1    && <8.4,                        ghc-tcplugins-extra       >= 0.2,                        ghc-typelits-natnormalise >= 0.5.2    && <0.6,                        singletons                >= 2.2      && <3.0,
src/GHC/TypeLits/KnownNat.hs view
@@ -85,6 +85,7 @@ -}  {-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE CPP                   #-} {-# LANGUAGE DataKinds             #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE KindSignatures        #-}@@ -116,15 +117,29 @@  import Data.Bits              (shiftL) import Data.Proxy             (Proxy (..))+#if MIN_VERSION_ghc(8,2,0)+import GHC.TypeNats+  (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=), natVal)+import GHC.TypeLits           (Symbol)+#else import GHC.TypeLits           (KnownNat, Nat, Symbol, type (+), type (*),                                type (^), type (-), type (<=), natVal)+#endif import Data.Singletons        (type (~>), type (@@)) import Data.Promotion.Prelude (type (:+$), type (:*$), type (:^$), type (:-$))+#if MIN_VERSION_ghc(8,2,0)+import Numeric.Natural        (Natural)+#endif  import GHC.TypeLits.KnownNat.TH --- | Singleton natural number (represented by an integer)-newtype SNatKn (n :: Nat) = SNatKn Integer+-- | Singleton natural number+newtype SNatKn (n :: Nat) =+#if MIN_VERSION_ghc(8,2,0)+  SNatKn Natural+#else+  SNatKn Integer+#endif  -- | Class for arithmetic functions with /one/ argument. --@@ -171,7 +186,7 @@   natSing2 = let x = natVal (Proxy @ a)                  y = natVal (Proxy @ b)                  z = case x of-                       2 -> shiftL 1 (fromInteger y)+                       2 -> shiftL 1 (fromIntegral y)                        _ -> x ^ y              in  SNatKn z   {-# INLINE natSing2 #-}
tests/Main.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators,+{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators,              TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}@@ -8,7 +8,12 @@  import Data.Proxy import Data.Type.Equality ((:~:)(..))+#if __GLASGOW_HASKELL__ >= 802+import GHC.TypeNats+import Numeric.Natural+#else import GHC.TypeLits+#endif import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck@@ -16,14 +21,20 @@  import TestFunctions -addT :: Integer -> Integer -> Integer+#if __GLASGOW_HASKELL__ >= 802+type Number = Natural+#else+type Number = Integer+#endif++addT :: Number -> Number -> Number addT a b = withNat a $            \(Proxy :: Proxy a) ->              withNat b $              \(Proxy :: Proxy b) ->                natVal (Proxy :: Proxy (a + b)) -subT :: Integer -> Integer -> Integer+subT :: Number -> Number -> Number subT a b   | a >= b = withNat a $              \(Proxy :: Proxy a) ->@@ -34,77 +45,77 @@                      natVal (Proxy :: Proxy (a - b))   | otherwise = error "a - b < 0" -mulT :: Integer -> Integer -> Integer+mulT :: Number -> Number -> Number mulT a b = withNat a $            \(Proxy :: Proxy a) ->              withNat b $              \(Proxy :: Proxy b) ->                natVal (Proxy :: Proxy (a * b)) -maxT :: Integer -> Integer -> Integer+maxT :: Number -> Number -> Number maxT a b = withNat a $            \(Proxy :: Proxy a) ->              withNat b $              \(Proxy :: Proxy b) ->                natVal (Proxy :: Proxy (Max a b)) -logT :: Integer -> Integer+logT :: Number -> Number logT n = withNat n $ \(Proxy :: Proxy n) ->                            natVal (Proxy :: Proxy (Log n)) -test1 :: forall n . KnownNat n => Proxy n -> Integer+test1 :: forall n . KnownNat n => Proxy n -> Number test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) -test2 :: forall n . KnownNat n => Proxy n -> Integer+test2 :: forall n . KnownNat n => Proxy n -> Number test2 _ = natVal (Proxy :: Proxy (n*3)) -test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test3 _ _ = natVal (Proxy :: Proxy (n+m)) -test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test4 _ _ = natVal (Proxy :: Proxy (n*m)) -test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test5 _ _ = natVal (Proxy :: Proxy (n^m)) -test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) -test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Integer+test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Number test7 _ _ = natVal (Proxy :: Proxy (Max n m + 1)) -test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Integer+test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Number test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1)) -test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Integer+test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Number test9 _ _ = natVal (Proxy :: Proxy (m-n)) -test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Integer+test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Number test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) -test11 :: forall m . (KnownNat m) => Proxy m -> Integer+test11 :: forall m . (KnownNat m) => Proxy m -> Number test11 _ = natVal (Proxy @ (m*m)) -test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Integer+test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number test12 = natVal -test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Integer+test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number test13 = natVal -test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Integer+test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Number test14 = natVal  type family Foo (m :: Nat) = (result :: Nat) | result -> m fakeFooEvidence :: 1 :~: Foo 1 fakeFooEvidence = unsafeCoerce Refl -test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Integer+test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Number test15 _ _ = natVal (Proxy @ (Foo 1 + 7)) -test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Integer+test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Number test16 _ _ = natVal (Proxy @ (Foo 1 + 7 + Foo 1)) -test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Integer+test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1))  data SNat :: Nat -> * where@@ -131,19 +142,19 @@ test19 :: SNat (a+b) -> SNat b -> SNat a test19 = subSNat -test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer+test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Number test20 _ = natVal (Proxy @ (2 * a)) -test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer+test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Number test21 _ _ = natVal (Proxy :: Proxy n) -test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number test22 _ _ = natVal (Proxy :: Proxy (y*x*y))  test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat -test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer+test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number test24 = natVal  tests :: TestTree
tests/TestFunctions.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,+{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures,              MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell,              TypeApplications, TypeFamilies, TypeOperators,              UndecidableInstances #-}@@ -9,7 +9,12 @@ import Data.Singletons.TH    (genDefunSymbols) import Data.Type.Bool        (If) import GHC.TypeLits.KnownNat+#if __GLASGOW_HASKELL__ >= 802+import GHC.TypeNats+import Numeric.Natural+#else import GHC.TypeLits+#endif  type family Max (a :: Nat) (b :: Nat) :: Nat where   Max 0 b = b -- See [Note: single equation TFs are treated like synonyms]@@ -38,17 +43,26 @@   Min a b = If (a <=? b) a b  -- Unary functions.-+#if __GLASGOW_HASKELL__ >= 802+withNat :: Natural -> (forall n. (KnownNat n) => Proxy n -> r) -> r+withNat n f = case someNatVal n of+  SomeNat proxy -> f proxy+#else withNat :: Integer -> (forall n. (KnownNat n) => Proxy n -> r) -> r withNat n f = case someNatVal n of                Just (SomeNat proxy) -> f proxy                Nothing              -> error ("withNat: negative value (" ++ show n ++ ")")+#endif  type family Log (n :: Nat) :: Nat where  genDefunSymbols [''Log] +#if __GLASGOW_HASKELL__ >= 802+logInt :: Natural -> Natural+#else logInt :: Integer -> Integer+#endif logInt 0 = error "log 0" logInt n = go 0   where