summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKevinQuick <>2020-05-22 23:52:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2020-05-22 23:52:00 (GMT)
commit50cfee6650ccedc56e12a277ada8c6a4534923bc (patch)
treea2dd7515a48e8c796667923ac858afcf722d965f
parent55638de78cdaec85b1738d16c129db8506742307 (diff)
version 2.1.0HEAD2.1.0master
-rwxr-xr-xChangelog.md15
-rw-r--r--parameterized-utils.cabal8
-rw-r--r--src/Data/Parameterized/Classes.hs6
-rw-r--r--src/Data/Parameterized/Compose.hs2
-rw-r--r--src/Data/Parameterized/Context.hs1
-rw-r--r--src/Data/Parameterized/Context/Safe.hs6
-rw-r--r--src/Data/Parameterized/Context/Unsafe.hs4
-rw-r--r--src/Data/Parameterized/HashTable.hs2
-rw-r--r--src/Data/Parameterized/Map.hs8
-rw-r--r--src/Data/Parameterized/NatRepr.hs5
-rw-r--r--src/Data/Parameterized/Nonce/Transformers.hs2
-rw-r--r--src/Data/Parameterized/TH/GADT.hs1
12 files changed, 40 insertions, 20 deletions
diff --git a/Changelog.md b/Changelog.md
index 6d3e534..2e78476 100755
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,20 @@
# Changelog for the `parameterized-utils` package
+## 2.1.0 -- *2020 May 08*
+
+ * Added `plusAssoc` to the `NatRepr` module to produce `+` associativity evidence.
+ * Changed the `HashTable` module to use the Basic instead of the Cuckoo
+ implementation strategy.
+ * Added explicit kind parameters to various definitions to support
+ GHC 8.10's adoption of [proposal 103](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0103-no-kind-vars.rst).
+ This is a modification to the type signatures which _may impact_
+ backward-compatibility and require updates, especially for any
+ uses of
+ [`TypeApplications`](https://gitlab.haskell.org/ghc/ghc/-/wikis/type-application).
+ * No longer verifying support for GHC 8.2 or earlier.
+ * Updated the minimum cabal version to 1.10 and specify the
+ default-language as Haskell2010.
+
## 2.0.2 -- *2020 Feb 10*
* Add the `dropPrefix` operation to `Context` which splits an `Assignment`.
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
index 6309527..f232094 100644
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,10 +1,10 @@
Name: parameterized-utils
-Version: 2.0.2
+Version: 2.1.0
Author: Galois Inc.
Maintainer: jhendrix@galois.com, kquick@galois.com
stability: stable
Build-type: Simple
-Cabal-version: >= 1.9.2
+Cabal-version: >= 1.10
Copyright: ©2016-2020 Galois, Inc.
License: BSD3
License-file: LICENSE
@@ -19,7 +19,7 @@ Description:
extra-source-files: Changelog.md
homepage: https://github.com/GaloisInc/parameterized-utils
bug-reports: https://github.com/GaloisInc/parameterized-utils/issues
-tested-with: GHC==8.2.2, GHC==8.4.4, GHC==8.6.4, GHC==8.8.2
+tested-with: GHC==8.4.4, GHC==8.6.5, GHC==8.8.3, GHC==8.10.1
-- Many (but not all, sadly) uses of unsafe operations are
-- controlled by this compile flag. When this flag is set
@@ -89,6 +89,7 @@ library
Data.Parameterized.NatRepr.Internal
ghc-options: -Wall
+ default-language: Haskell2010
if flag(unsafe-operations)
cpp-options: -DUNSAFE_OPS
@@ -99,6 +100,7 @@ test-suite parameterizedTests
hs-source-dirs: test
ghc-options: -Wall
+ default-language: Haskell2010
main-is: UnitTest.hs
other-modules:
diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs
index 94a22f3..c1de1aa 100644
--- a/src/Data/Parameterized/Classes.hs
+++ b/src/Data/Parameterized/Classes.hs
@@ -147,7 +147,7 @@ fromOrdering GT = GTF
-- | @joinOrderingF x y@ first compares on @x@, returning an
-- equivalent value if it is not `EQF`. If it is `EQF`, it returns @y@.
-joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k)
+joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k)
. OrderingF a b
-> (a ~ b => OrderingF c d)
-> OrderingF c d
@@ -197,7 +197,7 @@ class TestEquality ktp => OrdF (ktp :: k -> *) where
-- | Compare two values, and if they are equal compare the next values,
-- otherwise return LTF or GTF
-lexCompareF :: forall (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k)
+lexCompareF :: forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k)
. OrdF f
=> f a
-> f b
@@ -208,7 +208,7 @@ lexCompareF x y = joinOrderingF (compareF x y)
-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
-- for the \"inner\" functor. The type-level evidence of equality is deduced
-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
-ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y.
+ordFCompose :: forall k l (f :: k -> *) (g :: l -> k) x y.
(forall w z. f w -> f z -> OrderingF w z)
-> Compose f g x
-> Compose f g y
diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs
index a82e76e..73994ac 100644
--- a/src/Data/Parameterized/Compose.hs
+++ b/src/Data/Parameterized/Compose.hs
@@ -27,7 +27,7 @@ import Data.Type.Equality
-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
--
-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
-testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y.
+testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
(forall w z. f w -> f z -> Maybe (w :~: z))
-> Compose f g x
-> Compose f g y
diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs
index 2446a8b..613b2e2 100644
--- a/src/Data/Parameterized/Context.hs
+++ b/src/Data/Parameterized/Context.hs
@@ -101,7 +101,6 @@ import Data.Functor (void)
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import GHC.TypeLits (Nat, type (-))
-import Data.Monoid ((<>))
import Data.Parameterized.Classes
import Data.Parameterized.Some
diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
index 186c584..ef26788 100644
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -491,11 +491,11 @@ adjustM f = go (\x -> x)
type instance IndexF (Assignment (f :: k -> Type) ctx) = Index ctx
type instance IxValueF (Assignment (f :: k -> Type) ctx) = f
-instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
+instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
ixF idx f = adjustM f idx
-instance forall (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
+instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
ixF' idx f = adjustM f idx
@@ -590,7 +590,7 @@ instance TraversableFC Assignment where
map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
map = fmapFC
-traverseF :: forall (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
+traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
. Applicative m
=> (forall tp . f tp -> m (g tp))
-> Assignment f c
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
index b82e093..faaf4a8 100644
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -853,11 +853,11 @@ adjustM f (Index i) (Assignment a) = Assignment <$> (unsafe_bin_adjust f a i 0)
type instance IndexF (Assignment f ctx) = Index ctx
type instance IxValueF (Assignment f ctx) = f
-instance forall (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) ctx) where
+instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) ctx) where
ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
ixF' idx f = adjustM f idx
-instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
+instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
ixF = ixF'
-- This is an unsafe version of update that changes the type of the expression.
diff --git a/src/Data/Parameterized/HashTable.hs b/src/Data/Parameterized/HashTable.hs
index 731020d..2e2fa51 100644
--- a/src/Data/Parameterized/HashTable.hs
+++ b/src/Data/Parameterized/HashTable.hs
@@ -30,7 +30,7 @@ module Data.Parameterized.HashTable
import Control.Applicative
import Control.Monad.ST
-import qualified Data.HashTable.ST.Cuckoo as H
+import qualified Data.HashTable.ST.Basic as H
import GHC.Exts (Any)
import Unsafe.Coerce
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
index ee42088..2b10eff 100644
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -247,12 +247,12 @@ type instance IndexF (MapF k v) = k
type instance IxValueF (MapF k v) = v
-- | Turn a map key into a traversal that visits the indicated element in the map, if it exists.
-instance forall (k:: a -> Type) v. OrdF k => IxedF a (MapF k v) where
+instance forall a (k:: a -> Type) v. OrdF k => IxedF a (MapF k v) where
ixF :: k x -> Traversal' (MapF k v) (v x)
ixF i f m = updatedValue <$> updateAtKey i (pure Nothing) (\x -> Set <$> f x) m
-- | Turn a map key into a lens that points into the indicated position in the map.
-instance forall (k:: a -> Type) v. OrdF k => AtF a (MapF k v) where
+instance forall a (k:: a -> Type) v. OrdF k => AtF a (MapF k v) where
atF :: k x -> Lens' (MapF k v) (Maybe (v x))
atF i f m = updatedValue <$> updateAtKey i (f Nothing) (\x -> maybe Delete Set <$> f (Just x)) m
@@ -540,7 +540,7 @@ toList = toAscList
-- | Generate a map from a foldable collection of keys and a
-- function from keys to values.
-fromKeys :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
+fromKeys :: forall k m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
. (Monad m, Foldable t, OrdF a)
=> (forall tp . a tp -> m (v tp))
-- ^ Function for evaluating a register value.
@@ -553,7 +553,7 @@ fromKeys f = foldM go empty
-- | Generate a map from a foldable collection of keys and a monadic
-- function from keys to values.
-fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
+fromKeysM :: forall k m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)
. (Monad m, Foldable t, OrdF a)
=> (forall tp . a tp -> m (v tp))
-- ^ Function for evaluating an input value to store the result in the map.
diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
index 0a578d5..bdcbaae 100644
--- a/src/Data/Parameterized/NatRepr.hs
+++ b/src/Data/Parameterized/NatRepr.hs
@@ -109,6 +109,7 @@ module Data.Parameterized.NatRepr
, leqMulMono
-- * Arithmetic proof
, plusComm
+ , plusAssoc
, mulComm
, plusMinusCancel
, minusPlusCancel
@@ -305,6 +306,10 @@ maxNat x y
plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m
plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n)
+-- | Produce evidence that @+@ is associative.
+plusAssoc :: forall f m g n h o . f m -> g n -> h o -> m+(n+o) :~: (m+n)+o
+plusAssoc = unsafeCoerce (Refl :: m+(n+o) :~: m+(n+o))
+
-- | Produce evidence that @*@ is commutative.
mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
mulComm _ _ = unsafeCoerce Refl
diff --git a/src/Data/Parameterized/Nonce/Transformers.hs b/src/Data/Parameterized/Nonce/Transformers.hs
index b8efa40..981eaa1 100644
--- a/src/Data/Parameterized/Nonce/Transformers.hs
+++ b/src/Data/Parameterized/Nonce/Transformers.hs
@@ -34,7 +34,7 @@ import Data.Parameterized.Nonce
-- set that the 'Nonce' came from).
class Monad m => MonadNonce m where
type NonceSet m :: *
- freshNonceM :: forall (tp :: k) . m (Nonce (NonceSet m) tp)
+ freshNonceM :: forall k (tp :: k) . m (Nonce (NonceSet m) tp)
-- | This transformer adds a nonce generator to a given monad.
newtype NonceT s m a =
diff --git a/src/Data/Parameterized/TH/GADT.hs b/src/Data/Parameterized/TH/GADT.hs
index e431639..fc6563c 100644
--- a/src/Data/Parameterized/TH/GADT.hs
+++ b/src/Data/Parameterized/TH/GADT.hs
@@ -36,7 +36,6 @@ module Data.Parameterized.TH.GADT
) where
import Control.Monad
-import Data.Hashable (hashWithSalt)
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set