parameterized-utils 2.1.2.0 → 2.1.3.0

raw patch · 24 files changed

+392/−110 lines, 24 filesdep ~constraintsdep ~lensdep ~tastyPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: constraints, lens, tasty

API changes (from Hackage documentation)

Files

• Changelog.md +21/−0
• parameterized-utils.cabal +22/−13
• src/Data/Parameterized/All.hs +2/−1
• src/Data/Parameterized/Classes.hs +10/−10
• src/Data/Parameterized/ClassesC.hs +3/−2
• src/Data/Parameterized/Compose.hs +2/−1
• src/Data/Parameterized/Context.hs +42/−6
• src/Data/Parameterized/Context/Safe.hs +26/−11
• src/Data/Parameterized/Context/Unsafe.hs +17/−7
• src/Data/Parameterized/Ctx.hs +6/−0
• src/Data/Parameterized/DataKind.hs +2/−1
• src/Data/Parameterized/HashTable.hs +6/−5
• src/Data/Parameterized/List.hs +3/−2
• src/Data/Parameterized/NatRepr.hs +1/−1
• src/Data/Parameterized/Nonce.hs +3/−7
• src/Data/Parameterized/Nonce/Transformers.hs +2/−1
• src/Data/Parameterized/Pair.hs +2/−1
• src/Data/Parameterized/Some.hs +2/−1
• src/Data/Parameterized/TraversableF.hs +9/−8
• src/Data/Parameterized/TraversableFC.hs +8/−7
• src/Data/Parameterized/Vector.hs +127/−20
• src/Data/Parameterized/WithRepr.hs +2/−1
• test/Test/Context.hs +14/−1
• test/Test/Vector.hs +60/−3

@@ -1,5 +1,26 @@ # Changelog for the `parameterized-utils` package +## 2.1.3.0 -- *2021 Mar 23*++  * Add support for GHC 9.+  * In the `Context` module:+    * Added `sizeToNatRepr` function for converting a `Context` `Size`.+    * Added `unzip` to unzip an `Assignment` of `Product(Pair)` into a+      separate `Assignment` for each element of the `Pair` (the+      inverse of the `zipWith Pair` operation).+    * Added `flattenAssignment` to convert an `Assignment` of+      `Assignment` into an `Assignment` of `CtxFlatten`.  Also adds+      `flattenSize` to combine the sizes of each context into the size+      of the corresponding `CtxFlatten`.+  * In the `Vector` module:+    * Added `fromAssignment` and `toAssignment` to allow conversions+      between `Assignment` and `Vector`.+    * Added `unsnoc`, `unfoldr`, `unfoldrM`, `unfoldrWithIndex`, and+      `unfoldrWithIndexM` functions.+  * Various haddock documentation updates and corrections.+  * Updated the Cabal specification to Cabal-version 2.2.++ ## 2.1.2 -- *2021 Jan 25*    * Added `SomeSym` and `viewSomeSym` for existentially hidden Symbol

@@ -1,12 +1,12 @@+Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.1.2.0+Version:       2.1.3.0 Author:        Galois Inc. Maintainer:    jhendrix@galois.com, kquick@galois.com stability:     stable Build-type:    Simple-Cabal-version: >= 1.10 Copyright:     ©2016-2021 Galois, Inc.-License:       BSD3+License:       BSD-3-Clause License-file:  LICENSE category:      Data Structures, Dependent Types Synopsis: Classes and data structures for working with data-kind indexed types@@ -19,7 +19,7 @@ extra-source-files: Changelog.md homepage:      https://github.com/GaloisInc/parameterized-utils bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues-tested-with:   GHC==8.6.5, GHC==8.8.3, GHC==8.10.1+tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.1  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -34,17 +34,31 @@   type: git   location: https://github.com/GaloisInc/parameterized-utils ++common bldflags+  ghc-options: -Wall+               -Wcompat+               -Wpartial-fields+               -Wincomplete-uni-patterns+               -Werror=incomplete-patterns+               -Werror=missing-methods+               -Werror=overlapping-patterns+               -fhide-source-paths+  default-language: Haskell2010++ library+  import: bldflags   build-depends: base >= 4.10 && < 5                , base-orphans   >=0.8.2 && <0.9                , th-abstraction >=0.3  && <0.5-               , constraints    >=0.10 && <0.13+               , constraints    >=0.10 && <0.14                , containers                , deepseq                , ghc-prim                , hashable       >=1.2  && <1.4                , hashtables     ==1.2.*-               , lens           >=4.16 && <4.20+               , lens           >=4.16 && <5.1                , mtl                , template-haskell                , text@@ -88,20 +102,15 @@   other-modules:     Data.Parameterized.NatRepr.Internal -  ghc-options: -Wall-  default-language: Haskell2010-   if flag(unsafe-operations)     cpp-options: -DUNSAFE_OPS   test-suite parameterizedTests+  import: bldflags   type: exitcode-stdio-1.0   hs-source-dirs: test -  ghc-options: -Wall-  default-language: Haskell2010-   main-is: UnitTest.hs   other-modules:     Test.Context@@ -117,7 +126,7 @@                , lens                , mtl                , parameterized-utils-               , tasty >= 1.2 && < 1.4+               , tasty >= 1.2 && < 1.5                , tasty-ant-xml == 1.1.*                , tasty-hunit >= 0.9 && < 0.11                , tasty-hedgehog

