parameterized-utils 2.1.5.0 → 2.1.6.0

raw patch · 19 files changed

+1643/−347 lines, 19 filesdep ~hashabledep ~hashtablesdep ~lensPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: hashable, hashtables, lens, tasty-hedgehog, th-abstraction, vector

API changes (from Hackage documentation)

Files

• Changelog.md +11/−0
• parameterized-utils.cabal +13/−8
• src/Data/Parameterized/Classes.hs +1/−1
• src/Data/Parameterized/Context/Safe.hs +2/−2
• src/Data/Parameterized/Context/Unsafe.hs +2/−2
• src/Data/Parameterized/Fin.hs +37/−0
• src/Data/Parameterized/FinMap.hs +79/−0
• src/Data/Parameterized/FinMap/Safe.hs +248/−0
• src/Data/Parameterized/FinMap/Unsafe.hs +249/−0
• src/Data/Parameterized/NatRepr.hs +28/−3
• src/Data/Parameterized/Some.hs +8/−1
• src/Data/Parameterized/Vector.hs +1/−4
• test/Test/Context.hs +284/−206
• test/Test/Fin.hs +22/−3
• test/Test/FinMap.hs +393/−0
• test/Test/NatRepr.hs +9/−5
• test/Test/Some.hs +74/−0
• test/Test/Vector.hs +178/−112
• test/UnitTest.hs +4/−0

@@ -1,5 +1,16 @@ # Changelog for the `parameterized-utils` package +## 2.1.6.0 -- *2022 Dec 18*++  * Added `FinMap`: an integer map with a statically-known maximum size.+  * Added `someLens` to `Some` to create a parameterized lens.+  * Allow building with `hashable-1.4.*`. Because `hashable-1.4.0.0` adds an+    `Eq` superclass to `Hashable`, some instances of `Hashable` in+    `parameterized-utils` now require additional `TestEquality` constraints, as+    the corresponding `Eq` instances for these data types also require+    `TestEquality` constraints.+  * Bump constraints to allow: vector-0.13, lens-5.2, tasty-hedgehog-1.3.0.0--1.4.0.0, GHC-9.4+ ## 2.1.5.0 -- *2022 Mar 08*    * Add support for GHC 9.2.  Drop support for GHC 8.4 (or earlier).

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.1.5.0+Version:       2.1.6.0 Author:        Galois Inc. Maintainer:    kquick@galois.com stability:     stable@@ -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.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1+tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1, GHC==9.4.3  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -51,20 +51,20 @@   import: bldflags   build-depends: base >= 4.10 && < 5                , base-orphans   >=0.8.2 && <0.9-               , th-abstraction >=0.3  && <0.5+               , th-abstraction >=0.4.2 && <0.5                , constraints    >=0.10 && <0.14                , containers                , deepseq                , ghc-prim-               , hashable       >=1.2  && <1.4-               , hashtables     ==1.2.*+               , hashable       >=1.2  && <1.5+               , hashtables     >=1.2  && <1.4                , indexed-traversable-               , lens           >=4.16 && <5.2+               , lens           >=4.16 && <5.3                , mtl                , profunctors    >=5.6 && < 5.7                , template-haskell                , text-               , vector         ==0.12.*+               , vector         >=0.12 && < 0.14    hs-source-dirs: src @@ -84,6 +84,9 @@     Data.Parameterized.DataKind     Data.Parameterized.DecidableEq     Data.Parameterized.Fin+    Data.Parameterized.FinMap+    Data.Parameterized.FinMap.Safe+    Data.Parameterized.FinMap.Unsafe     Data.Parameterized.HashTable     Data.Parameterized.List     Data.Parameterized.Map@@ -120,8 +123,10 @@   other-modules:     Test.Context     Test.Fin+    Test.FinMap     Test.List     Test.NatRepr+    Test.Some     Test.SymbolRepr     Test.TH     Test.Vector@@ -138,7 +143,7 @@                , tasty >= 1.2 && < 1.5                , tasty-ant-xml == 1.1.*                , tasty-hunit >= 0.9 && < 0.11-               , tasty-hedgehog+               , tasty-hedgehog >= 1.2    if impl(ghc >= 8.6)     build-depends:

@@ -351,7 +351,7 @@ instance ShowF f => Show (TypeAp f tp) where   showsPrec p (TypeAp x) = showsPrecF p x -instance HashableF f => Hashable (TypeAp f tp) where+instance (HashableF f, TestEquality f) => Hashable (TypeAp f tp) where   hashWithSalt s (TypeAp x) = hashWithSaltF s x  ------------------------------------------------------------------------

@@ -595,10 +595,10 @@ instance HashableF (Index ctx) where   hashWithSaltF s i = hashWithSalt s (indexVal i) -instance HashableF f => HashableF (Assignment f) where+instance (HashableF f, TestEquality f) => HashableF (Assignment f) where   hashWithSaltF = hashWithSalt -instance HashableF f => Hashable (Assignment f ctx) where+instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where   hashWithSalt s AssignmentEmpty = s   hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x 

@@ -851,10 +851,10 @@ instance Hashable (Index ctx tp) where   hashWithSalt = hashWithSaltF -instance HashableF f => Hashable (Assignment f ctx) where+instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where   hashWithSalt s (Assignment a) = hashWithSaltF s a -instance HashableF f => HashableF (Assignment f) where+instance (HashableF f, TestEquality f) => HashableF (Assignment f) where   hashWithSaltF = hashWithSalt  instance ShowF f => Show (Assignment f ctx) where

