Hello community,
here is the log from the commit of package ghc-ghc-typelits-knownnat for
openSUSE:Factory checked in at 2017-05-17 10:55:27
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/ghc-ghc-typelits-knownnat (Old)
and /work/SRC/openSUSE:Factory/.ghc-ghc-typelits-knownnat.new (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "ghc-ghc-typelits-knownnat"
Wed May 17 10:55:27 2017 rev:2 rq:495444 version:0.2.4
Changes:
--------
---
/work/SRC/openSUSE:Factory/ghc-ghc-typelits-knownnat/ghc-ghc-typelits-knownnat.changes
2017-05-09 18:01:13.441221971 +0200
+++
/work/SRC/openSUSE:Factory/.ghc-ghc-typelits-knownnat.new/ghc-ghc-typelits-knownnat.changes
2017-05-17 10:55:28.849317587 +0200
@@ -1,0 +2,5 @@
+Wed Apr 19 13:32:14 UTC 2017 - [email protected]
+
+- Update to version 0.2.4 with cabal2obs.
+
+-------------------------------------------------------------------
Old:
----
ghc-typelits-knownnat-0.2.3.tar.gz
New:
----
ghc-typelits-knownnat-0.2.4.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ ghc-ghc-typelits-knownnat.spec ++++++
--- /var/tmp/diff_new_pack.zhICjG/_old 2017-05-17 10:55:29.697198306 +0200
+++ /var/tmp/diff_new_pack.zhICjG/_new 2017-05-17 10:55:29.701197743 +0200
@@ -19,7 +19,7 @@
%global pkg_name ghc-typelits-knownnat
%bcond_with tests
Name: ghc-%{pkg_name}
-Version: 0.2.3
+Version: 0.2.4
Release: 0
Summary: Derive KnownNat constraints from other KnownNat constraints
License: BSD-2-Clause
@@ -38,6 +38,7 @@
%if %{with tests}
BuildRequires: ghc-tasty-devel
BuildRequires: ghc-tasty-hunit-devel
+BuildRequires: ghc-tasty-quickcheck-devel
%endif
%description
++++++ ghc-typelits-knownnat-0.2.3.tar.gz -> ghc-typelits-knownnat-0.2.4.tar.gz
++++++
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-knownnat-0.2.3/CHANGELOG.md
new/ghc-typelits-knownnat-0.2.4/CHANGELOG.md
--- old/ghc-typelits-knownnat-0.2.3/CHANGELOG.md 2017-01-15
18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/CHANGELOG.md 2017-04-10
17:31:37.000000000 +0200
@@ -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 -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-knownnat-0.2.3/LICENSE
new/ghc-typelits-knownnat-0.2.4/LICENSE
--- old/ghc-typelits-knownnat-0.2.3/LICENSE 2017-01-15 18:51:06.000000000
+0100
+++ new/ghc-typelits-knownnat-0.2.4/LICENSE 2017-04-10 17:27:52.000000000
+0200
@@ -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 -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-knownnat-0.2.3/ghc-typelits-knownnat.cabal
new/ghc-typelits-knownnat-0.2.4/ghc-typelits-knownnat.cabal
--- old/ghc-typelits-knownnat-0.2.3/ghc-typelits-knownnat.cabal 2017-01-15
18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/ghc-typelits-knownnat.cabal 2017-04-10
17:27:52.000000000 +0200
@@ -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 -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-knownnat-0.2.3/src/GHC/TypeLits/KnownNat/Solver.hs
new/ghc-typelits-knownnat-0.2.4/src/GHC/TypeLits/KnownNat/Solver.hs
--- old/ghc-typelits-knownnat-0.2.3/src/GHC/TypeLits/KnownNat/Solver.hs
2017-01-15 18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/src/GHC/TypeLits/KnownNat/Solver.hs
2017-04-10 17:27:52.000000000 +0200
@@ -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 -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-knownnat-0.2.3/src/GHC/TypeLits/KnownNat.hs
new/ghc-typelits-knownnat-0.2.4/src/GHC/TypeLits/KnownNat.hs
--- old/ghc-typelits-knownnat-0.2.3/src/GHC/TypeLits/KnownNat.hs
2017-01-15 18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/src/GHC/TypeLits/KnownNat.hs
2017-04-10 17:27:52.000000000 +0200
@@ -106,6 +106,7 @@
( -- * Singleton natural number
SNatKn (..)
-- * Constraint-level arithmetic classes
+ , KnownNat1 (..)
, KnownNat2 (..)
, KnownNat3 (..)
-- * Template Haskell helper
@@ -125,6 +126,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.
--
-- The 'Symbol' /f/ must correspond to the fully qualified name of the
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-knownnat-0.2.3/tests/Main.hs
new/ghc-typelits-knownnat-0.2.4/tests/Main.hs
--- old/ghc-typelits-knownnat-0.2.3/tests/Main.hs 2017-01-15
18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/tests/Main.hs 2017-04-10
17:27:52.000000000 +0200
@@ -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 -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-knownnat-0.2.3/tests/TestFunctions.hs
new/ghc-typelits-knownnat-0.2.4/tests/TestFunctions.hs
--- old/ghc-typelits-knownnat-0.2.3/tests/TestFunctions.hs 2017-01-15
18:51:06.000000000 +0100
+++ new/ghc-typelits-knownnat-0.2.4/tests/TestFunctions.hs 2017-04-10
17:27:52.000000000 +0200
@@ -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)