@@ -46,11 +46,12 @@   ) where  import Data.Functor.Const (Const(..))+import Data.Kind  import Data.Parameterized.Classes import Data.Parameterized.TraversableF -newtype All (f :: k -> *) = All { getAll :: forall x. f x }+newtype All (f :: k -> Type) = All { getAll :: forall x. f x }  instance FunctorF All where   fmapF f (All a) = All (f a)

@@ -80,7 +80,7 @@ --   all the types of a family.  We generally use this to witness --   the fact that the type parameter to @rtp@ is a phantom type --   by giving an implementation in terms of Data.Coerce.coerce.-class CoercibleF (rtp :: k -> *) where+class CoercibleF (rtp :: k -> Type) where   coerceF :: rtp a -> rtp b  instance CoercibleF (Const x) where@@ -97,7 +97,7 @@ -- type when they are equal. Thus this can be implemented over -- parameterized types that are unable to provide evidence that their -- type arguments are equal.-class EqF (f :: k -> *) where+class EqF (f :: k -> Type) where   eqF :: f a -> f a -> Bool  instance Eq a => EqF (Const a) where@@ -179,7 +179,7 @@ -- -- Minimal complete definition: either 'compareF' or 'leqF'. -- Using 'compareF' can be more efficient for complex types.-class TestEquality ktp => OrdF (ktp :: k -> *) where+class TestEquality ktp => OrdF (ktp :: k -> Type) where   {-# MINIMAL compareF | leqF #-}    compareF :: ktp x -> ktp y -> OrderingF x y@@ -219,7 +219,7 @@  -- | Compare two values, and if they are equal compare the next values, -- otherwise return LTF or GTF-lexCompareF :: forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k)+lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k)              .  OrdF f             => f a             -> f b@@ -230,7 +230,7 @@ -- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated -- for the \"inner\" functor. The type-level evidence of equality is deduced -- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.-ordFCompose :: forall k l (f :: k -> *) (g :: l -> k) x y.+ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y.                 (forall w z. f w -> f z -> OrderingF w z)             -> Compose f g x             -> Compose f g y@@ -252,7 +252,7 @@ -- To implement @'ShowF' g@, one should implement an instance @'Show' -- (g tp)@ for all argument types @tp@, then write an empty instance -- @instance 'ShowF' g@.-class ShowF (f :: k -> *) where+class ShowF (f :: k -> Type) where   -- | Provides a show instance for each type.   withShow :: p f -> q tp -> (Show (f tp) => a) -> a @@ -275,8 +275,8 @@ ------------------------------------------------------------------------ -- IxedF -type family IndexF       (m :: *) :: k -> *-type family IxValueF     (m :: *) :: k -> *+type family IndexF       (m :: Type) :: k -> Type+type family IxValueF     (m :: Type) :: k -> Type  -- | Parameterized generalization of the lens @Ixed@ class. class IxedF k m where@@ -315,7 +315,7 @@ {-# INLINE defaultSalt #-}  -- | A parameterized type that is hashable on all instances.-class HashableF (f :: k -> *) where+class HashableF (f :: k -> Type) where   hashWithSaltF :: Int -> f tp -> Int    -- | Hash with default salt.@@ -355,5 +355,5 @@ -- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of -- singleton types indexed by @k@), and an index parameter @ctx@ of -- kind @k@.-class KnownRepr (f :: k -> *) (ctx :: k) where+class KnownRepr (f :: k -> Type) (ctx :: k) where   knownRepr :: f ctx

@@ -26,17 +26,18 @@   ) where  import Data.Type.Equality ((:~:)(..))+import Data.Kind import Data.Maybe (isJust) import Data.Parameterized.Classes (OrderingF, toOrdering) import Data.Parameterized.Some (Some(..)) -class TestEqualityC (t :: (k -> *) -> *) where+class TestEqualityC (t :: (k -> Type) -> Type) where   testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))                 -> t f                 -> t f                 -> Bool -class TestEqualityC t => OrdC (t :: (k -> *) -> *) where+class TestEqualityC t => OrdC (t :: (k -> Type) -> Type) where   compareC :: (forall x y. f x -> g y -> OrderingF x y)            -> t f            -> t g

@@ -21,13 +21,14 @@   ) where  import Data.Functor.Compose+import Data.Kind import Data.Orphans () -- For the TestEquality (Compose f g) instance import Data.Type.Equality  -- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@. -- -- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.-testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.+testEqualityComposeBare :: forall k l (f :: k -> Type) (g :: l -> k) x y.                            (forall w z. f w -> f z -> Maybe (w :~: z))                         -> Compose f g x                         -> Compose f g y

