ghc-typelits-knownnat 0.2.3 → 0.2.4

raw patch · 7 files changed

+118/−10 lines, 7 filesdep +tasty-quickcheckPVP ok

version bump matches the API change (PVP)

Dependencies added: tasty-quickcheck

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• LICENSE +2/−1
• ghc-typelits-knownnat.cabal +3/−2
• src/GHC/TypeLits/KnownNat.hs +10/−0
• src/GHC/TypeLits/KnownNat/Solver.hs +21/−6
• tests/Main.hs +51/−0
• tests/TestFunctions.hs +26/−1

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 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)+  * Use type-substituted [G]iven KnownNats (partial solve for [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13))+ ## 0.2.3 *January 15th 2017* * Solve normalised literal constraints, i.e.:   * `KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2`

@@ -1,5 +1,6 @@ Copyright (c) 2015-2016, University of Twente,-              2017, QBayLogic+              2017, QBayLogic,+              2017, Google Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -1,5 +1,5 @@ name:                ghc-typelits-knownnat-version:             0.2.3+version:             0.2.4 synopsis:            Derive KnownNat constraints from other KnownNat constraints description:   A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -104,7 +104,8 @@                        ghc-typelits-natnormalise >= 0.5   && <0.6,                        singletons                >= 2.2   && <3.0,                        tasty                     >= 0.10,-                       tasty-hunit               >= 0.9+                       tasty-hunit               >= 0.9,+                       tasty-quickcheck          >= 0.8   hs-source-dirs:      tests   default-language:    Haskell2010   other-extensions:    DataKinds

@@ -106,6 +106,7 @@   ( -- * Singleton natural number     SNatKn (..)     -- * Constraint-level arithmetic classes+  , KnownNat1 (..)   , KnownNat2 (..)   , KnownNat3 (..)     -- * Template Haskell helper@@ -124,6 +125,15 @@  -- | Singleton natural number (represented by an integer) newtype SNatKn (n :: Nat) = SNatKn Integer++-- | Class for arithmetic functions with /one/ argument.+--+-- The 'Symbol' /f/ must correspond to the fully qualified name of the+-- type-level operation. Use 'nameToSymbol' to get the fully qualified+-- TH Name as a 'Symbol'+class KnownNat1 (f :: Symbol) (a :: Nat) where+  type KnownNatF1 f :: Nat ~> Nat+  natSing1 :: SNatKn (KnownNatF1 f @@ a)  -- | Class for arithmetic functions with /two/ arguments. --

@@ -121,9 +121,10 @@                    ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,                    mkNonCanonical, setCtLoc, setCtLocSpan) import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)-import Type       (PredTree (ClassPred), PredType, classifyPredType, dropForAlls,-                   funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys,-                   splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe)+import Type+  (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType,+   dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,+   piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe) import TyCon      (tyConName) import TyCoRep    (Type (..), TyLit (..)) import Var        (DFunId)@@ -270,9 +271,11 @@ lookupKnownNatDefs :: TcPluginM KnownNatDefs lookupKnownNatDefs = do     md     <- lookupModule myModule myPackage+    kn1C   <- look md "KnownNat1"     kn2C   <- look md "KnownNat2"     kn3C   <- look md "KnownNat3"-    return $ (\case { 2 -> Just kn2C+    return $ (\case { 1 -> Just kn1C+                    ; 2 -> Just kn2C                     ; 3 -> Just kn3C                     ; _ -> Nothing                     })@@ -369,17 +372,29 @@     -- the two are a constant offset apart.     offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))     offset want = runMaybeT $ do-      let unKn ty' = case classifyPredType ty' of+      let -- Get the knownnat contraints+          unKn ty' = case classifyPredType ty' of                        ClassPred cls' [ty'']                          | className cls' == knownNatClassName                          -> Just ty''                        _ -> Nothing+          -- Get the rewrites+          unEq ty' = case classifyPredType ty' of+                       EqPred NomEq ty1 ty2 -> Just (ty1,ty2)+                       _ -> Nothing+          rewrites = mapMaybe (unEq . unCType . fst) givens+          -- Rewrite+          rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2+                                  | ty2 `eqType` tyK = Just ty1+                                  | otherwise        = Nothing           -- Get only the [G]iven KnownNat constraints           knowns   = mapMaybe (unKn . unCType . fst) givens+          -- Get all the rewritten KNs+          knownsR  = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns           -- pair up the sum-of-products KnownNat constraints           -- with the original Nat operation           subWant  = mkTyConApp typeNatSubTyCon . (:[want])-          exploded = map (normaliseNat . subWant &&& id) knowns+          exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR)           -- interesting cases for us are those where           -- wanted and given only differ by a constant           examineDiff (S [P [I n]]) entire = Just (entire,I n)

