packages feed

parameterized-utils 2.0 → 2.0.1.0

raw patch · 24 files changed

+901/−279 lines, 24 filesdep +hedgehogdep +tasty-hedgehogdep −QuickCheckdep −tasty-quickcheckdep ~constraintsdep ~hashabledep ~lens

Dependencies added: hedgehog, tasty-hedgehog

Dependencies removed: QuickCheck, tasty-quickcheck

Dependency ranges changed: constraints, hashable, lens, th-abstraction

Files

Changelog.md view
@@ -1,5 +1,39 @@ # Changelog for the `parameterized-utils` package +## 2.0.1 -- *2019 Nov 06*++  * Documentation updates+  * Dependency constraint updates: constraints, lens, th-abstraction, hashable, hashtables, and vector.+  * Now supports building under GHC 8.8.1.+  * Added monadic folds and more traversals:+      * lazy folds: `foldlMF`, `foldrMF`, `foldlMFC`, `foldrMFC`+      * strict folds: `foldlMF'`, `foldrMF'`, `foldlMFC'`, `foldrMFC'`+      * `forF`, `forF_`+      * `forFC`, `forFC_`+      * `lengthF`+  * Added monadic folds, ascending or descending list conversions to `Parameterized.Map`:+      * Added monadic folds: `foldlMWithKey`, `foldrMWithKey`+      * Added ascending or descending list conversions: `toAscList` (equivalent to existing `toList`) and `toDescList`.+      * Added `findWithDefault` to lookup a key or return a default value.+      * Added `traverseMaybeWithKey`.+      * Fixes traverse to do an in-order rather than a pre-order traversal.+  * Added the `Data.Parameterized.All` module for universal quantification/parametricity over a type variable.+  * Additions to `Data.Parameterized.Context`:+      * Added `IndexView` type and `viewIndex` functions.+      * Added `addDiff` function to explicitly describe the (flipped) binary operator for the `Diff` instance of the `Category` class from `Control.Category`.+      * Added `traverseWithIndex_`+  * Added `Data.Parameterized.DataKind` providing the `PairRepr` type with associated `fst` and `snd` functions.+  * Added `TypeAp` to `Data.Parameterized.Classes`+  * Added `runSTNonceGenerator` to `Data.Parameterized.Nonce` for a *global* ST generator.+  * Added a `Hashable` instance for list `Index l x` types.+  * Changes in GADT TH code generator:+      * Added `structuralHashWithSalt` to+      * Fixed off by one bug in output+      * Fixed generation and constructor generation to use constructor type arguments, not type parameters.+  * The `Some` type is now an instance of `FunctorF`, `FoldableF`, and `TraversableF`.+  * Adjusted `structuralShowsPrec` precedence to match GHC derived `Show` instances.+  * The `Data.Parameterized.Nonce.Unsafe` module is now deprecated: clients should switch to `Data.Parameterized.Nonce`.+ ## 2.0 -- *2019 Apr 03*    * Drop support for GHC versions prior to GHC 8.2
parameterized-utils.cabal view
@@ -1,5 +1,5 @@ Name:          parameterized-utils-Version:       2.0+Version:       2.0.1.0 Author:        Galois Inc. Maintainer:    jhendrix@galois.com, kquick@galois.com stability:     stable@@ -11,7 +11,7 @@ category:      Data Structures, Dependent Types Synopsis: Classes and data structures for working with data-kind indexed types Description:-  This packages contains collection classes and type representations+  This package contains collection classes and type representations   used for working with values that have a single parameter.  It's   intended for things like expression libraries where one wishes   to leverage the Haskell type-checker to improve type-safety by encoding@@ -36,24 +36,25 @@  library   build-depends: base >= 4.10 && < 5-               , th-abstraction >=0.1 && <0.3-               , constraints == 0.10.*+               , th-abstraction >=0.3  && <0.4+               , constraints    >=0.10 && <0.12                , containers                , deepseq                , ghc-prim-               , hashable == 1.2.*-               , hashtables == 1.2.*-               , lens == 4.17.*+               , hashable       >=1.2  && <1.4+               , hashtables     ==1.2.*+               , lens           >=4.16 && <4.19                , mtl                , template-haskell                , text-               , vector == 0.12.*+               , vector         ==0.12.*    hs-source-dirs: src    exposed-modules:     Data.Parameterized-    Data.Parameterized.BoolRepr                  +    Data.Parameterized.All+    Data.Parameterized.BoolRepr     Data.Parameterized.Classes     Data.Parameterized.ClassesC     Data.Parameterized.Compose@@ -62,6 +63,7 @@     Data.Parameterized.Context.Unsafe     Data.Parameterized.Ctx     Data.Parameterized.Ctx.Proofs+    Data.Parameterized.DataKind     Data.Parameterized.DecidableEq     Data.Parameterized.HashTable     Data.Parameterized.List@@ -80,7 +82,7 @@     Data.Parameterized.Utils.BinTree     Data.Parameterized.Utils.Endian     Data.Parameterized.Vector-    Data.Parameterized.WithRepr                  +    Data.Parameterized.WithRepr    other-modules:     Data.Parameterized.NatRepr.Internal@@ -106,6 +108,7 @@   build-depends: base                , hashable                , hashtables+               , hedgehog                , ghc-prim                , lens                , mtl@@ -113,5 +116,4 @@                , tasty == 1.2.*                , tasty-ant-xml == 1.1.*                , tasty-hunit >= 0.9 && < 0.11-               , tasty-quickcheck >= 0.8.1 && < 0.11-               , QuickCheck >= 2.7 && < 2.14+               , tasty-hedgehog
+ src/Data/Parameterized/All.hs view
@@ -0,0 +1,68 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.All+-- Copyright        : (c) Galois, Inc 2019+-- Maintainer       : Langston Barrett <langston@galois.com>+-- Description      : Universal quantification, in a datatype+--+-- This module provides 'All', a GADT that encodes universal+-- quantification/parametricity over a type variable.+--+-- The following is an example of a situation in which it might be necessary+-- to use 'All' (though it is a bit contrived):+--+-- @+--   {-# LANGUAGE FlexibleInstances #-}+--   {-# LANGUAGE GADTs #-}+--+--   data F (x :: Bool) where+--     FTrue :: F 'True+--     FFalse :: F 'False+--     FIndeterminate :: F b+--+--   data Value =+--     VAllF (All F)+--+--   class Valuable a where+--     valuation :: a -> Value+--+--   instance Valuable (All F) where+--     valuation = VAllF+--+--   val1 :: Value+--   val1 = valuation (All FIndeterminate)+-- @+--+-- For a less contrived but more complex example, see this blog+-- post: http://comonad.com/reader/2008/rotten-bananas/+------------------------------------------------------------------------++{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}++module Data.Parameterized.All+  ( All(..)+  , allConst+  ) where++import Data.Functor.Const (Const(..))++import Data.Parameterized.Classes+import Data.Parameterized.TraversableF++newtype All (f :: k -> *) = All { getAll :: forall x. f x }++instance FunctorF All where+  fmapF f (All a) = All (f a)++instance FoldableF All where+  foldMapF toMonoid (All x) = toMonoid x++instance ShowF f => Show (All f) where+  show (All fa) = showF fa++instance EqF f => Eq (All f) where+  (All x) == (All y) = eqF x y++allConst :: a -> All (Const a)+allConst a = All (Const a)
src/Data/Parameterized/BoolRepr.hs view
@@ -38,15 +38,13 @@ import           Data.Parameterized.Some  import           Data.Type.Bool-import           Data.Hashable --- | +-- | A Boolean flag data BoolRepr (b :: Bool) where   FalseRepr :: BoolRepr 'False   TrueRepr  :: BoolRepr 'True -  --- | conditional +-- | conditional ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c) ifRepr TrueRepr b _ = b ifRepr FalseRepr _ c = c@@ -56,17 +54,17 @@ notRepr TrueRepr = FalseRepr notRepr FalseRepr = TrueRepr --- | Conjunction +-- | Conjunction (%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b) FalseRepr %&& _ = FalseRepr TrueRepr  %&& a = a infixr 3 %&& --- | Disjunction +-- | Disjunction (%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b) FalseRepr %|| a = a TrueRepr  %|| _ = TrueRepr-infixr 2 %||  +infixr 2 %||  instance Hashable (BoolRepr n) where   hashWithSalt i TrueRepr  = hashWithSalt i True@@ -99,12 +97,11 @@ instance Show (BoolRepr m) where   show FalseRepr = "FalseRepr"   show TrueRepr  = "TrueRepr"-  + instance ShowF BoolRepr  instance HashableF BoolRepr where   hashWithSaltF = hashWithSalt-  ---------------------------------------------------------- -- * Implicit runtime booleans
src/Data/Parameterized/Classes.hs view
@@ -8,6 +8,7 @@ "Data.Functor.Classes" types as they work with any kind @k@, and are not restricted to '*'. -}+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-}@@ -17,6 +18,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} #if MIN_VERSION_base(4,9,0)@@ -44,6 +46,8 @@   , showsF   , HashableF(..)   , CoercibleF(..)+    -- * Type function application constructor+  , TypeAp(..)     -- * Optics generalizations   , IndexF   , IxValueF@@ -53,11 +57,13 @@     -- * KnownRepr   , KnownRepr(..)     -- * Re-exports+  , Data.Hashable.Hashable(..)   , Data.Maybe.isJust   ) where  import Data.Functor.Const import Data.Functor.Compose (Compose(..))+import Data.Kind import Data.Hashable import Data.Maybe (isJust) import Data.Proxy@@ -296,6 +302,29 @@  instance Hashable a => HashableF (Const a) where   hashWithSaltF s (Const x) = hashWithSalt s x++------------------------------------------------------------------------+-- TypeAp++-- | Captures the value obtained from applying a type to a function so+-- that we can use parameterized class instance to provide unparameterized+-- instances for specific types.+--+-- This is the same as `Ap` from @Control.Applicative@, but we introduce+-- our own new type to avoid orphan instances.+newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)++instance TestEquality f => Eq (TypeAp f tp) where+  TypeAp x == TypeAp y = isJust $ testEquality x y++instance OrdF f => Ord (TypeAp f tp) where+  compare (TypeAp x) (TypeAp y) = toOrdering (compareF x y)++instance ShowF f => Show (TypeAp f tp) where+  showsPrec p (TypeAp x) = showsPrecF p x++instance HashableF f => Hashable (TypeAp f tp) where+  hashWithSalt s (TypeAp x) = hashWithSaltF s x  ------------------------------------------------------------------------ -- KnownRepr
src/Data/Parameterized/Compose.hs view
@@ -6,7 +6,8 @@ Utilities for working with "Data.Functor.Compose".  NB: This module contains an orphan instance. It will be included in GHC 8.10,-see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273 and also+https://github.com/haskell-compat/base-orphans/issues/49. -}  {-# LANGUAGE GADTs #-}
src/Data/Parameterized/Context.hs view
@@ -1,17 +1,26 @@---------------------------------------------------------------------------- |--- Module           : Data.Parameterized.Context--- Copyright        : (c) Galois, Inc 2014-2019--- Maintainer       : Joe Hendrix <jhendrix@galois.com>------ This module reexports either "Data.Parameterized.Context.Safe"--- or "Data.Parameterized.Context.Unsafe" depending on the--- the unsafe-operations compile-time flag.------ It also defines some utility typeclasses for transforming--- between curried and uncurried versions of functions over contexts.-------------------------------------------------------------------------+{-|+Module           : Data.Parameterized.Context+Copyright        : (c) Galois, Inc 2014-2019+Maintainer       : Joe Hendrix <jhendrix@galois.com> +This module reexports either "Data.Parameterized.Context.Safe"+or "Data.Parameterized.Context.Unsafe" depending on the+the unsafe-operations compile-time flag.++It also defines some utility typeclasses for transforming+between curried and uncurried versions of functions over contexts.++The 'Assignment' type is isomorphic to the 'Data.Parameterized.List'+type, except 'Assignment's construct lists from the right-hand side,+and instead of using type-level @'[]@-style lists, an 'Assignment' is+indexed by a type-level 'Data.Parameterized.Context.Ctx'. The+implementation of 'Assignment's is also more efficent than+'Data.Parameterized.List' for lists of many elements, as it uses a+balanced binary tree representation rather than a linear-time+list. For a motivating example, see 'Data.Parameterized.List'.++-}+ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-}@@ -52,6 +61,7 @@   , generateSomeM   , fromList   , traverseAndCollect+  , traverseWithIndex_      -- * Context extension and embedding utilities   , CtxEmbedding(..)@@ -86,6 +96,7 @@  import           Control.Applicative (liftA2) import           Control.Lens hiding (Index, (:>), Empty)+import           Data.Functor (void) import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import           GHC.TypeLits (Nat, type (-))@@ -380,6 +391,14 @@   m w traverseAndCollect f =   runCollector . traverseWithIndex (\i x -> Collector (f i x))++-- | Visit each of the elements in an @Assignment@ in order+--   from left to right, executing an action with each.+traverseWithIndex_ :: Applicative m+                   => (forall tp . Index ctx tp -> f tp -> m ())+                   -> Assignment f ctx+                   -> m ()+traverseWithIndex_ f = void . traverseAndCollect f  -------------------------------------------------------------------------------- -- Size and Index values
src/Data/Parameterized/Context/Safe.hs view
@@ -42,6 +42,8 @@ {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeInType #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# OPTIONS_HADDOCK hide #-} module Data.Parameterized.Context.Safe   ( module Data.Parameterized.Ctx     -- * Size@@ -58,6 +60,7 @@     -- * Diff   , Diff   , noDiff+  , addDiff   , extendRight   , appendDiff   , DiffView(..)@@ -77,6 +80,8 @@   , forIndex   , forIndexRange   , intIndex+  , IndexView(..)+  , viewIndex     -- * Assignments   , Assignment   , size@@ -127,6 +132,12 @@   SizeZero :: Size 'EmptyCtx   SizeSucc :: !(Size ctx) -> Size (ctx '::> tp) +-- | Renders as integer literal+instance Show (Size ctx) where+  show = show . sizeInt++instance ShowF Size+ -- | Convert a context size to an 'Int'. sizeInt :: Size ctx -> Int sizeInt SizeZero = 0@@ -180,10 +191,16 @@   DiffHere :: Diff ctx ctx   DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp) --- | The identity difference.+-- | The identity difference. Identity element of 'Category' instance. noDiff :: Diff l l noDiff = DiffHere +-- | The addition of differences. Flipped binary operation+-- of 'Category' instance.+addDiff :: Diff a b -> Diff b c -> Diff a c+addDiff x DiffHere = x+addDiff x (DiffThere y) = DiffThere (addDiff x y)+ -- | Extend the difference to a sub-context of the right side. extendRight :: Diff l r -> Diff l (r '::> tp) extendRight diff = DiffThere diff@@ -192,13 +209,10 @@ appendDiff SizeZero = DiffHere appendDiff (SizeSucc sz) = DiffThere (appendDiff sz) -composeDiff :: Diff a b -> Diff b c -> Diff a c-composeDiff x DiffHere = x-composeDiff x (DiffThere y) = DiffThere (composeDiff x y)-+-- | Implemented with 'noDiff' and 'addDiff' instance Cat.Category Diff where   id = DiffHere-  d1 . d2 = composeDiff d2 d1+  d1 . d2 = addDiff d2 d1  -- | Extend the size by a given difference. extSize :: Size l -> Diff l r -> Size r@@ -364,10 +378,27 @@ intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) intIndex n sz = listToMaybe $ drop n $ indexList sz +-- | Renders as integer literal instance Show (Index ctx tp) where    show = show . indexVal  instance ShowF (Index ctx)++-- | View of indexes as pointing to the last element in the+-- index range or pointing to an earlier element in a smaller+-- range.+data IndexView ctx tp where+  IndexViewLast :: Size  ctx   -> IndexView (ctx '::> t) t+  IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t++instance ShowF (IndexView ctx)+deriving instance Show (IndexView ctx tp)++-- | Project an index+viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp+viewIndex _ (IndexHere sz) = IndexViewLast sz+viewIndex _ (IndexThere i) = IndexViewInit i+-- NB: the unused size parameter is needed in the Unsafe module  ------------------------------------------------------------------------ -- Assignment
src/Data/Parameterized/Context/Unsafe.hs view
@@ -13,7 +13,9 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeInType #-}+{-# OPTIONS_HADDOCK hide #-} module Data.Parameterized.Context.Unsafe   ( module Data.Parameterized.Ctx   , KnownContext(..)@@ -30,6 +32,7 @@     -- * Diff   , Diff   , noDiff+  , addDiff   , extendRight   , appendDiff   , DiffView(..)@@ -49,6 +52,8 @@   , forIndex   , forIndexRange   , intIndex+  , IndexView(..)+  , viewIndex     -- ** IndexRange   , IndexRange   , allRange@@ -131,6 +136,8 @@ instance Show (Size ctx) where   show (Size i) = show i +instance ShowF Size+ -- | A context that can be determined statically at compiler time. class KnownContext (ctx :: Ctx k) where   knownSize :: Size ctx@@ -151,10 +158,17 @@  type role Diff nominal nominal --- | The identity difference.+-- | The identity difference. Identity element of 'Category' instance. noDiff :: Diff l l noDiff = Diff 0+{-# INLINE noDiff #-} +-- | The addition of differences. Flipped binary operation+-- of 'Category' instance.+addDiff :: Diff a b -> Diff b c -> Diff a c+addDiff (Diff x) (Diff y) = Diff (x + y)+{-# INLINE addDiff #-}+ -- | Extend the difference to a sub-context of the right side. extendRight :: Diff l r -> Diff l (r '::> tp) extendRight (Diff i) = Diff (i+1)@@ -162,9 +176,10 @@ appendDiff :: Size r -> Diff l (l <+> r) appendDiff (Size r) = Diff r +-- | Implemented with 'noDiff' and 'addDiff' instance Cat.Category Diff where-  id = Diff 0-  Diff j . Diff i = Diff (i + j)+  id = noDiff+  j . i = addDiff i j  -- | Extend the size by a given difference. extSize :: Size l -> Diff l r -> Size r@@ -292,6 +307,24 @@    show = show . indexVal  instance ShowF (Index ctx)++-- | View of indexes as pointing to the last element in the+-- index range or pointing to an earlier element in a smaller+-- range.+data IndexView ctx tp where+  IndexViewLast :: !(Size  ctx  ) -> IndexView (ctx '::> t) t+  IndexViewInit :: !(Index ctx t) -> IndexView (ctx '::> u) t++deriving instance Show (IndexView ctx tp)+instance ShowF (IndexView ctx)++-- | Project an index+viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp+viewIndex (Size sz) (Index i)+  | sz' == i  = unsafeCoerce (IndexViewLast (Size sz'))+  | otherwise = unsafeCoerce (IndexViewInit (Index i))+  where+    sz' = sz-1  ------------------------------------------------------------------------ -- IndexRange
src/Data/Parameterized/Ctx.hs view
@@ -5,6 +5,10 @@  This module defines type-level lists used for representing the type of variables in a context.++A 'Ctx' is never intended to be manipulated at the value level; it is+used purely as a type-level list, just like @'[]@. To see how it is+used, see the module header for "Data.Parameterized.Context". -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}
+ src/Data/Parameterized/DataKind.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}++module Data.Parameterized.DataKind+  ( PairRepr(..), Fst, Snd, fst, snd+  ) where++import           Data.Parameterized.Classes+import qualified Data.Parameterized.TH.GADT as TH++import           Prelude hiding ( fst, snd )++data PairRepr (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)) where+  PairRepr :: f a -> g b -> PairRepr f g '(a, b)++type family Fst (pair :: (k1, k2)) where+  Fst '(a, _) = a+type family Snd (pair :: (k1, k2)) where+  Snd '(_, b) = b++fst :: PairRepr f g p -> f (Fst p)+fst (PairRepr a _) = a++snd :: PairRepr f g p -> g (Snd p)+snd (PairRepr _ b) = b++$(return [])++instance ( ShowF f, ShowF g ) => Show (PairRepr f g p) where+  show (PairRepr a b) = showChar '(' . showsF a . showChar ',' . showsF b $ ")"+instance ( ShowF f, ShowF g ) => ShowF (PairRepr f g)++deriving instance ( Eq (f a), Eq (g b) ) => Eq (PairRepr f g '(a, b))+instance ( TestEquality f, TestEquality g ) => TestEquality (PairRepr f g) where+  testEquality =+    $(TH.structuralTypeEquality [t|PairRepr|]+      [+        ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|testEquality|] )+      , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|testEquality|] )+      ])++deriving instance ( Ord (f a), Ord (g b) ) => Ord (PairRepr f g '(a, b))+instance ( OrdF f, OrdF g ) => OrdF (PairRepr f g) where+  compareF =+    $(TH.structuralTypeOrd [t|PairRepr|]+      [ ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|compareF|] )+      , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|compareF|] )+      ])
src/Data/Parameterized/List.hs view
@@ -8,8 +8,117 @@ second is a list of types with kind @k@ that provide the indices for the values in the list. -This type is closely related to the @Context@ type in-@Data.Parameterized.Context@.+This type is closely related to the+'Data.Parameterized.Context.Assignment' type in+"Data.Parameterized.Context".++= Motivating example - the 'Data.Parameterized.List.List' type++For this example, we need the following extensions:++@+\{\-\# LANGUAGE DataKinds \#\-\}+\{\-\# LANGUAGE GADTs \#\-\}+\{\-\# LANGUAGE KindSignatures \#\-\}+\{\-\# LANGUAGE TypeOperators \#\-\}+@++We also require the following imports:++@+import Data.Parameterized+import Data.Parameterized.List+import GHC.TypeLits+@++Suppose we have a bitvector type:++@+data BitVector (w :: Nat) :: * where+  BV :: NatRepr w -> Integer -> BitVector w+@++This type contains a 'Data.Parameterized.NatRepr.NatRepr', a value-level+representative of the vector width, and an 'Integer', containing the+actual value of the bitvector. We can create values of this type as+follows:++@+BV (knownNat @8) 0xAB+@++We can also create a smart constructor to handle the+'Data.Parameterized.NatRepr.NatRepr' automatically, when the width is known+from the type context:++@+bitVector :: KnownNat w => Integer -> BitVector w+bitVector x = BV knownNat x+@++Note that this does not check that the value can be represented in the+given number of bits; that is not important for this example.++If we wish to construct a list of @BitVector@s of a particular length,+we can do:++@+[bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8+@++However, what if we wish to construct a list of 'BitVector's of+different lengths? We could try:++@+[bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]+@++However, this gives us an error:++@+\<interactive\>:3:33: error:+    • Couldn't match type ‘16’ with ‘8’+      Expected type: BitVector 8+        Actual type: BitVector 16+    • In the expression: bitVector 0x1234 :: BitVector 16+      In the expression:+        [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]+      In an equation for ‘it’:+          it+            = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]+@++A vanilla Haskell list cannot contain two elements of different types,+and even though the two elements here are both @BitVector@s, they do+not have the same type! One solution is to use the+'Data.Parameterized.Some.Some' type:++@+[Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]+@++The type of the above expression is @[Some BitVector]@, which may be+perfectly acceptable. However, there is nothing in this type that+tells us what the widths of the bitvectors are, or what the length of+the overall list is. If we want to actually track that information on+the type level, we can use the 'List' type from this module.++@+(bitVector 0xAB :: BitVector 8) :< (bitVector 0x1234 :: BitVector 16) :< Nil+@++The type of the above expression is @List BitVector '[8, 16]@ -- That+is, a two-element list of @BitVector@s, where the first element has+width 8 and the second has width 16.++== Summary++In general, if we have a type constructor @Foo@ of kind @k -> *@ (in+our example, @Foo@ is just @BitVector@, and we want to create a list+of @Foo@s where the parameter @k@ varies, /and/ we wish to keep track+of what each value of @k@ is inside the list at compile time, we can+use the 'Data.Parameterized.List.List' type for this purpose.+ -} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-}@@ -40,10 +149,10 @@   ) where  import qualified Control.Lens as Lens-import Prelude hiding ((!!))+import           Prelude hiding ((!!)) -import Data.Parameterized.Classes-import Data.Parameterized.TraversableFC+import           Data.Parameterized.Classes+import           Data.Parameterized.TraversableFC  -- | Parameterized list of elements. data List :: (k -> *) -> [k] -> * where@@ -137,6 +246,9 @@         go i (IndexThere x) = seq j $ go j x           where j = i+1 +instance Hashable (Index l x) where+  hashWithSalt s i = s `hashWithSalt` (indexValue i)+ -- | Index 0 index0 :: Index (x:r) x index0 = IndexHere@@ -172,7 +284,7 @@     x :< rest -> x :< update rest th upd  -- | Provides a lens for manipulating the element at the given index.-indexed :: Index l x -> Lens.Simple Lens.Lens (List f l) (f x)+indexed :: Index l x -> Lens.Lens' (List f l) (f x) indexed IndexHere      f (x :< rest) = (:< rest) <$> f x indexed (IndexThere i) f (x :< rest) = (x :<) <$> indexed i f rest
src/Data/Parameterized/Map.hs view
@@ -32,6 +32,7 @@     -- * Query   , null   , lookup+  , findWithDefault   , member   , notMember   , size@@ -40,6 +41,8 @@   , elems   , fromList   , toList+  , toAscList+  , toDescList   , fromKeys   , fromKeysM    -- * Filter@@ -53,6 +56,8 @@   , foldrWithKey   , foldrWithKey'   , foldMapWithKey+  , foldlMWithKey+  , foldrMWithKey     -- * Traversals   , map   , mapWithKey@@ -60,6 +65,7 @@   , mapMaybeWithKey   , traverseWithKey   , traverseWithKey_+  , traverseMaybeWithKey     -- * Complex interface.   , UpdateRequest(..)   , Updated(..)@@ -199,7 +205,8 @@ -- | Traverse elements in a map traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g) traverse _ Tip = pure Tip-traverse f (Bin sx kx x l r) = Bin sx kx <$> f x <*> traverse f l <*> traverse f r+traverse f (Bin sx kx x l r) =+  (\l' x' r' -> Bin sx kx x' l' r') <$> traverse f l <*> f x <*> traverse f r  -- | Traverse elements in a map traverseWithKey@@ -209,7 +216,7 @@   -> m (MapF ktp g) traverseWithKey _ Tip = pure Tip traverseWithKey f (Bin sx kx x l r) =-   Bin sx kx <$> f kx x <*> traverseWithKey f l <*> traverseWithKey f r+   (\l' x' r' -> Bin sx kx x' l' r') <$> traverseWithKey f l <*> f kx x <*> traverseWithKey f r  -- | Traverse elements in a map without returning result. traverseWithKey_@@ -217,9 +224,23 @@   => (forall tp . ktp tp -> f tp -> m ())   -> MapF ktp f   -> m ()-traverseWithKey_ _ Tip = pure ()-traverseWithKey_ f (Bin _ kx x l r) = f kx x *> traverseWithKey_ f l *> traverseWithKey_ f r+traverseWithKey_ = \f -> foldrWithKey (\k v r -> f k v *> r) (pure ())+{-# INLINABLE traverseWithKey_ #-} +-- | Traverse keys\/values and collect the 'Just' results.+traverseMaybeWithKey :: Applicative f+                     => (forall tp . k tp -> a tp -> f (Maybe (b tp)))+                     -> MapF k a -> f (MapF k b)+traverseMaybeWithKey _ Tip = pure Tip+traverseMaybeWithKey f (Bin _ kx x Tip Tip) = maybe Tip (\x' -> Bin 1 kx x' Tip Tip) <$> f kx x+traverseMaybeWithKey f (Bin _ kx x l r) =+    liftA3 combine (traverseMaybeWithKey f l) (f kx x) (traverseMaybeWithKey f r)+  where+    combine l' mx r' = seq l' $ seq r' $+      case mx of+        Just x' -> Bin.link (Pair kx x') l' r'+        Nothing -> Bin.merge l' r'+{-# INLINABLE traverseMaybeWithKey #-}  type instance IndexF   (MapF k v) = k type instance IxValueF (MapF k v) = v@@ -248,6 +269,20 @@         EQF -> Just x {-# INLINABLE lookup #-} +-- | @findWithDefault d k m@ returns the value bound to @k@ in the map @m@, or @d@+-- if @k@ is not bound in the map.+findWithDefault :: OrdF k => a tp -> k tp -> MapF k a -> a tp+findWithDefault = \def k -> seq k (go def k)+  where+    go :: OrdF k => a tp -> k tp -> MapF k a -> a tp+    go d _ Tip = d+    go d k (Bin _ kx x l r) =+      case compareF k kx of+        LTF -> go d k l+        GTF -> go d k r+        EQF -> x+{-# INLINABLE findWithDefault #-}+ -- | Return true if key is bound in map. member :: OrdF k => k tp -> MapF k a -> Bool member k0 = seq k0 (go k0)@@ -308,9 +343,7 @@ foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b foldrWithKey _ z Tip = z foldrWithKey f z (Bin _ kx x l r) =-  let rz = foldrWithKey f z r-      kz = f kx x rz-   in foldrWithKey f kz l+  foldrWithKey f (f kx x (foldrWithKey f z r)) l  -- | Perform a strict right fold with the key also provided. foldrWithKey' :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b@@ -325,6 +358,15 @@ foldMapWithKey _ Tip = mempty foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r +-- | A monadic left-to-right fold over keys and values in the map.+foldlMWithKey :: Monad m => (forall s . b -> k s -> a s -> m b) -> b -> MapF k a -> m b+foldlMWithKey f z0 m = foldrWithKey (\k a r z ->  f z k a >>= r) pure m z0++-- | A monadic right-to-left fold over keys and values in the map.+foldrMWithKey :: Monad m => (forall s . k s -> a s -> b -> m b) -> b -> MapF k a -> m b+foldrMWithKey f z0 m = foldlWithKey (\r k a z ->  f k a z >>= r) pure m z0++-- | Pretty print keys and values in map. showMap :: (forall tp . ktp tp -> String)         -> (forall tp . rtp tp -> String)         -> MapF ktp rtp@@ -406,7 +448,10 @@ {-# INLINABLE delete #-} {-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-} --- | Union two sets+-- | 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 #-}@@ -481,8 +526,17 @@ fromList :: OrdF k => [Pair k a] -> MapF k a fromList = foldl' (\m (Pair k a) -> insert k a m) Data.Parameterized.Map.empty +-- | Return list of key-values pairs in map in ascending order.+toAscList :: MapF k a -> [Pair k a]+toAscList = foldrWithKey (\k x l -> Pair k x : l) []++-- | Return list of key-values pairs in map in descending order.+toDescList :: MapF k a -> [Pair k a]+toDescList = foldlWithKey (\l k x -> Pair k x : l) []++-- | Return list of key-values pairs in map. toList :: MapF k a -> [Pair k a]-toList = foldrWithKey (\k x m -> Pair k x : m) []+toList = toAscList  -- | Generate a map from a foldable collection of keys and a -- function from keys to values.@@ -519,6 +573,23 @@ filterLtMaybe (JustS k) m = filterLt k m  -- | 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 must not introduce 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. mergeWithKeyM :: forall k a b c m                . (Applicative m, OrdF k)               => (forall tp . k tp -> a tp -> b tp -> m (Maybe (c tp)))@@ -579,7 +650,7 @@   --- Helper function for 'mergeWithKey'. The @'trimLookupLo' lk hk t@ performs both+-- 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
src/Data/Parameterized/Nonce.hs view
@@ -39,6 +39,7 @@   , newIONonceGenerator   , withIONonceGenerator   , withSTNonceGenerator+  , runSTNonceGenerator     -- * Global nonce generator   , withGlobalSTNonceGenerator   , GlobalNonceGenerator@@ -103,12 +104,21 @@ newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t))) newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0) +-- | This combines `runST` and `newSTNonceGenerator` to create a nonce+-- generator that shares the same phantom type parameter as the @ST@ monad.+--+-- This can be used to reduce the number of type parameters when we know a+-- ST computation only needs a single `NonceGenerator`.+runSTNonceGenerator :: (forall s . NonceGenerator (ST s) s -> ST s a)+                    -> a+runSTNonceGenerator f = runST $ f . STNG =<< newSTRef 0+ -- | Create a new nonce generator in the 'ST' monad. newIONonceGenerator :: IO (Some (NonceGenerator IO)) newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0)  -- | Run a 'ST' computation with a new nonce generator in the 'ST' monad.-withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> (ST t) r) -> ST t r+withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> ST t r) -> ST t r withSTNonceGenerator f = do   Some r <- newSTNonceGenerator   f r
src/Data/Parameterized/Nonce/Unsafe.hs view
@@ -1,6 +1,6 @@ ------------------------------------------------------------------------ -- |--- Module           : Data.Parameterized.NonceGenerator+-- Module           : Data.Parameterized.Nonce.Unsafe -- Description      : A counter in the ST monad. -- Copyright        : (c) Galois, Inc 2014 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>@@ -19,28 +19,16 @@ -- Nonces from different origins would allow users to build 'unsafeCoerce' -- via the 'testEquality' function. ----- A somewhat safer API would be to brand the generated Nonces with the--- state type variable of the NonceGenerator whence they came, and to only--- provide NonceGenerators via a Rank-2 continuation-passing API, similar to--- 'runST'. This would (via a meta-argument involving parametricity)--- help to prevent nonces of different origin from being compared.--- However, this would force us to push the 'ST' type brand into a significant--- number of other structures and APIs.------ Another alternative would be to use 'unsafePerformIO' magic to make--- a global nonce generator, and make that the only way to generate nonces.--- It is not clear that this is actually an improvement from a type safety--- point of view, but an argument could be made.------ For now, be careful using Nonces, and ensure that you do not mix--- Nonces from different NonceGenerators.-------------------------------------------------------------------------+-- This module is deprecated, and should not be used in new code.+-- Clients of this module should migrate to use "Data.Parameterized.Nonce".+------------------------------------------------------------------------- {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE Unsafe #-} module Data.Parameterized.Nonce.Unsafe+  {-# DEPRECATED "Migrate to use Data.Parameterized.Nonce instead, this module will be removed soon." #-}   ( NonceGenerator   , newNonceGenerator   , freshNonce
src/Data/Parameterized/Pair.hs view
@@ -1,5 +1,5 @@ {-|-nDescription : A 2-tuple with identically parameterized elements+Description : A 2-tuple with identically parameterized elements Copyright   : (c) Galois, Inc 2017-2019  This module defines a 2-tuple where both elements are parameterized over the
src/Data/Parameterized/Peano.hs view
@@ -45,7 +45,7 @@      Peano      , Z , S -     -- * Basic arithmetic +     -- * Basic arithmetic      , Plus, Minus, Mul,  Max, Min      , plusP, minusP, mulP, maxP, minP      , zeroP, succP, predP@@ -53,7 +53,6 @@      -- * Counting      , Repeat, CtxSizeP      , repeatP, ctxSizeP-           -- * Comparisons      , Le, Lt, Gt, Ge      , leP, ltP, gtP, geP@@ -64,7 +63,7 @@      , PeanoView(..), peanoView, viewRepr       -- * 'Some Peano'-     , mkPeanoRepr, peanoValue     +     , mkPeanoRepr, peanoValue      , somePeano      , maxPeano      , minPeano@@ -88,7 +87,6 @@ import           Data.Parameterized.Some import           Data.Parameterized.Context -import           Data.Hashable import           Data.Word  #ifdef UNSAFE_OPS@@ -185,7 +183,7 @@ peanoValue ZRepr     = 0 peanoValue (SRepr m) = 1 + peanoValue m #endif-                                    + -- | When we have optimized the runtime representation, -- we need to have a "view" that decomposes the representation -- into the standard form.@@ -227,13 +225,13 @@   testEquality (PeanoRepr m) (PeanoRepr n)     | m == n = Just (unsafeCoerce Refl)     | otherwise = Nothing-#else +#else   testEquality ZRepr ZRepr = Just Refl   testEquality (SRepr m1) (SRepr m2)     | Just Refl <- testEquality m1 m2     = Just Refl   testEquality _ _ = Nothing-  + #endif  instance DecidableEq PeanoRepr where@@ -418,7 +416,7 @@ mkPeanoRepr 0 = Some ZRepr mkPeanoRepr n = case mkPeanoRepr (n - 1) of                  Some mr -> Some (SRepr mr)-#endif                 +#endif  -- | Turn an @Integral@ value into a 'PeanoRepr'.  Returns @Nothing@ --   if the given value is negative.@@ -468,7 +466,7 @@ -- | Minus distributes over plus -- minusPlusAxiom :: forall n t t'.-  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->    +  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->   Minus n (Plus t' t) :~: Minus (Minus n t') t #ifdef UNSAFE_OPS minusPlusAxiom _n _t _t' = unsafeCoerce Refl
src/Data/Parameterized/Some.hs view
@@ -21,6 +21,7 @@  import Data.Hashable import Data.Parameterized.Classes+import Data.Parameterized.TraversableF   data Some (f:: k -> *) = forall x . Some (f x)@@ -58,3 +59,7 @@ -- | Modify the inner value. traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m () traverseSome_ f (Some x) = (\_ -> ()) `fmap` f x++instance FunctorF     Some where fmapF     = mapSome+instance FoldableF    Some where foldMapF  = foldMapFDefault+instance TraversableF Some where traverseF = traverseSome
src/Data/Parameterized/TH/GADT.hs view
@@ -23,6 +23,7 @@   , structuralTraversal   , structuralShowsPrec   , structuralHash+  , structuralHashWithSalt   , PolyEq(..)     -- * Template haskell utilities that may be useful in other contexts.   , DataD@@ -91,9 +92,8 @@     False -> return False matchTypePat _ AnyType _ = return True matchTypePat tps (DataArg i) tp-  | i < 0 || i > length tps = error $ "Illegal type pattern index " ++ show i-  | otherwise = do-    return $ stripSigT (tps !! i) == tp+  | i < 0 || i >= length tps = error ("Type pattern index " ++ show i ++ " out of bounds")+  | otherwise = return (stripSigT (tps !! i) == tp)   where     -- th-abstraction can annotate type parameters with their kinds,     -- we ignore these for matching@@ -104,11 +104,17 @@   return (tp' == tp) matchTypePat _ _ _ = return False +-- | The dataParamTypes function returns the list of Type arguments+-- for the constructor.  For example, if passed the DatatypeInfo for a+-- @newtype Id a = MkId a@ then this would return @['SigT' ('VarT' a)+-- 'StarT']@.  Note that there may be type *variables* not referenced+-- in the returned array; this simply returns the type *arguments*. dataParamTypes :: DatatypeInfo -> [Type]-dataParamTypes = datatypeVars+dataParamTypes = datatypeInstTypes+ -- see th-abstraction 'dataTypeVars' for the type variables if needed  -- | Find value associated with first pattern that matches given pat if any.-assocTypePats :: [Type] -> [(TypePat,v)] -> Type -> Q (Maybe v)+assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v) assocTypePats _ [] _ = return Nothing assocTypePats dTypes ((p,v):pats) tp = do   r <- matchTypePat dTypes p tp@@ -141,7 +147,7 @@  matchEqArguments :: [Type]                     -- ^ Types bound by data arguments.-                  -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+                 -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments                  -> Name                      -- ^ Name of constructor.                  -> Set Name@@ -193,7 +199,10 @@       -> Bool -- ^ wildcard case required       -> ExpQ mkEqF d pats con =-  let dVars = datatypeVars d+  let dVars = dataParamTypes d  -- the type arguments for the constructor+      -- bnd is the list of type arguments for this datatype.  Since+      -- this is Functor equality, ignore the final type since this is+      -- a higher-kinded equality.       bnd | null dVars = Set.empty           | otherwise  = typeVars (init dVars)   in mkSimpleEqF dVars bnd pats con@@ -346,16 +355,19 @@        -> Maybe ExpQ -- ^ optional right constructr index        -> [Name]        -> Q [MatchQ]-mkOrdF d pats = mkSimpleOrdF (datatypeVars d) pats+mkOrdF d pats = mkSimpleOrdF (datatypeInstTypes d) pats --- | @recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@.-recurseArg :: (Type -> Q (Maybe ExpQ))-           -> ExpQ -- ^ Function to apply-           -> ExpQ-           -> Type-           -> Q (Maybe Exp)-recurseArg m f v tp = do-  mr <- m tp+-- | @genTraverseOfType f var tp@ applies @f@ to @var@ where @var@ has type @tp@.+genTraverseOfType :: [Type]+                    -- ^ Argument types for the data declaration.+                 -> [(TypePat, ExpQ)]+                    -- ^ Patterrns the user provided for overriding type lookup.+                  -> ExpQ -- ^ Function to apply+                  -> ExpQ -- ^ Expression denoting value of this constructor field.+                  -> Type -- ^ Type bound for this constructor field.+                  -> Q (Maybe Exp)+genTraverseOfType dataArgs pats f v tp = do+  mr <- assocTypePats dataArgs pats tp   case mr of     Just g ->  Just <$> [| $(g) $(f) $(v) |]     Nothing ->@@ -364,16 +376,18 @@         AppT (VarT _) _ -> Just <$> [| $(f) $(v) |]         _ -> return Nothing --- | @traverseAppMatch f c@ builds a case statement that matches a term with+-- | @traverseAppMatch patMatch cexp @ builds a case statement that matches a term with -- the constructor @c@ and applies @f@ to each argument.-traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- ^ Pattern match function-                 -> ExpQ -- ^ Function to apply to each argument recursively.+traverseAppMatch :: [Type]+                    -- ^ Argument types for the data declaration.+                 -> [(TypePat, ExpQ)]+                    -- ^ Patterrns the user provided for overriding type lookup.+                 -> ExpQ -- ^ Function @f@ given to `traverse`                  -> ConstructorInfo -- ^ Constructor to match.-                 -> MatchQ -- ^ Match expression that-traverseAppMatch pats fv c0 = do+                 -> MatchQ+traverseAppMatch dataArgs pats fv c0 = do   (pat,patArgs) <- conPat c0 "p"-  exprs <- zipWithM (recurseArg pats fv) (varE <$> patArgs) (constructorFields c0)-+  exprs <- zipWithM (genTraverseOfType dataArgs pats fv) (varE <$> patArgs) (constructorFields c0)   let mkRes :: ExpQ -> [(Name, Maybe Exp)] -> ExpQ       mkRes e [] = e       mkRes e ((v,Nothing):r) =@@ -405,28 +419,56 @@   a <- newName "a"   lamE [varP f, varP a] $       caseE (varE a)-      (traverseAppMatch (assocTypePats (datatypeVars d) pats0) (varE f) <$> datatypeCons d)+      (traverseAppMatch (datatypeInstTypes d) pats0 (varE f) <$> datatypeCons d) -asTypeCon :: Monad m => String -> Type -> m Name+asTypeCon :: String -> Type -> Q Name asTypeCon _ (ConT nm) = return nm-asTypeCon fn _ = fail $ fn ++ " expected type constructor."+asTypeCon fn _ = fail (fn ++ " expected type constructor.")  -- | @structuralHash tp@ generates a function with the type -- @Int -> tp -> Int@ that hashes type.+--+-- All arguments use `hashable`, and `structuralHashWithSalt` can be+-- used instead as it allows user-definable patterns to be used at+-- specific types. structuralHash :: TypeQ -> ExpQ-structuralHash tpq = do+structuralHash tpq = structuralHashWithSalt tpq []+{-# DEPRECATED structuralHash "Use structuralHashWithSalt" #-}++-- | @structuralHashWithSalt tp@ generates a function with the type+-- @Int -> tp -> Int@ that hashes type.+--+-- The second arguments is for generating user-defined patterns to replace+-- `hashWithSalt` for specific types.+structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ+structuralHashWithSalt tpq pats = do   d <- reifyDatatype =<< asTypeCon "structuralHash" =<< tpq   s <- newName "s"   a <- newName "a"   lamE [varP s, varP a] $-    caseE (varE a) (zipWith (matchHashCtor (varE s)) [0..] (datatypeCons d))+    caseE (varE a) (zipWith (matchHashCtor d pats (varE s)) [0..] (datatypeCons d)) -matchHashCtor :: ExpQ -> Integer  -> ConstructorInfo -> MatchQ-matchHashCtor s0 i c = do+-- | This matches one of the constructors in a datatype when generating+-- a `hashWithSalt` function.+matchHashCtor :: DatatypeInfo+                 -- ^ Data declaration of type we are hashing.+              -> [(TypePat, ExpQ)]+                 -- ^ User provide type patterns+              -> ExpQ -- ^ Initial salt expression+              -> Integer -- ^ Index of constructor+              -> ConstructorInfo -- ^ Constructor information+              -> MatchQ+matchHashCtor d pats s0 i c = do   (pat,vars) <- conPat c "x"-  let args = [| $(litE (IntegerL i)) :: Int |] : (varE <$> vars)-  let go s e = [| hashWithSalt $(s) $(e) |]-  let rhs = foldl go s0 args+  let go s (e, tp) = do+        mr <- assocTypePats (datatypeInstTypes d) pats tp+        case mr of+          Just f -> do+            [| $(f) $(s) $(e) |]+          Nothing ->+            [| hashWithSalt $(s) $(e) |]+  let s1 = [| hashWithSalt $(s0) ($(litE (IntegerL i)) :: Int) |]+  let rhs = foldl go s1 (zip (varE <$> vars) (constructorFields c))   match (pure pat) (normalB rhs) []  -- | @structuralShow tp@ generates a function with the type@@ -443,10 +485,10 @@ showCon p nm n = do   vars <- newNames "x" n   let pat = ConP nm (VarP <$> vars)-  let go s e = [| $(s) . showChar ' ' . showsPrec 10 $(varE e) |]+  let go s e = [| $(s) . showChar ' ' . showsPrec 11 $(varE e) |]   let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |]   let rhs | null vars = ctor-          | otherwise = [| showParen ($(p) >= 10) $(foldl go ctor vars) |]+          | otherwise = [| showParen ($(p) >= 11) $(foldl go ctor vars) |]   match (pure pat) (normalB rhs) []  matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ
src/Data/Parameterized/TraversableF.hs view
@@ -16,12 +16,19 @@ module Data.Parameterized.TraversableF   ( FunctorF(..)   , FoldableF(..)+  , foldlMF+  , foldlMF'+  , foldrMF+  , foldrMF'   , TraversableF(..)   , traverseF_+  , forF_+  , forF   , fmapFDefault   , foldMapFDefault   , allF   , anyF+  , lengthF   ) where  import Control.Applicative@@ -82,6 +89,26 @@   toListF :: (forall tp . f tp -> a) -> t f -> [a]   toListF f t = build (\c n -> foldrF (\e v -> c (f e) v) n t) +-- | Monadic fold over the elements of a structure from left to right.+foldlMF :: (FoldableF t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f -> m b+foldlMF f z0 xs = foldrF f' return xs z0+  where f' x k z = f z x >>= k++-- | Monadic strict fold over the elements of a structure from left to right.+foldlMF' :: (FoldableF t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f -> m b+foldlMF' f z0 xs = seq z0 (foldrF f' return xs z0)+  where f' x k z = f z x >>= \r -> seq r (k r)++-- | Monadic fold over the elements of a structure from right to left.+foldrMF :: (FoldableF t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f -> m b+foldrMF f z0 xs = foldlF f' return xs z0+  where f' k x z = f x z >>= k++-- | Monadic strict fold over the elements of a structure from right to left.+foldrMF' :: (FoldableF t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f -> m b+foldrMF' f z0 xs = seq z0 $ foldlF f' return xs z0+  where f' k x z = f x z >>= \r -> seq r (k r)+ -- | Return 'True' if all values satisfy the predicate. allF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool allF p = getAll #. foldMapF (All #. p)@@ -90,6 +117,10 @@ anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool anyF p = getAny #. foldMapF (Any #. p) +-- | Return number of elements that we fold over.+lengthF :: FoldableF t => t f -> Int+lengthF = foldrF (const (+1)) 0+ instance FoldableF (Const x) where   foldMapF _ _ = mempty @@ -105,6 +136,11 @@ instance TraversableF (Const x) where   traverseF _ (Const x) = pure (Const x) +-- | Flipped 'traverseF'+forF :: (TraversableF t, Applicative m) => t e -> (forall s . e s -> m (f s)) -> m (t f)+forF f x = traverseF x f+{-# INLINE forF #-}+ -- | This function may be used as a value for `fmapF` in a `FunctorF` -- instance. fmapFDefault :: TraversableF t => (forall s . e s -> f s) -> t e -> t f@@ -120,6 +156,13 @@ -- these actions from left to right, and ignore the results. traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f () traverseF_ f = foldrF (\e r -> f e *> r) (pure ())+++-- | Map each element of a structure to an action, evaluate+-- these actions from left to right, and ignore the results.+forF_ :: (FoldableF t, Applicative m) => t f -> (forall x. f x -> m a) -> m ()+forF_ v f = traverseF_ f v+{-# INLINE forF_ #-}  ------------------------------------------------------------------------ -- TraversableF (Compose s t)
src/Data/Parameterized/TraversableFC.hs view
@@ -19,9 +19,15 @@   , HashableFC(..)   , FunctorFC(..)   , FoldableFC(..)+  , foldlMFC+  , foldlMFC'+  , foldrMFC+  , foldrMFC'   , TraversableFC(..)   , traverseFC_   , forMFC_+  , forFC_+  , forFC   , fmapFCDefault   , foldMapFCDefault   , allFC@@ -117,6 +123,26 @@   toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])   toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t) +-- | Monadic fold over the elements of a structure from left to right.+foldlMFC :: (FoldableFC t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f c -> m b+foldlMFC f z0 xs = foldrFC f' return xs z0+  where f' x k z = f z x >>= k++-- | Monadic strict fold over the elements of a structure from left to right.+foldlMFC' :: (FoldableFC t, Monad m) => (forall x . b -> f x -> m b) -> b -> t f c -> m b+foldlMFC' f z0 xs = seq z0 $ foldrFC f' return xs z0+  where f' x k z = f z x >>= \r -> seq r (k r)++-- | Monadic fold over the elements of a structure from right to left.+foldrMFC :: (FoldableFC t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f c -> m b+foldrMFC f z0 xs = foldlFC f' return xs z0+  where f' k x z = f x z >>= k++-- | Monadic strict fold over the elements of a structure from right to left.+foldrMFC' :: (FoldableFC t, Monad m) => (forall x . f x -> b -> m b) -> b -> t f c -> m b+foldrMFC' f z0 xs = seq z0 (foldlFC f' return xs z0)+  where f' k x z = f x z >>= \r -> seq r (k r)+ -- | Return 'True' if all values satisfy predicate. allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool) allFC p = getAll #. foldMapFC (All #. p)@@ -125,7 +151,7 @@ anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool) anyFC p = getAny #. foldMapFC (Any #. p) --- | Return number of elements in list.+-- | Return number of elements that we fold over. lengthFC :: FoldableFC t => t f x -> Int lengthFC = foldrFC (const (+1)) 0 @@ -160,3 +186,17 @@ forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m () forMFC_ v f = traverseFC_ f v {-# INLINE forMFC_ #-}+{-# DEPRECATED forMFC_ "Use forFC_" #-}++-- | Map each element of a structure to an action, evaluate+-- these actions from left to right, and ignore the results.+forFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()+forFC_ v f = traverseFC_ f v+{-# INLINE forFC_ #-}++-- | Flipped 'traverseFC'+forFC ::+  (TraversableFC t, Applicative m) =>+  t f x -> (forall y. f y -> m (g y)) -> m (t g x)+forFC v f = traverseFC f v+{-# INLINE forFC #-}
test/Test/Context.hs view
@@ -4,21 +4,22 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} module Test.Context-( contextTests-) where--import Test.Tasty-import Test.QuickCheck-import Test.Tasty.QuickCheck--import Control.Lens-import Data.Parameterized.Classes-import Data.Parameterized.TraversableFC-import Data.Parameterized.Some+  ( contextTests+  )+where +import           Control.Lens+import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as C import qualified Data.Parameterized.Context.Safe as S import qualified Data.Parameterized.Context.Unsafe as U+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC+import           Hedgehog+import qualified Hedgehog.Gen as HG+import           Hedgehog.Range+import           Test.Tasty+import           Test.Tasty.Hedgehog  data Payload (ty :: *) where   IntPayload    :: Int -> Payload Int@@ -38,13 +39,17 @@  instance ShowF Payload -instance Arbitrary (Some Payload) where-  arbitrary = oneof-    [ Some . IntPayload <$> arbitrary-    , Some . StringPayload <$> arbitrary-    , Some . BoolPayload <$> arbitrary-    ]+genSomePayload :: Monad m => GenT m (Some Payload)+genSomePayload = HG.choice [ Some . IntPayload    <$> HG.integral (linearBounded :: Range Int)+                           , Some . StringPayload <$> HG.string (linear 1 32) HG.ascii+                           , Some . BoolPayload   <$> HG.element [ True, False ]+                           ] +-- generate a non-empty list of payload entries+genSomePayloadList :: Monad m => GenT m [Some Payload]+genSomePayloadList = HG.list (linear 1 10) genSomePayload++ type UAsgn = U.Assignment Payload type SAsgn = S.Assignment Payload @@ -60,109 +65,120 @@        go a [] = Some a        go a (Some x : xs) = go (S.extend a x) xs -instance Arbitrary (Some UAsgn) where-  arbitrary = mkUAsgn <$> arbitrary-instance Arbitrary (Some SAsgn) where-  arbitrary = mkSAsgn <$> arbitrary  twiddle :: Payload a -> Payload a twiddle (IntPayload n) = IntPayload (n+1) twiddle (StringPayload str) = StringPayload (str++"asdf") twiddle (BoolPayload b) = BoolPayload (not b) + contextTests :: IO TestTree contextTests = testGroup "Context" <$> return-   [ testProperty "safe_index_eq" $ \v vs i -> ioProperty $ do-         let vals = v:vs-         let i' = min (max 0 i) (length vals - 1)-         Some a <- return $ mkSAsgn vals-         Just (Some idx) <- return $ S.intIndex i' (S.size a)-         return (Some (a S.! idx) == vals !! i')-   , testProperty "unsafe_index_eq" $ \v vs i -> ioProperty $ do-         let vals = v:vs-         let i' = min (max 0 i) (length vals - 1)-         Some a <- return $ mkUAsgn vals-         Just (Some idx) <- return $ U.intIndex i' (U.size a)-         return (Some (a U.! idx) == vals !! i')-   , testProperty "safe_tolist" $ \vals -> ioProperty $ do-         Some a <- return $ mkSAsgn vals-         let vals' = toListFC Some a-         return (vals == vals')-   , testProperty "unsafe_tolist" $ \vals -> ioProperty $ do-         Some a <- return $ mkUAsgn vals-         let vals' = toListFC Some a-         return (vals == vals')-   , testProperty "adjust test monadic" $ \v vs i -> ioProperty $ do-         let vals = v:vs  -- ensures vals is not an empty array-         Some x <- return $ mkUAsgn vals-         Some y <- return $ mkSAsgn vals-         let i' = min (max 0 i) (length vals - 1)+   [ testProperty "safe_index_eq" $ 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' -         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)-         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)+   , 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' -         x' <- U.adjustM (return . twiddle) idx_x x-         y' <- S.adjustM (return . twiddle) idx_y y+   , 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' -         return (toListFC Some x' == toListFC Some y')+   , testProperty "adjust test monadic" $ property $+     do vals <- forAll genSomePayloadList+        i' <- forAll $ HG.int (linear 0 $ length vals - 1) -   , testProperty "adjust test" $ \v vs i -> ioProperty $ do-         let vals = v:vs  -- ensures vals is not an empty array-         Some x <- return $ mkUAsgn vals-         Some y <- return $ mkSAsgn vals-         let i' = min (max 0 i) (length vals - 1)+        Some x <- return $ mkUAsgn vals+        Some y <- return $ mkSAsgn vals -         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)-         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)+        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+        Just (Some idx_y) <- return $ S.intIndex i' (S.size y) -         let x' = x & ixF idx_x %~ twiddle-             y' = y & ixF idx_y %~ twiddle+        x' <- U.adjustM (return . twiddle) idx_x x+        y' <- S.adjustM (return . twiddle) idx_y y -         return (toListFC Some x' == toListFC Some y' &&-                 -- adjust actually modified the entry-                 toListFC Some x /= toListFC Some x' &&-                 toListFC Some y /= toListFC Some y')+        toListFC Some x' === toListFC Some y' -   , testProperty "update test" $ \v vs i -> ioProperty $ do-         let vals = v:vs  -- ensures vals is not an empty array-         Some x <- return $ mkUAsgn vals-         Some y <- return $ mkSAsgn vals-         let i' = min (max 0 i) (length vals - 1)+   , testProperty "adjust test" $ 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) -         return (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' = x & ixF idx_x %~ twiddle+            y' = y & ixF idx_y %~ twiddle -   , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do-         Some x <- return $ mkSAsgn vals1-         Some y <- return $ mkSAsgn vals2-         case testEquality x y of-           Just Refl -> return $ vals1 == vals2-           Nothing   -> return $ vals1 /= vals2-   , testProperty "unsafe_eq" $ \vals1 vals2 -> ioProperty $ do-         Some x <- return $ mkUAsgn vals1-         Some y <- return $ mkUAsgn vals2-         case testEquality x y of-           Just Refl -> return $ vals1 == vals2-           Nothing   -> return $ vals1 /= vals2+        toListFC Some x' === toListFC Some y'+        -- adjust actually modified the entry+        toListFC Some x /== toListFC Some x'+        toListFC Some y /== toListFC Some y' -   , testProperty "append_take" $ \vals1 vals2 -> ioProperty $ do-         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-         return $ isJust $ testEquality x x'+   , testProperty "update test" $ property $+     do vals <- forAll genSomePayloadList+        i' <- forAll $ HG.int (linear 0 $ length vals - 1)++        Some x <- return $ mkUAsgn vals+        Some y <- return $ mkSAsgn vals++        Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+        Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++        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++        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 "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++   , 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'+    ]
test/Test/NatRepr.hs view
@@ -1,18 +1,23 @@ module Test.NatRepr-( natTests-) where+  ( natTests+  )+where -import Test.Tasty-import Test.Tasty.QuickCheck+import           Hedgehog+import qualified Hedgehog.Gen as HG+import           Hedgehog.Range+import           Test.Tasty+import           Test.Tasty.Hedgehog -import Data.Parameterized.NatRepr-import Data.Parameterized.Some-import GHC.TypeLits+import           Data.Parameterized.NatRepr+import           Data.Parameterized.Some+import           GHC.TypeLits  natTests :: IO TestTree natTests = testGroup "Nat" <$> return-  [ testProperty "withKnownNat" $ \nInt ->+  [ testProperty "withKnownNat" $ property $ do+      nInt <- forAll $ HG.int (linearBounded :: Range Int)       case someNat nInt of-        Nothing -> nInt < 0-        Just (Some r) -> nInt == withKnownNat r (natVal r)+        Nothing       -> diff nInt (<) 0+        Just (Some r) -> nInt === withKnownNat r (fromEnum $ natVal r)   ]
test/Test/Vector.hs view
@@ -1,70 +1,91 @@+{-# LANGUAGE TypeApplications #-}+{-# Language CPP #-} {-# Language DataKinds #-} {-# Language ExplicitForAll #-}-{-# Language TypeOperators #-}-{-# Language TypeFamilies #-} {-# Language FlexibleInstances #-} {-# Language ScopedTypeVariables #-} {-# Language StandaloneDeriving #-}-{-# Language CPP #-}+{-# Language TypeFamilies #-}+{-# Language TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans #-} #if __GLASGOW_HASKELL__ >= 805 {-# Language NoStarIsType #-} #endif module Test.Vector-( vecTests-) where--import Test.Tasty-import Test.Tasty.QuickCheck ( Arbitrary(..), testProperty, vectorOf )+  ( vecTests+  )+where -import Data.Parameterized.NatRepr-import Data.Parameterized.Vector-import GHC.TypeLits-import Data.Semigroup-import Prelude hiding (reverse)+import           Data.Parameterized.NatRepr+import           Data.Parameterized.Vector+import           Data.Semigroup+import           GHC.TypeLits+import           Hedgehog+import qualified Hedgehog.Gen as HG+import           Hedgehog.Range+import           Prelude hiding (reverse)+import           Test.Tasty+import           Test.Tasty.Hedgehog  -instance KnownNat n => Arbitrary (NatRepr n) where-  arbitrary = return knownNat-+genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)+genVector genElem =+  do let n = knownNat+         w = widthVal n+     l <- HG.list (constant w w) genElem+     case fromList n l of+       Just v -> return v+       Nothing -> error ("fromList failure for size " <> show w) -instance forall a n. ( 1 <= n-                     , Arbitrary a-                     , KnownNat n) =>-         Arbitrary (Vector n a) where-  arbitrary = do-    n <- arbitrary-    l <- vectorOf (widthVal n) arbitrary-    case fromList n l of-      Just v -> return v-      Nothing -> error ("fromList failure for size " <> show n)+genOrdering :: Monad m => GenT m Ordering+genOrdering = HG.element [ LT, EQ, GT ]   instance Show (Int -> Ordering) where   show _ = "unshowable" + -- We use @Ordering@ just because it's simple vecTests :: IO TestTree vecTests = testGroup "Vector" <$> return-  [ testProperty "reverse100" $-      \n v -> fromList (n :: NatRepr 100) (v :: [Ordering]) ==-              (reverse <$> (reverse <$> (fromList n v)))-  , testProperty "reverseSingleton" $-      \n v -> fromList (n :: NatRepr 1) (v :: [Ordering]) ==-              (reverse <$> (fromList n v))-  , testProperty "split-join" $-      \n w v -> (v :: Vector (5 * 5) Ordering) ==-                (join (n :: NatRepr 5) $ split n (w :: NatRepr 5) $ v)+  [ testProperty "reverse100" $ property $+    do v <- forAll $ genVector @100 genOrdering+       v === (reverse $ reverse v)+  , testProperty "reverseSingleton" $ property $+    do l <- (:[]) <$> forAll genOrdering+       Just v <- return $ fromList (knownNat @1) l+       v === reverse v++  , testProperty "split-join" $ property $+    do let n = knownNat @5+       v <- forAll $ genVector @(5 * 5) genOrdering+       v === (join n $ split n (knownNat @5) v)+   -- @cons@ is the same for vectors or lists-  , testProperty "cons" $-      \n v x -> (cons x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==-                (fromList (incNat n) (x:v))+  , 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)+   -- @snoc@ is like appending to a list-  , testProperty "snoc" $-      \n v x -> (flip snoc x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==-                (fromList (incNat n) (v ++ [x]))+  , 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])+   -- @generate@ is like mapping a function over indices-  , testProperty "generate" $-      \n f -> Just (generate (n :: NatRepr 55) ((f :: Int -> Ordering) . widthVal)) ==-              (fromList (incNat n) (map f [0..widthVal n]) :: Maybe (Vector 56 Ordering))+  , 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])   ]