@@ -64,6 +64,9 @@   , traverseAndCollect   , traverseWithIndex_   , dropPrefix+  , unzip+  , flattenAssignment+  , flattenSize      -- * Context extension and embedding utilities   , CtxEmbedding(..)@@ -97,9 +100,13 @@   , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6   ) where +import           Prelude hiding (unzip)+ import           Control.Applicative (liftA2) import           Control.Lens hiding (Index, (:>), Empty) import           Data.Functor (void)+import           Data.Functor.Product (Product(Pair))+import           Data.Kind import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import           GHC.TypeLits (Nat, type (-))@@ -157,7 +164,6 @@   return vm {-# INLINABLE toVector #-} - -- | Utility function for testing if @xs@ is an assignment with --   `prefix` as a prefix, and computing the tail of xs --   not in the prefix, if so.@@ -187,9 +193,39 @@       Just Refl -> success Empty       Nothing   -> err +-- | Unzip an assignment of pairs into a pair of assignments.+--+-- This is the inverse of @'zipWith' 'Pair'@.+unzip :: Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)+unzip fgs =+  case viewAssign fgs of+    AssignEmpty -> (empty, empty)+    AssignExtend rest (Pair f g) ->+      let (fs, gs) = unzip rest+      in (extend fs f, extend gs g) +-- | Flattens a nested assignment over a context of contexts @ctxs :: Ctx (Ctx+-- a)@ into a flat assignment over the flattened context @CtxFlatten ctxs@.+flattenAssignment ::+  Assignment (Assignment f) ctxs ->+  Assignment f (CtxFlatten ctxs)+flattenAssignment ctxs =+  case viewAssign ctxs of+    AssignEmpty -> empty+    AssignExtend ctxs' ctx -> flattenAssignment ctxs' <++> ctx +-- | Given the size of each context in @ctxs@, returns the size of @CtxFlatten+-- ctxs@.  You can obtain the former from any nested assignment @Assignment+-- (Assignment f) ctxs@, by calling @fmapFC size@.+flattenSize ::+  Assignment Size ctxs ->+  Size (CtxFlatten ctxs)+flattenSize a =+  case viewAssign a of+    AssignEmpty -> zeroSize+    AssignExtend b s -> addSize (flattenSize b) s + -------------------------------------------------------------------------------- -- Patterns @@ -272,16 +308,16 @@                        (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2) ctxeAssignment = lens _ctxeAssignment (\s v -> s { _ctxeAssignment = v }) -class ApplyEmbedding (f :: Ctx k -> *) where+class ApplyEmbedding (f :: Ctx k -> Type) where   applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx' -class ApplyEmbedding' (f :: Ctx k -> k' -> *) where+class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where   applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v -class ExtendContext (f :: Ctx k -> *) where+class ExtendContext (f :: Ctx k -> Type) where   extendContext :: Diff ctx ctx' -> f ctx -> f ctx' -class ExtendContext' (f :: Ctx k -> k' -> *) where+class ExtendContext' (f :: Ctx k -> k' -> Type) where   extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v  instance ApplyEmbedding' Index where@@ -384,7 +420,7 @@ -- > CurryAssignment (EmptyCtx ::> a) f x = f a -> x -- > CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x -- > CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x-type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where+type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) (x :: Type) :: Type where    CurryAssignment EmptyCtx    f x = x    CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x) 

@@ -57,6 +57,7 @@   , addSize   , SizeView(..)   , viewSize+  , sizeToNatRepr   , KnownContext(..)     -- * Diff   , Diff@@ -120,6 +121,7 @@  import Data.Parameterized.Classes import Data.Parameterized.Ctx+import Data.Parameterized.NatRepr import Data.Parameterized.Some import Data.Parameterized.TraversableFC @@ -168,6 +170,16 @@ viewSize SizeZero = ZeroSize viewSize (SizeSucc s) = IncSize s +-- | Convert a 'Size' into a 'NatRepr'.+sizeToNatRepr :: Size items -> NatRepr (CtxSize items)+sizeToNatRepr sz =+  case viewSize sz of+    ZeroSize -> knownRepr+    IncSize sz' ->+      let oldRep = sizeToNatRepr sz'+      in case plusComm (knownRepr :: NatRepr 1) oldRep of+           Refl -> incNat oldRep+ ------------------------------------------------------------------------ -- Size @@ -332,8 +344,8 @@   IndexViewLast _ -> lastIndex (addSize sz sz')   IndexViewInit idx' -> skipIndex (extendIndexAppendLeft sz (decSize sz') idx') --- | Given a size @n@, an initial value @v0@, and a function @f@, the--- expression @forIndex n v0 f@ calls @f@ on each index less than @n@+-- | Given a size @n@, a function @f@, and an initial value @v0@, the+-- expression @forIndex n f v0@ calls @f@ on each index less than @n@ -- starting from @0@ and @v0@, with the value @v@ obtained from the -- last call. forIndex :: forall ctx r@@ -374,9 +386,9 @@ forIndexRangeImpl i (SizeSucc sz) d f r =   forIndexRangeImpl (i-1) sz (LDiffThere d) f r --- | Given an index @i@, size @n@, a function @f@, value @v@, and a--- function @f@, the expression @forIndexRange i n f v@ is equivalent--- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@+-- | Given an index @i@, size @n@, a function @f@, and a value @v@,+-- the expression @forIndexRange i n f v@ is equivalent+-- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@ -- otherwise. forIndexRange :: Int               -> Size ctx@@ -484,6 +496,9 @@ empty :: Assignment f 'EmptyCtx empty = AssignmentEmpty +-- n.b. see 'singleton' in Data/Parameterized/Context.hs++-- | Extend an indexed vector with a new entry. extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp) extend asgn e = AssignmentExtend asgn e @@ -506,7 +521,7 @@ type instance IxValueF (Assignment (f :: k -> Type) ctx) = f  instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where-  ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)+  ixF :: Index ctx x -> Lens.Traversal' (Assignment f ctx) (f x)   ixF idx f = adjustM f idx  instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where@@ -544,7 +559,7 @@ testEq _ AssignmentExtend{} AssignmentEmpty = Nothing  instance TestEqualityFC Assignment where-   testEqualityFC = testEq+   testEqualityFC f = testEq f instance TestEquality f => TestEquality (Assignment f) where    testEquality x y = testEq testEquality x y instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where@@ -565,7 +580,7 @@               EQF -> EQF  instance OrdFC Assignment where-  compareFC = compareAsgn+  compareFC f = compareAsgn f  instance OrdF f => OrdF (Assignment f) where   compareF = compareAsgn compareF@@ -598,11 +613,11 @@   foldMapFC = foldMapFCDefault  instance TraversableFC Assignment where-  traverseFC = traverseF+  traverseFC f = traverseF f  -- | Map assignment map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c-map = fmapFC+map f = fmapFC f  traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)            . Applicative m@@ -616,7 +631,7 @@ toList :: (forall tp . f tp -> a)        -> Assignment f c        -> [a]-toList = toListFC+toList f = toListFC f  zipWithM :: Applicative m          => (forall tp . f tp -> g tp -> m (h tp))

@@ -29,6 +29,7 @@   , addSize   , SizeView(..)   , viewSize+  , sizeToNatRepr     -- * Diff   , Diff   , noDiff@@ -100,6 +101,8 @@ import           Data.Parameterized.Classes import           Data.Parameterized.Ctx import           Data.Parameterized.Ctx.Proofs+import           Data.Parameterized.NatRepr+import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr)) import           Data.Parameterized.Some import           Data.Parameterized.TraversableFC @@ -136,6 +139,10 @@ viewSize (Size 0) = unsafeCoerce ZeroSize viewSize (Size n) = assert (n > 0) (unsafeCoerce (IncSize (Size (n-1)))) +-- | Convert a 'Size' into a 'NatRepr'.+sizeToNatRepr :: Size items -> NatRepr (CtxSize items)+sizeToNatRepr (Size n) = NatRepr (fromIntegral n)+ instance Show (Size ctx) where   show (Size i) = show i @@ -290,9 +297,9 @@ extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp extendIndexAppendLeft (Size l) _ (Index idx) = Index (idx + l) --- | Given a size @n@, an initial value @v0@, and a function @f@, the--- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is--- zero, and @f (forIndex (n-1) v0) n@ otherwise.  Unlike the safe+-- | Given a size @n@, a function @f@, and an initial value @v0@, the+-- expression @forIndex n f v0@ is equivalent to @v0@ when @n@ is+-- zero, and @f (forIndex (n-1) f v0) n@ otherwise.  Unlike the safe -- version, which starts from 'Index' @0@ and increments 'Index' -- values, this version starts at 'Index' @(n-1)@ and decrements -- 'Index' values to 'Index' @0@.@@ -306,9 +313,9 @@     ZeroSize -> r     IncSize p -> f (forIndex p (coerce f) r) (nextIndex p) --- | Given an index @i@, size @n@, a function @f@, value @v@, and a--- function @f@, the expression @forIndex i n f v@ is equivalent to--- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@+-- | Given an index @i@, size @n@, a function @f@, and a value @v@,+-- the expression @forIndex i n f v@ is equivalent to+-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@ -- otherwise. forIndexRange :: forall ctx r                . Int@@ -794,6 +801,9 @@ empty :: Assignment f EmptyCtx empty = Assignment Empty +-- n.b. see 'singleton' in Data/Parameterized/Context.hs++-- | Extend an indexed vector with a new entry. extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x) extend (Assignment x) y = Assignment $ append x (BalLeaf y) @@ -870,7 +880,7 @@   ixF' idx f = adjustM f idx  instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where-  ixF = ixF'+  ixF idx = ixF' idx  -- This is an unsafe version of update that changes the type of the expression. unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'

