diff --git a/Changelog.md b/Changelog.md --- a/Changelog.md +++ b/Changelog.md @@ -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. diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal --- a/parameterized-utils.cabal +++ b/parameterized-utils.cabal @@ -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 diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs --- a/src/Data/Parameterized/Classes.hs +++ b/src/Data/Parameterized/Classes.hs @@ -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 = diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs --- a/src/Data/Parameterized/Context.hs +++ b/src/Data/Parameterized/Context.hs @@ -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 diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs --- a/src/Data/Parameterized/Context/Safe.hs +++ b/src/Data/Parameterized/Context/Safe.hs @@ -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 diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs --- a/src/Data/Parameterized/Context/Unsafe.hs +++ b/src/Data/Parameterized/Context/Unsafe.hs @@ -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 #-} ------------------------------------------------------------------------ diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs --- a/src/Data/Parameterized/Map.hs +++ b/src/Data/Parameterized/Map.hs @@ -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 diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs --- a/src/Data/Parameterized/NatRepr.hs +++ b/src/Data/Parameterized/NatRepr.hs @@ -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 diff --git a/src/Data/Parameterized/Nonce.hs b/src/Data/Parameterized/Nonce.hs --- a/src/Data/Parameterized/Nonce.hs +++ b/src/Data/Parameterized/Nonce.hs @@ -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 diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs --- a/src/Data/Parameterized/Peano.hs +++ b/src/Data/Parameterized/Peano.hs @@ -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 diff --git a/src/Data/Parameterized/SymbolRepr.hs b/src/Data/Parameterized/SymbolRepr.hs --- a/src/Data/Parameterized/SymbolRepr.hs +++ b/src/Data/Parameterized/SymbolRepr.hs @@ -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 diff --git a/test/Test/Context.hs b/test/Test/Context.hs --- a/test/Test/Context.hs +++ b/test/Test/Context.hs @@ -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 + ] diff --git a/test/Test/SymbolRepr.hs b/test/Test/SymbolRepr.hs new file mode 100644 --- /dev/null +++ b/test/Test/SymbolRepr.hs @@ -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)) + + ] diff --git a/test/UnitTest.hs b/test/UnitTest.hs --- a/test/UnitTest.hs +++ b/test/UnitTest.hs @@ -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 ]