packages feed

parameterized-utils 2.1.1 → 2.1.2.0

raw patch · 14 files changed

+367/−81 lines, 14 filesdep ~th-abstraction

Dependency ranges changed: th-abstraction

Files

Changelog.md view
@@ -1,5 +1,14 @@ # Changelog for the `parameterized-utils` package +## 2.1.2 -- *2021 Jan 25*++  * Added `SomeSym` and `viewSomeSym` for existentially hidden Symbol+    values which retain the `KnownSymbol` constraint.+  * Added `leftIndex` and `rightIndex` for re-casting indexes of the+    individual parts of an Assignment into the concatenated+    Assignment.+  * Additional tests and updated documentation.+ ## 2.1.1 -- *2020 Jul 30*    * Added `drop` and `appendEmbeddingLeft` functions to the `Context` module.
parameterized-utils.cabal view
@@ -1,11 +1,11 @@ Name:          parameterized-utils-Version:       2.1.1+Version:       2.1.2.0 Author:        Galois Inc. Maintainer:    jhendrix@galois.com, kquick@galois.com stability:     stable Build-type:    Simple Cabal-version: >= 1.10-Copyright:     ©2016-2020 Galois, Inc.+Copyright:     ©2016-2021 Galois, Inc. License:       BSD3 License-file:  LICENSE category:      Data Structures, Dependent Types@@ -37,7 +37,7 @@ library   build-depends: base >= 4.10 && < 5                , base-orphans   >=0.8.2 && <0.9-               , th-abstraction >=0.3  && <0.4+               , th-abstraction >=0.3  && <0.5                , constraints    >=0.10 && <0.13                , containers                , deepseq@@ -106,6 +106,7 @@   other-modules:     Test.Context     Test.NatRepr+    Test.SymbolRepr     Test.Vector    build-depends: base
src/Data/Parameterized/Classes.hs view
@@ -17,15 +17,11 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}-#if MIN_VERSION_base(4,9,0)-{-# LANGUAGE Safe #-}-#else-{-# LANGUAGE Trustworthy #-}-#endif module Data.Parameterized.Classes   ( -- * Equality exports     Equality.TestEquality(..)@@ -158,14 +154,40 @@ ------------------------------------------------------------------------ -- OrdF --- | A parameterized type that can be compared on distinct instances.+-- | The `OrdF` class is a total ordering over parameterized types so+-- that types with different parameters can be compared.+--+-- Instances of `OrdF` are expected to satisfy the following laws:+--+-- [__Transitivity__]: if @leqF x y && leqF y z@ = 'True', then @leqF x = z@ = @True@+-- [__Reflexivity__]: @leqF x x@ = @True@+-- [__Antisymmetry__]: if @leqF x y && leqF y x@ = 'True', then @testEquality x y@ = @Just Refl@+--+-- Note that the following operator interactions are expected to hold:+--+-- * @geqF x y@ iff @leqF y x@+-- * @ltF  x y@ iff @leqF x y && testEquality x y = Nothing@+-- * @gtF  x y@ iff @ltF y x@+-- * @ltF  x y@ iff @compareF x y == LTF@+-- * @gtF  x y@ iff @compareF x y == GTF@+-- * @isJust (testEquality x y)@ iff @compareF x y == EQF@+--+-- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect:+--+-- * @compareF x y == EQF@ equals @compare x y@ when @Ord (k tp)@ has an instance.+-- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance.+--+-- Minimal complete definition: either 'compareF' or 'leqF'.+-- Using 'compareF' can be more efficient for complex types. class TestEquality ktp => OrdF (ktp :: k -> *) where-  {-# MINIMAL compareF #-}+  {-# MINIMAL compareF | leqF #-} -  -- | compareF compares two keys with different type parameters.-  -- Instances must ensure that keys are only equal if the type-  -- parameters are equal.   compareF :: ktp x -> ktp y -> OrderingF x y+  compareF x y =+    case testEquality x y of+      Just Refl -> EQF+      Nothing | leqF x y -> LTF+              | otherwise -> GTF    leqF :: ktp x -> ktp y -> Bool   leqF x y =
src/Data/Parameterized/Context.hs view
@@ -205,10 +205,7 @@ pattern (:>) a v <- (viewAssign -> AssignExtend a v)   where a :> v = extend a v --- The COMPLETE pragma was not defined until ghc 8.2.*-#if MIN_VERSION_base(4,10,0) {-# COMPLETE (:>), Empty :: Assignment  #-}-#endif  -------------------------------------------------------------------------------- -- Views
src/Data/Parameterized/Context/Safe.hs view
@@ -27,6 +27,7 @@ {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}@@ -75,6 +76,8 @@   , skipIndex   , lastIndex   , nextIndex+  , leftIndex+  , rightIndex   , extendIndex   , extendIndex'   , extendIndexAppendLeft@@ -115,11 +118,6 @@ import Prelude hiding (init, map, null, replicate, succ, zipWith) import Data.Kind(Type) -#if !MIN_VERSION_base(4,8,0)-import Data.Functor-import Control.Applicative (Applicative(..))-#endif- import Data.Parameterized.Classes import Data.Parameterized.Ctx import Data.Parameterized.Some@@ -304,6 +302,17 @@ lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp lastIndex (SizeSucc s) = IndexHere s +-- | Adapts an index in the left hand context of an append operation.+leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp+leftIndex sr il = extendIndex' (appendDiff sr) il++-- | Adapts an index in the right hand context of an append operation.+rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp+rightIndex sl sr ir =+  case viewIndex sr ir of+    IndexViewInit i -> skipIndex (rightIndex sl (decSize sr) i)+    IndexViewLast s -> lastIndex (incSize (addSize sl s))+ {-# INLINE extendIndex #-} extendIndex :: KnownDiff l r => Index l tp -> Index r tp extendIndex = extendIndex' knownDiff@@ -492,12 +501,6 @@   go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')   go g (IndexHere _)     (AssignmentExtend asgn x) = AssignmentExtend (map g asgn) <$> f (g x)   go g (IndexThere idx)  (AssignmentExtend asgn x) = flip AssignmentExtend (g x)   <$> go g idx asgn-#if !MIN_VERSION_base(4,9,0)--- GHC 7.10.3 and early does not recognize that the above definition is complete,--- and so need the equation below.  GHC 8.0.1 does not require the additional--- equation.-  go _ _ _ = error "SafeTypeContext.adjustM: impossible!"-#endif  type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx type instance IxValueF (Assignment (f :: k -> Type) ctx) = f@@ -513,7 +516,7 @@ idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp idxlookup f (AssignmentExtend _   x) (IndexHere _) = f x idxlookup f (AssignmentExtend ctx _) (IndexThere idx) = idxlookup f ctx idx-idxlookup _ AssignmentEmpty _ = error "Data.Parameterized.Context.Safe.lookup: impossible case"+idxlookup _ AssignmentEmpty idx = case idx of {}  -- | Return value of assignment. (!) :: Assignment f ctx -> Index ctx tp -> f tp
src/Data/Parameterized/Context/Unsafe.hs view
@@ -47,6 +47,8 @@   , skipIndex   , lastIndex   , nextIndex+  , leftIndex+  , rightIndex   , extendIndex   , extendIndex'   , extendIndexAppendLeft@@ -264,6 +266,14 @@ lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp lastIndex n = Index (sizeInt n - 1) +-- | Adapts an index in the left hand context of an append operation.+leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp+leftIndex _ (Index il) = Index il++-- | Adapts an index in the right hand context of an append operation.+rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp+rightIndex (Size sl) _ (Index ir) = Index (sl + ir)+ {-# INLINE extendIndex #-} extendIndex :: KnownDiff l r => Index l tp -> Index r tp extendIndex = extendIndex' knownDiff@@ -282,7 +292,10 @@  -- | 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-1)@ otherwise.+-- zero, and @f (forIndex (n-1) 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@. forIndex :: forall ctx r           . Size ctx          -> (forall tp . r -> Index ctx tp -> r)@@ -394,17 +407,10 @@     Refl <- testEqualityFC test x1 y1     Refl <- testEqualityFC test x2 y2     return Refl-#if !MIN_VERSION_base(4,9,0)-  testEqualityFC _ _ _ = Nothing-#endif  instance OrdFC (BalancedTree h) where   compareFC test (BalLeaf x) (BalLeaf y) =     joinOrderingF (test x y) $ EQF-#if !MIN_VERSION_base(4,9,0)-  compareFC _ BalLeaf{} _ = LTF-  compareFC _ _ BalLeaf{} = GTF-#endif   compareFC test (BalPair x1 x2) (BalPair y1 y2) =     joinOrderingF (compareFC test x1 y1) $     joinOrderingF (compareFC test x2 y2) $@@ -518,9 +524,6 @@ bal_zipWithM f (BalPair x1 x2) (BalPair y1 y2) =   BalPair <$> bal_zipWithM f x1 (unsafeCoerce y1)           <*> bal_zipWithM f x2 (unsafeCoerce y2)-#if !MIN_VERSION_base(4,9,0)-bal_zipWithM _ _ _ = error "illegal args to bal_zipWithM"-#endif {-# INLINABLE bal_zipWithM #-}  ------------------------------------------------------------------------
src/Data/Parameterized/Map.hs view
@@ -85,6 +85,7 @@ import           Data.Kind (Type) import           Data.List (intercalate, foldl') import           Data.Monoid+import           Prelude hiding (filter, lookup, map, traverse, null)  import           Data.Parameterized.Classes import           Data.Parameterized.Some@@ -103,12 +104,6 @@   , glue   ) import qualified Data.Parameterized.Utils.BinTree as Bin--#if MIN_VERSION_base(4,8,0)-import           Prelude hiding (filter, lookup, map, traverse, null)-#else-import           Prelude hiding (filter, lookup, map, null)-#endif  ------------------------------------------------------------------------ -- * Pair
src/Data/Parameterized/NatRepr.hs view
@@ -33,9 +33,7 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-}-#if MIN_VERSION_base(4,9,0) {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}-#endif #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif
src/Data/Parameterized/Nonce.hs view
@@ -24,9 +24,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE Trustworthy #-}-#if MIN_VERSION_base(4,9,0) {-# LANGUAGE TypeInType #-}-#endif module Data.Parameterized.Nonce   ( -- * NonceGenerator     NonceGenerator@@ -58,7 +56,7 @@ import Data.Parameterized.Classes import Data.Parameterized.Some -#if MIN_VERSION_base(4,9,0) && __GLASGOW_HASKELL__ < 805+#if __GLASGOW_HASKELL__ < 805 import Data.Kind #endif @@ -70,12 +68,7 @@   STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s   IONG :: !(IORef Word64) -> NonceGenerator IO s -#if MIN_VERSION_base(4,9,0)--- We have to make the k explicit in GHC 8.0 to avoid a warning. freshNonce :: forall m s k (tp :: k) . NonceGenerator m s -> m (Nonce s tp)-#else-freshNonce :: forall m s (tp :: k) . NonceGenerator m s -> m (Nonce s tp)-#endif freshNonce (IONG r) =   atomicModifyIORef' r $ \n -> (n+1, Nonce n) freshNonce (STNG r) = do@@ -113,17 +106,17 @@                     -> a runSTNonceGenerator f = runST $ f . STNG =<< newSTRef 0 --- | Create a new nonce generator in the 'ST' monad.+-- | Create a new nonce generator in the 'IO' 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.+-- | Run an '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 f = do   Some r <- newSTNonceGenerator   f r --- | Create a new nonce generator in the 'IO' monad.+-- | Run an 'IO' computation with a new nonce generator in the 'IO' monad. withIONonceGenerator :: (forall s . NonceGenerator IO s -> IO r) -> IO r withIONonceGenerator f = do   Some r <- newIONonceGenerator
src/Data/Parameterized/Peano.hs view
@@ -34,9 +34,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -#if MIN_VERSION_base(4,9,0) {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}-#endif #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif
src/Data/Parameterized/SymbolRepr.hs view
@@ -29,20 +29,23 @@   , symbolRepr   , knownSymbol   , someSymbol+  , SomeSym(SomeSym)+  , viewSomeSym     -- * Re-exports   , type GHC.Symbol   , GHC.KnownSymbol   ) where -import GHC.TypeLits as GHC-import Unsafe.Coerce (unsafeCoerce)+import           GHC.TypeLits as GHC+import           Unsafe.Coerce (unsafeCoerce) -import Data.Hashable-import Data.Proxy+import           Data.Hashable+import           Data.Kind ( Type )+import           Data.Proxy import qualified Data.Text as Text -import Data.Parameterized.Classes-import Data.Parameterized.Some+import           Data.Parameterized.Classes+import           Data.Parameterized.Some  -- | A runtime representation of a GHC type-level symbol. newtype SymbolRepr (nm::GHC.Symbol)@@ -103,3 +106,19 @@   show (SymbolRepr nm) = Text.unpack nm  instance ShowF SymbolRepr+++-- | The SomeSym hides a Symbol parameter but preserves a+-- KnownSymbol constraint on the hidden parameter.++data SomeSym (c :: GHC.Symbol -> Type) =+  forall (s :: GHC.Symbol) . GHC.KnownSymbol s => SomeSym (c s)+++-- | Projects a value out of a SomeSym into a function, re-ifying the+-- Symbol type parameter to the called function, along with the+-- KnownSymbol constraint on that Symbol value.++viewSomeSym :: (forall (s :: GHC.Symbol) . GHC.KnownSymbol s => c s -> r) ->+               SomeSym c -> r+viewSomeSym f (SomeSym x) = f x
test/Test/Context.hs view
@@ -1,8 +1,12 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+ module Test.Context   ( contextTests   )@@ -11,22 +15,30 @@ import           Control.Lens import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as C-import qualified Data.Parameterized.Ctx.Proofs as P import qualified Data.Parameterized.Context.Safe as S import qualified Data.Parameterized.Context.Unsafe as U+import           Data.Parameterized.Ctx+import qualified Data.Parameterized.Ctx.Proofs as P 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.HUnit ( (@=?), (@?=), testCaseSteps ) import           Test.Tasty.Hedgehog +----------------------------------------------------------------------+-- Create a Payload GADT which is the parameterized type used for many+-- of the Context/Assignment tests in this module.+ data Payload (ty :: *) where   IntPayload    :: Int -> Payload Int   StringPayload :: String -> Payload String   BoolPayload   :: Bool -> Payload Bool +deriving instance Eq (Payload ty)+ instance TestEquality Payload where   testEquality (IntPayload x) (IntPayload y) = if x == y then Just Refl else Nothing   testEquality (StringPayload x) (StringPayload y) = if x == y then Just Refl else Nothing@@ -34,17 +46,45 @@   testEquality _ _ = Nothing  instance Show (Payload tp) where-  show (IntPayload x) = show x-  show (StringPayload x) = show x-  show (BoolPayload x) = show x+  show (IntPayload x) = show x <> " :: Int"+  show (StringPayload x) = show x <> " :: String"+  show (BoolPayload x) = show x <> " :: Bool"  instance ShowF Payload ++twiddle :: Payload a -> Payload a+twiddle (IntPayload n) = IntPayload (n+1)+twiddle (StringPayload str) = StringPayload (str++"asdf")+twiddle (BoolPayload b) = BoolPayload (not b)+++----------------------------------------------------------------------+-- Create another parameterized type for testing.  This one is not a+-- GADT, which will require some interesting implementation tricks.+--+-- The common 'Maybe' type is potentially useable for this type, but+-- there are some restrictions on 'Maybe'.  For example, it is not+-- possible to create a @ShowF Maybe@ because although 'Maybe' is of type+-- @(k -> type)@, @k@ is unconstrained and doesn't contain a 'Show'+-- constraint.++data MyMaybe t = (Show t) => MyJust t | MyNothing+instance ShowF MyMaybe+instance Show (MyMaybe t) where+  show (MyJust x) = "MyJust " <> show x+  show MyNothing = "MyNothing"++----------------------------------------------------------------------+-- Some Hedgehog generators+ 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 ]-                           ]+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]@@ -66,17 +106,27 @@        go a [] = Some a        go a (Some x : xs) = go (S.extend a x) xs +----------------------------------------------------------------------+-- A Ctx type that will be used for some of the Assignments tested here -twiddle :: Payload a -> Payload a-twiddle (IntPayload n) = IntPayload (n+1)-twiddle (StringPayload str) = StringPayload (str++"asdf")-twiddle (BoolPayload b) = BoolPayload (not b)+type TestCtx = U.EmptyCtx '::> Int '::> String '::> Int '::> Bool  +----------------------------------------------------------------------+ contextTests :: IO TestTree contextTests = testGroup "Context" <$> return-   [ testProperty "safe_index_eq" $ property $+   [ testProperty "size (unsafe)" $ property $      do vals <- forAll genSomePayloadList+        Some a <- return $ mkUAsgn vals+        length vals === U.sizeInt (U.size a)+   , testProperty "size (safe)" $ property $+     do vals <- forAll genSomePayloadList+        Some a <- return $ mkSAsgn vals+        length vals === S.sizeInt (S.size a)++   , 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)@@ -195,6 +245,7 @@         case P.leftId z of           Refl -> let r = C.drop U.zeroSize (U.size z) z in                     assert $ isJust $ testEquality z r+    , testProperty "take all" $ property $      do vals1 <- forAll genSomePayloadList         vals2 <- forAll genSomePayloadList@@ -215,6 +266,7 @@         let z = w U.<++> x U.<++> y         let r = C.drop (U.size z) U.zeroSize z         assert $ isJust $ testEquality U.empty r+    , testProperty "append_take" $ property $      do vals1 <- forAll genSomePayloadList         vals2 <- forAll genSomePayloadList@@ -223,6 +275,7 @@         let z = x U.<++> y         let x' = C.take (U.size x) (U.size y) z         assert $ isJust $ testEquality x x'+    , testProperty "append_take_drop" $ property $      do vals1 <- forAll genSomePayloadList         vals2 <- forAll genSomePayloadList@@ -233,6 +286,7 @@         let y' = C.drop (U.size x) (U.size y) z         assert $ isJust $ testEquality x x'         assert $ isJust $ testEquality y y'+    , testProperty "append_take_drop_multiple" $ property $      do vals1 <- forAll genSomePayloadList         vals2 <- forAll genSomePayloadList@@ -256,4 +310,163 @@         assert $ isJust $ testEquality uv uv'         assert $ isJust $ testEquality wxy wxy'         withWXY $ \t -> assert $ isJust $ testEquality wxy' t++   , testCaseSteps "explicit indexing (unsafe)" $ \step -> do+       let mkUPayload :: U.Assignment Payload TestCtx+           mkUPayload = U.empty+                        `U.extend` IntPayload 1+                        `U.extend` StringPayload "two"+                        `U.extend` IntPayload 3+                        `U.extend` BoolPayload True++           -- Alternative construction using the 'generate' and a+           -- function consuming @Index ctx tp@ selectors to return+           -- the corresponding value+           mkUMyMaybe :: U.Assignment MyMaybe TestCtx+           mkUMyMaybe = U.generate U.knownSize setMyValue+           setMyValue :: U.Index TestCtx tp -> MyMaybe tp+           setMyValue idx+             | Just Refl <- testEquality (U.lastIndex U.knownSize) idx+             = MyJust False+             | Just Refl <- testEquality (U.skipIndex $ U.skipIndex $ U.skipIndex U.baseIndex) idx+             = MyJust 10+             | Just Refl <- testEquality (U.skipIndex $ U.skipIndex $ U.nextIndex U.knownSize) idx+             = MyJust "twenty"+             | Just Refl <- testEquality (U.skipIndex $ U.nextIndex U.knownSize) idx+             = MyNothing+             | otherwise = error $ "setMyValue with unrecognized Index " <> show idx++       step "Verify size of Assignment"+       U.sizeInt (U.size mkUPayload) @?= 4++       step "Verify show of Assignment"+       "[1 :: Int, \"two\" :: String, 3 :: Int, True :: Bool]" @=? show mkUPayload+       "[MyJust 10, MyJust \"twenty\", MyNothing, MyJust False]" @=? show mkUMyMaybe++       step "Verify show explicit indexing"+       Just "\"two\" :: String" @=?+         do Some i <- U.intIndex 1 (U.size mkUPayload)+            return $ show $ mkUPayload U.! i+       Just "1 :: Int" @=?+         do Some i <- U.intIndex 0 (U.size mkUPayload)+            return $ show $ mkUPayload U.! i+       "#<; @0=1 :: Int; @1=\"two\" :: String; @2=3 :: Int; @3=True :: Bool" @=?+         U.forIndex U.knownSize+         (\s idx -> s <> "; @" <> show idx <> "=" <>+                    show (mkUPayload U.! idx))+         "#<"+       (Nothing @String) @=?+         do Some i <- U.intIndex 8 (U.size mkUPayload)+            return $ show $ mkUPayload U.! i++       step "Verify invalid type at index"+       (Nothing :: Maybe Bool) @=?+         do Some i <- U.intIndex 1 (U.size mkUPayload)+            Refl <- testEquality (mkUPayload U.! i) (IntPayload 1)+            return True++   , testCaseSteps "explicit indexing (safe)" $ \step -> do+       let mkSPayload :: S.Assignment Payload TestCtx+           mkSPayload = S.empty+                        `S.extend` IntPayload 1+                        `S.extend` StringPayload "two"+                        `S.extend` IntPayload 3+                        `S.extend` BoolPayload True++           -- Alternative construction using the 'generate' and a+           -- function consuming @Index ctx tp@ selectors to return+           -- the corresponding value+           mkSMyMaybe :: S.Assignment MyMaybe TestCtx+           mkSMyMaybe = S.generate S.knownSize setMyValue+           setMyValue :: S.Index TestCtx tp -> MyMaybe tp+           setMyValue idx+             | Just Refl <- testEquality (S.lastIndex S.knownSize) idx+             = MyJust False+             | Just Refl <- testEquality (S.skipIndex $ S.skipIndex $ S.skipIndex S.baseIndex) idx+             = MyJust 10+             | Just Refl <- testEquality (S.skipIndex $ S.skipIndex $ S.nextIndex S.knownSize) idx+             = MyJust "twenty"+             | Just Refl <- testEquality (S.skipIndex $ S.nextIndex S.knownSize) idx+             = MyNothing+             | otherwise = error $ "setMyValue with unrecognized Index " <> show idx++       step "Verify size of Assignment"+       S.sizeInt (S.size mkSPayload) @?= 4++       step "Verify show of Assignment"+       "[1 :: Int, \"two\" :: String, 3 :: Int, True :: Bool]" @=? show mkSPayload+       "[MyJust 10, MyJust \"twenty\", MyNothing, MyJust False]" @=? show mkSMyMaybe++       step "Verify show explicit indexing"+       Just "\"two\" :: String" @=?+         do Some i <- S.intIndex 1 (S.size mkSPayload)+            return $ show $ mkSPayload S.! i+       Just "1 :: Int" @=?+         do Some i <- S.intIndex 0 (S.size mkSPayload)+            return $ show $ mkSPayload S.! i+       "#<; @3=True :: Bool; @2=3 :: Int; @1=\"two\" :: String; @0=1 :: Int" @=?+         S.forIndex S.knownSize+         (\s idx -> s <> "; @" <> show idx <> "=" <>+                    show (mkSPayload S.! idx))+         "#<"+       (Nothing @String) @=?+         do Some i <- S.intIndex 8 (S.size mkSPayload)+            return $ show $ mkSPayload S.! i++       step "Verify invalid type at index"+       (Nothing :: Maybe Bool) @=?+         do Some i <- S.intIndex 1 (S.size mkSPayload)+            Refl <- testEquality (mkSPayload S.! i) (IntPayload 1)+            return True++   , testCaseSteps "joined Assigment operations (unsafe)" $ \step -> do+       let mkU1 = U.empty+                  `U.extend` IntPayload 1+           mkU2 = U.empty+                  `U.extend` StringPayload "two"+                  `U.extend` IntPayload 3+                  `U.extend` BoolPayload True++       step "Length"+       U.sizeInt (U.size mkU1) + U.sizeInt (U.size mkU2) @?=+         U.sizeInt (U.size (mkU1 U.<++> mkU2))++       step "Index adjustments"+       Just (Some i1) <- return $ U.intIndex 0 (U.size mkU1)+       v1s <- return $ show $ mkU1 U.! i1+       "1 :: Int" @=? v1s+       Just (Some i2) <- return $ U.intIndex 2 (U.size mkU2)+       v2s <- return $ show $ mkU2 U.! i2+       "True :: Bool" @=? v2s+       let mkUB = mkU1 U.<++> mkU2+       v1s' <- return $ show $ mkUB U.! (U.leftIndex (U.size mkU2) i1)+       v1s' @?= v1s+       v2s' <- return $ show $ mkUB U.! (U.rightIndex (U.size mkU1) (U.size mkU2) i2)+       v2s' @?= v2s++   , testCaseSteps "joined Assigment operations (safe)" $ \step -> do+       let mkS1 = S.empty+                  `S.extend` IntPayload 1+           mkS2 = S.empty+                  `S.extend` StringPayload "two"+                  `S.extend` IntPayload 3+                  `S.extend` BoolPayload True++       step "Length"+       S.sizeInt (S.size mkS1) + S.sizeInt (S.size mkS2) @?=+         S.sizeInt (S.size (mkS1 S.<++> mkS2))++       step "Index adjustments"+       Just (Some i1) <- return $ S.intIndex 0 (S.size mkS1)+       v1s <- return $ show $ mkS1 S.! i1+       "1 :: Int" @=? v1s+       Just (Some i2) <- return $ S.intIndex 2 (S.size mkS2)+       v2s <- return $ show $ mkS2 S.! i2+       "True :: Bool" @=? v2s+       let mkSB = mkS1 S.<++> mkS2+       v1s' <- return $ show $ mkSB S.! (S.leftIndex (S.size mkS2) i1)+       v1s' @?= v1s+       v2s' <- return $ show $ mkSB S.! (S.rightIndex (S.size mkS1) (S.size mkS2) i2)+       v2s' @?= v2s+    ]
+ test/Test/SymbolRepr.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}++module Test.SymbolRepr+  (+    symbolTests+  )+where++import           Test.Tasty+import           Test.Tasty.HUnit ( (@=?), testCase )++import           Data.Parameterized.SymbolRepr+import           GHC.TypeLits+++data Bird (name :: Symbol) where+  Jay :: String -> Bird "Jay"+  Dove :: Bird "Dove"+  Hawk :: Bird "Hawk"++symbolTests :: IO TestTree+symbolTests = testGroup "Symbol" <$> return+  [+    testCase "SomeSym" $ do+      let syms = [ SomeSym (Jay "Blue")+                 , SomeSym Dove+                 , SomeSym Hawk+                 ]+      "Dove" @=? viewSomeSym symbolVal (head (tail syms))++  ]
test/UnitTest.hs view
@@ -4,6 +4,7 @@  import qualified Test.Context import qualified Test.NatRepr+import qualified Test.SymbolRepr import qualified Test.Vector  main :: IO ()@@ -20,5 +21,6 @@ tests = testGroup "ParameterizedUtils" <$> sequence   [ Test.Context.contextTests   , Test.NatRepr.natTests+  , Test.SymbolRepr.symbolTests   , Test.Vector.vecTests   ]