@@ -31,6 +31,7 @@   , CtxUpdate   , CtxLookupRight   , CtxUpdateRight+  , CtxFlatten   , CheckIx   , ValidIx   , FromLeft@@ -101,3 +102,8 @@ --   is out of range, the context is unchanged. type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k)   = CtxUpdateRight (FromLeft ctx n) x ctx++-- | Flatten a nested context+type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where+  CtxFlatten EmptyCtx = EmptyCtx+  CtxFlatten (ctxs ::> ctx) = CtxFlatten ctxs <+> ctx

@@ -13,9 +13,10 @@ import           Data.Parameterized.Classes import qualified Data.Parameterized.TH.GADT as TH +import           Data.Kind import           Prelude hiding ( fst, snd ) -data PairRepr (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)) where+data PairRepr (f :: k1 -> Type) (g :: k2 -> Type) (p :: (k1, k2)) where   PairRepr :: f a -> g b -> PairRepr f g '(a, b)  type family Fst (pair :: (k1, k2)) where

@@ -31,6 +31,7 @@ import Control.Applicative import Control.Monad.ST import qualified Data.HashTable.ST.Basic as H+import Data.Kind import GHC.Exts (Any) import Unsafe.Coerce @@ -40,7 +41,7 @@ import Data.Parameterized.Some  -- | A hash table mapping nonces to values.-newtype HashTable s (key :: k -> *) (val :: k -> *)+newtype HashTable s (key :: k -> Type) (val :: k -> Type)       = HashTable (H.HashTable s (Some key) Any)  -- | Create a new empty table.@@ -73,7 +74,7 @@  -- | Insert new key and value mapping into table. insert :: (HashableF key, TestEquality key)-       => HashTable s (key :: k -> *) (val :: k -> *)+       => HashTable s (key :: k -> Type) (val :: k -> Type)        -> key tp        -> val tp        -> ST s ()@@ -81,18 +82,18 @@  -- | Return true if the key is in the hash table. member :: (HashableF key, TestEquality key)-       => HashTable s (key :: k -> *) (val :: k -> *)+       => HashTable s (key :: k -> Type) (val :: k -> Type)        -> key (tp :: k)        -> ST s Bool member (HashTable h) k = isJust <$> H.lookup h (Some k)  -- | Delete an element from the hash table. delete :: (HashableF key, TestEquality key)-       => HashTable s (key :: k -> *) (val :: k -> *)+       => HashTable s (key :: k -> Type) (val :: k -> Type)        -> key (tp :: k)        -> ST s () delete (HashTable h) k = H.delete h (Some k)  clear :: (HashableF key, TestEquality key)-      => HashTable s (key :: k -> *) (val :: k -> *) -> ST s ()+      => HashTable s (key :: k -> Type) (val :: k -> Type) -> ST s () clear (HashTable h) = H.mapM_ (\(k,_) -> H.delete h k) h

