diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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` diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -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 diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs --- a/src/GHC/TypeLits/KnownNat.hs +++ b/src/GHC/TypeLits/KnownNat.hs @@ -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. -- diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -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) diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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)) ] ] diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs --- a/tests/TestFunctions.hs +++ b/tests/TestFunctions.hs @@ -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)