diff --git a/Changelog.md b/Changelog.md --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,14 @@ # Changelog for the `parameterized-utils` package +## 2.0.2 -- *2020 Feb 10* + + * Add the `dropPrefix` operation to `Context` which splits an `Assignment`. + * Add `intersectWithKeyMaybe` and `mergeWithKey` to `Map`. + * Add `mapAt`, `mapAtM`, and `replace` to `Vector`. + * Add dependency on `base-orphans` to handle the `TestEquality` + instance for `Compose`; needed for GHC 8.10. + * Bump upper limit of `lens` dependency to allow 4.19. + ## 2.0.1 -- *2019 Nov 06* * Documentation updates diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal --- a/parameterized-utils.cabal +++ b/parameterized-utils.cabal @@ -1,11 +1,11 @@ Name: parameterized-utils -Version: 2.0.1.0 +Version: 2.0.2 Author: Galois Inc. Maintainer: jhendrix@galois.com, kquick@galois.com stability: stable Build-type: Simple Cabal-version: >= 1.9.2 -Copyright: ©2016-2019 Galois, Inc. +Copyright: ©2016-2020 Galois, Inc. License: BSD3 License-file: LICENSE category: Data Structures, Dependent Types @@ -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 +tested-with: GHC==8.2.2, GHC==8.4.4, GHC==8.6.4, GHC==8.8.2 -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag. When this flag is set @@ -36,6 +36,7 @@ library build-depends: base >= 4.10 && < 5 + , base-orphans >=0.8.2 && <0.9 , th-abstraction >=0.3 && <0.4 , constraints >=0.10 && <0.12 , containers @@ -43,7 +44,7 @@ , ghc-prim , hashable >=1.2 && <1.4 , hashtables ==1.2.* - , lens >=4.16 && <4.19 + , lens >=4.16 && <4.20 , mtl , template-haskell , text diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs --- a/src/Data/Parameterized/Compose.hs +++ b/src/Data/Parameterized/Compose.hs @@ -16,12 +16,12 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE Safe #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} module Data.Parameterized.Compose ( testEqualityComposeBare ) where import Data.Functor.Compose +import Data.Orphans () -- For the TestEquality (Compose f g) instance import Data.Type.Equality -- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@. @@ -36,12 +36,3 @@ case (testEquality_ x y :: Maybe (g x :~: g y)) of Just Refl -> Just (Refl :: x :~: y) Nothing -> Nothing - -testEqualityCompose :: forall (f :: k -> *) (g :: l -> k) x y. (TestEquality f) - => Compose f g x - -> Compose f g y - -> Maybe (x :~: y) -testEqualityCompose = testEqualityComposeBare testEquality - -instance (TestEquality f) => TestEquality (Compose f g) where - testEquality = testEqualityCompose diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs --- a/src/Data/Parameterized/Context.hs +++ b/src/Data/Parameterized/Context.hs @@ -62,6 +62,7 @@ , fromList , traverseAndCollect , traverseWithIndex_ + , dropPrefix -- * Context extension and embedding utilities , CtxEmbedding(..) @@ -154,6 +155,39 @@ MV.write vm (indexVal i) (f (a ! i)) return vm {-# INLINABLE toVector #-} + + +-- | Utility function for testing if @xs@ is an assignment with +-- `prefix` as a prefix, and computing the tail of xs +-- not in the prefix, if so. +dropPrefix :: forall f xs prefix a. + TestEquality f => + Assignment f xs {- ^ Assignment to split -} -> + Assignment f prefix {- ^ Expected prefix -} -> + a {- ^ error continuation -} -> + (forall addl. (xs ~ (prefix <+> addl)) => Assignment f addl -> a) + {- ^ success continuation -} -> + a +dropPrefix xs0 prefix err = go xs0 (sizeInt (size xs0)) + where + sz_prefix = sizeInt (size prefix) + + go :: forall ys. + Assignment f ys -> + Int -> + (forall addl. (ys ~ (prefix <+> addl)) => Assignment f addl -> a) -> + a + + go (xs' :> z) sz_x success | sz_x > sz_prefix = + go xs' (sz_x-1) (\zs -> success (zs :> z)) + + go xs _ success = + case testEquality xs prefix of + Just Refl -> success Empty + Nothing -> err + + + -------------------------------------------------------------------------------- -- Patterns diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs --- a/src/Data/Parameterized/Map.hs +++ b/src/Data/Parameterized/Map.hs @@ -29,6 +29,7 @@ , insertWith , delete , union + , intersectWithKeyMaybe -- * Query , null , lookup @@ -71,6 +72,7 @@ , Updated(..) , updatedValue , updateAtKey + , mergeWithKey , mergeWithKeyM , module Data.Parameterized.Classes -- * Pair @@ -177,7 +179,6 @@ #-} #endif - -- | Apply function to all elements in map. mapWithKey :: (forall tp . ktp tp -> f tp -> g tp) @@ -448,10 +449,9 @@ {-# INLINABLE delete #-} {-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-} --- | Left-biased union of two maps. The resulting map will --- contain the union of the keys of the two arguments. When --- a key is contained in both maps the value from the first --- map will be preserved. +-- | Left-biased union of two maps. The resulting map will contain the +-- union of the keys of the two arguments. When a key is contained in +-- both maps the value from the first map will be preserved. union :: OrdF k => MapF k a -> MapF k a -> MapF k a union t1 t2 = Bin.union comparePairKeys t1 t2 {-# INLINABLE union #-} @@ -572,18 +572,66 @@ filterLtMaybe NothingS m = m filterLtMaybe (JustS k) m = filterLt k m --- | Merge bindings in two maps to get a third. +-- | Returns only entries that are strictly between the two keys. +filterMiddle :: OrdF k => k x -> k y -> MapF k a -> MapF k a +filterMiddle lo hi (Bin _ k _ _ r) + | k `leqF` lo = filterMiddle lo hi r +filterMiddle lo hi (Bin _ k _ l _) + | k `geqF` hi = filterMiddle lo hi l +filterMiddle _ _ t = t +{-# INLINABLE filterMiddle #-} + +{-------------------------------------------------------------------- + [trim blo bhi t] trims away all subtrees that surely contain no + values between the range [blo] to [bhi]. The returned tree is either + empty or the key of the root is between @blo@ and @bhi@. +--------------------------------------------------------------------} +trim :: OrdF k => MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k a +trim NothingS NothingS t = t +trim (JustS lk) NothingS t = filterGt lk t +trim NothingS (JustS hk) t = filterLt hk t +trim (JustS lk) (JustS hk) t = filterMiddle lk hk t + +-- Helper function for 'mergeWithKeyM'. The @'trimLookupLo' lk hk t@ performs both +-- @'trim' (JustS lk) hk t@ and @'lookup' lk t@. + +-- See Note: Type of local 'go' function +trimLookupLo :: OrdF k => k tp -> MaybeS (k y) -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) +trimLookupLo lk NothingS t = greater lk t + where greater :: OrdF k => k tp -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) + greater lo t'@(Bin _ kx x l r) = + case compareF lo kx of + LTF -> Bin.PairS (lookup lo l) t' + EQF -> Bin.PairS (Just x) r + GTF -> greater lo r + greater _ Tip = Bin.PairS Nothing Tip +trimLookupLo lk (JustS hk) t = middle lk hk t + where middle :: OrdF k => k tp -> k y -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) + middle lo hi t'@(Bin _ kx x l r) = + case compareF lo kx of + LTF | kx `ltF` hi -> Bin.PairS (lookup lo l) t' + | otherwise -> middle lo hi l + EQF -> Bin.PairS (Just x) (lesser hi r) + GTF -> middle lo hi r + middle _ _ Tip = Bin.PairS Nothing Tip + + lesser :: OrdF k => k y -> MapF k a -> MapF k a + lesser hi (Bin _ k _ l _) | k `geqF` hi = lesser hi l + lesser _ t' = t' + +-- | Merge bindings in two maps using monadic actions to get a third. -- -- The first function is used to merge elements that occur under the -- same key in both maps. Return Just to add an entry into the -- resulting map under this key or Nothing to remove this key from the -- resulting map. -- --- The second function will be applied to submaps of the first map argument --- where no keys overlap with the second map argument. The result of this --- function must be a map with a subset of the keys of its argument. --- This means the function can alter the values of its argument and it can --- remove key-value pairs from it, but it must not introduce new keys. +-- The second function will be applied to submaps of the first map +-- argument where no keys overlap with the second map argument. The +-- result of this function must be a map with a subset of the keys of +-- its argument. This means the function can alter the values of its +-- argument and it can remove key-value pairs from it, but it can +-- break `MapF` ordering invariants if it introduces new keys. -- -- Third function is analogous to the second function except that it applies -- to the second map argument of 'mergeWithKeyM' instead of the first. @@ -626,53 +674,47 @@ <*> hedgeMerge blo bmi l (trim blo bmi t2) <*> hedgeMerge bmi bhi r trim_t2 where bmi = JustS kx -{-# INLINABLE mergeWithKeyM #-} -{-------------------------------------------------------------------- - [trim blo bhi t] trims away all subtrees that surely contain no - values between the range [blo] to [bhi]. The returned tree is either - empty or the key of the root is between @blo@ and @bhi@. ---------------------------------------------------------------------} -trim :: OrdF k => MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k a -trim NothingS NothingS t = t -trim (JustS lk) NothingS t = filterGt lk t -trim NothingS (JustS hk) t = filterLt hk t -trim (JustS lk) (JustS hk) t = filterMiddle lk hk t - --- | Returns only entries that are strictly between the two keys. -filterMiddle :: OrdF k => k x -> k y -> MapF k a -> MapF k a -filterMiddle lo hi (Bin _ k _ _ r) - | k `leqF` lo = filterMiddle lo hi r -filterMiddle lo hi (Bin _ k _ l _) - | k `geqF` hi = filterMiddle lo hi l -filterMiddle _ _ t = t -{-# INLINABLE filterMiddle #-} - - - --- Helper function for 'mergeWithKeyM'. The @'trimLookupLo' lk hk t@ performs both --- @'trim' (JustS lk) hk t@ and @'lookup' lk t@. +{-# INLINABLE mergeWithKeyM #-} --- See Note: Type of local 'go' function -trimLookupLo :: OrdF k => k tp -> MaybeS (k y) -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) -trimLookupLo lk NothingS t = greater lk t - where greater :: OrdF k => k tp -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) - greater lo t'@(Bin _ kx x l r) = - case compareF lo kx of - LTF -> Bin.PairS (lookup lo l) t' - EQF -> Bin.PairS (Just x) r - GTF -> greater lo r - greater _ Tip = Bin.PairS Nothing Tip -trimLookupLo lk (JustS hk) t = middle lk hk t - where middle :: OrdF k => k tp -> k y -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) - middle lo hi t'@(Bin _ kx x l r) = - case compareF lo kx of - LTF | kx `ltF` hi -> Bin.PairS (lookup lo l) t' - | otherwise -> middle lo hi l - EQF -> Bin.PairS (Just x) (lesser hi r) - GTF -> middle lo hi r - middle _ _ Tip = Bin.PairS Nothing Tip +-- | Merge bindings in two maps to get a third. +-- +-- The first function is used to merge elements that occur under the +-- same key in both maps. Return Just to add an entry into the +-- resulting map under this key or Nothing to remove this key from the +-- resulting map. +-- +-- The second function will be applied to submaps of the first map +-- argument where no keys overlap with the second map argument. The +-- result of this function must be a map with a subset of the keys of +-- its argument. This means the function can alter the values of its +-- argument and it can remove key-value pairs from it, but it can +-- break `MapF` ordering invariants if it introduces new keys. +-- +-- Third function is analogous to the second function except that it applies +-- to the second map argument of 'mergeWithKeyM' instead of the first. +-- +-- Common examples of the two functions include 'id' when constructing a union +-- or 'const' 'empty' when constructing an intersection. +mergeWithKey :: forall k a b c + . OrdF k + => (forall tp . k tp -> a tp -> b tp -> Maybe (c tp)) + -> (MapF k a -> MapF k c) + -> (MapF k b -> MapF k c) + -> MapF k a + -> MapF k b + -> MapF k c +mergeWithKey f g1 g2 x y = runIdentity $ + mergeWithKeyM (\k a b -> pure $! f k a b) (pure . g1) (pure . g2) x y - lesser :: OrdF k => k y -> MapF k a -> MapF k a - lesser hi (Bin _ k _ l _) | k `geqF` hi = lesser hi l - lesser _ t' = t' +-- | Applies a function to the pairwise common elements of two maps. +-- +-- Formally, we have that @intersectWithKeyMaybe f x y@ contains a +-- binding from a key @k@ to a value @v@ if and only if @x@ and @y@ +-- bind @k@ to @x_k@ and @y_k@ and @f x_k y_k = Just v@. +intersectWithKeyMaybe :: OrdF k + => (forall tp . k tp -> a tp -> b tp -> Maybe (c tp)) + -> MapF k a + -> MapF k b + -> MapF k c +intersectWithKeyMaybe f = mergeWithKey f (const empty) (const empty) diff --git a/src/Data/Parameterized/Vector.hs b/src/Data/Parameterized/Vector.hs --- a/src/Data/Parameterized/Vector.hs +++ b/src/Data/Parameterized/Vector.hs @@ -38,6 +38,9 @@ , uncons , slice , Data.Parameterized.Vector.take + , replace + , mapAt + , mapAtM -- * Zipping , zipWith @@ -196,6 +199,35 @@ take | LeqProof <- prf = slice (knownNat @0) where prf = leqAdd (leqRefl (Proxy @n)) (Proxy @x) + +-- | Scope a monadic function to a sub-section of the given vector. +mapAtM :: Monad m => (i + w <= n, 1 <= w) => + NatRepr i {- ^ Start index -} -> + NatRepr w {- ^ Section width -} -> + (Vector w a -> m (Vector w a)) {-^ map for the sub-vector -} -> + Vector n a -> m (Vector n a) +mapAtM i w f (Vector vn) = + let + (vhead, vtail) = Vector.splitAt (widthVal i) vn + (vsect, vend) = Vector.splitAt (widthVal w) vtail + in do + Vector vsect' <- f (Vector vsect) + return $ Vector $ vhead Vector.++ vsect' Vector.++ vend + +-- | Scope a function to a sub-section of the given vector. +mapAt :: (i + w <= n, 1 <= w) => + NatRepr i {- ^ Start index -} -> + NatRepr w {- ^ Section width -} -> + (Vector w a -> Vector w a) {-^ map for the sub-vector -} -> + Vector n a -> Vector n a +mapAt i w f vn = runIdentity $ mapAtM i w (pure . f) vn + +-- | Replace a sub-section of a vector with the given sub-vector. +replace :: (i + w <= n, 1 <= w) => + NatRepr i {- ^ Start index -} -> + Vector w a {- ^ sub-vector -} -> + Vector n a -> Vector n a +replace i vw vn = mapAt i (length vw) (const vw) vn --------------------------------------------------------------------------------