@@ -149,13 +149,14 @@   ) where  import qualified Control.Lens as Lens+import           Data.Kind import           Prelude hiding ((!!))  import           Data.Parameterized.Classes import           Data.Parameterized.TraversableFC  -- | Parameterized list of elements.-data List :: (k -> *) -> [k] -> * where+data List :: (k -> Type) -> [k] -> Type where   Nil  :: List f '[]   (:<) :: f tp -> List f tps -> List f (tp : tps) @@ -215,7 +216,7 @@ -- | Represents an index into a type-level list. Used in place of integers to --   1. ensure that the given index *does* exist in the list --   2. guarantee that it has the given kind-data Index :: [k] -> k -> *  where+data Index :: [k] -> k -> Type  where   IndexHere :: Index (x:r) x   IndexThere :: !(Index r y) -> Index (x:r) y 

@@ -540,7 +540,7 @@             . NatRepr h            -> (forall n. (n <= h) => NatRepr n -> a)            -> [a]-natFromZero = natForEach (knownNat @0)+natFromZero h f = natForEach (knownNat @0) h f  -- | Recursor for natural numbeers. natRec :: forall p f

@@ -14,7 +14,6 @@ (via 'unsafeCoerce') that the types ascribed to the nonces are equal if their values are equal. -}-{-# LANGUAGE CPP #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE GADTs #-}@@ -46,6 +45,7 @@  import Control.Monad.ST import Data.Hashable+import Data.Kind import Data.IORef import Data.STRef import Data.Typeable@@ -56,15 +56,11 @@ import Data.Parameterized.Classes import Data.Parameterized.Some -#if __GLASGOW_HASKELL__ < 805-import Data.Kind-#endif- -- | Provides a monadic action for getting fresh typed names. -- -- The first type parameter @m@ is the monad used for generating names, and -- the second parameter @s@ is used for the counter.-data NonceGenerator (m :: * -> *) (s :: *) where+data NonceGenerator (m :: Type -> Type) (s :: Type) where   STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s   IONG :: !(IORef Word64) -> NonceGenerator IO s @@ -123,7 +119,7 @@   f r  -- | An index generated by the counter.-newtype Nonce (s :: *) (tp :: k) = Nonce { indexValue :: Word64 }+newtype Nonce (s :: Type) (tp :: k) = Nonce { indexValue :: Word64 }   deriving (Eq, Ord, Hashable, Show)  --  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce

@@ -25,6 +25,7 @@ import Control.Monad.Reader import Control.Monad.ST import Control.Monad.State+import Data.Kind  import Data.Parameterized.Nonce @@ -33,7 +34,7 @@ -- (where we view the phantom type parameter of 'Nonce' as a designator of the -- set that the 'Nonce' came from). class Monad m => MonadNonce m where-  type NonceSet m :: *+  type NonceSet m :: Type   freshNonceM :: forall k (tp :: k) . m (Nonce (NonceSet m) tp)  -- | This transformer adds a nonce generator to a given monad.

@@ -17,13 +17,14 @@   , viewPair   ) where +import Data.Kind import Data.Parameterized.Classes import Data.Parameterized.Some import Data.Parameterized.TraversableF  -- | Like a 2-tuple, but with an existentially quantified parameter that both of -- the elements share.-data Pair (a :: k -> *) (b :: k -> *) where+data Pair (a :: k -> Type) (b :: k -> Type) where   Pair :: !(a tp) -> !(b tp) -> Pair a b  instance (TestEquality a, EqF b) => Eq (Pair a b) where

