parameterized-utils 2.0.2 → 2.1.0

raw patch · 12 files changed

+40/−20 lines, 12 files

Files

• Changelog.md +15/−0
• parameterized-utils.cabal +5/−3
• src/Data/Parameterized/Classes.hs +3/−3
• src/Data/Parameterized/Compose.hs +1/−1
• src/Data/Parameterized/Context.hs +0/−1
• src/Data/Parameterized/Context/Safe.hs +3/−3
• src/Data/Parameterized/Context/Unsafe.hs +2/−2
• src/Data/Parameterized/HashTable.hs +1/−1
• src/Data/Parameterized/Map.hs +4/−4
• src/Data/Parameterized/NatRepr.hs +5/−0
• src/Data/Parameterized/Nonce/Transformers.hs +1/−1
• src/Data/Parameterized/TH/GADT.hs +0/−1

@@ -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`.

@@ -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 @@ 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 @@     Data.Parameterized.NatRepr.Internal    ghc-options: -Wall+  default-language: Haskell2010    if flag(unsafe-operations)     cpp-options: -DUNSAFE_OPS@@ -99,6 +100,7 @@   hs-source-dirs: test    ghc-options: -Wall+  default-language: Haskell2010    main-is: UnitTest.hs   other-modules:

@@ -147,7 +147,7 @@  -- | @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 @@  -- | 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 @@ -- | 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

@@ -27,7 +27,7 @@ -- | 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

@@ -101,7 +101,6 @@ 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

@@ -491,11 +491,11 @@ 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 @@ 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

@@ -853,11 +853,11 @@ 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.

@@ -30,7 +30,7 @@  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 

@@ -247,12 +247,12 @@ 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 @@  -- | 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 @@  -- | 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.

@@ -109,6 +109,7 @@   , leqMulMono     -- * Arithmetic proof   , plusComm+  , plusAssoc   , mulComm   , plusMinusCancel   , minusPlusCancel@@ -304,6 +305,10 @@ -- | Produce evidence that @+@ is commutative. 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)

@@ -34,7 +34,7 @@ -- 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 =

@@ -36,7 +36,6 @@   ) where  import Control.Monad-import Data.Hashable (hashWithSalt) import Data.Maybe import Data.Set (Set) import qualified Data.Set as Set