@@ -11,10 +11,47 @@ import GHC.TypeLits import Test.Tasty import Test.Tasty.HUnit+import Test.Tasty.QuickCheck import Unsafe.Coerce (unsafeCoerce)  import TestFunctions +addT :: Integer -> Integer -> Integer+addT a b = withNat a $+           \(Proxy :: Proxy a) ->+             withNat b $+             \(Proxy :: Proxy b) ->+               natVal (Proxy :: Proxy (a + b))++subT :: Integer -> Integer -> Integer+subT a b+  | a >= b = withNat a $+             \(Proxy :: Proxy a) ->+               withNat b $+               \(Proxy :: Proxy b) ->+                 case unsafeCoerce Refl of+                   (Refl :: (b <=? a) :~: True) ->+                     natVal (Proxy :: Proxy (a - b))+  | otherwise = error "a - b < 0"++mulT :: Integer -> Integer -> Integer+mulT a b = withNat a $+           \(Proxy :: Proxy a) ->+             withNat b $+             \(Proxy :: Proxy b) ->+               natVal (Proxy :: Proxy (a * b))++maxT :: Integer -> Integer -> Integer+maxT a b = withNat a $+           \(Proxy :: Proxy a) ->+             withNat b $+             \(Proxy :: Proxy b) ->+               natVal (Proxy :: Proxy (Max a b))++logT :: Integer -> Integer+logT n = withNat n $ \(Proxy :: Proxy n) ->+                           natVal (Proxy :: Proxy (Log n))+ test1 :: forall n . KnownNat n => Proxy n -> Integer test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @@ -106,6 +143,9 @@ test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat +test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer+test24 = natVal+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise"   [ testGroup "Basic functionality"@@ -191,6 +231,17 @@     , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $       show (test23 (SNat @ 8)) @?=       "2"+    , testCase "(KnownNat n, n ~ m + 1) ~ KnownNat m" $+      show (test24 (Proxy @4)) @?=+      "4"++    ],+    testGroup "QuickCheck"+    [ testProperty "addT = (+)" $ (\a b -> (a >= 0 && b >= 0) ==> (addT a b === a + b)),+      testProperty "subT = (-)" $ (\a b -> (a >= b && b >= 0) ==> (subT a b === a - b)),+      testProperty "mulT = (*)" $ (\a b -> (a >= 0 && b >= 0) ==> (mulT a b === a * b)),+      testProperty "maxT = max" $ (\a b -> (a >= 0 && b >= 0) ==> (maxT a b === max a b)),+      testProperty "logT = logInt" $ (\a -> (a > 0) ==> (logT a == logInt a))     ]   ] 

@@ -1,5 +1,5 @@ {-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,-             MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,+             MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell,              TypeApplications, TypeFamilies, TypeOperators,              UndecidableInstances #-} @@ -36,3 +36,28 @@ type family Min (a :: Nat) (b :: Nat) :: Nat where   Min 0 b = 0 -- See [Note: single equation TFs are treated like synonyms]   Min a b = If (a <=? b) a b++-- Unary functions.++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 ++ ")")++type family Log (n :: Nat) :: Nat where++genDefunSymbols [''Log]++logInt :: Integer -> Integer+logInt 0 = error "log 0"+logInt n = go 0+  where+    go k = case compare (2^k) n of+             LT -> go (k + 1)+             EQ -> k+             GT -> k - 1++instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where+  type KnownNatF1 $(nameToSymbol ''Log) = LogSym0+  natSing1 = let x = natVal (Proxy @ a)+             in SNatKn (logInt x)