diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,6 @@ +# Version 0.9 + +* Builds with GHC 9.4. + +* This library exports the `Show`, `Read`, `Eq` `Ord` and `Generic` + instances previously exported from `exinst-0.8`, as well as its tests. diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,30 @@ +Copyright (c) 2015-2018, Renzo Carbonara + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Renzo Carbonara nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +# exinst-base + +See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/exinst-base/LICENSE.txt) +file to learn about the legal terms and conditions for this library. + + diff --git a/exinst-base.cabal b/exinst-base.cabal new file mode 100644 --- /dev/null +++ b/exinst-base.cabal @@ -0,0 +1,47 @@ +name: exinst-base +version: 0.9 +author: Renzo Carbonara +maintainer: renĪ»ren!zone +copyright: Renzo Carbonara 2015 +license: BSD3 +license-file: LICENSE.txt +extra-source-files: README.md CHANGELOG.md +category: Data +build-type: Simple +cabal-version: 1.18 +synopsis: @exinst@ support for @base@ package. +homepage: https://github.com/k0001/exinst +bug-reports: https://github.com/k0001/exinst/issues + + +library + hs-source-dirs: lib + default-language: Haskell2010 + exposed-modules: Exinst.Base + build-depends: + base >=4.9 && <5.0 + , constraints + , exinst >= 0.9 + , singletons + , singletons-base + ghcjs-options: -Wall -O3 + ghc-options: -Wall -O2 + +test-suite tests + default-language: Haskell2010 + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: Main.hs + build-depends: + base + , binary + , bytestring + , deepseq + , exinst + , exinst-base + , hashable + , QuickCheck + , tasty + , tasty-quickcheck + ghcjs-options: -Wall -O0 + ghc-options: -Wall -O0 diff --git a/lib/Exinst/Base.hs b/lib/Exinst/Base.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Base.hs @@ -0,0 +1,621 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Show', 'Read', 'Eq', 'Ord' and 'Generic' instances for 'Exinst.Some1', +-- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst", provided situable +-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme +module Exinst.Base () where + +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons +import Data.Singletons.Base.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) +import Data.Bool.Singletons (SBool(STrue, SFalse)) +import qualified Data.List.Singletons as List +import Data.Tuple.Singletons (Tuple2Sym1) +import Data.Singletons.Decide +import qualified GHC.Generics as G +import Prelude +import qualified Text.Read as Read + +import Exinst hiding (Some1(..), Some2(..), Some3(..), Some4(..)) +import qualified Exinst as Exinst + +-------------------------------------------------------------------------------- +-- Show + +-- Internal wrappers used to avoid writing the string manipulation in 'Show'. +data Some1'Show r1 x = Some1 r1 x deriving (Show) +data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show) +data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show) +data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show) + +instance forall k1 (f :: k1 -> Type) + . ( SingKind k1 + , Show (Demote k1) + , Dict1 Show f + ) => Show (Exinst.Some1 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Show (f a1)) of + Dict -> showsPrec n (Some1 (fromSing sa1) x) + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , Show (Demote k2) + , Show (Demote k1) + , Dict2 Show f + ) => Show (Exinst.Some2 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of + Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x) + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Show (Demote k3) + , Show (Demote k2) + , Show (Demote k1) + , Dict3 Show f + ) => Show (Exinst.Some3 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of + Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x) + +instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Show (Demote k4) + , Show (Demote k3) + , Show (Demote k2) + , Show (Demote k1) + , Dict4 Show f + ) => Show (Exinst.Some4 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f a4 a3 a2 a1)) of + Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3) + (fromSing sa2) (fromSing sa1) x) + +-------------------------------------------------------------------------------- +-- Read + +instance forall k1 (f :: k1 -> Type) + . ( SingKind k1 + , Read (Demote k1) + , Dict1 Read f + ) => Read (Exinst.Some1 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some1" <- Read.lexP + rsa1 <- Read.readPrec + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Read (f a1)) of + Dict -> do + x :: f a1 <- Read.readPrec + pure (Exinst.Some1 sa1 x) + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , Read (Demote k2) + , Read (Demote k1) + , Dict2 Read f + ) => Read (Exinst.Some2 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some2" <- Read.lexP + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Read (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Read.readPrec + pure (Exinst.Some2 sa2 sa1 x) + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Read (Demote k3) + , Read (Demote k2) + , Read (Demote k1) + , Dict3 Read f + ) => Read (Exinst.Some3 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some3" <- Read.lexP + rsa3 <- Read.readPrec + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Read (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Read.readPrec + pure (Exinst.Some3 sa3 sa2 sa1 x) + +instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Read (Demote k4) + , Read (Demote k3) + , Read (Demote k2) + , Read (Demote k1) + , Dict4 Read f + ) => Read (Exinst.Some4 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some4" <- Read.lexP + rsa4 <- Read.readPrec + rsa3 <- Read.readPrec + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Read (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Read.readPrec + pure (Exinst.Some4 sa4 sa3 sa2 sa1 x) + +-------------------------------------------------------------------------------- +-- Eq + +instance forall k1 (f :: k1 -> Type). + ( SDecide k1 + , Dict1 Eq f + ) => Eq (Exinst.Some1 f) + where + {-# INLINABLE (==) #-} + (==) = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f a1x) -> + withSome1Sing som1y $ \sa1y (y :: f a1y) -> + maybe False id $ do + Refl <- decideEquality sa1x sa1y + case dict1 sa1x :: Dict (Eq (f a1x)) of + Dict -> Just (x == y) + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SDecide k2 + , SDecide k1 + , Dict2 Eq f + ) => Eq (Exinst.Some2 f) + where + {-# INLINABLE (==) #-} + (==) = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> + maybe False id $ do + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of + Dict -> Just (x == y) + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SDecide k3 + , SDecide k2 + , SDecide k1 + , Dict3 Eq f + ) => Eq (Exinst.Some3 f) + where + {-# INLINABLE (==) #-} + (==) = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> + maybe False id $ do + Refl <- decideEquality sa3x sa3y + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of + Dict -> Just (x == y) + +instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SDecide k4 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Dict4 Eq f + ) => Eq (Exinst.Some4 f) + where + {-# INLINABLE (==) #-} + (==) = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> + maybe False id $ do + Refl <- decideEquality sa4x sa4y + Refl <- decideEquality sa3x sa3y + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of + Dict -> Just (x == y) + +-------------------------------------------------------------------------------- +-- Ord + +instance forall k1 (f :: k1 -> Type) + . ( SingKind k1 + , SDecide k1 + , Ord (Demote k1) + , Dict1 Ord f + , Eq (Exinst.Some1 f) + ) => Ord (Exinst.Some1 f) + where + {-# INLINABLE compare #-} + compare = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f a1x) -> + withSome1Sing som1y $ \sa1y (y :: f a1y) -> + let termCompare = compare (fromSing sa1x) (fromSing sa1y) + in maybe termCompare id $ do + Refl <- decideEquality sa1x sa1y + case dict1 sa1x :: Dict (Ord (f a1x)) of + Dict -> Just (compare x y) + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , SDecide k2 + , SDecide k1 + , Ord (Demote k2) + , Ord (Demote k1) + , Dict2 Ord f + , Eq (Exinst.Some2 f) + ) => Ord (Exinst.Some2 f) + where + {-# INLINABLE compare #-} + compare = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> + let termCompare = compare (fromSing sa2x, fromSing sa1x) + (fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of + Dict -> Just (compare x y) + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Ord (Demote k3) + , Ord (Demote k2) + , Ord (Demote k1) + , Dict3 Ord f + , Eq (Exinst.Some3 f) + ) => Ord (Exinst.Some3 f) + where + {-# INLINABLE compare #-} + compare = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> + let termCompare = compare + (fromSing sa3x, fromSing sa2x, fromSing sa1x) + (fromSing sa3y, fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- decideEquality sa3x sa3y + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of + Dict -> Just (compare x y) + +instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , SDecide k4 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Ord (Demote k4) + , Ord (Demote k3) + , Ord (Demote k2) + , Ord (Demote k1) + , Dict4 Ord f + , Eq (Exinst.Some4 f) + ) => Ord (Exinst.Some4 f) + where + {-# INLINABLE compare #-} + compare = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> + let termCompare = compare + (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x) + (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- decideEquality sa4x sa4y + Refl <- decideEquality sa3x sa3y + Refl <- decideEquality sa2x sa2y + Refl <- decideEquality sa1x sa1y + case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of + Dict -> Just (compare x y) + +-------------------------------------------------------------------------------- +-- Generic + +type Eithers1 (f :: k1 -> Type) = + Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where + Eithers1' (x ': '[]) f = f x + Eithers1' (x ': xs) f = Either (f x) (Eithers1' xs f) + +instance forall k1 (f :: k1 -> Type) + . ( SingKind k1 + , PEnum (Demote k1) + , PBounded (Demote k1) + , G.Generic (Demote k1) + , Dict1 G.Generic f + , Dict1 (Inj (Eithers1 f)) f + ) => G.Generic (Exinst.Some1 f) + where + type Rep (Exinst.Some1 (f :: k1 -> Type)) = + G.Rep (Demote k1, Eithers1 f) + {-# INLINABLE from #-} + from = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (G.Generic (f a1)) of + Dict -> case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of + Dict -> G.from (fromSing sa1, inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 da1) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some1 sa1 (x :: f a1) + Nothing -> error "Generic Some1: Malformed Rep" + +--- +type Eithers2 (f :: k2 -> k1 -> Type) = + Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where + Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1 + Eithers2' ( '(x2, x1) ': xs) f = Either (f x2 x1) (Eithers2' xs f) + +type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where + Cartesian2 '[] xs1 = '[] + Cartesian2 (x2 ': xs2) xs1 = + List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1] + + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict2 G.Generic f + , Dict2 (Inj (Eithers2 f)) f + ) => G.Generic (Exinst.Some2 f) + where + type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) = + G.Rep ((Demote k2, Demote k1), Eithers2 f) + {-# INLINABLE from #-} + from = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (G.Generic (f a2 a1)) of + Dict -> case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of + Dict -> G.from ((fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some2 sa2 sa1 (x :: f a2 a1) + Nothing -> error "Generic Some2: Malformed Rep" + + +--- +type Eithers3 (f :: k3 -> k2 -> k1 -> Type) = + Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) + (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where + Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1 + Eithers3' ( '(x3, '(x2, x1)) ': xs) f = Either (f x3 x2 x1) (Eithers3' xs f) + +-- | We use nested 2-tuples instead of 3-tuples because it's easier to implement. +type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where + Cartesian3 '[] xs2 xs1 = '[] + Cartesian3 (x3 ': xs3) xs2 xs1 = + List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1) + , Cartesian3 xs3 xs2 xs1 ] + + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , PEnum (Demote k3) + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k3) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k3) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict3 G.Generic f + , Dict3 (Inj (Eithers3 f)) f + ) => G.Generic (Exinst.Some3 f) + where + type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) = + G.Rep ((Demote k3, Demote k2, Demote k1), Eithers3 f) + {-# INLINABLE from #-} + from = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (G.Generic (f a3 a2 a1)) of + Dict -> case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of + Dict -> G.from ((fromSing sa3, fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some3 sa3 sa2 sa1 (x :: f a3 a2 a1) + Nothing -> error "Generic Some3: Malformed Rep" + + +--- +type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) = + Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4)) + (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) + (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where + Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1 + Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs) f = Either (f x4 x3 x2 x1) (Eithers4' xs f) + +-- | We use nested 2-tuples instead of 4-tuples because it's easier to implement. +type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where + Cartesian4 '[] xs3 xs2 xs1 = '[] + Cartesian4 (x4 ': xs4) xs3 xs2 xs1 = + List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1) + , Cartesian4 xs4 xs3 xs2 xs1 ] + + +instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , PEnum (Demote k4) + , PEnum (Demote k3) + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k4) + , PBounded (Demote k3) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k4) + , G.Generic (Demote k3) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict4 G.Generic f + , Dict4 (Inj (Eithers4 f)) f + ) => G.Generic (Exinst.Some4 f) + where + type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) = + G.Rep ((Demote k4, Demote k3, Demote k2, Demote k1), Eithers4 f) + {-# INLINABLE from #-} + from = \s4x -> withSome4Sing s4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of + Dict -> case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of + Dict -> G.from ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da4, da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some4 sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) + Nothing -> error "Generic Some4: Malformed Rep" + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +-- Out of the box 'DictX' instances for some @base@ types + +instance forall c. + (c 'False, c 'True + ) => Dict0 (c :: Bool -> Constraint) where + {-# INLINABLE dict0 #-} + dict0 = \case { SFalse -> Dict; STrue -> Dict } + +instance forall k0 c f. + ( c (f 'False), c (f 'True) + ) => Dict1 c (f :: Bool -> k0) where + {-# INLINABLE dict1 #-} + dict1 = \case { SFalse -> Dict; STrue -> Dict } + +instance forall k1 k0 c f. + ( Dict1 c (f 'False), Dict1 c (f 'True) + ) => Dict2 c (f :: Bool -> k1 -> k0) where + {-# INLINABLE dict2 #-} + dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 } + +instance forall k2 k1 k0 c f. + ( Dict2 c (f 'False), Dict2 c (f 'True) + ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where + {-# INLINABLE dict3 #-} + dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 } + +instance forall k3 k2 k1 k0 c f. + ( Dict3 c (f 'False), Dict3 c (f 'True) + ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where + {-# INLINABLE dict4 #-} + dict4 = \x -> case x of { SFalse -> dict3; STrue -> dict3 } + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +-- Misc + +class Inj b a where + inj :: a -> b + prj :: b -> Maybe a +instance Inj a a where + {-# INLINE inj #-} + inj = id + {-# INLINE prj #-} + prj = Just +instance Inj (Either a b) a where + {-# INLINE inj #-} + inj = Left + {-# INLINE prj #-} + prj = either Just (const Nothing) +-- | TODO: Make this logarithmic. +instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where + {-# INLINE inj #-} + inj = Right . inj + {-# INLINE prj #-} + prj = either (const Nothing) prj + diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,268 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} + +module Main where + +import Control.DeepSeq (NFData(rnf)) +import qualified Data.Binary as Bin +import qualified Data.ByteString.Lazy as BSL +import Data.Hashable (Hashable(hash)) +import Data.Int (Int32) +import Data.Kind (Type) +import qualified GHC.Generics as G +import qualified Test.Tasty as Tasty +import qualified Test.Tasty.Runners as Tasty +import Test.Tasty.QuickCheck ((===)) +import qualified Test.Tasty.QuickCheck as QC +import Text.Read (readMaybe) + +import Exinst +import Exinst.Base () + +-------------------------------------------------------------------------------- + +main :: IO () +main = Tasty.defaultMainWithIngredients + [ Tasty.consoleTestReporter + , Tasty.listingTests + ] tt + +-------------------------------------------------------------------------------- + +data family X1 :: Bool -> Type +data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) + +data family X2 :: Bool -> Bool -> Type +data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) + +data family X3 :: Bool -> Bool -> Bool -> Type +data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) + +data family X4 :: Bool -> Bool -> Bool -> Bool -> Type +data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) +data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData) + +#define INSTANCETRON(c) \ + instance c (X1 'False); \ + instance c (X1 'True); \ + instance c (X2 'False 'False); \ + instance c (X2 'False 'True); \ + instance c (X2 'True 'False); \ + instance c (X2 'True 'True); \ + instance c (X3 'False 'False 'False); \ + instance c (X3 'False 'False 'True); \ + instance c (X3 'False 'True 'False); \ + instance c (X3 'False 'True 'True); \ + instance c (X3 'True 'False 'False); \ + instance c (X3 'True 'False 'True); \ + instance c (X3 'True 'True 'False); \ + instance c (X3 'True 'True 'True); \ + instance c (X4 'False 'False 'False 'False); \ + instance c (X4 'False 'False 'False 'True); \ + instance c (X4 'False 'False 'True 'False); \ + instance c (X4 'False 'False 'True 'True); \ + instance c (X4 'False 'True 'False 'False); \ + instance c (X4 'False 'True 'False 'True); \ + instance c (X4 'False 'True 'True 'False); \ + instance c (X4 'False 'True 'True 'True); \ + instance c (X4 'True 'False 'False 'False); \ + instance c (X4 'True 'False 'False 'True); \ + instance c (X4 'True 'False 'True 'False); \ + instance c (X4 'True 'False 'True 'True); \ + instance c (X4 'True 'True 'False 'False); \ + instance c (X4 'True 'True 'False 'True); \ + instance c (X4 'True 'True 'True 'False); \ + instance c (X4 'True 'True 'True 'True) + +-------------------------------------------------------------------------------- +-- Arbitrary instances + +instance QC.Arbitrary (X1 'False) where arbitrary = QC.oneof [ pure XF1, fmap XF2 QC.arbitrary ] +instance QC.Arbitrary (X1 'True) where arbitrary = QC.oneof [ pure XT1, fmap XT2 QC.arbitrary ] + +instance QC.Arbitrary (X2 'False 'False) where arbitrary = QC.oneof [ pure XFF1, fmap XFF2 QC.arbitrary ] +instance QC.Arbitrary (X2 'False 'True) where arbitrary = QC.oneof [ pure XFT1, fmap XFT2 QC.arbitrary ] +instance QC.Arbitrary (X2 'True 'False) where arbitrary = QC.oneof [ pure XTF1, fmap XTF2 QC.arbitrary ] +instance QC.Arbitrary (X2 'True 'True) where arbitrary = QC.oneof [ pure XTT1, fmap XTT2 QC.arbitrary ] + +instance QC.Arbitrary (X3 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFF1, fmap XFFF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFT1, fmap XFFT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'True 'False) where arbitrary = QC.oneof [ pure XFTF1, fmap XFTF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'True 'True) where arbitrary = QC.oneof [ pure XFTT1, fmap XFTT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'False 'False) where arbitrary = QC.oneof [ pure XTFF1, fmap XTFF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'False 'True) where arbitrary = QC.oneof [ pure XTFT1, fmap XTFT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTF1, fmap XTTF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTT1, fmap XTTT2 QC.arbitrary ] + +instance QC.Arbitrary (X4 'False 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFFF1, fmap XFFFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFFT1, fmap XFFFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'True 'False) where arbitrary = QC.oneof [ pure XFFTF1, fmap XFFTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'True 'True) where arbitrary = QC.oneof [ pure XFFTT1, fmap XFFTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'False 'False) where arbitrary = QC.oneof [ pure XFTFF1, fmap XFTFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'False 'True) where arbitrary = QC.oneof [ pure XFTFT1, fmap XFTFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'True 'False) where arbitrary = QC.oneof [ pure XFTTF1, fmap XFTTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'True 'True) where arbitrary = QC.oneof [ pure XFTTT1, fmap XFTTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'False 'False) where arbitrary = QC.oneof [ pure XTFFF1, fmap XTFFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'False 'True) where arbitrary = QC.oneof [ pure XTFFT1, fmap XTFFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'True 'False) where arbitrary = QC.oneof [ pure XTFTF1, fmap XTFTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'True 'True) where arbitrary = QC.oneof [ pure XTFTT1, fmap XTFTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'False 'False) where arbitrary = QC.oneof [ pure XTTFF1, fmap XTTFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'False 'True) where arbitrary = QC.oneof [ pure XTTFT1, fmap XTTFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTTF1, fmap XTTTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTTT1, fmap XTTTT2 QC.arbitrary ] + +-------------------------------------------------------------------------------- + +tt :: Tasty.TestTree +tt = + Tasty.testGroup "main" + [ tt_nfdata + , tt_id "Identity through Show/Read" id_show_read + , tt_id "Identity through GHC's Generic" id_generic + , tt_id "Identity through Binary's Binary" id_binary + ] + +type MegaCtx a = + ( G.Generic a + , Show a + , Read a + , Hashable a + , Bin.Binary a + ) + +tt_id + :: String + -> (forall a. MegaCtx a => a -> Maybe a) + -- ^ It's easier to put all the constraints here in the 'MegaCtx' monster. + -> Tasty.TestTree +tt_id = \title id' -> Tasty.testGroup title + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> Just x === id' x + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> Just x === id' x + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> Just x === id' x + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> Just x === id' x + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> Just x === id' x + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> Just x === id' x + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> Just x === id' x + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> Just x === id' x + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> Just x === id' x + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> Just x === id' x + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> Just x === id' x + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> Just x === id' x + ] + +tt_nfdata :: Tasty.TestTree +tt_nfdata = Tasty.testGroup "NFData" + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === rnf x + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === rnf x + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === rnf x + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === rnf x + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === rnf x + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === rnf x + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === rnf x + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === rnf x + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === rnf x + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === rnf x + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === rnf x + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === rnf x + ] + +INSTANCETRON(Hashable) + +tt_hashable :: Tasty.TestTree +tt_hashable = Tasty.testGroup "Hashable" + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === (hash x `seq` ()) + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === (hash x `seq` ()) + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === (hash x `seq` ()) + ] + +-------------------------------------------------------------------------------- + +id_show_read :: (Show a, Read a) => a -> Maybe a +id_show_read = readMaybe . show + +id_generic :: G.Generic a => a -> Maybe a +id_generic = Just . G.to . G.from + +id_binary :: Bin.Binary a => a -> Maybe a +id_binary = \a -> + case Bin.decodeOrFail (Bin.encode a) of + Right (z,_,a') | BSL.null z -> Just a' + _ -> Nothing +