@@ -6,6 +6,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}  {-| Copyright        : (c) Galois, Inc 2021@@ -22,11 +23,14 @@ module Data.Parameterized.Fin   ( Fin   , mkFin+  , buildFin+  , countFin   , viewFin   , finToNat   , embed   , tryEmbed   , minFin+  , incFin   , fin0Void   , fin1Unit   , fin2Bool@@ -62,12 +66,39 @@  mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n mkFin = Fin+{-# INLINE mkFin #-} +newtype Fin' n = Fin' { getFin' :: Fin (n + 1) }++buildFin ::+  forall m.+  NatRepr m ->+  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Fin (n + 1 + 1)) ->+  Fin (m + 1)+buildFin m f =+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> Fin' k -> Fin' (k + 1)+      f' = (\n (Fin' fin) -> Fin' (f n fin))+  in getFin' (natRecStrictlyBounded m (Fin' minFin) f')++-- | Count all of the numbers up to @m@ that meet some condition.+countFin ::+  NatRepr m ->+  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Bool) ->+  Fin (m + 1)+countFin m f =+  buildFin m $+    \n count ->+      if f n count+      then incFin count+      else case leqSucc count of+              LeqProof -> embed count+ viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r viewFin f (Fin i) = f i  finToNat :: Fin n -> Natural finToNat (Fin i) = natValue i+{-# INLINABLE finToNat #-}  embed :: forall n m. (n <= m) => Fin n -> Fin m embed =@@ -86,6 +117,12 @@ -- | The smallest element of @'Fin' n@ minFin :: (1 <= n) => Fin n minFin = Fin (knownNat @0)+{-# INLINABLE minFin #-}++incFin :: forall n. Fin n -> Fin (n + 1)+incFin (Fin (i :: NatRepr i)) =+  case leqAdd2 (LeqProof :: LeqProof (i + 1) n) (LeqProof :: LeqProof 1 1) of+    LeqProof -> mkFin (incNat i)  fin0Void :: Iso' (Fin 0) Void fin0Void =

@@ -0,0 +1,79 @@+{-|+Copyright        : (c) Galois, Inc 2022++@'FinMap' n a@ conceptually (see NOTE) a map with @'Data.Parameterized.Fin.Fin'+n@ keys, implying a maximum size of @n@. Here's how 'FinMap' compares to other+map-like types:++* @'FinMap' n a@ is conceptually isomorphic to a+  @'Data.Parameterized.Vector' n ('Maybe' a)@, but can be more space-efficient+  especially if @n@ is large and the vector is populated with a small number of+  'Just' values.+* @'FinMap'@ is less general than 'Data.Map.Map', because it has a fixed key+  type (@'Data.Parameterized.Fin.Fin' n@).+* @'FinMap' n a@ is similar to @'Data.IntMap.IntMap' a@, but it provides a+  static guarantee of a maximum size, and its operations (such as 'size') allow+  the recovery of more type-level information.+* @'FinMap'@ is dissimilar from "Data.Parameterized.Map.MapF" in that neither+  the key nor value type of 'FinMap' is parameterized.++The type parameter @n@ doesn't track the /current/ number of key-value pairs in+a @'FinMap' n@ (i.e., the size of the map), but rather /an upper bound/.+'insert' and 'delete' don't alter @n@, whereas 'incMax' does - despite the fact+that it has no effect on the keys and values in the 'FinMap'.++The 'FinMap' interface has two implementations:++* The implementation in "Data.Parameterized.FinMap.Unsafe" is backed by an+  'Data.IntMap.IntMap', and must have a size of at most @'maxBound' :: 'Int'@.+  This module uses unsafe operations like 'Unsafe.Coerce.unsafeCoerce'+  internally for the sake of time and space efficiency.+* The implementation in "Data.Parameterized.FinMap.Safe" is backed by an+  @'Data.Map.Map' ('Data.Parameterized.Fin.Fin' n)@. All of its functions are+  implemented using safe operations.++The implementation in 'Data.Parameterized.FinMap.Unsafe.FinMap' is property+tested against that in 'Data.Parameterized.FinMap.Safe.FinMap' to ensure+they have the same behavior.++In this documentation, /W/ is used in big-O notations the same way as in the+"Data.IntMap" documentation.++NOTE: Where the word "conceptually" is used, it implies that this correspondence+is not literally true, but is true modulo some details such as differences+between bounded types like 'Int' and unbounded types like 'Integer'.++Several of the functions in both implementations are marked @INLINE@ or+@INLINABLE@. There are three reasons for this:++* Some of these just have very small definitions and so inlining is likely more+  beneficial than harmful.+* Some participate in @RULES@ relevant to functions used in their+  implementations.+* They are thin wrappers (often just newtype wrappers) around functions marked+  @INLINE@, which should therefore also be inlined.+-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.FinMap+  (+#ifdef UNSAFE_OPS+    module Data.Parameterized.FinMap.Unsafe+#else+    module Data.Parameterized.FinMap.Safe+#endif+  ) where++#ifdef UNSAFE_OPS+import Data.Parameterized.FinMap.Unsafe+#else+import Data.Parameterized.FinMap.Safe+#endif

@@ -0,0 +1,248 @@+{-|+Copyright        : (c) Galois, Inc 2022++See "Data.Parameterized.FinMap".+-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.FinMap.Safe+  ( FinMap+  -- * Query+  , null+  , lookup+  , size+  -- * Construction+  , incMax+  , embed+  , empty+  , singleton+  , insert+  , buildFinMap+  , append+  , fromVector+  -- * Operations+  , delete+  , decMax+  , mapWithKey+  , unionWithKey+  , unionWith+  , union+  ) where++import           Prelude hiding (lookup, null)++import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))+import           Data.Functor.WithIndex (FunctorWithIndex(imap))+import           Data.Maybe (isJust)+import           Data.Proxy (Proxy(Proxy))+import           Data.Map (Map)+import qualified Data.Map as Map+import           GHC.TypeLits (KnownNat, Nat)++import           Data.Parameterized.Fin (Fin)+import qualified Data.Parameterized.Fin as Fin+import           Data.Parameterized.NatRepr (NatRepr, type (+), type (<=))+import qualified Data.Parameterized.NatRepr as NatRepr+import           Data.Parameterized.Vector (Vector)+import qualified Data.Parameterized.Vector as Vec++------------------------------------------------------------------------+-- Type++-- | @'FinMap' n a@ is a map with @'Fin' n@ keys and @a@ values.+data FinMap (n :: Nat) a =+  FinMap+    { getFinMap :: Map (Fin n) a+    , maxSize :: NatRepr n+    }++instance Eq a => Eq (FinMap n a) where+  fm1 == fm2 = getFinMap fm1 == getFinMap fm2+  {-# INLINABLE (==) #-}++instance Semigroup (FinMap n a) where+  (<>) = union+  {-# INLINE (<>) #-}++instance KnownNat n => Monoid (FinMap n a) where+  mempty = empty+  {-# INLINE mempty #-}++instance Functor (FinMap n) where+  fmap f fm = fm { getFinMap = fmap f (getFinMap fm) }+  {-# INLINABLE fmap #-}++instance Foldable (FinMap n) where+  foldMap f = foldMap f . getFinMap+  {-# INLINABLE foldMap #-}++instance Traversable (FinMap n) where+  traverse f fm = FinMap <$> traverse f (getFinMap fm) <*> pure (maxSize fm)++instance FunctorWithIndex (Fin n) (FinMap n) where+  imap f fm = fm { getFinMap = Map.mapWithKey f (getFinMap fm) }+  -- Inline so that RULES for Map.mapWithKey can fire+  {-# INLINE imap #-}++instance FoldableWithIndex (Fin n) (FinMap n) where+  ifoldMap f = Map.foldMapWithKey f . getFinMap+  {-# INLINABLE ifoldMap #-}++-- | Non-lawful instance, provided for testing+instance Show a => Show (FinMap n a) where+  show fm = show (getFinMap fm)+  {-# INLINABLE show #-}++------------------------------------------------------------------------+-- Query++-- | /O(1)/. Is the map empty?+null :: FinMap n a -> Bool+null = Map.null . getFinMap+{-# INLINABLE null #-}++-- | /O(log n)/. Fetch the value at the given key in the map.+lookup :: Fin n -> FinMap n a -> Maybe a+lookup k = Map.lookup k . getFinMap+{-# INLINABLE lookup #-}++-- | /O(nlog(n))/. Number of elements in the map.+--+-- This operation is much slower than 'Data.Parameterized.FinMap.Unsafe.size'+-- because its implementation must provide significant evidence to the+-- type-checker, and the easiest way to do that is fairly inefficient.+-- If speed is a concern, use "Data.Parameterized.FinMap.Unsafe".+size :: forall n a. FinMap n a -> Fin (n + 1)+size fm =+  Fin.countFin (maxSize fm) (\k _count -> isJust (lookup (Fin.mkFin k) fm))++------------------------------------------------------------------------+-- Construction++-- | /O(n log n)/. Increase maximum key/size by 1.+--+-- This does not alter the key-value pairs in the map, but rather increases the+-- maximum number of key-value pairs that the map can hold. See+-- "Data.Parameterized.FinMap" for more information.+--+-- Requires @n + 1 < (maxBound :: Int)@.+incMax :: forall n a. FinMap n a -> FinMap (n + 1) a+incMax fm =+  case NatRepr.leqSucc (Proxy :: Proxy n) of+    NatRepr.LeqProof -> embed (NatRepr.incNat (maxSize fm)) fm++-- | /O(n log n)/. Increase maximum key/size.+--+-- Requires @m < (maxBound :: Int)@.+embed :: (n <= m) => NatRepr m -> FinMap n a -> FinMap m a+embed m fm =+  FinMap+    { getFinMap = Map.mapKeys Fin.embed (getFinMap fm)+    , maxSize = m+    }++-- | /O(1)/. The empty map.+empty :: KnownNat n => FinMap n a+empty = FinMap Map.empty NatRepr.knownNat+{-# INLINABLE empty #-}++-- | /O(1)/. A map with one element.+singleton :: a -> FinMap 1 a+singleton item =+  FinMap+    { getFinMap = Map.singleton (Fin.mkFin (NatRepr.knownNat :: NatRepr 0)) item+    , maxSize = NatRepr.knownNat :: NatRepr 1+    }++-- | /O(log n)/.+insert :: Fin n -> a -> FinMap n a -> FinMap n a+insert k v fm = fm { getFinMap = Map.insert k v (getFinMap fm) }+{-# INLINABLE insert #-}++-- buildFinMap, append, and fromVector are duplicated exactly between the safe+-- and unsafe modules because they are used in comparative testing (and so+-- implementations must be available for both types).++newtype FinMap' a (n :: Nat) = FinMap' { unFinMap' :: FinMap n a }++buildFinMap ::+  forall m a.+  NatRepr m ->+  (forall n. (n + 1 <= m) => NatRepr n -> FinMap n a -> FinMap (n + 1) a) ->+  FinMap m a+buildFinMap m f =+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> FinMap' a k -> FinMap' a (k + 1)+      f' = (\n (FinMap' fin) -> FinMap' (f n fin))+  in unFinMap' (NatRepr.natRecStrictlyBounded m (FinMap' empty) f')++-- | /O(min(n,W))/.+append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a+append k v fm =+  case NatRepr.leqSucc k of+    NatRepr.LeqProof -> insert (Fin.mkFin k) v (incMax fm)++fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a+fromVector v =+  buildFinMap+    (Vec.length v)+    (\k m ->+      case Vec.elemAt k v of+        Just e -> append k e m+        Nothing -> incMax m)++------------------------------------------------------------------------+-- Operations++-- | /O(log n)/.+delete :: Fin n -> FinMap n a -> FinMap n a+delete k fm = fm { getFinMap = Map.delete k (getFinMap fm) }+{-# INLINABLE delete #-}++-- | Decrement the key/size, removing the item at key @n + 1@ if present.+decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a+decMax n fm =+  FinMap+    { getFinMap = maybeMapKeys (Fin.tryEmbed sz n) (getFinMap fm)+    , maxSize = n+    }+  where+    sz = maxSize fm++    maybeMapKeys :: Ord k2 => (k1 -> Maybe k2) -> Map k1 a -> Map k2 a+    maybeMapKeys f m =+      Map.foldrWithKey+        (\k v accum ->+           case f k of+             Just k' -> Map.insert k' v accum+             Nothing -> accum)+        Map.empty+        m++mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b+mapWithKey f fm = fm { getFinMap = Map.mapWithKey f (getFinMap fm) }+-- Inline so that RULES for Map.mapWithKey can fire+{-# INLINE mapWithKey #-}++-- | /O(n+m)/.+unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a+unionWithKey f fm1 fm2 =+  FinMap+    { getFinMap = Map.unionWithKey f (getFinMap fm1) (getFinMap fm2)+    , maxSize = maxSize fm1+    }++-- | /O(n+m)/.+unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a+unionWith f = unionWithKey (\_ v1 v2 -> f v1 v2)++-- | /O(n+m)/. Left-biased union, i.e. (@'union' == 'unionWith' 'const'@).+union :: FinMap n a -> FinMap n a -> FinMap n a+union = unionWith const

@@ -0,0 +1,249 @@+{-|+Copyright        : (c) Galois, Inc 2022++See "Data.Parameterized.FinMap".+-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.FinMap.Unsafe+  ( FinMap+  -- * Query+  , null+  , lookup+  , size+  -- * Construction+  , incMax+  , embed+  , empty+  , singleton+  , insert+  , buildFinMap+  , append+  , fromVector+  -- * Operations+  , delete+  , decMax+  , mapWithKey+  , unionWithKey+  , unionWith+  , union+  ) where++import           Prelude hiding (lookup, null)++import           Data.Functor.WithIndex (FunctorWithIndex(imap))+import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))+import           Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import           GHC.TypeLits (KnownNat, Nat)+import           Numeric.Natural (Natural)+import           Unsafe.Coerce (unsafeCoerce)++import           Data.Parameterized.Fin (Fin, mkFin)+import qualified Data.Parameterized.Fin as Fin+import           Data.Parameterized.NatRepr (LeqProof, NatRepr, type (+), type (<=))+import qualified Data.Parameterized.NatRepr as NatRepr+import           Data.Parameterized.Some (Some(Some))+import           Data.Parameterized.Vector (Vector)+import qualified Data.Parameterized.Vector as Vec++-- This is pulled out as a function so that it's obvious that its use is safe+-- (since Natural is unbounded).+intToNat :: Int -> Natural+intToNat = fromIntegral+{-# INLINE intToNat #-}++-- These are pulled out as functions so that it's obvious that their use is+-- unsafe (since Natural is unbounded).++unsafeFinToInt :: Fin n -> Int+unsafeFinToInt = fromIntegral . Fin.finToNat+{-# INLINE unsafeFinToInt #-}++unsafeNatReprToInt :: NatRepr n -> Int+unsafeNatReprToInt = fromIntegral . NatRepr.natValue+{-# INLINE unsafeNatReprToInt #-}++------------------------------------------------------------------------+-- Type++-- This datatype has two important invariants:+--+-- * Its keys must be less than the nat in its type.+-- * Its size must be less than the maximum Int.+--+-- If these invariants hold, all of the unsafe operations in this module+-- (fromJust, unsafeCoerce) will work as intended.++-- | @'FinMap' n a@ is a map with @'Fin' n@ keys and @a@ values.+newtype FinMap (n :: Nat) a = FinMap { getFinMap :: IntMap a }++instance Eq a => Eq (FinMap n a) where+  fm1 == fm2 = getFinMap fm1 == getFinMap fm2+  {-# INLINABLE (==) #-}++instance Semigroup (FinMap n a) where+  (<>) = union+  {-# INLINE (<>) #-}++instance KnownNat n => Monoid (FinMap n a) where+  mempty = empty+  {-# INLINE mempty #-}++instance Functor (FinMap n) where+  fmap f = FinMap . fmap f . getFinMap+  {-# INLINABLE fmap #-}++instance Foldable (FinMap n) where+  foldMap f = foldMap f . getFinMap+  {-# INLINABLE foldMap #-}++instance Traversable (FinMap n) where+  traverse f fm = FinMap <$> traverse f (getFinMap fm)++instance FunctorWithIndex (Fin n) (FinMap n) where+  imap f = FinMap . IntMap.mapWithKey (f . unsafeFin) . getFinMap+  -- Inline so that RULES for IntMap.mapWithKey can fire+  {-# INLINE imap #-}++instance FoldableWithIndex (Fin n) (FinMap n) where+  ifoldMap f = IntMap.foldMapWithKey (f . unsafeFin) . getFinMap++-- | Non-lawful instance, provided for testing+instance Show a => Show (FinMap n a) where+  show fm = show (getFinMap fm)+  {-# INLINABLE show #-}++------------------------------------------------------------------------+-- Query++-- | /O(1)/. Is the map empty?+null :: FinMap n a -> Bool+null = IntMap.null . getFinMap+{-# INLINABLE null #-}++-- | /O(min(n,W))/. Fetch the value at the given key in the map.+lookup :: Fin n -> FinMap n a -> Maybe a+lookup k = IntMap.lookup (unsafeFinToInt k) . getFinMap+{-# INLINABLE lookup #-}++-- | Unsafely create a @'Fin' n@ from an 'Int' which is known to be less than+-- @n@ for reasons not visible to the type system.+unsafeFin :: forall n. Int -> Fin n+unsafeFin i =+  case NatRepr.mkNatRepr (intToNat i) of+    Some (repr :: NatRepr m) ->+      case unsafeCoerce (NatRepr.LeqProof :: LeqProof 0 0) :: LeqProof (m + 1) n of+        NatRepr.LeqProof -> mkFin @m @n repr++-- | /O(1)/. Number of elements in the map.+size :: forall n a. FinMap n a -> Fin (n + 1)+size = unsafeFin . IntMap.size . getFinMap+{-# INLINEABLE size #-}++------------------------------------------------------------------------+-- Construction++-- | /O(1)/. Increase maximum key/size by 1.+--+-- This does not alter the key-value pairs in the map, but rather increases the+-- maximum number of key-value pairs that the map can hold. See+-- "Data.Parameterized.FinMap" for more information.+--+-- Requires @n + 1 < (maxBound :: Int)@.+incMax :: FinMap n a -> FinMap (n + 1) a+incMax = FinMap . getFinMap+{-# INLINE incMax #-}++-- | /O(1)/. Increase maximum key/size.+--+-- Requires @m < (maxBound :: Int)@.+embed :: (n <= m) => NatRepr m -> FinMap n a -> FinMap m a+embed _ = FinMap . getFinMap+{-# INLINE embed #-}++-- | /O(1)/. The empty map.+empty :: KnownNat n => FinMap n a+empty = FinMap IntMap.empty+{-# INLINE empty #-}++-- | /O(1)/. A map with one element.+singleton :: a -> FinMap 1 a+singleton = FinMap . IntMap.singleton 0+{-# INLINABLE singleton #-}++-- | /O(min(n,W))/.+insert :: Fin n -> a -> FinMap n a -> FinMap n a+insert k v = FinMap . IntMap.insert (unsafeFinToInt k) v . getFinMap+{-# INLINABLE insert #-}++-- buildFinMap, append, and fromVector are duplicated exactly between the safe+-- and unsafe modules because they are used in comparative testing (and so+-- implementations must be available for both types).++newtype FinMap' a (n :: Nat) = FinMap' { unFinMap' :: FinMap n a }++buildFinMap ::+  forall m a.+  NatRepr m ->+  (forall n. (n + 1 <= m) => NatRepr n -> FinMap n a -> FinMap (n + 1) a) ->+  FinMap m a+buildFinMap m f =+  let f' :: forall k. (k + 1 <= m) => NatRepr k -> FinMap' a k -> FinMap' a (k + 1)+      f' = (\n (FinMap' fin) -> FinMap' (f n fin))+  in unFinMap' (NatRepr.natRecStrictlyBounded m (FinMap' empty) f')++-- | /O(min(n,W))/.+append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a+append k v fm =+  case NatRepr.leqSucc k of+    NatRepr.LeqProof -> insert (mkFin k) v (incMax fm)++fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a+fromVector v =+  buildFinMap+    (Vec.length v)+    (\k m ->+      case Vec.elemAt k v of+        Just e -> append k e m+        Nothing -> incMax m)++------------------------------------------------------------------------+-- Operations++-- | /O(min(n,W))/.+delete :: Fin n -> FinMap n a -> FinMap n a+delete k = FinMap . IntMap.delete (unsafeFinToInt k) . getFinMap+{-# INLINABLE delete #-}++-- | Decrement the key/size, removing the item at key @n + 1@ if present.+decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a+decMax k = FinMap . IntMap.delete (unsafeNatReprToInt k) . getFinMap+{-# INLINABLE decMax #-}++mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b+mapWithKey f = FinMap . IntMap.mapWithKey (f . unsafeFin) . getFinMap+-- Inline so that RULES for IntMap.mapWithKey can fire+{-# INLINE mapWithKey #-}++-- | /O(n+m)/.+unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a+unionWithKey f fm1 fm2 =+  FinMap (IntMap.unionWithKey (f . unsafeFin) (getFinMap fm1) (getFinMap fm2))++-- | /O(n+m)/.+unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a+unionWith f = unionWithKey (\_ v1 v2 -> f v1 v2)++-- | /O(n+m)/. Left-biased union, i.e. (@'union' == 'unionWith' 'const'@).+union :: FinMap n a -> FinMap n a -> FinMap n a+union = unionWith const

@@ -63,6 +63,7 @@   , natRec   , natRecStrong   , natRecBounded+  , natRecStrictlyBounded   , natForEach   , natFromZero   , NatCases(..)@@ -86,6 +87,7 @@   , testLeq   , testStrictLeq   , leqRefl+  , leqSucc   , leqTrans   , leqZero   , leqAdd2@@ -177,8 +179,6 @@       -- We have n = m + 1 for some m.       let         -- | x <= x + 1-        leqSucc:: forall x. LeqProof x (x+1)-        leqSucc = leqAdd2 (LeqProof :: LeqProof x x) (LeqProof :: LeqProof 0 1)         leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y         leqPlus fx =           case (plusComm fx (knownNat @1) :: x + 1 :~: 1 + x)    of { Refl ->@@ -187,7 +187,7 @@           case (LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ->             leqTrans (LeqProof :: LeqProof 1 (y-x))                      (leqSub (LeqProof :: LeqProof y y)-                             (leqTrans (leqSucc :: LeqProof x (x+1))+                             (leqTrans (leqSucc (Proxy :: Proxy x))                                        (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)           }}}}       in leqPlus (predNat n)@@ -423,6 +423,9 @@ leqRefl :: forall f n . f n -> LeqProof n n leqRefl _ = LeqProof +leqSucc :: forall f z. f z -> LeqProof z (z + 1)+leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)+ -- | Apply transitivity to LeqProof leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)@@ -613,6 +616,28 @@             }}         Right f {- :: (m <= h) -> Void -} ->           absurd $ f (LeqProof :: LeqProof m h)++-- | A version of 'natRecBounded' which doesn't require the type index of the+-- result to be greater than @0@ and provides a strict inequality constraint.+natRecStrictlyBounded ::+  forall m f.+  NatRepr m ->+  f 0 ->+  (forall n. (n + 1 <= m) => NatRepr n -> f n -> f (n + 1)) ->+  f m+natRecStrictlyBounded m base indH =+  case isZeroNat m of+    ZeroNat -> base+    NonZeroNat ->+      case predNat m of+        (p :: NatRepr p) ->+          natRecBounded+            p+            p+            base+            (\(k :: NatRepr n) (v :: f n) ->+              case leqAdd2 (LeqProof :: LeqProof n p) (LeqProof :: LeqProof 1 1) of+                LeqProof -> indH k v)  mulCancelR ::   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)

@@ -17,8 +17,10 @@   , mapSome   , traverseSome   , traverseSome_+  , someLens   ) where +import Control.Lens (Lens', lens, (&), (^.), (.~)) import Data.Hashable import Data.Kind import Data.Parameterized.Classes@@ -33,7 +35,7 @@ instance OrdF f => Ord (Some f) where   compare (Some x) (Some y) = toOrdering (compareF x y) -instance HashableF f => Hashable (Some f) where+instance (HashableF f, TestEquality f) => Hashable (Some f) where   hashWithSalt s (Some x) = hashWithSaltF s x   hash (Some x) = hashF x @@ -64,3 +66,8 @@ instance FunctorF     Some where fmapF     = mapSome instance FoldableF    Some where foldMapF  = foldMapFDefault instance TraversableF Some where traverseF = traverseSome++-- | A lens that is polymorphic in the index may be used on a value with an+-- existentially-quantified index.+someLens :: (forall tp. Lens' (f tp) a) -> Lens' (Some f) a+someLens l = lens (\(Some x) -> x ^. l) (\(Some x) v -> Some (x & l .~ v))

