parameterized-utils 2.0.1.0 → 2.0.2
raw patch · 6 files changed
+181/−72 lines, 6 filesdep +base-orphansdep ~lens
Dependencies added: base-orphans
Dependency ranges changed: lens
Files
- Changelog.md +9/−0
- parameterized-utils.cabal +5/−4
- src/Data/Parameterized/Compose.hs +1/−10
- src/Data/Parameterized/Context.hs +34/−0
- src/Data/Parameterized/Map.hs +100/−58
- src/Data/Parameterized/Vector.hs +32/−0
Changelog.md view
@@ -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
parameterized-utils.cabal view
@@ -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
src/Data/Parameterized/Compose.hs view
@@ -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
src/Data/Parameterized/Context.hs view
@@ -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
src/Data/Parameterized/Map.hs view
@@ -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)
src/Data/Parameterized/Vector.hs view
@@ -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 --------------------------------------------------------------------------------