@@ -20,11 +20,12 @@   ) where  import Data.Hashable+import Data.Kind import Data.Parameterized.Classes import Data.Parameterized.TraversableF  -data Some (f:: k -> *) = forall x . Some (f x)+data Some (f:: k -> Type) = forall x . Some (f x)  instance TestEquality f => Eq (Some f) where   Some x == Some y = isJust (testEquality x y)

@@ -35,6 +35,7 @@ import Control.Monad.Identity import Data.Coerce import Data.Functor.Compose (Compose(..))+import Data.Kind import Data.Monoid import GHC.Exts (build) @@ -57,7 +58,7 @@  -- | This is a generalization of the 'Foldable' class to -- structures over parameterized terms.-class FoldableF (t :: (k -> *) -> *) where+class FoldableF (t :: (k -> Type) -> Type) where   {-# MINIMAL foldMapF | foldrF #-}    -- | Map each element of the structure to a monoid,@@ -167,24 +168,24 @@ ------------------------------------------------------------------------ -- TraversableF (Compose s t) -instance ( FunctorF (s :: (k -> *) -> *)-         , FunctorFC (t :: (l -> *) -> (k -> *))+instance ( FunctorF (s :: (k -> Type) -> Type)+         , FunctorFC (t :: (l -> Type) -> (k -> Type))          ) =>          FunctorF (Compose s t) where   fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v -instance ( TraversableF (s :: (k -> *) -> *)-         , TraversableFC (t :: (l -> *) -> (k -> *))+instance ( TraversableF (s :: (k -> Type) -> Type)+         , TraversableFC (t :: (l -> Type) -> (k -> Type))          ) =>          FoldableF (Compose s t) where   foldMapF = foldMapFDefault  -- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.-instance ( TraversableF (s :: (k -> *) -> *)-         , TraversableFC (t :: (l -> *) -> (k -> *))+instance ( TraversableF (s :: (k -> Type) -> Type)+         , TraversableFC (t :: (l -> Type) -> (k -> Type))          ) =>          TraversableF (Compose s t) where-  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>+  traverseF :: forall (f :: l -> Type) (g :: l -> Type) m. (Applicative m) =>                (forall (u :: l). f u -> m (g u))             -> Compose s t f -> m (Compose s t g)   traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v

@@ -38,6 +38,7 @@ import Control.Applicative (Const(..) ) import Control.Monad.Identity ( Identity (..) ) import Data.Coerce+import Data.Kind import Data.Monoid import GHC.Exts (build) import Data.Type.Equality@@ -45,13 +46,13 @@ import Data.Parameterized.Classes  -- | A parameterized type that is a function on all instances.-class FunctorFC (t :: (k -> *) -> l -> *) where+class FunctorFC (t :: (k -> Type) -> l -> Type) where   fmapFC :: forall f g. (forall x. f x -> g x) ->                         (forall x. t f x -> t g x)  -- | A parameterized class for types which can be shown, when given --   functions to show parameterized subterms.-class ShowFC (t :: (k -> *) -> l -> *) where+class ShowFC (t :: (k -> Type) -> l -> Type) where   {-# MINIMAL showFC | showsPrecFC #-}    showFC :: forall f. (forall x. f x -> String)@@ -65,19 +66,19 @@  -- | A parameterized class for types which can be hashed, when given --   functions to hash parameterized subterms.-class HashableFC (t :: (k -> *) -> l -> *) where+class HashableFC (t :: (k -> Type) -> l -> Type) where   hashWithSaltFC :: forall f. (forall x. Int -> f x -> Int) ->                               (forall x. Int -> t f x -> Int)  -- | A parameterized class for types which can be tested for parameterized equality, --   when given an equality test for subterms.-class TestEqualityFC (t :: (k -> *) -> l -> *) where+class TestEqualityFC (t :: (k -> Type) -> l -> Type) where   testEqualityFC :: forall f. (forall x y. f x -> f y -> (Maybe (x :~: y))) ->                               (forall x y. t f x -> t f y -> (Maybe (x :~: y)))  -- | A parameterized class for types which can be tested for parameterized ordering, --   when given an comparison test for subterms.-class TestEqualityFC t => OrdFC (t :: (k -> *) -> l -> *) where+class TestEqualityFC t => OrdFC (t :: (k -> Type) -> l -> Type) where   compareFC :: forall f. (forall x y. f x -> f y -> OrderingF x y) ->                          (forall x y. t f x -> t f y -> OrderingF x y) @@ -91,7 +92,7 @@  -- | This is a generalization of the 'Foldable' class to -- structures over parameterized terms.-class FoldableFC (t :: (k -> *) -> l -> *) where+class FoldableFC (t :: (k -> Type) -> l -> Type) where   {-# MINIMAL foldMapFC | foldrFC #-}    -- | Map each element of the structure to a monoid,@@ -158,7 +159,7 @@ ------------------------------------------------------------------------ -- TraversableF -class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *) where+class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> Type) -> l -> Type) where   traverseFC :: forall f g m. Applicative m              => (forall x. f x -> m (g x))              -> (forall x. t f x -> m (t g x))

@@ -1,6 +1,8 @@ {-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-} {-# Language PatternGuards #-}+{-# Language PolyKinds #-} {-# Language TypeApplications, ScopedTypeVariables #-}+{-# Language TupleSections #-} {-# Language Rank2Types, RoleAnnotations #-} {-# Language CPP #-} #if __GLASGOW_HASKELL__ >= 805@@ -20,6 +22,10 @@   , fromList   , toList +    -- * Assignments+  , fromAssignment+  , toAssignment+     -- * Length   , length   , nonEmpty@@ -36,6 +42,7 @@      -- * Sub sequences   , uncons+  , unsnoc   , slice   , Data.Parameterized.Vector.take   , replace@@ -62,6 +69,11 @@   , snoc   , generate   , generateM+  -- ** Unfolding+  , unfoldr+  , unfoldrM+  , unfoldrWithIndex+  , unfoldrWithIndexM      -- * Splitting and joining     -- ** General@@ -90,6 +102,7 @@ import Prelude hiding (length,reverse,zipWith) import Numeric.Natural +import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Utils.Endian  -- | Fixed-size non-empty vectors.@@ -170,7 +183,19 @@              Right Refl    -> Left Refl {-# Inline uncons #-} +-- | Remove the last element of the vector, and return the rest, if any.+unsnoc :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))+unsnoc v@(Vector xs) = (Vector.last xs, mbTail)+  where+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)+  mbTail = case testStrictLeq (knownNat @1) (length v) of+             Left n2_leq_n ->+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))+                  return (Vector (Vector.slice 0 (Vector.length xs - 1) xs))+             Right Refl    -> Left Refl+{-# Inline unsnoc #-} + --------------------------------------------------------------------------------  -- | Make a vector of the given length and element type.@@ -185,7 +210,34 @@   v = Vector.fromList xs {-# INLINE fromList #-} +-- | Convert a non-empty 'Ctx.Assignment' to a fixed-size 'Vector'.+--+-- This function uses the same ordering convention as 'Ctx.toVector'.+fromAssignment ::+  forall f ctx tp e.+  (forall tp'. f tp' -> e) ->+  Ctx.Assignment f (ctx Ctx.::> tp) ->+  Vector (Ctx.CtxSize (ctx Ctx.::> tp)) e+fromAssignment f assign =+  case Ctx.viewAssign assign of+    Ctx.AssignExtend assign' _ ->+      case leqAdd (leqRefl (knownNat @1)) (Ctx.sizeToNatRepr (Ctx.size assign')) of+        LeqProof -> Vector (Ctx.toVector assign f) +-- | Convert a 'Vector' into a 'Ctx.Assignment'.+--+-- This function uses the same ordering convention as 'Ctx.toVector'.+toAssignment ::+  Ctx.Size ctx ->+  (forall tp. Ctx.Index ctx tp -> e -> f tp) ->+  Vector (Ctx.CtxSize ctx) e ->+  Ctx.Assignment f ctx+toAssignment sz g vec =+  -- The unsafe indexing here relies on the safety of the rest of the Vector+  -- API, specifically the inability to construct vectors that have an+  -- underlying size that differs from the size in their type.+  Ctx.generate sz (\idx -> g idx (elemAtUnsafe (Ctx.indexVal idx) vec))+ -- | Extract a subvector of the given vector. slice :: (i + w <= n, 1 <= w) =>             NatRepr i {- ^ Start index -} ->@@ -219,7 +271,7 @@             NatRepr i {- ^ Start index -} ->             NatRepr w {- ^ Section width -} ->             (Vector w a -> Vector w a) {-^ map for the sub-vector -} ->-            Vector n a -> Vector n a +            Vector n a -> Vector n a mapAt i w f vn = runIdentity $ mapAtM i w (pure . f) vn  -- | Replace a sub-section of a vector with the given sub-vector.@@ -371,30 +423,12 @@ unVector' :: Vector' a n -> Vector (n+1) a unVector' (MkVector' v) = v -snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)-snoc' v = MkVector' . snoc (unVector' v)- generate' :: forall h a            . NatRepr h           -> (forall n. (n <= h) => NatRepr n -> a)           -> Vector' a h generate' h gen =-  case isZeroOrGT1 h of-    Left Refl -> base-    Right LeqProof ->-      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->-      natRecBounded (decNat h) (decNat h) base step-      }-  where base :: Vector' a 0-        base = MkVector' $ singleton (gen (knownNat @0))-        step :: forall m. (1 <= h, m <= h - 1)-             => NatRepr m -> Vector' a m -> Vector' a (m + 1)-        step m v =-          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->-          case (leqAdd2 (LeqProof :: LeqProof m (h-1))-                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->-            snoc' v (gen (incNat m))-          }}+  runIdentity $ unfoldrWithIndexM' h (\n _last -> Identity (gen n, ())) ()  -- | Apply a function to each element in a range starting at zero; -- return the a vector of values obtained.@@ -412,6 +446,79 @@           -> (forall n. (n <= h) => NatRepr n -> m a)           -> m (Vector (h + 1) a) generateM h gen = sequence $ generate h gen++newtype Compose3 m f g a = Compose3 { getCompose3 :: m (f (g a)) }++unfoldrWithIndexM' :: forall m h a b. (Monad m)+                  => NatRepr h+                  -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))+                  -> b+                  -> m (Vector' a h)+unfoldrWithIndexM' h gen start =+  case isZeroOrGT1 h of+    Left Refl -> snd <$> getCompose3 base+    Right LeqProof ->+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->+        snd <$> getCompose3 (natRecBounded (decNat h) (decNat h) base step)+      }+  where base :: Compose3 m ((,) b) (Vector' a) 0+        base = Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start+        step :: forall p. (1 <= h, p <= h - 1)+             => NatRepr p+             -> Compose3 m ((,) b) (Vector' a) p+             -> Compose3 m ((,) b) (Vector' a) (p + 1)+        step p (Compose3 mv) =+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->+          case (leqAdd2 (LeqProof :: LeqProof p (h-1))+                        (LeqProof :: LeqProof 1 1) :: LeqProof (p+1) h) of { LeqProof ->+            Compose3 $+              do (seed, MkVector' v) <- mv+                 (next, nextSeed) <- gen (incNat p) seed+                 pure $ (nextSeed, MkVector' $ snoc v next)+          }}++-- | Monadically unfold a vector, with access to the current index.+--+-- c.f. @Data.Vector.unfoldrExactNM@+unfoldrWithIndexM :: forall m h a b. (Monad m)+                 => NatRepr h+                 -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))+                 -> b+                 -> m (Vector (h + 1) a)+unfoldrWithIndexM h gen start = unVector' <$> unfoldrWithIndexM' h gen start++-- | Unfold a vector, with access to the current index.+--+-- c.f. @Data.Vector.unfoldrExactN@+unfoldrWithIndex :: forall h a b+                . NatRepr h+                -> (forall n. (n <= h) => NatRepr n -> b -> (a, b))+                -> b+                -> Vector (h + 1) a+unfoldrWithIndex h gen start =+  unVector' $ runIdentity $ unfoldrWithIndexM' h (\n v -> Identity (gen n v)) start++-- | Monadically construct a vector with exactly @h + 1@ elements by repeatedly+-- applying a generator function to a seed value.+--+-- c.f. @Data.Vector.unfoldrExactNM@+unfoldrM :: forall m h a b. (Monad m)+        => NatRepr h+        -> (b -> m (a, b))+        -> b+        -> m (Vector (h + 1) a)+unfoldrM h gen start = unfoldrWithIndexM h (\_ v -> gen v) start++-- | Construct a vector with exactly @h + 1@ elements by repeatedly applying a+-- generator function to a seed value.+--+-- c.f. @Data.Vector.unfoldrExactN@+unfoldr :: forall h a b+        . NatRepr h+       -> (b -> (a, b))+       -> b+       -> Vector (h + 1) a+unfoldr h gen start = unfoldrWithIndex h (\_ v -> gen v) start  -------------------------------------------------------------------------------- 

@@ -58,6 +58,7 @@ -} module Data.Parameterized.WithRepr(IsRepr(..)) where +import Data.Kind import Data.Parameterized.Classes  #ifdef UNSAFE_OPS@@ -75,7 +76,7 @@ import Data.Parameterized.BoolRepr  -- | Turn an explicit Repr value into an implict KnownRepr constraint-class IsRepr (f :: k -> *) where+class IsRepr (f :: k -> Type) where    withRepr :: f a -> (KnownRepr f a => r) -> r 

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-}@@ -9,10 +10,15 @@  module Test.Context   ( contextTests+  , genSomePayloadList+  , mkUAsgn+  , mkSAsgn   ) where  import           Control.Lens+import           Data.Functor.Product (Product(Pair))+import           Data.Kind import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as C import qualified Data.Parameterized.Context.Safe as S@@ -32,7 +38,7 @@ -- Create a Payload GADT which is the parameterized type used for many -- of the Context/Assignment tests in this module. -data Payload (ty :: *) where+data Payload (ty :: Type) where   IntPayload    :: Int -> Payload Int   StringPayload :: String -> Payload String   BoolPayload   :: Bool -> Payload Bool@@ -310,6 +316,13 @@         assert $ isJust $ testEquality uv uv'         assert $ isJust $ testEquality wxy wxy'         withWXY $ \t -> assert $ isJust $ testEquality wxy' t++   , 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''     , testCaseSteps "explicit indexing (unsafe)" $ \step -> do        let mkUPayload :: U.Assignment Payload TestCtx

@@ -3,6 +3,7 @@ {-# Language DataKinds #-} {-# Language ExplicitForAll #-} {-# Language FlexibleInstances #-}+{-# Language LambdaCase #-} {-# Language ScopedTypeVariables #-} {-# Language StandaloneDeriving #-} {-# Language TypeFamilies #-}@@ -16,16 +17,23 @@   ) where +import           Data.Functor.Const (Const(..))+import           Data.Maybe (isJust)+import qualified Data.List as List+import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.NatRepr+import           Data.Parameterized.Some 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           Prelude hiding (take, reverse)+import qualified Prelude as P import           Test.Tasty import           Test.Tasty.Hedgehog+import           Test.Context (genSomePayloadList, mkUAsgn)   genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)@@ -41,7 +49,7 @@ genOrdering = HG.element [ LT, EQ, GT ]  -instance Show (Int -> Ordering) where+instance Show (a -> b) where   show _ = "unshowable"  @@ -77,6 +85,14 @@        x <- forAll genOrdering        (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x]) +  -- @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+   -- @generate@ is like mapping a function over indices   , testProperty "generate" $ property $     do let n = knownNat @55@@ -88,4 +104,45 @@                    ]        f <- forAll $ HG.element funs        Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])-  ]++  -- @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))++  -- 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))+    ]