@@ -441,10 +441,7 @@ singleton a = Vector (Vector.singleton a)  leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)-leqLen v =-  let leqSucc :: forall f z. f z -> LeqProof z (z + 1)-      leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)-  in leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))+leqLen v = leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))  -- | Add an element to the head of a vector cons :: forall n a. a -> Vector n a -> Vector (n+1) a

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}@@ -131,250 +132,327 @@  type TestCtx = U.EmptyCtx '::> Int '::> String '::> Int '::> Bool - ----------------------------------------------------------------------+-- Hedgehog properties -contextTests :: IO TestTree-contextTests = testGroup "Context" <$> return-   [ testProperty "size (unsafe)" $ property $-     do vals <- forAll genSomePayloadList-        Some a <- return $ mkUAsgn vals-        length vals === U.sizeInt (U.size a)-   , testProperty "size (safe)" $ property $-     do vals <- forAll genSomePayloadList-        Some a <- return $ mkSAsgn vals-        length vals === S.sizeInt (S.size a)+prop_sizeUnsafe :: Property+prop_sizeUnsafe = property $+  do vals <- forAll genSomePayloadList+     Some a <- return $ mkUAsgn vals+     length vals === U.sizeInt (U.size a) -   , testProperty "safe_index_eq" $ property $+prop_sizeSafe :: Property+prop_sizeSafe = property $+  do vals <- forAll genSomePayloadList+     Some a <- return $ mkSAsgn vals+     length vals === S.sizeInt (S.size a)++prop_safeIndexEq :: Property+prop_safeIndexEq = property $      do vals <- forAll genSomePayloadList         i' <- forAll $ HG.int (linear 0 $ length vals - 1)         Some a <- return $ mkSAsgn vals         Just (Some idx) <- return $ S.intIndex i' (S.size a)         Some (a S.! idx) === vals !! i' -   , testProperty "unsafe_index_eq" $ property $-     do vals <- forAll genSomePayloadList-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)-        Some a <- return $ mkUAsgn vals-        Just (Some idx) <- return $ U.intIndex i' (U.size a)-        Some (a U.! idx) === vals !! i'+prop_unsafeIndexEq :: Property+prop_unsafeIndexEq = property $+  do vals <- forAll genSomePayloadList+     i' <- forAll $ HG.int (linear 0 $ length vals - 1)+     Some a <- return $ mkUAsgn vals+     Just (Some idx) <- return $ U.intIndex i' (U.size a)+     Some (a U.! idx) === vals !! i' -   , testProperty "safe_tolist" $ property $-     do vals <- forAll genSomePayloadList-        Some a <- return $ mkSAsgn vals-        let vals' = toListFC Some a-        vals === vals'-   , testProperty "unsafe_tolist" $ property $-     do vals <- forAll genSomePayloadList-        Some a <- return $ mkUAsgn vals-        let vals' = toListFC Some a-        vals === vals'+prop_safeToList :: Property+prop_safeToList = property $+  do vals <- forAll genSomePayloadList+     Some a <- return $ mkSAsgn vals+     let vals' = toListFC Some a+     vals === vals' -   , testProperty "adjust test monadic" $ property $-     do vals <- forAll genSomePayloadList-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)+prop_unsafeToList :: Property+prop_unsafeToList = property $+  do vals <- forAll genSomePayloadList+     Some a <- return $ mkUAsgn vals+     let vals' = toListFC Some a+     vals === vals' -        Some x <- return $ mkUAsgn vals-        Some y <- return $ mkSAsgn vals+prop_adjustTestMonadic :: Property+prop_adjustTestMonadic = property $+  do vals <- forAll genSomePayloadList+     i' <- forAll $ HG.int (linear 0 $ length vals - 1) -        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)+     Some x <- return $ mkUAsgn vals+     Some y <- return $ mkSAsgn vals -        x' <- U.adjustM (return . twiddle) idx_x x-        y' <- S.adjustM (return . twiddle) idx_y y+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y) -        toListFC Some x' === toListFC Some y'+     x' <- U.adjustM (return . twiddle) idx_x x+     y' <- S.adjustM (return . twiddle) idx_y y -   , testProperty "adjust test" $ property $-     do vals <- forAll genSomePayloadList-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)+     toListFC Some x' === toListFC Some y' -        Some x <- return $ mkUAsgn vals-        Some y <- return $ mkSAsgn vals+prop_adjustTest :: Property+prop_adjustTest = property $+  do vals <- forAll genSomePayloadList+     i' <- forAll $ HG.int (linear 0 $ length vals - 1) -        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)+     Some x <- return $ mkUAsgn vals+     Some y <- return $ mkSAsgn vals -        let x' = x & ixF idx_x %~ twiddle-            y' = y & ixF idx_y %~ twiddle+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y) -        toListFC Some x' === toListFC Some y'-        -- adjust actually modified the entry-        toListFC Some x /== toListFC Some x'-        toListFC Some y /== toListFC Some y'+     let x' = x & ixF idx_x %~ twiddle+         y' = y & ixF idx_y %~ twiddle -   , testProperty "update test" $ property $-     do vals <- forAll genSomePayloadList-        i' <- forAll $ HG.int (linear 0 $ length vals - 1)+     toListFC Some x' === toListFC Some y'+     -- adjust actually modified the entry+     toListFC Some x /== toListFC Some x'+     toListFC Some y /== toListFC Some y' -        Some x <- return $ mkUAsgn vals-        Some y <- return $ mkSAsgn vals+prop_updateTest :: Property+prop_updateTest = property $+  do vals <- forAll genSomePayloadList+     i' <- forAll $ HG.int (linear 0 $ length vals - 1) -        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)-        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)+     Some x <- return $ mkUAsgn vals+     Some y <- return $ mkSAsgn vals -        let x' = over (ixF idx_x) twiddle x-            y' = (ixF idx_y) %~ twiddle $ y-            updX = x & ixF idx_x .~ x' U.! idx_x-            updY = y & ixF idx_y .~ y' S.! idx_y+     Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+     Just (Some idx_y) <- return $ S.intIndex i' (S.size y) -        toListFC Some updX === toListFC Some updY-        -- update actually modified the entry-        toListFC Some x /== toListFC Some updX-        toListFC Some y /== toListFC Some updY-        -- update modified the expected entry-        toListFC Some x' === toListFC Some updX-        toListFC Some y' === toListFC Some updY+     let x' = over (ixF idx_x) twiddle x+         y' = (ixF idx_y) %~ twiddle $ y+         updX = x & ixF idx_x .~ x' U.! idx_x+         updY = y & ixF idx_y .~ y' S.! idx_y -   , testProperty "safe_eq" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        Some x <- return $ mkSAsgn vals1-        Some y <- return $ mkSAsgn vals2-        case testEquality x y of-          Just Refl -> vals1 === vals2-          Nothing   -> vals1 /== vals2-   , testProperty "unsafe_eq" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        Some x <- return $ mkUAsgn vals1-        Some y <- return $ mkUAsgn vals2-        case testEquality x y of-          Just Refl -> vals1 === vals2-          Nothing   -> vals1 /== vals2+     toListFC Some updX === toListFC Some updY+     -- update actually modified the entry+     toListFC Some x /== toListFC Some updX+     toListFC Some y /== toListFC Some updY+     -- update modified the expected entry+     toListFC Some x' === toListFC Some updX+     toListFC Some y' === toListFC Some updY -   , testProperty "take none" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        vals3 <- forAll genSomePayloadList-        Some w <- return $ mkUAsgn vals1-        Some x <- return $ mkUAsgn vals2-        Some y <- return $ mkUAsgn vals3-        let z = w U.<++> x U.<++> y-        case P.leftId z of-          Refl -> let r = C.take U.zeroSize (U.size z) z in-                    assert $ isJust $ testEquality U.empty r-   , testProperty "drop none" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        vals3 <- forAll genSomePayloadList-        Some w <- return $ mkUAsgn vals1-        Some x <- return $ mkUAsgn vals2-        Some y <- return $ mkUAsgn vals3-        let z = w U.<++> x U.<++> y-        case P.leftId z of-          Refl -> let r = C.drop U.zeroSize (U.size z) z in-                    assert $ isJust $ testEquality z r+prop_safeEq :: Property+prop_safeEq = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     Some x <- return $ mkSAsgn vals1+     Some y <- return $ mkSAsgn vals2+     case testEquality x y of+       Just Refl -> vals1 === vals2+       Nothing   -> vals1 /== vals2 -   , testProperty "take all" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        vals3 <- forAll genSomePayloadList-        Some w <- return $ mkUAsgn vals1-        Some x <- return $ mkUAsgn vals2-        Some y <- return $ mkUAsgn vals3-        let z = w U.<++> x U.<++> y-        let r = C.take (U.size z) U.zeroSize z-        assert $ isJust $ testEquality z r-   , testProperty "drop all" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        vals3 <- forAll genSomePayloadList-        Some w <- return $ mkUAsgn vals1-        Some x <- return $ mkUAsgn vals2-        Some y <- return $ mkUAsgn vals3-        let z = w U.<++> x U.<++> y-        let r = C.drop (U.size z) U.zeroSize z-        assert $ isJust $ testEquality U.empty r+prop_unsafeEq :: Property+prop_unsafeEq = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     Some x <- return $ mkUAsgn vals1+     Some y <- return $ mkUAsgn vals2+     case testEquality x y of+       Just Refl -> vals1 === vals2+       Nothing   -> vals1 /== vals2 -   , testProperty "append_take" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        Some x <- return $ mkUAsgn vals1-        Some y <- return $ mkUAsgn vals2-        let z = x U.<++> y-        let x' = C.take (U.size x) (U.size y) z-        assert $ isJust $ testEquality x x'+prop_takeNone :: Property+prop_takeNone = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     vals3 <- forAll genSomePayloadList+     Some w <- return $ mkUAsgn vals1+     Some x <- return $ mkUAsgn vals2+     Some y <- return $ mkUAsgn vals3+     let z = w U.<++> x U.<++> y+     case P.leftId z of+       Refl -> let r = C.take U.zeroSize (U.size z) z in+                 assert $ isJust $ testEquality U.empty r -   , testProperty "append_take_drop" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        Some x <- return $ mkUAsgn vals1-        Some y <- return $ mkUAsgn vals2-        let z = x U.<++> y-        let x' = C.take (U.size x) (U.size y) z-        let y' = C.drop (U.size x) (U.size y) z-        assert $ isJust $ testEquality x x'-        assert $ isJust $ testEquality y y'+prop_dropNone :: Property+prop_dropNone = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     vals3 <- forAll genSomePayloadList+     Some w <- return $ mkUAsgn vals1+     Some x <- return $ mkUAsgn vals2+     Some y <- return $ mkUAsgn vals3+     let z = w U.<++> x U.<++> y+     case P.leftId z of+       Refl -> let r = C.drop U.zeroSize (U.size z) z in+                 assert $ isJust $ testEquality z r -   , testProperty "append_take_drop_multiple" $ property $-     do vals1 <- forAll genSomePayloadList-        vals2 <- forAll genSomePayloadList-        vals3 <- forAll genSomePayloadList-        vals4 <- forAll genSomePayloadList-        vals5 <- forAll genSomePayloadList-        Some u <- return $ mkUAsgn vals1-        Some v <- return $ mkUAsgn vals2-        Some w <- return $ mkUAsgn vals3-        Some x <- return $ mkUAsgn vals4-        Some y <- return $ mkUAsgn vals5-        let uv = u U.<++> v-        let wxy = w U.<++> x U.<++> y-        -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y-        let z = uv U.<++> wxy-        let uv' = C.take (U.size uv) (U.size wxy) z-        let wxy' = C.drop (U.size uv) (U.size wxy) z-        let withWXY = C.dropPrefix z uv (error "failed dropPrefix")-        assert $ isJust $ testEquality (u U.<++> v) uv'-        assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'-        assert $ isJust $ testEquality uv uv'-        assert $ isJust $ testEquality wxy wxy'-        withWXY $ \t -> assert $ isJust $ testEquality wxy' t+prop_takeAll :: Property+prop_takeAll = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     vals3 <- forAll genSomePayloadList+     Some w <- return $ mkUAsgn vals1+     Some x <- return $ mkUAsgn vals2+     Some y <- return $ mkUAsgn vals3+     let z = w U.<++> x U.<++> y+     let r = C.take (U.size z) U.zeroSize z+     assert $ isJust $ testEquality z r -   , testProperty "zip/unzip" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        let zipped = C.zipWith Pair x x-        let (x', x'') = C.unzip zipped-        assert $ isJust $ testEquality x x'-        assert $ isJust $ testEquality x x''+prop_dropAll :: Property+prop_dropAll = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     vals3 <- forAll genSomePayloadList+     Some w <- return $ mkUAsgn vals1+     Some x <- return $ mkUAsgn vals2+     Some y <- return $ mkUAsgn vals3+     let z = w U.<++> x U.<++> y+     let r = C.drop (U.size z) U.zeroSize z+     assert $ isJust $ testEquality U.empty r -   , testProperty "fmapFC_identity" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        assert $ isJust $ testEquality x (fmapFC id x)+prop_appendTake :: Property+prop_appendTake = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     Some x <- return $ mkUAsgn vals1+     Some y <- return $ mkUAsgn vals2+     let z = x U.<++> y+     let x' = C.take (U.size x) (U.size y) z+     assert $ isJust $ testEquality x x' -   , testProperty "fmapFC_assoc" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        Fun f <- forAll $ HG.element funs-        Fun g <- forAll $ HG.element funs-        assert $ isJust $ testEquality-                            (fmapFC g (fmapFC f x))-                            (fmapFC (g . f) x)+prop_appendTakeDrop :: Property+prop_appendTakeDrop = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     Some x <- return $ mkUAsgn vals1+     Some y <- return $ mkUAsgn vals2+     let z = x U.<++> y+     let x' = C.take (U.size x) (U.size y) z+     let y' = C.drop (U.size x) (U.size y) z+     assert $ isJust $ testEquality x x'+     assert $ isJust $ testEquality y y' -   , testProperty "imapFC_index_noop" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        assert $-          isJust $-            testEquality x (imapFC (\idx _ -> x U.! idx) x)+prop_appendTakeDropMultiple :: Property+prop_appendTakeDropMultiple = property $+  do vals1 <- forAll genSomePayloadList+     vals2 <- forAll genSomePayloadList+     vals3 <- forAll genSomePayloadList+     vals4 <- forAll genSomePayloadList+     vals5 <- forAll genSomePayloadList+     Some u <- return $ mkUAsgn vals1+     Some v <- return $ mkUAsgn vals2+     Some w <- return $ mkUAsgn vals3+     Some x <- return $ mkUAsgn vals4+     Some y <- return $ mkUAsgn vals5+     let uv = u U.<++> v+     let wxy = w U.<++> x U.<++> y+     -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y+     let z = uv U.<++> wxy+     let uv' = C.take (U.size uv) (U.size wxy) z+     let wxy' = C.drop (U.size uv) (U.size wxy) z+     let withWXY = C.dropPrefix z uv (error "failed dropPrefix")+     assert $ isJust $ testEquality (u U.<++> v) uv'+     assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'+     assert $ isJust $ testEquality uv uv'+     assert $ isJust $ testEquality wxy wxy'+     withWXY $ \t -> assert $ isJust $ testEquality wxy' t -   , testProperty "imapFC/fmapFC" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        Fun f <- forAll $ HG.element funs-        assert $ isJust $ testEquality-                            (fmapFC f x)-                            (imapFC (const f) x)+prop_zipUnzip :: Property+prop_zipUnzip = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     let zipped = C.zipWith Pair x x+     let (x', x'') = C.unzip zipped+     assert $ isJust $ testEquality x x'+     assert $ isJust $ testEquality x x'' -   , testProperty "ifoldMapFC/foldMapFC" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        assert $ foldMapFC show x == ifoldMapFC (const show) x+prop_fmapFCIdentity :: Property+prop_fmapFCIdentity = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     assert $ isJust $ testEquality x (fmapFC id x) -   , testProperty "itraverseFC/traverseFC" $ property $-     do Some x <- mkUAsgn <$> forAll genSomePayloadList-        Fun f <- forAll $ HG.element funs-        let f' :: forall a. Payload a -> Identity (Payload a)-            f' = Identity . f-        assert $ isJust $ testEquality-                            (runIdentity (traverseFC f' x))-                            (runIdentity (itraverseFC (const f') x))+prop_fmapFCAssoc :: Property+prop_fmapFCAssoc = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     Fun f <- forAll $ HG.element funs+     Fun g <- forAll $ HG.element funs+     assert $ isJust $ testEquality+                         (fmapFC g (fmapFC f x))+                         (fmapFC (g . f) x)++prop_imapFCIndexNoop :: Property+prop_imapFCIndexNoop = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     assert $+       isJust $+         testEquality x (imapFC (\idx _ -> x U.! idx) x)++prop_imapFCFmapFC :: Property+prop_imapFCFmapFC = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     Fun f <- forAll $ HG.element funs+     assert $ isJust $ testEquality+                         (fmapFC f x)+                         (imapFC (const f) x)++prop_ifoldMapFCFoldMapFC :: Property+prop_ifoldMapFCFoldMapFC = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     assert $ foldMapFC show x == ifoldMapFC (const show) x++prop_itraverseFCTraverseFC :: Property+prop_itraverseFCTraverseFC = property $+  do Some x <- mkUAsgn <$> forAll genSomePayloadList+     Fun f <- forAll $ HG.element funs+     let f' :: forall a. Payload a -> Identity (Payload a)+         f' = Identity . f+     assert $ isJust $ testEquality+                         (runIdentity (traverseFC f' x))+                         (runIdentity (itraverseFC (const f') x))++----------------------------------------------------------------------++contextTests :: IO TestTree+contextTests = testGroup "Context" <$> return+   [ testPropertyNamed "size (unsafe)" "prop_sizeUnsafe" prop_sizeUnsafe+   , testPropertyNamed "size (safe)" "prop_sizeSafe" prop_sizeSafe++   , testPropertyNamed "safe_index_eq" "prop_safeIndexEq" prop_safeIndexEq++   , testPropertyNamed "unsafe_index_eq" "prop_unsafeIndexEq" prop_unsafeIndexEq++   , testPropertyNamed "safe_tolist" "prop_safeToList" prop_safeToList+   , testPropertyNamed "unsafe_tolist" "prop_unsafeToList" prop_unsafeToList++   , testPropertyNamed "adjust test monadic" "prop_adjustTestMonadic" prop_adjustTestMonadic++   , testPropertyNamed "adjust test" "prop_adjustTest" prop_adjustTest++   , testPropertyNamed "update test" "prop_updateTest" prop_updateTest++   , testPropertyNamed "safe_eq" "prop_safeEq" prop_safeEq+   , testPropertyNamed "unsafe_eq" "prop_unsafeEq" prop_unsafeEq++   , testPropertyNamed "take none" "prop_takeNone" prop_takeNone+   , testPropertyNamed "drop none" "prop_dropNone" prop_dropNone++   , testPropertyNamed "take all" "prop_takeAll" prop_takeAll+   , testPropertyNamed "drop all" "prop_dropAll" prop_dropAll++   , testPropertyNamed "append_take" "prop_appendTake" prop_appendTake++   , testPropertyNamed "append_take_drop" "prop_appendTakeDrop" prop_appendTakeDrop++   , testPropertyNamed "append_take_drop_multiple" "prop_appendTakeDropMultiple" prop_appendTakeDropMultiple++   , testPropertyNamed "zip/unzip" "prop_zipUnzip" prop_zipUnzip++   , testPropertyNamed "fmapFC_identity" "prop_fmapFCIdentity" prop_fmapFCIdentity++   , testPropertyNamed "fmapFC_assoc" "prop_fmapFCAssoc" prop_fmapFCAssoc++   , testPropertyNamed "imapFC_index_noop" "prop_imapFCIndexNoop" prop_imapFCIndexNoop++   , testPropertyNamed "imapFC/fmapFC" "prop_imapFCFmapFC" prop_imapFCFmapFC++   , testPropertyNamed "ifoldMapFC/foldMapFC" "prop_ifoldMapFCFoldMapFC" prop_ifoldMapFCFoldMapFC++   , testPropertyNamed "itraverseFC/traverseFC" "prop_itraverseFCTraverseFC" prop_itraverseFCTraverseFC     , testCaseSteps "explicit indexing (unsafe)" $ \step -> do        let mkUPayload :: U.Assignment Payload TestCtx

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# Language CPP #-}@@ -16,6 +17,7 @@ import qualified Hedgehog.Gen as HG import           Hedgehog.Range (linear) import           Test.Tasty (TestTree, testGroup)+import           Test.Tasty.Hedgehog (testPropertyNamed) import           Test.Tasty.HUnit (assertBool, testCase)  import           Data.Parameterized.NatRepr@@ -26,15 +28,29 @@ import qualified Hedgehog.Classes as HC #endif -genFin :: (0 <= n, Monad m) => NatRepr n -> GenT m (Fin n)+genNatRepr :: (Monad m) => Natural -> GenT m (Some NatRepr)+genNatRepr bound =+  do x0 <- HG.integral (linear 0 bound)+     return (mkNatRepr x0)++genFin :: (1 <= n, Monad m) => NatRepr n -> GenT m (Fin n) genFin n =-  do x0 <- HG.integral (linear 0 ((natValue n) - 1 :: Natural))-     Some x <- return (mkNatRepr x0)+  do Some x <- genNatRepr (natValue n - 1 :: Natural)      return $        case testLeq (incNat x) n of          Just LeqProof -> mkFin x          Nothing -> error "Impossible" +prop_count_true :: Property+prop_count_true = property $+  do Some n <- forAll (genNatRepr 100)+     finToNat (countFin n (\_ _ -> True)) === natValue n++prop_count_false :: Property+prop_count_false = property $+  do Some n <- forAll (genNatRepr 100)+     finToNat (countFin n (\_ _ -> False)) === 0+ finTests :: IO TestTree finTests =   testGroup "Fin" <$>@@ -47,6 +63,9 @@           assertBool             "minBound <= maxBound (2)"             ((minBound :: Fin 2) <= (minBound :: Fin 2))++      , testPropertyNamed "count-true" "prop_count_true" prop_count_true+      , testPropertyNamed "count-false" "prop_count_false" prop_count_false  #if __GLASGOW_HASKELL__ >= 806       , testCase "Eq-Fin-laws-1" $

@@ -0,0 +1,393 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+++module Test.FinMap (finMapTests) where++import           Control.Monad (foldM)+import           Data.Foldable.WithIndex (itoList)+import           Data.Functor.WithIndex (FunctorWithIndex(imap))+import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))+import           Data.Proxy (Proxy(Proxy))+import           Data.Type.Equality ((:~:)(Refl))++import           Data.Parameterized.Fin (Fin)+import qualified Data.Parameterized.Fin as Fin+import           Data.Parameterized.NatRepr (LeqProof, NatRepr, type (<=), type (+))+import qualified Data.Parameterized.NatRepr as NatRepr++import           Hedgehog+import qualified Hedgehog.Gen as HG+import           Hedgehog.Range (linear)+import           Test.Tasty+import           Test.Tasty.Hedgehog++#if __GLASGOW_HASKELL__ >= 806+import           Test.Tasty.HUnit (assertBool, testCase)+import qualified Hedgehog.Classes as HC+#endif++import qualified Data.Parameterized.FinMap.Safe as S+import qualified Data.Parameterized.FinMap.Unsafe as U+import qualified Data.Parameterized.Vector as Vec++import           Test.Fin (genFin)+import           Test.Vector (SomeVector(..), genSomeVector, genVectorOfLength, genOrdering, orderingEndomorphisms, orderingToStringFuns)++data SomeSafeFinMap a = forall n. SomeSafeFinMap (NatRepr n) (S.FinMap n a)+data SomeUnsafeFinMap a = forall n. SomeUnsafeFinMap (NatRepr n) (U.FinMap n a)++instance Show a => Show (SomeSafeFinMap a) where+  show (SomeSafeFinMap _ v) = show v+instance Show a => Show (SomeUnsafeFinMap a) where+  show (SomeUnsafeFinMap _ v) = show v++genSafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (S.FinMap (n + 1) a)+genSafeFinMap n genElem = S.fromVector <$> genVectorOfLength n (HG.maybe genElem)++genUnsafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (U.FinMap (n + 1) a)+genUnsafeFinMap n genElem = U.fromVector <$> genVectorOfLength n (HG.maybe genElem)++genSomeSafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeSafeFinMap a)+genSomeSafeFinMap genElem =+  do SomeVector v <- genSomeVector (HG.maybe genElem)+     return (SomeSafeFinMap (Vec.length v) (S.fromVector v))++genSomeUnsafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeUnsafeFinMap a)+genSomeUnsafeFinMap genElem =+  do SomeVector v <- genSomeVector (HG.maybe genElem)+     return (SomeUnsafeFinMap (Vec.length v) (U.fromVector v))++prop_incMax_size_safe :: Property+prop_incMax_size_safe = property $+  do SomeSafeFinMap _ fm <- forAll $ genSomeSafeFinMap genOrdering+     Fin.finToNat (S.size (S.incMax fm)) === Fin.finToNat (S.size fm)++prop_incMax_size_unsafe :: Property+prop_incMax_size_unsafe = property $+  do SomeUnsafeFinMap _ fm <- forAll $ genSomeUnsafeFinMap genOrdering+     Fin.finToNat (U.size (U.incMax fm)) === Fin.finToNat (U.size fm)++prop_imap_const_safe :: Property+prop_imap_const_safe = property $+  do f <- forAll (HG.element orderingEndomorphisms)+     SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)+     imap (const f) fm === fmap f fm++prop_imap_const_unsafe :: Property+prop_imap_const_unsafe = property $+  do f <- forAll (HG.element orderingEndomorphisms)+     SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)+     imap (const f) fm === fmap f fm++prop_ifoldMap_const_safe :: Property+prop_ifoldMap_const_safe = property $+  do f <- forAll (HG.element orderingToStringFuns)+     SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)+     ifoldMap (const f) fm === foldMap f fm++prop_ifoldMap_const_unsafe :: Property+prop_ifoldMap_const_unsafe = property $+  do f <- forAll (HG.element orderingToStringFuns)+     SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)+     ifoldMap (const f) fm === foldMap f fm++cancelPlusOne ::+  forall f g i n.+  f i ->+  g n ->+  LeqProof (i + 1) (n + 1) ->+  LeqProof i n+cancelPlusOne i n NatRepr.LeqProof =+  case NatRepr.plusMinusCancel n (NatRepr.knownNat :: NatRepr 1) of+    Refl ->+      case NatRepr.plusMinusCancel i (NatRepr.knownNat :: NatRepr 1) of+        Refl ->+          case NatRepr.leqSub2+                  (NatRepr.LeqProof :: LeqProof (i + 1) (n + 1))+                  (NatRepr.LeqProof :: LeqProof 1 1) of+            NatRepr.LeqProof -> NatRepr.LeqProof++withIndexSafe ::+  SomeSafeFinMap a ->+  (forall n. Fin n -> S.FinMap n a -> PropertyT IO ()) ->+  PropertyT IO ()+withIndexSafe (SomeSafeFinMap n fm) k =+  case NatRepr.isZeroOrGT1 n of+    Left Refl -> k Fin.minFin (S.incMax fm)+    Right NatRepr.LeqProof ->+      do idx <- forAll (genFin n)+         k idx fm++withIndexUnsafe ::+  SomeUnsafeFinMap a ->+  (forall n. Fin n -> U.FinMap n a -> PropertyT IO ()) ->+  PropertyT IO ()+withIndexUnsafe (SomeUnsafeFinMap n fm) k =+  case NatRepr.isZeroOrGT1 n of+    Left Refl -> k Fin.minFin (U.incMax fm)+    Right NatRepr.LeqProof ->+      do idx <- forAll (genFin n)+         k idx fm++withSizeUnsafe ::+  U.FinMap n a ->+  (forall i. (i + 1 <= n + 1, i <= n) => NatRepr i -> r) ->+  r+withSizeUnsafe fm k =+  case U.size fm of+    (sz :: Fin (n + 1)) ->+      Fin.viewFin+        (\(i :: NatRepr i) ->+          case cancelPlusOne i (Proxy :: Proxy n) NatRepr.LeqProof of+            NatRepr.LeqProof -> k i)+        sz++prop_insert_size_safe :: Property+prop_insert_size_safe = property $+  do sfm <- forAll $ genSomeSafeFinMap genOrdering+     withIndexSafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      let size = Fin.finToNat (S.size fm)+      let newSize = Fin.finToNat (S.size (S.insert (Fin.embed idx) o fm))+      assert (size == newSize || size + 1 == newSize)++prop_insert_size_unsafe :: Property+prop_insert_size_unsafe = property $+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering+     withIndexUnsafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      let size = Fin.finToNat (U.size fm)+      let newSize = Fin.finToNat (U.size (U.insert (Fin.embed idx) o fm))+      assert (size == newSize || size + 1 == newSize)++prop_insert_delete_safe :: Property+prop_insert_delete_safe = property $+  do sfm <- forAll $ genSomeSafeFinMap genOrdering+     withIndexSafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      S.delete idx (S.insert idx o fm) === S.delete idx fm++prop_insert_delete_unsafe :: Property+prop_insert_delete_unsafe = property $+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering+     withIndexUnsafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      U.delete idx (U.insert idx o fm) === U.delete idx fm++prop_delete_insert_safe :: Property+prop_delete_insert_safe = property $+  do sfm <- forAll $ genSomeSafeFinMap genOrdering+     withIndexSafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      S.insert idx o (S.delete idx fm) === S.insert idx o fm++prop_delete_insert_unsafe :: Property+prop_delete_insert_unsafe = property $+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering+     withIndexUnsafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      U.insert idx o (U.delete idx fm) === U.insert idx o fm++prop_empty_insert_safe :: Property+prop_empty_insert_safe = property $+  do withIndexSafe (SomeSafeFinMap (NatRepr.knownNat @0) S.empty) $ \idx fm -> do+      o <- forAll genOrdering+      fm /== S.insert idx o fm++prop_empty_insert_unsafe :: Property+prop_empty_insert_unsafe = property $+  do withIndexUnsafe (SomeUnsafeFinMap (NatRepr.knownNat @0) U.empty) $ \idx fm -> do+      o <- forAll genOrdering+      fm /== U.insert idx o fm++prop_insert_insert_safe :: Property+prop_insert_insert_safe = property $+  do sfm <- forAll $ genSomeSafeFinMap genOrdering+     withIndexSafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      S.insert idx o (S.insert idx o fm) === S.insert idx o fm++prop_insert_insert_unsafe :: Property+prop_insert_insert_unsafe = property $+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering+     withIndexUnsafe sfm $ \idx fm -> do+      o <- forAll genOrdering+      U.insert idx o (U.insert idx o fm) === U.insert idx o fm++prop_delete_delete_safe :: Property+prop_delete_delete_safe = property $+  do sfm <- forAll $ genSomeSafeFinMap genOrdering+     withIndexSafe sfm $ \idx fm -> do+      S.delete idx (S.delete idx fm) === S.delete idx fm++prop_delete_delete_unsafe :: Property+prop_delete_delete_unsafe = property $+  do sfm <- forAll $ genSomeUnsafeFinMap genOrdering+     withIndexUnsafe sfm $ \idx fm -> do+      U.delete idx (U.delete idx fm) === U.delete idx fm++-- | Type used for comparative API tests+data MatchedMaps a =+  forall n.+  MatchedMaps+    { _unsafe :: U.FinMap n a+    , _safe :: S.FinMap n a+    }++operations ::+  Show a =>+  Gen a ->+  -- | For testing 'fmap'.+  [a -> a] ->+  [MatchedMaps a -> PropertyT IO (MatchedMaps a)]+operations genValue valEndomorphisms =+  [ \(MatchedMaps u s) ->+      withSizeUnsafe u $ \sz -> do+        case NatRepr.isZeroOrGT1 sz of+          Left Refl ->+            do v <- forAll genValue+               return $+                 MatchedMaps+                   (U.insert Fin.minFin v (U.incMax u))+                   (S.insert Fin.minFin v (S.incMax s))+          Right NatRepr.LeqProof ->+            do idx <- Fin.embed <$> forAll (genFin sz)+               v <- forAll genValue+               return (MatchedMaps (U.insert idx v u) (S.insert idx v s))+  , \(MatchedMaps u s) ->+      withSizeUnsafe u $ \sz -> do+        case NatRepr.isZeroOrGT1 sz of+          Left Refl -> return (MatchedMaps u s)+          Right NatRepr.LeqProof ->+            do idx <- Fin.embed <$> forAll (genFin sz)+               return (MatchedMaps (U.delete idx u) (S.delete idx s))+  , \(MatchedMaps u s) ->+        return (MatchedMaps (U.incMax u) (S.incMax s))+  , \(MatchedMaps u s) ->+      do f <- forAll (HG.element (id:valEndomorphisms))+         return (MatchedMaps (fmap f u) (fmap f s))+  , \(MatchedMaps u s) ->+      do f <- forAll (HG.element (id:valEndomorphisms))+         return (MatchedMaps (imap (const f) u) (imap (const f) s))+  , \(MatchedMaps _ _) ->+      do v <- forAll genValue+         return (MatchedMaps (U.singleton v) (S.singleton v))+  , \(MatchedMaps _ _) ->+      return (MatchedMaps (U.empty @0) S.empty)+  , \(MatchedMaps _ _) ->+      return (MatchedMaps (U.empty @8) S.empty)+  ]++-- | Possibly the most important and far-reaching test: The unsafe API should+-- yield the same results as the safe API, after some randomized sequence of+-- operations.+prop_safe_unsafe :: Property+prop_safe_unsafe = property $+  do numOps <- forAll (HG.integral (linear 0 (99 :: Int)))+     let empty = MatchedMaps (U.empty @0) S.empty+     MatchedMaps u s <-+       doTimes (chooseAndApply orderingOps) numOps empty+     itoList u === itoList s+  where+    orderingOps = operations genOrdering orderingEndomorphisms++    chooseAndApply :: [a -> PropertyT IO b] -> a -> PropertyT IO b+    chooseAndApply funs arg =+      do f <- forAll (HG.element funs)+         f arg++    doTimes f n m = foldM (\accum () -> f accum) m (replicate n ())+++finMapTests :: IO TestTree+finMapTests = testGroup "FinMap" <$> return+  [ testPropertyNamed "incSize-decSize-safe" "prop_incMax_size_safe" prop_incMax_size_safe+  , testPropertyNamed "incSize-decSize-unsafe" "prop_incMax_size_unsafe" prop_incMax_size_unsafe+  , testPropertyNamed "insert-size-safe" "prop_insert_size_safe" prop_insert_size_safe+  , testPropertyNamed "insert-size-unsafe" "prop_insert_size_unsafe" prop_insert_size_unsafe+  , testPropertyNamed "insert-delete-safe" "prop_insert_delete_safe" prop_insert_delete_safe+  , testPropertyNamed "insert-delete-unsafe" "prop_insert_delete_unsafe" prop_insert_delete_unsafe+  , testPropertyNamed "delete-insert-safe" "prop_delete_insert_safe" prop_delete_insert_safe+  , testPropertyNamed "delete-insert-unsafe" "prop_delete_insert_unsafe" prop_delete_insert_unsafe+  , testPropertyNamed "empty-insert-safe" "prop_empty_insert_safe" prop_empty_insert_safe+  , testPropertyNamed "empty-insert-unsafe" "prop_empty_insert_unsafe" prop_empty_insert_unsafe+  , testPropertyNamed "insert-insert-safe" "prop_insert_insert_safe" prop_insert_insert_safe+  , testPropertyNamed "insert-insert-unsafe" "prop_insert_insert_unsafe" prop_insert_insert_unsafe+  , testPropertyNamed "delete-delete-safe" "prop_delete_delete_safe" prop_delete_delete_safe+  , testPropertyNamed "delete-delete-unsafe" "prop_delete_delete_unsafe" prop_delete_delete_unsafe+  , testPropertyNamed "imap-const-safe" "prop_imap_const_safe" prop_imap_const_safe+  , testPropertyNamed "imap-const-unsafe" "prop_imap_const_unsafe" prop_imap_const_unsafe+  , testPropertyNamed "ifoldMap-const-safe" "prop_ifoldMap_const_safe" prop_ifoldMap_const_safe+  , testPropertyNamed "ifoldMap-const-unsafe" "prop_ifoldMap_const_unsafe" prop_ifoldMap_const_unsafe+  , testPropertyNamed "safe-unsafe" "prop_safe_unsafe" prop_safe_unsafe++#if __GLASGOW_HASKELL__ >= 806+  , testCase "Eq-Safe-FinMap-laws-1" $+      assertBool "Eq-Safe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Eq-Unsafe-FinMap-laws-1" $+      assertBool "Eq-Unsafe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Eq-Safe-FinMap-laws-10" $+      assertBool "Eq-Safe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Eq-Unsafe-FinMap-laws-10" $+      assertBool "Eq-Unsafe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Semigroup-Safe-FinMap-laws-1" $+      assertBool "Semigroup-Safe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Semigroup-Unsafe-FinMap-laws-1" $+      assertBool "Semigroup-Unsafe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Semigroup-Safe-FinMap-laws-10" $+      assertBool "Semigroup-Safe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Semigroup-Unsafe-FinMap-laws-10" $+      assertBool "Semigroup-Unsafe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Monoid-Safe-FinMap-laws-1" $+      assertBool "Monoid-Safe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Monoid-Unsafe-FinMap-laws-1" $+      assertBool "Monoid-Unsafe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))+  , testCase "Monoid-Safe-FinMap-laws-10" $+      assertBool "Monoid-Safe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Monoid-Unsafe-FinMap-laws-10" $+      assertBool "Monoid-Unsafe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))+  , testCase "Foldable-Safe-FinMap-laws-1" $+      assertBool "Foldable-Safe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @1)))+  , testCase "Foldable-Unsafe-FinMap-laws-1" $+      assertBool "Foldable-Unsafe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))+  , testCase "Foldable-Safe-FinMap-laws-10" $+      assertBool "Foldable-Safe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @10)))+  , testCase "Foldable-Unsafe-FinMap-laws-10" $+      assertBool "Foldable-Unsafe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))+  , testCase "Traversable-Safe-FinMap-laws-1" $+      assertBool "Traversable-Safe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @1)))+  , testCase "Traversable-Unsafe-FinMap-laws-1" $+      assertBool "Traversable-Unsafe-FinMap-laws-1" =<<+        HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))+  , testCase "Traversable-Safe-FinMap-laws-10" $+      assertBool "Traversable-Safe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @10)))+  , testCase "Traversable-Unsafe-FinMap-laws-10" $+      assertBool "Traversable-Unsafe-FinMap-laws-10" =<<+        HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))+#endif+  ]

@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedStrings #-} module Test.NatRepr   ( natTests   )@@ -13,11 +14,14 @@ import           Data.Parameterized.Some import           GHC.TypeLits +prop_withKnownNat :: Property+prop_withKnownNat = property $+  do nInt <- forAll $ HG.int (linearBounded :: Range Int)+     case someNat nInt of+       Nothing       -> diff nInt (<) 0+       Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)+ natTests :: IO TestTree natTests = testGroup "Nat" <$> return-  [ testProperty "withKnownNat" $ property $ do-      nInt <- forAll $ HG.int (linearBounded :: Range Int)-      case someNat nInt of-        Nothing       -> diff nInt (<) 0-        Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)+  [ testPropertyNamed "withKnownNat" "prop_withKnownNat" prop_withKnownNat   ]

@@ -0,0 +1,74 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}++module Test.Some+  ( someTests+  )+where++import           Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))+import           Control.Lens (Lens', lens, view, set)++import           Test.Tasty (TestTree, testGroup)+import           Test.Tasty.HUnit (assertEqual, testCase)++import           Data.Parameterized.Classes (ShowF)+import           Data.Parameterized.Some (Some(Some), someLens)++data Item b where+  BoolItem :: Item Bool+  IntItem :: Item Int++instance Show (Item b) where+  show =+    \case+      BoolItem -> "BoolItem"+      IntItem -> "IntItem"++instance TestEquality Item where+  testEquality x y =+    case (x, y) of+      (BoolItem, BoolItem) -> Just Refl+      (IntItem, IntItem) -> Just Refl+      _ -> Nothing++data Pair a b =+  Pair+    { _fir :: a+    , _sec :: Item b+    }++-- This instance isn't compatible with the intended use of TestEquality (which+-- is supposed to be just for singletons), but it seems fine for tests.+instance Eq a => TestEquality (Pair a) where+  testEquality x y =+    case testEquality (_sec x) (_sec y) of+      Just Refl -> if _fir x == _fir y then Just Refl else Nothing+      Nothing -> Nothing++instance (Show a) => Show (Pair a b) where+  show (Pair a b) = "Pair(" ++ show a ++ ", " ++ show b ++ ")"++instance Show a => ShowF (Pair a)++fir :: Lens' (Pair a b) a+fir = lens _fir (\s v -> s { _fir = v })++someFir :: Lens' (Some (Pair a)) a+someFir = someLens fir++someTests :: IO TestTree+someTests =+  testGroup "Some" <$>+    return+      [ testCase "someLens: view . set" $+          assertEqual+            "view l . set l x == const x"+            (view someFir (set someFir 5 (Some (Pair 1 BoolItem))))+            (5 :: Int)+      , testCase "someLens: set . set" $+          assertEqual+            "set l y . set l x == set l y"+            (set someFir 4 (set someFir 5 (Some (Pair 1 IntItem))))+            (Some (Pair (4 :: Int) IntItem))+      ]

@@ -5,6 +5,7 @@ {-# Language ExplicitForAll #-} {-# Language FlexibleInstances #-} {-# Language LambdaCase #-}+{-# Language OverloadedStrings #-} {-# Language ScopedTypeVariables #-} {-# Language StandaloneDeriving #-} {-# Language TypeFamilies #-}@@ -15,6 +16,12 @@ #endif module Test.Vector   ( vecTests+  , SomeVector(..)+  , genSomeVector+  , genVectorOfLength+  , genOrdering+  , orderingEndomorphisms+  , orderingToStringFuns   ) where @@ -97,149 +104,208 @@       EQ -> GT       GT -> LT   ]+  +-- | Used to test ifoldMap.+orderingToStringFuns :: [ Ordering -> String ]+orderingToStringFuns =+  [ const "s"+  , show+  ] +prop_reverse100 :: Property+prop_reverse100 = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     case testLeq (knownNat @1) (length v) of+       Nothing -> pure ()+       Just LeqProof -> v === (reverse $ reverse v)++prop_reverseSingleton :: Property+prop_reverseSingleton = property $+  do l <- (:[]) <$> forAll genOrdering+     Just v <- return $ fromList (knownNat @1) l+     v === reverse v++prop_splitJoin :: Property+prop_splitJoin = property $+  do let n = knownNat @5+     v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering+     v === (join n $ split n (knownNat @5) v)++prop_cons :: Property+prop_cons = property $+  do let n = knownNat @20+         w = widthVal n+     l <- forAll $ HG.list (constant w w) genOrdering+     x <- forAll genOrdering+     (cons x <$> fromList n l) === fromList (incNat n) (x:l)++prop_snoc :: Property+prop_snoc = property $+  do let n = knownNat @20+         w = widthVal n+     l <- forAll $ HG.list (constant w w) genOrdering+     x <- forAll genOrdering+     (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])++prop_snocUnsnoc :: Property+prop_snocUnsnoc = property $+  do let n = knownNat @20+         w = widthVal n+     l <- forAll $ HG.list (constant w w) genOrdering+     x <- forAll genOrdering+     (fst  . unsnoc . flip snoc x <$> fromList n l) === Just x++prop_generate :: Property+prop_generate = property $+  do let n = knownNat @55+         w = widthVal n+         funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values+         funs =  [ const EQ+                 , \i -> if i < 10 then LT else if i > 15 then GT else EQ+                 , \i -> if i == 0 then EQ else GT+                 ]+     f <- forAll $ HG.element funs+     Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])++prop_unfold :: Property+prop_unfold = property $+  do let n = knownNat @55+         w = widthVal n+         funs :: [ Ordering -> (Ordering, Ordering) ]  -- some miscellaneous functions to generate Vector values+         funs =  [ const (EQ, EQ)+                 , \case+                     LT -> (LT, GT)+                     GT -> (GT, LT)+                     EQ -> (EQ, EQ)+                 ]+     f <- forAll $ HG.element funs+     o <- forAll $ HG.element [EQ, LT, GT]+     Just (unfoldr n f o) === fromList (incNat n) (P.take (w + 1) (List.unfoldr (Just . f) o))++prop_toFromAssignment :: Property+prop_toFromAssignment = property $+  do vals <- forAll genSomePayloadList+     Some a <- return $ mkUAsgn vals+     let sz = Ctx.size a+     case Ctx.viewSize sz of+       Ctx.ZeroSize -> pure ()+       Ctx.IncSize _ ->+         let a' =+               toAssignment+                 sz+                 (\_idx val -> Const val)+                 (fromAssignment Some a)+         in do assert $+                 isJust $+                   testEquality+                     (Ctx.sizeToNatRepr sz)+                     (Ctx.sizeToNatRepr (Ctx.size a'))+               viewSome+                 (\lastElem ->+                    assert $+                      isJust $+                        testEquality+                          (a Ctx.! Ctx.lastIndex sz) lastElem)+                 (getConst (a' Ctx.! Ctx.lastIndex sz))++prop_fmapId :: Property+prop_fmapId = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     fmap id v === v++prop_fmapCompose :: Property+prop_fmapCompose = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     f <- forAll $ HG.element orderingEndomorphisms+     g <- forAll $ HG.element orderingEndomorphisms+     fmap (g . f) v === fmap g (fmap f v)++prop_iterateNRange :: Property+prop_iterateNRange = property $+  do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))+     toList (iterateN len (+1) 0) === [0..(natValue len)]++prop_indicesOfRange :: Property+prop_indicesOfRange = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]++prop_imapConst :: Property+prop_imapConst = property $+  do f <- forAll $ HG.element orderingEndomorphisms+     SomeVector v <- forAll $ genSomeVector genOrdering+     imap (const f) v === fmap f v++prop_ifoldMapConst :: Property+prop_ifoldMapConst = property $+  do f <- forAll $ HG.element orderingToStringFuns+     SomeVector v <- forAll $ genSomeVector genOrdering+     ifoldMap (const f) v === foldMap f v++prop_imapConstIndicesOf :: Property+prop_imapConstIndicesOf = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     imap const v === indicesOf v++prop_imapElemAt :: Property+prop_imapElemAt = property $+  do SomeVector v <- forAll $ genSomeVector genOrdering+     imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v++prop_OrdEqVectorIndex :: Property+prop_OrdEqVectorIndex = property $+  do i <- forAll $ genFin (knownNat @10)+     j <- forAll $ genFin (knownNat @10)+     (i == j) === (compare i j == EQ)+ -- We use @Ordering@ just because it's simple vecTests :: IO TestTree vecTests = testGroup "Vector" <$> return-  [ testProperty "reverse100" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       case testLeq (knownNat @1) (length v) of-         Nothing -> pure ()-         Just LeqProof -> v === (reverse $ reverse v)-  , testProperty "reverseSingleton" $ property $-    do l <- (:[]) <$> forAll genOrdering-       Just v <- return $ fromList (knownNat @1) l-       v === reverse v+  [ testPropertyNamed "reverse100" "prop_reverse100" prop_reverse100+  , testPropertyNamed "reverseSingleton" "prop_reverseSingleton" prop_reverseSingleton -  , testProperty "split-join" $ property $-    do let n = knownNat @5-       v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering-       v === (join n $ split n (knownNat @5) v)+  , testPropertyNamed "split-join" "prop_splitJoin" prop_splitJoin    -- @cons@ is the same for vectors or lists-  , testProperty "cons" $ property $-    do let n = knownNat @20-           w = widthVal n-       l <- forAll $ HG.list (constant w w) genOrdering-       x <- forAll genOrdering-       (cons x <$> fromList n l) === fromList (incNat n) (x:l)+  , testPropertyNamed "cons" "prop_cons" prop_cons    -- @snoc@ is like appending to a list-  , testProperty "snoc" $ property $-    do let n = knownNat @20-           w = widthVal n-       l <- forAll $ HG.list (constant w w) genOrdering-       x <- forAll genOrdering-       (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])+  , testPropertyNamed "snoc" "prop_snoc" prop_snoc    -- @snoc@ and @unsnoc@ are inverses-  , testProperty "snoc/unsnoc" $ property $-    do let n = knownNat @20-           w = widthVal n-       l <- forAll $ HG.list (constant w w) genOrdering-       x <- forAll genOrdering-       (fst  . unsnoc . flip snoc x <$> fromList n l) === Just x+  , testPropertyNamed "snoc/unsnoc" "prop_snocUnsnoc" prop_snocUnsnoc    -- @generate@ is like mapping a function over indices-  , testProperty "generate" $ property $-    do let n = knownNat @55-           w = widthVal n-           funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values-           funs =  [ const EQ-                   , \i -> if i < 10 then LT else if i > 15 then GT else EQ-                   , \i -> if i == 0 then EQ else GT-                   ]-       f <- forAll $ HG.element funs-       Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])+  , testPropertyNamed "generate" "prop_generate" prop_generate    -- @unfold@ works like @unfold@ on lists-  , testProperty "unfold" $ property $-    do let n = knownNat @55-           w = widthVal n-           funs :: [ Ordering -> (Ordering, Ordering) ]  -- some miscellaneous functions to generate Vector values-           funs =  [ const (EQ, EQ)-                   , \case-                       LT -> (LT, GT)-                       GT -> (GT, LT)-                       EQ -> (EQ, EQ)-                   ]-       f <- forAll $ HG.element funs-       o <- forAll $ HG.element [EQ, LT, GT]-       Just (unfoldr n f o) === fromList (incNat n) (P.take (w + 1) (List.unfoldr (Just . f) o))+  , testPropertyNamed "unfold" "prop_unfold" prop_unfold    -- Converting to and from assignments preserves size and last element-  , testProperty "to-from-assignment" $ property $-    do vals <- forAll genSomePayloadList-       Some a <- return $ mkUAsgn vals-       let sz = Ctx.size a-       case Ctx.viewSize sz of-         Ctx.ZeroSize -> pure ()-         Ctx.IncSize _ ->-           let a' =-                 toAssignment-                   sz-                   (\_idx val -> Const val)-                   (fromAssignment Some a)-           in do assert $-                   isJust $-                     testEquality-                       (Ctx.sizeToNatRepr sz)-                       (Ctx.sizeToNatRepr (Ctx.size a'))-                 viewSome-                   (\lastElem ->-                      assert $-                        isJust $-                          testEquality-                            (a Ctx.! Ctx.lastIndex sz) lastElem)-                   (getConst (a' Ctx.! Ctx.lastIndex sz))+  , testPropertyNamed "to-from-assignment" "prop_toFromAssignment" prop_toFromAssignment    -- NOTE: We don't use hedgehog-classes here, because the way the types work   -- would require this to only tests vectors of some fixed size.   --   -- Also, for 'fmap-compose', hedgehog-classes only tests two fixed functions   -- over integers.-  , testProperty "fmap-id" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       fmap id v === v+  , testPropertyNamed "fmap-id" "prop_fmapId" prop_fmapId -  , testProperty "fmap-compose" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       f <- forAll $ HG.element orderingEndomorphisms-       g <- forAll $ HG.element orderingEndomorphisms-       fmap (g . f) v === fmap g (fmap f v)+  , testPropertyNamed "fmap-compose" "prop_fmapCompose" prop_fmapCompose -  , testProperty "iterateN-range" $ property $-    do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))-       toList (iterateN len (+1) 0) === [0..(natValue len)]+  , testPropertyNamed "iterateN-range" "prop_iterateNRange" prop_iterateNRange -  , testProperty "indicesOf-range" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]+  , testPropertyNamed "indicesOf-range" "prop_indicesOfRange" prop_indicesOfRange -  , testProperty "imap-const" $ property $-    do f <- forAll $ HG.element orderingEndomorphisms-       SomeVector v <- forAll $ genSomeVector genOrdering-       imap (const f) v === fmap f v+  , testPropertyNamed "imap-const" "prop_imapConst" prop_imapConst -  , testProperty "ifoldMap-const" $ property $-    do let funs :: [ Ordering -> String ]-           funs = [const "s", show]-       f <- forAll $ HG.element funs-       SomeVector v <- forAll $ genSomeVector genOrdering-       ifoldMap (const f) v === foldMap f v+  , testPropertyNamed "ifoldMap-const" "prop_ifoldMapConst" prop_ifoldMapConst -  , testProperty "imap-const-indicesOf" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       imap const v === indicesOf v+  , testPropertyNamed "imap-const-indicesOf" "prop_imapConstIndicesOf" prop_imapConstIndicesOf -  , testProperty "imap-elemAt" $ property $-    do SomeVector v <- forAll $ genSomeVector genOrdering-       imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v+  , testPropertyNamed "imap-elemAt" "prop_imapElemAt" prop_imapElemAt -  , testProperty "Ord-Eq-VectorIndex" $ property $-    do i <- forAll $ genFin (knownNat @10)-       j <- forAll $ genFin (knownNat @10)-       (i == j) === (compare i j == EQ)+  , testPropertyNamed "Ord-Eq-VectorIndex" "prop_OrdEqVectorIndex" prop_OrdEqVectorIndex  #if __GLASGOW_HASKELL__ >= 806   -- Test a few different sizes since the types force each test to use a

@@ -4,8 +4,10 @@  import qualified Test.Context import qualified Test.Fin+import qualified Test.FinMap import qualified Test.List import qualified Test.NatRepr+import qualified Test.Some import qualified Test.SymbolRepr import qualified Test.TH import qualified Test.Vector@@ -25,7 +27,9 @@   [ Test.Context.contextTests   , pure Test.List.tests   , Test.Fin.finTests+  , Test.FinMap.finMapTests   , Test.NatRepr.natTests+  , Test.Some.someTests   , Test.SymbolRepr.symbolTests   , Test.TH.thTests   , Test.Vector.vecTests