diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,14 @@ +# Version 0.7 + +* BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: All of the cabal flags + for turning on and off instances were removed. The `hashable` are now + always exported from the `exinst`, and the `aeson`, `bytes`, + `cereal` and `serialise` instances are now exported from new + packages `exinst-aeson`, `exinst-bytes`, `exinst-cereal` and + `exinst-serialise`. The instances exported from those packages are + the same as the ones exported with `exinst-0.6`. + + # Version 0.6 * The `binary` and `deepseq` Cabal flags were removed since these two packages diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,11 +1,9 @@ # exinst -[![Build Status](https://travis-ci.org/k0001/exinst.svg?branch=master)](https://travis-ci.org/k0001/exinst) - -See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt) +See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/exinst/LICENSE.txt) file to learn about the legal terms and conditions for this library. Find documentation for this library in the top-level -[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/src/lib/Exinst.hs) +[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/lib/Exinst.hs) module. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,4 +1,2 @@ -#! /usr/bin/env nix-shell -#! nix-shell ./shell.nix -i runghc import Distribution.Simple main = defaultMain diff --git a/exinst.cabal b/exinst.cabal --- a/exinst.cabal +++ b/exinst.cabal @@ -1,5 +1,5 @@ name: exinst -version: 0.6 +version: 0.7 author: Renzo Carbonara maintainer: renzoλcarbonara.com.ar copyright: Renzo Carbonara 2015-2018 @@ -23,48 +23,40 @@ Exinst.Internal Exinst.Internal.Product Exinst.Internal.Sum - Exinst.Instances.Base - Exinst.Instances.Binary - Exinst.Instances.DeepSeq + Exinst.Base + Exinst.Binary + Exinst.DeepSeq + Exinst.Hashable + Exinst.QuickCheck build-depends: base >=4.9 && <5.0 , binary , constraints >=0.4 , deepseq + , hashable , profunctors >=5.0 , singletons >=2.3.1 + , QuickCheck ghcjs-options: -Wall -O3 ghc-options: -Wall -O2 - if flag(aeson) - build-depends: aeson - other-modules: Exinst.Instances.Aeson - cpp-options: -DHAS_aeson - if flag(bytes) - build-depends: bytes >=0.15 - other-modules: Exinst.Instances.Bytes - cpp-options: -DHAS_bytes - if flag(cereal) || flag(bytes) - build-depends: cereal - other-modules: Exinst.Instances.Cereal - cpp-options: -DHAS_cereal - if flag(hashable) - build-depends: hashable - other-modules: Exinst.Instances.Hashable - cpp-options: -DHAS_hashable - if flag(quickcheck) - build-depends: QuickCheck - other-modules: Exinst.Instances.QuickCheck - cpp-options: -DHAS_quickcheck - if flag(serialise) - build-depends: cborg, serialise - other-modules: Exinst.Instances.Serialise - cpp-options: -DHAS_serialise +-- if flag(bytes) +-- build-depends: bytes >=0.15 +-- other-modules: Exinst.Instances.Bytes +-- cpp-options: -DHAS_bytes +-- if flag(cereal) || flag(bytes) +-- build-depends: cereal +-- other-modules: Exinst.Instances.Cereal +-- cpp-options: -DHAS_cereal +-- if flag(serialise) +-- build-depends: cborg, serialise +-- other-modules: Exinst.Instances.Serialise +-- cpp-options: -DHAS_serialise test-suite tests default-language: Haskell2010 type: exitcode-stdio-1.0 - hs-source-dirs: tests lib + hs-source-dirs: tests main-is: Main.hs build-depends: base @@ -72,6 +64,8 @@ , bytestring , constraints , deepseq + , exinst + , hashable , profunctors , QuickCheck , singletons @@ -80,45 +74,38 @@ , tasty-quickcheck ghcjs-options: -Wall -O0 ghc-options: -Wall -O0 - cpp-options: - -DHAS_quickcheck - if flag(aeson) - build-depends: aeson - cpp-options: -DHAS_aeson - if flag(bytes) - build-depends: bytes - cpp-options: -DHAS_bytes - if flag(cereal) || flag(bytes) - build-depends: cereal - cpp-options: -DHAS_cereal - if flag(hashable) - build-depends: hashable - cpp-options: -DHAS_hashable - if flag(serialise) - build-depends: cborg, serialise - cpp-options: -DHAS_serialise - -flag aeson - description: Provide instances for @aeson@ - default: True - manual: True -flag bytes - description: Provide instances for @bytes@ (implies @ceral@ and @binary@). - default: True - manual: True -flag cereal - description: Provide instances for @cereal@. - default: True - manual: True -flag hashable - description: Provide instances for @hashable@ - default: True - manual: True -flag quickcheck - description: Provide instances for @QuickCheck@ - default: True - manual: True -flag serialise - description: Provide instances for @serialise@ - default: True - manual: True +-- cpp-options: +-- -DHAS_quickcheck +-- if flag(bytes) +-- build-depends: bytes +-- cpp-options: -DHAS_bytes +-- if flag(cereal) || flag(bytes) +-- build-depends: cereal +-- cpp-options: -DHAS_cereal +-- if flag(hashable) +-- build-depends: hashable +-- cpp-options: -DHAS_hashable +-- if flag(serialise) +-- build-depends: cborg, serialise +-- cpp-options: -DHAS_serialise +-- +-- flag bytes +-- description: Provide instances for @bytes@ (implies @ceral@ and @binary@). +-- default: True +-- manual: True +-- flag cereal +-- description: Provide instances for @cereal@. +-- default: True +-- manual: True +-- flag hashable +-- description: Provide instances for @hashable@ +-- default: True +-- manual: True +-- flag quickcheck +-- description: Provide instances for @QuickCheck@ +-- default: True +-- manual: True +-- flag serialise +-- description: Provide instances for @serialise@ +-- default: True +-- manual: True diff --git a/lib/Exinst.hs b/lib/Exinst.hs --- a/lib/Exinst.hs +++ b/lib/Exinst.hs @@ -117,34 +117,11 @@ import Exinst.Internal.Product import Exinst.Internal.Sum -import Exinst.Instances.Base () -import Exinst.Instances.Binary () -import Exinst.Instances.DeepSeq () - -#ifdef HAS_aeson -import Exinst.Instances.Aeson () -#endif - -#ifdef HAS_bytes -import Exinst.Instances.Bytes () -#endif - -#ifdef HAS_cereal -import Exinst.Instances.Cereal () -#endif - -#ifdef HAS_hashable -import Exinst.Instances.Hashable () -#endif - -#ifdef HAS_quickcheck -import Exinst.Instances.QuickCheck () -#endif - -#ifdef HAS_serialise -import Exinst.Instances.Serialise () -#endif - +import Exinst.Base () +import Exinst.Binary () +import Exinst.DeepSeq () +import Exinst.Hashable () +import Exinst.QuickCheck () {- $motivation @@ -404,12 +381,6 @@ * 'Eq', 'Ord', 'Show' from the @base@ package. -* 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ package. - -* 'Data.Bytes.Serial' from the @bytes@ package. - -* 'Cereal.Serialize.Serialize' from the @cereal@ package. - * 'Data.Binary.Binary' from the @binary@ package. * 'Data.Hashable.Hashable' from the @hashable@ package. @@ -417,6 +388,23 @@ * 'Control.DeepSeq.NFData' from the @deepseq@ package. * 'Test.QuickCheck.Arbitrary' from the @QuickCheck@ package. + +Furthermore, other libraries export other orphan instances for the datatypes +exported by 'exinst': + +* [exinst-aeson](https://hackage.haskell.org/package/exinst-aeson) exports +instances for 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ +package. + +* [exinst-bytes](https://hackage.haskell.org/package/exinst-bytes) exports +instances for 'Data.Bytes.Serial' from the @bytes@ package. + +* [exinst-cereal](https://hackage.haskell.org/package/exinst-cereal) exports +instances for 'Cereal.Serialize.Serialize' from the @cereal@ package. + +* [exinst-serialise](https://hackage.haskell.org/package/exinst-serialise) +exports instances for 'Codec.Serialise.Serialise' from the @serialise@ package. + You are invited to read the instance heads for said instances so as to understand what you need to provide in order to get those instances “for free”. As a rule of 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,622 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# 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', 'Eq' and 'Ord' 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.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) +import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse)) +import qualified Data.Singletons.Prelude.List as List +import Data.Singletons.Prelude.Tuple (Tuple2Sym1) +import Data.Singletons.Decide +import Data.Type.Equality +import qualified GHC.Generics as G +import Prelude +import qualified Text.Read as Read + +import Exinst.Internal + hiding (Some1(..), Some2(..), Some3(..), Some4(..)) +import qualified Exinst.Internal 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 <- testEquality sa1x sa1y + case dict1 sa1x :: Dict (Eq (f a1x)) of + Dict -> Just (x == y) + +instance forall (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 <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of + Dict -> Just (x == y) + +instance forall (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 <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of + Dict -> Just (x == y) + +instance forall (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 <- testEquality sa4x sa4y + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of + Dict -> Just (x == y) + +-------------------------------------------------------------------------------- +-- Ord + +instance forall (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 <- testEquality sa1x sa1y + case dict1 sa1x :: Dict (Ord (f a1x)) of + Dict -> Just (compare x y) + +instance forall (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 <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of + Dict -> Just (compare x y) + +instance forall (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 <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of + Dict -> Just (compare x y) + +instance forall (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 <- testEquality sa4x sa4y + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality 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 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 + (c 'False, c 'True + ) => Dict0 (c :: Bool -> Constraint) where + {-# INLINABLE dict0 #-} + dict0 = \case { SFalse -> Dict; STrue -> Dict } + +instance + ( c (f 'False), c (f 'True) + ) => Dict1 c (f :: Bool -> k0) where + {-# INLINABLE dict1 #-} + dict1 = \case { SFalse -> Dict; STrue -> Dict } + +instance + ( 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 + ( 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 + ( 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/lib/Exinst/Binary.hs b/lib/Exinst/Binary.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Binary.hs @@ -0,0 +1,155 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Bin.Binary' instances for 'Some1', 'Some2', 'Some3' +-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', +-- 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Binary () where + +import qualified Data.Binary as Bin +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons +import Prelude + +import Exinst.Internal +import Exinst.Internal.Sum +import Exinst.Internal.Product + +-------------------------------------------------------------------------------- + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k1 -> Type). + ( SingKind k1 + , Bin.Binary (Demote k1) + , Dict1 Bin.Binary f + ) => Bin.Binary (Some1 f) where + {-# INLINABLE put #-} + put = \some1x -> + withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Bin.Binary (f a1)) of + Dict -> do + Bin.put (fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + rsa1 <- Bin.get + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Bin.Binary (f a1)) of + Dict -> do + x :: f a1 <- Bin.get + pure (Some1 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k2 -> k1 -> Type). + ( SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict2 Bin.Binary f + ) => Bin.Binary (Some2 f) where + {-# INLINABLE put #-} + put = \some2x -> + withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of + Dict -> do + Bin.put (fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa2, rsa1) <- Bin.get + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Bin.get + pure (Some2 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k3 -> k2 -> k1 -> Type). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k3) + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict3 Bin.Binary f + ) => Bin.Binary (Some3 f) where + {-# INLINABLE put #-} + put = \some3x -> + withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of + Dict -> do + Bin.put (fromSing sa3, fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa3, rsa2, rsa1) <- Bin.get + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Bin.get + pure (Some3 sa3 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k4) + , Bin.Binary (Demote k3) + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict4 Bin.Binary f + ) => Bin.Binary (Some4 f) where + {-# INLINABLE put #-} + put = \some4x -> + withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of + Dict -> do + Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa4, rsa3, rsa2, rsa1) <- Bin.get + 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 (Bin.Binary (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Bin.get + pure (Some4 sa4 sa3 sa2 sa1 x) + +-------------------------------------------------------------------------------- + +instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1) +instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1) +instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1) +instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1) + +-------------------------------------------------------------------------------- + +instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1) +instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1) +instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1) +instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1) diff --git a/lib/Exinst/DeepSeq.hs b/lib/Exinst/DeepSeq.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/DeepSeq.hs @@ -0,0 +1,76 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and +-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' +-- and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.DeepSeq () where + +import Control.DeepSeq (NFData(rnf)) +import Data.Constraint +import Prelude + +import Exinst.Internal +import Exinst.Internal.Sum +import Exinst.Internal.Product + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *). + ( Dict1 NFData f + ) => NFData (Some1 f) where + {-# INLINABLE rnf #-} + rnf = \(!some1x) -> + withSome1Sing some1x $ \ !sa1 !(x :: f a1) -> + case dict1 sa1 :: Dict (NFData (f a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k2 -> k1 -> *). + ( Dict2 NFData f + ) => NFData (Some2 f) where + {-# INLINABLE rnf #-} + rnf = \(!some2x) -> + withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k3 -> k2 -> k1 -> *). + ( Dict3 NFData f + ) => NFData (Some3 f) where + {-# INLINABLE rnf #-} + rnf = \(!some3x) -> + withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). + ( Dict4 NFData f + ) => NFData (Some4 f) where + {-# INLINABLE rnf #-} + rnf = \(!some4x) -> + withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of + Dict -> rnf x `seq` () + +-------------------------------------------------------------------------------- + +instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1) +instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1) +instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1) +instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1) + +-------------------------------------------------------------------------------- + +instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1) +instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1) +instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1) +instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1) + diff --git a/lib/Exinst/Hashable.hs b/lib/Exinst/Hashable.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Hashable.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and +-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' +-- and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Hashable () where + +import Data.Hashable (Hashable(hashWithSalt)) +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons +import Prelude + +import Exinst.Internal +import Exinst.Internal.Sum +import Exinst.Internal.Product + +-------------------------------------------------------------------------------- + +-- | Some salt we add to hashes calculated in this module. +salt0 :: Int +salt0 = 6700417 + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> Type) + . ( SingKind k1 + , Hashable (Demote k1) + , Dict1 Hashable f + ) => Hashable (Some1 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Hashable (f a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict2 Hashable f + ) => Hashable (Some2 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Hashable (Demote k3) + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict3 Hashable f + ) => Hashable (Some3 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa3 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Hashable (Demote k4) + , Hashable (Demote k3) + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict4 Hashable f + ) => Hashable (Some4 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa4 + `hashWithSalt` fromSing sa3 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +-------------------------------------------------------------------------------- + +instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1) +instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1) +instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1) +instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1) + +-------------------------------------------------------------------------------- + +instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1) +instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1) +instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1) +instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1) + diff --git a/lib/Exinst/Instances/Aeson.hs b/lib/Exinst/Instances/Aeson.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Aeson.hs +++ /dev/null @@ -1,161 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Ae.FromJSON' and 'Ae.ToJSON' instances for 'Some1', --- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable --- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Aeson () where - -import qualified Data.Aeson as Ae -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Ae.ToJSON (Demote k1) - , Dict1 Ae.ToJSON f - ) => Ae.ToJSON (Some1 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Ae.ToJSON (f a1)) of - Dict -> Ae.toJSON (fromSing sa1, x) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Ae.ToJSON (Demote k2) - , Ae.ToJSON (Demote k1) - , Dict2 Ae.ToJSON f - ) => Ae.ToJSON (Some2 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.ToJSON (Demote k3) - , Ae.ToJSON (Demote k2) - , Ae.ToJSON (Demote k1) - , Dict3 Ae.ToJSON f - ) => Ae.ToJSON (Some3 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.ToJSON (Demote k4) - , Ae.ToJSON (Demote k3) - , Ae.ToJSON (Demote k2) - , Ae.ToJSON (Demote k1) - , Dict4 Ae.ToJSON f - ) => Ae.ToJSON (Some4 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x) - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Ae.FromJSON (Demote k1) - , Dict1 Ae.FromJSON f - ) => Ae.FromJSON (Some1 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - (rsa1, v') <- Ae.parseJSON v - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of - Dict -> do - x :: f a1 <- Ae.parseJSON v' - pure (Some1 sa1 x) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Ae.FromJSON (Demote k2) - , Ae.FromJSON (Demote k1) - , Dict2 Ae.FromJSON f - ) => Ae.FromJSON (Some2 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa2, rsa1), v') <- Ae.parseJSON v - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Ae.parseJSON v' - pure (Some2 sa2 sa1 x) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.FromJSON (Demote k3) - , Ae.FromJSON (Demote k2) - , Ae.FromJSON (Demote k1) - , Dict3 Ae.FromJSON f - ) => Ae.FromJSON (Some3 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Ae.parseJSON v' - pure (Some3 sa3 sa2 sa1 x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.FromJSON (Demote k4) - , Ae.FromJSON (Demote k3) - , Ae.FromJSON (Demote k2) - , Ae.FromJSON (Demote k1) - , Dict4 Ae.FromJSON f - ) => Ae.FromJSON (Some4 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v - 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 (Ae.FromJSON (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Ae.parseJSON v' - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Base.hs b/lib/Exinst/Instances/Base.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Base.hs +++ /dev/null @@ -1,622 +0,0 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# 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', 'Eq' and 'Ord' 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.Instances.Base () where - -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) -import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse)) -import qualified Data.Singletons.Prelude.List as List -import Data.Singletons.Prelude.Tuple (Tuple2Sym1) -import Data.Singletons.Decide -import Data.Type.Equality -import qualified GHC.Generics as G -import Prelude -import qualified Text.Read as Read - -import Exinst.Internal - hiding (Some1(..), Some2(..), Some3(..), Some4(..)) -import qualified Exinst.Internal 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 <- testEquality sa1x sa1y - case dict1 sa1x :: Dict (Eq (f a1x)) of - Dict -> Just (x == y) - -instance forall (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 <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of - Dict -> Just (x == y) - -instance forall (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 <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of - Dict -> Just (x == y) - -instance forall (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 <- testEquality sa4x sa4y - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of - Dict -> Just (x == y) - --------------------------------------------------------------------------------- --- Ord - -instance forall (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 <- testEquality sa1x sa1y - case dict1 sa1x :: Dict (Ord (f a1x)) of - Dict -> Just (compare x y) - -instance forall (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 <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of - Dict -> Just (compare x y) - -instance forall (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 <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of - Dict -> Just (compare x y) - -instance forall (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 <- testEquality sa4x sa4y - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality 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 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 - (c 'False, c 'True - ) => Dict0 (c :: Bool -> Constraint) where - {-# INLINABLE dict0 #-} - dict0 = \case { SFalse -> Dict; STrue -> Dict } - -instance - ( c (f 'False), c (f 'True) - ) => Dict1 c (f :: Bool -> k0) where - {-# INLINABLE dict1 #-} - dict1 = \case { SFalse -> Dict; STrue -> Dict } - -instance - ( 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 - ( 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 - ( 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/lib/Exinst/Instances/Binary.hs b/lib/Exinst/Instances/Binary.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Binary.hs +++ /dev/null @@ -1,139 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Bin.Binary' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Binary () where - -import qualified Data.Binary as Bin -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k1 -> Type). - ( SingKind k1 - , Bin.Binary (Demote k1) - , Dict1 Bin.Binary f - ) => Bin.Binary (Some1 f) where - {-# INLINABLE put #-} - put = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Bin.Binary (f a1)) of - Dict -> do - Bin.put (fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - rsa1 <- Bin.get - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Bin.Binary (f a1)) of - Dict -> do - x :: f a1 <- Bin.get - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> Type). - ( SingKind k2 - , SingKind k1 - , Bin.Binary (Demote k2) - , Bin.Binary (Demote k1) - , Dict2 Bin.Binary f - ) => Bin.Binary (Some2 f) where - {-# INLINABLE put #-} - put = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of - Dict -> do - Bin.put (fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa2, rsa1) <- Bin.get - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Bin.get - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> Type). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Bin.Binary (Demote k3) - , Bin.Binary (Demote k2) - , Bin.Binary (Demote k1) - , Dict3 Bin.Binary f - ) => Bin.Binary (Some3 f) where - {-# INLINABLE put #-} - put = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of - Dict -> do - Bin.put (fromSing sa3, fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa3, rsa2, rsa1) <- Bin.get - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Bin.get - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Bin.Binary (Demote k4) - , Bin.Binary (Demote k3) - , Bin.Binary (Demote k2) - , Bin.Binary (Demote k1) - , Dict4 Bin.Binary f - ) => Bin.Binary (Some4 f) where - {-# INLINABLE put #-} - put = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of - Dict -> do - Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa4, rsa3, rsa2, rsa1) <- Bin.get - 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 (Bin.Binary (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Bin.get - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Bytes.hs b/lib/Exinst/Instances/Bytes.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Bytes.hs +++ /dev/null @@ -1,140 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'By.Serial' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Bytes () where - -import qualified Data.Bytes.Serial as By -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k1 -> Type). - ( SingKind k1 - , By.Serial (Demote k1) - , Dict1 By.Serial f - ) => By.Serial (Some1 f) where - {-# INLINABLE serialize #-} - serialize = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (By.Serial (f a1)) of - Dict -> do - By.serialize (fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - rsa1 <- By.deserialize - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (By.Serial (f a1)) of - Dict -> do - x :: f a1 <- By.deserialize - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> Type). - ( SingKind k2 - , SingKind k1 - , By.Serial (Demote k2) - , By.Serial (Demote k1) - , Dict2 By.Serial f - ) => By.Serial (Some2 f) where - {-# INLINABLE serialize #-} - serialize = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of - Dict -> do - By.serialize (fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa2, rsa1) <- By.deserialize - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- By.deserialize - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> Type). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , By.Serial (Demote k3) - , By.Serial (Demote k2) - , By.Serial (Demote k1) - , Dict3 By.Serial f - ) => By.Serial (Some3 f) where - {-# INLINABLE serialize #-} - serialize = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of - Dict -> do - By.serialize (fromSing sa3, fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa3, rsa2, rsa1) <- By.deserialize - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- By.deserialize - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , By.Serial (Demote k4) - , By.Serial (Demote k3) - , By.Serial (Demote k2) - , By.Serial (Demote k1) - , Dict4 By.Serial f - ) => By.Serial (Some4 f) where - {-# INLINABLE serialize #-} - serialize = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of - Dict -> do - By.serialize (fromSing sa4, fromSing sa3, - fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa4, rsa3, rsa2, rsa1) <- By.deserialize - 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 (By.Serial (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- By.deserialize - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Cereal.hs b/lib/Exinst/Instances/Cereal.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Cereal.hs +++ /dev/null @@ -1,140 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Cer.Serialize' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Cereal () where - -import qualified Data.Serialize as Cer -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k1 -> Type). - ( SingKind k1 - , Cer.Serialize (Demote k1) - , Dict1 Cer.Serialize f - ) => Cer.Serialize (Some1 f) where - {-# INLINABLE put #-} - put = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of - Dict -> do - Cer.put (fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - rsa1 <- Cer.get - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of - Dict -> do - x :: f a1 <- Cer.get - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> Type). - ( SingKind k2 - , SingKind k1 - , Cer.Serialize (Demote k2) - , Cer.Serialize (Demote k1) - , Dict2 Cer.Serialize f - ) => Cer.Serialize (Some2 f) where - {-# INLINABLE put #-} - put = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of - Dict -> do - Cer.put (fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa2, rsa1) <- Cer.get - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Cer.get - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> Type). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Cer.Serialize (Demote k3) - , Cer.Serialize (Demote k2) - , Cer.Serialize (Demote k1) - , Dict3 Cer.Serialize f - ) => Cer.Serialize (Some3 f) where - {-# INLINABLE put #-} - put = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of - Dict -> do - Cer.put (fromSing sa3, fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa3, rsa2, rsa1) <- Cer.get - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Cer.get - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Cer.Serialize (Demote k4) - , Cer.Serialize (Demote k3) - , Cer.Serialize (Demote k2) - , Cer.Serialize (Demote k1) - , Dict4 Cer.Serialize f - ) => Cer.Serialize (Some4 f) where - {-# INLINABLE put #-} - put = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of - Dict -> do - Cer.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa4, rsa3, rsa2, rsa1) <- Cer.get - 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 (Cer.Serialize (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Cer.get - pure (Some4 sa4 sa3 sa2 sa1 x) - diff --git a/lib/Exinst/Instances/DeepSeq.hs b/lib/Exinst/Instances/DeepSeq.hs deleted file mode 100644 --- a/lib/Exinst/Instances/DeepSeq.hs +++ /dev/null @@ -1,60 +0,0 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and --- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' --- and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.DeepSeq () where - -import Control.DeepSeq (NFData(rnf)) -import Data.Constraint -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> *). - ( Dict1 NFData f - ) => NFData (Some1 f) where - {-# INLINABLE rnf #-} - rnf = \(!some1x) -> - withSome1Sing some1x $ \ !sa1 !(x :: f a1) -> - case dict1 sa1 :: Dict (NFData (f a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k2 -> k1 -> *). - ( Dict2 NFData f - ) => NFData (Some2 f) where - {-# INLINABLE rnf #-} - rnf = \(!some2x) -> - withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k3 -> k2 -> k1 -> *). - ( Dict3 NFData f - ) => NFData (Some3 f) where - {-# INLINABLE rnf #-} - rnf = \(!some3x) -> - withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). - ( Dict4 NFData f - ) => NFData (Some4 f) where - {-# INLINABLE rnf #-} - rnf = \(!some4x) -> - withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of - Dict -> rnf x `seq` () - diff --git a/lib/Exinst/Instances/Hashable.hs b/lib/Exinst/Instances/Hashable.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Hashable.hs +++ /dev/null @@ -1,101 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and --- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' --- and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Hashable () where - -import Data.Hashable (Hashable(hashWithSalt)) -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Some salt we add to hashes calculated in this module. -salt0 :: Int -salt0 = 6700417 - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Hashable (Demote k1) - , Dict1 Hashable f - ) => Hashable (Some1 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Hashable (f a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Hashable (Demote k2) - , Hashable (Demote k1) - , Dict2 Hashable f - ) => Hashable (Some2 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Hashable (Demote k3) - , Hashable (Demote k2) - , Hashable (Demote k1) - , Dict3 Hashable f - ) => Hashable (Some3 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa3 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Hashable (Demote k4) - , Hashable (Demote k3) - , Hashable (Demote k2) - , Hashable (Demote k1) - , Dict4 Hashable f - ) => Hashable (Some4 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa4 - `hashWithSalt` fromSing sa3 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x diff --git a/lib/Exinst/Instances/QuickCheck.hs b/lib/Exinst/Instances/QuickCheck.hs deleted file mode 100644 --- a/lib/Exinst/Instances/QuickCheck.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2', --- 'Some3' and '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.Instances.QuickCheck () where - -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons (SingKind, Sing, Demote, withSomeSing) -import qualified Test.QuickCheck as QC - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance - forall k1 (f :: k1 -> Type). - ( SingKind k1 - , QC.Arbitrary (Demote k1) - , Dict1 QC.Arbitrary f - ) => QC.Arbitrary (Some1 f) where - arbitrary = do - da1 <- QC.arbitrary - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of - Dict -> Some1 sa1 <$> QC.arbitrary - shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of - Dict -> Some1 sa1 <$> QC.shrink x - -instance - forall k2 k1 (f :: k2 -> k1 -> Type). - ( SingKind k2 - , SingKind k1 - , QC.Arbitrary (Demote k2) - , QC.Arbitrary (Demote k1) - , Dict2 QC.Arbitrary f - ) => QC.Arbitrary (Some2 f) where - arbitrary = do - da2 <- QC.arbitrary - da1 <- QC.arbitrary - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of - Dict -> Some2 sa2 sa1 <$> QC.arbitrary - shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of - Dict -> Some2 sa2 sa1 <$> QC.shrink x - -instance - forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , QC.Arbitrary (Demote k3) - , QC.Arbitrary (Demote k2) - , QC.Arbitrary (Demote k1) - , Dict3 QC.Arbitrary f - ) => QC.Arbitrary (Some3 f) where - arbitrary = do - da3 <- QC.arbitrary - da2 <- QC.arbitrary - da1 <- QC.arbitrary - withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of - Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary - shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of - Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x - -instance - forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , QC.Arbitrary (Demote k4) - , QC.Arbitrary (Demote k3) - , QC.Arbitrary (Demote k2) - , QC.Arbitrary (Demote k1) - , Dict4 QC.Arbitrary f - ) => QC.Arbitrary (Some4 f) where - arbitrary = do - da4 <- QC.arbitrary - da3 <- QC.arbitrary - da2 <- QC.arbitrary - da1 <- QC.arbitrary - 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 (QC.Arbitrary (f a4 a3 a2 a1)) of - Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary - shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of - Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x - diff --git a/lib/Exinst/Instances/Serialise.hs b/lib/Exinst/Instances/Serialise.hs deleted file mode 100644 --- a/lib/Exinst/Instances/Serialise.hs +++ /dev/null @@ -1,127 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Serialise' instances (which provide --- binary serialisation via the CBOR format) for 'Some1', --- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable --- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Serialise () where - -import Codec.Serialise -import Codec.Serialise.Decoding (decodeListLenOf) -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Serialise (Demote k1) - , Dict1 Serialise f - ) => Serialise (Some1 f) - where - {-# INLINABLE encode #-} - encode = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Serialise (f a1)) of - Dict -> encode (fromSing sa1, x) - {-# INLINABLE decode #-} - decode = do - decodeListLenOf 2 - rsa1 <- decode - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Serialise (f a1)) of - Dict -> do - x :: f a1 <- decode - pure (Some1 sa1 x) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Serialise (Demote k2) - , Serialise (Demote k1) - , Dict2 Serialise f - ) => Serialise (Some2 f) - where - {-# INLINABLE encode #-} - encode = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of - Dict -> encode (fromSing sa2, fromSing sa1, x) - - - {-# INLINABLE decode #-} - decode = do - decodeListLenOf 3 - rsa2 <- decode; rsa1 <- decode - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- decode - pure (Some2 sa2 sa1 x) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Serialise (Demote k3) - , Serialise (Demote k2) - , Serialise (Demote k1) - , Dict3 Serialise f - ) => Serialise (Some3 f) - where - {-# INLINABLE encode #-} - encode = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of - Dict -> encode (fromSing sa3, fromSing sa2, fromSing sa1, x) - {-# INLINABLE decode #-} - decode = do - decodeListLenOf 4 - rsa3 <- decode; rsa2 <- decode; rsa1 <- decode - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- decode - pure (Some3 sa3 sa2 sa1 x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Serialise (Demote k4) - , Serialise (Demote k3) - , Serialise (Demote k2) - , Serialise (Demote k1) - , Dict4 Serialise f - ) => Serialise (Some4 f) - where - {-# INLINABLE encode #-} - encode = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Serialise (f a4 a3 a2 a1)) of - Dict -> encode (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1, x) - {-# INLINABLE decode #-} - decode = do - decodeListLenOf 5 - rsa4 <- decode; rsa3 <- decode; rsa2 <- decode; rsa1 <- decode; - 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 (Serialise (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- decode - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Internal/Product.hs b/lib/Exinst/Internal/Product.hs --- a/lib/Exinst/Internal/Product.hs +++ b/lib/Exinst/Internal/Product.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PolyKinds #-} @@ -9,35 +8,8 @@ , P4(P4) ) where -import Control.DeepSeq (NFData) -import qualified Data.Binary as Bin import GHC.Generics (Generic) -#ifdef HAS_aeson -import Data.Aeson (FromJSON, ToJSON) -#endif - -#ifdef HAS_bytes -import qualified Data.Bytes.Serial as By -#endif - -#ifdef HAS_cereal -import qualified Data.Serialize as Cer -#endif - - -#ifdef HAS_hashable -import Data.Hashable (Hashable) -#endif - -#ifdef HAS_quickcheck -import qualified Test.QuickCheck as QC -#endif - -#ifdef HAS_serialise -import qualified Codec.Serialise as Cborg -#endif - -------------------------------------------------------------------------------- -- Products @@ -67,76 +39,3 @@ data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1) = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1) deriving (Eq, Show, Read, Ord, Generic) - --------------------------------------------------------------------------------- -#ifdef HAS_hashable -instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1) -instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1) -instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1) -instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1) -instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1) -instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1) -instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1) - --------------------------------------------------------------------------------- -#ifdef HAS_aeson -instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (P1 l r a1) -instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (P2 l r a2 a1) -instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (P3 l r a3 a2 a1) -instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (P4 l r a4 a3 a2 a1) - -instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (P1 l r a1) -instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (P2 l r a2 a1) -instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (P3 l r a3 a2 a1) -instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_bytes -instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (P1 l r a1) -instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (P2 l r a2 a1) -instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (P3 l r a3 a2 a1) -instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_cereal -instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (P1 l r a1) -instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (P2 l r a2 a1) -instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (P3 l r a3 a2 a1) -instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1) -instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1) -instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1) -instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1) - --------------------------------------------------------------------------------- -#ifdef HAS_quickcheck -instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where - arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary - shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where - arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary - shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where - arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary - shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where - arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary - shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_serialise -instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (P1 l r a1) -instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (P2 l r a2 a1) -instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (P3 l r a3 a2 a1) -instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (P4 l r a4 a3 a2 a1) -#endif diff --git a/lib/Exinst/Internal/Sum.hs b/lib/Exinst/Internal/Sum.hs --- a/lib/Exinst/Internal/Sum.hs +++ b/lib/Exinst/Internal/Sum.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PolyKinds #-} @@ -9,34 +8,8 @@ , S4(S4L,S4R) ) where -import Control.DeepSeq (NFData) -import qualified Data.Binary as Bin import GHC.Generics (Generic) -#ifdef HAS_aeson -import Data.Aeson (FromJSON, ToJSON) -#endif - -#ifdef HAS_bytes -import qualified Data.Bytes.Serial as By -#endif - -#ifdef HAS_cereal -import qualified Data.Serialize as Cer -#endif - -#ifdef HAS_hashable -import Data.Hashable (Hashable) -#endif - -#ifdef HAS_quickcheck -import qualified Test.QuickCheck as QC -#endif - -#ifdef HAS_serialise -import qualified Codec.Serialise as Cborg -#endif - -------------------------------------------------------------------------------- -- Sums @@ -67,79 +40,3 @@ = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1) deriving (Eq, Show, Read, Ord, Generic) --------------------------------------------------------------------------------- -#ifdef HAS_hashable -instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1) -instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1) -instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1) -instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1) -instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1) -instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1) -instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1) - --------------------------------------------------------------------------------- -#ifdef HAS_aeson -instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (S1 l r a1) -instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (S2 l r a2 a1) -instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (S3 l r a3 a2 a1) -instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (S4 l r a4 a3 a2 a1) - -instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (S1 l r a1) -instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (S2 l r a2 a1) -instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (S3 l r a3 a2 a1) -instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_bytes -instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (S1 l r a1) -instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (S2 l r a2 a1) -instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (S3 l r a3 a2 a1) -instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_cereal -instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (S1 l r a1) -instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (S2 l r a2 a1) -instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (S3 l r a3 a2 a1) -instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1) -instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1) -instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1) -instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1) - --------------------------------------------------------------------------------- -#ifdef HAS_quickcheck -instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where - arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ] - shrink (S1L l) = S1L <$> QC.shrink l - shrink (S1R r) = S1R <$> QC.shrink r -instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where - arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ] - shrink (S2L l) = S2L <$> QC.shrink l - shrink (S2R r) = S2R <$> QC.shrink r -instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where - arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ] - shrink (S3L l) = S3L <$> QC.shrink l - shrink (S3R r) = S3R <$> QC.shrink r -instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where - arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ] - shrink (S4L l) = S4L <$> QC.shrink l - shrink (S4R r) = S4R <$> QC.shrink r -#endif - --------------------------------------------------------------------------------- -#ifdef HAS_serialise -instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (S1 l r a1) -instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (S2 l r a2 a1) -instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (S3 l r a3 a2 a1) -instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (S4 l r a4 a3 a2 a1) -#endif diff --git a/lib/Exinst/QuickCheck.hs b/lib/Exinst/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/QuickCheck.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2', +-- 'Some3' and '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.QuickCheck () where + +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons (SingKind, Sing, Demote, withSomeSing) +import qualified Test.QuickCheck as QC + +import Exinst.Internal +import Exinst.Internal.Sum +import Exinst.Internal.Product + +-------------------------------------------------------------------------------- + +instance + forall k1 (f :: k1 -> Type). + ( SingKind k1 + , QC.Arbitrary (Demote k1) + , Dict1 QC.Arbitrary f + ) => QC.Arbitrary (Some1 f) where + arbitrary = do + da1 <- QC.arbitrary + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of + Dict -> Some1 sa1 <$> QC.arbitrary + shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of + Dict -> Some1 sa1 <$> QC.shrink x + +instance + forall k2 k1 (f :: k2 -> k1 -> Type). + ( SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict2 QC.Arbitrary f + ) => QC.Arbitrary (Some2 f) where + arbitrary = do + da2 <- QC.arbitrary + da1 <- QC.arbitrary + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of + Dict -> Some2 sa2 sa1 <$> QC.arbitrary + shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of + Dict -> Some2 sa2 sa1 <$> QC.shrink x + +instance + forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k3) + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict3 QC.Arbitrary f + ) => QC.Arbitrary (Some3 f) where + arbitrary = do + da3 <- QC.arbitrary + da2 <- QC.arbitrary + da1 <- QC.arbitrary + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of + Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary + shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of + Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x + +instance + forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k4) + , QC.Arbitrary (Demote k3) + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict4 QC.Arbitrary f + ) => QC.Arbitrary (Some4 f) where + arbitrary = do + da4 <- QC.arbitrary + da3 <- QC.arbitrary + da2 <- QC.arbitrary + da1 <- QC.arbitrary + 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 (QC.Arbitrary (f a4 a3 a2 a1)) of + Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary + shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of + Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x + +-------------------------------------------------------------------------------- + +instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where + arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ] + shrink (S1L l) = S1L <$> QC.shrink l + shrink (S1R r) = S1R <$> QC.shrink r +instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where + arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ] + shrink (S2L l) = S2L <$> QC.shrink l + shrink (S2R r) = S2R <$> QC.shrink r +instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where + arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ] + shrink (S3L l) = S3L <$> QC.shrink l + shrink (S3R r) = S3R <$> QC.shrink r +instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where + arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ] + shrink (S4L l) = S4L <$> QC.shrink l + shrink (S4R r) = S4R <$> QC.shrink r + +-------------------------------------------------------------------------------- + +instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where + arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary + shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where + arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary + shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where + arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary + shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where + arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary + shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -13,6 +13,7 @@ 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 @@ -22,28 +23,6 @@ import qualified Test.Tasty.QuickCheck as QC import Text.Read (readMaybe) -#ifdef HAS_aeson -import qualified Data.Aeson as Aeson -#endif - -#ifdef HAS_bytes -import qualified Data.Bytes.Get as Bytes -import qualified Data.Bytes.Put as Bytes -import qualified Data.Bytes.Serial as Bytes -#endif - -#ifdef HAS_cereal -import qualified Data.Serialize as Cer -#endif - -#ifdef HAS_hashable -import Data.Hashable (Hashable(hash)) -#endif - -#ifdef HAS_serialise -import qualified Codec.Serialise as Cborg -#endif - import Exinst -------------------------------------------------------------------------------- @@ -172,50 +151,14 @@ , 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 - -#ifdef HAS_aeson - , tt_id "Identity through Aeson's ToJSON/FromJSON" id_aeson -#endif - -#ifdef HAS_bytes - , tt_id "Identity through Bytes's Serial" id_bytes - , tt_id "Identity from Binary's Binary to Bytes's Serial" id_binary_to_bytes - , tt_id "Identity from Bytes's Serial to Binary's Binary" id_bytes_to_binary -#ifdef HAS_cereal - , tt_id "Identity from Cereal's Serialize to Bytes's Serial" id_cereal_to_bytes - , tt_id "Identity from Bytes's Serial to Cereal's Serialize" id_bytes_to_cereal -#endif -#endif - -#ifdef HAS_cereal - , tt_id "Identity through Cereal's Serialize" id_cereal - , tt_id "Identity from Binary's Binary to Cereal's Serialize" id_binary_to_cereal - , tt_id "Identity from Cereal's Serialize to Binary's Binary" id_cereal_to_binary -#endif - -#ifdef HAS_serialise - , tt_id "Identity through serialise's Serialise" id_serialise -#endif ] type MegaCtx a = ( G.Generic a , Show a , Read a + , Hashable a , Bin.Binary a -#ifdef HAS_aeson - , Aeson.FromJSON a - , Aeson.ToJSON a -#endif -#ifdef HAS_bytes - , Bytes.Serial a -#endif -#ifdef HAS_cereal - , Cer.Serialize a -#endif -#ifdef HAS_serialise - , Cborg.Serialise a -#endif ) tt_id @@ -278,7 +221,6 @@ QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === rnf x ] -#ifdef HAS_hashable INSTANCETRON(Hashable) tt_hashable :: Tasty.TestTree @@ -308,7 +250,6 @@ , QC.testProperty "Some4 (S4 X4 X4)" $ QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === (hash x `seq` ()) ] -#endif -------------------------------------------------------------------------------- @@ -318,80 +259,9 @@ id_generic :: G.Generic a => a -> Maybe a id_generic = Just . G.to . G.from -#ifdef HAS_aeson -INSTANCETRON(Aeson.ToJSON) -INSTANCETRON(Aeson.FromJSON) -id_aeson :: (Aeson.FromJSON a, Aeson.ToJSON a) => a -> Maybe a -id_aeson = Aeson.decode . Aeson.encode -#endif - -#ifdef HAS_bytes -INSTANCETRON(Bytes.Serial) -id_bytes :: Bytes.Serial a => a -> Maybe a -id_bytes = \a -> - case Bytes.runGetS Bytes.deserialize (Bytes.runPutS (Bytes.serialize a)) of - Left _ -> Nothing - Right a' -> Just a' - -id_binary_to_bytes :: (Bin.Binary a, Bytes.Serial a) => a -> Maybe a -id_binary_to_bytes = \a -> - case Bytes.runGetS Bytes.deserialize (BSL.toStrict (Bin.encode a)) of - Left _ -> Nothing - Right a' -> Just a' - -id_bytes_to_binary :: (Bytes.Serial a, Bin.Binary a) => a -> Maybe a -id_bytes_to_binary = \a -> - case Bin.decodeOrFail (Bytes.runPutL (Bytes.serialize a)) of - Right (z,_,a') | BSL.null z -> Just a' - _ -> Nothing -#endif - 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 -#ifdef HAS_cereal -INSTANCETRON(Cer.Serialize) -id_cereal :: Cer.Serialize a => a -> Maybe a -id_cereal = \a -> - case Cer.decodeLazy (Cer.encodeLazy a) of - Right a' -> Just a' - Left _ -> Nothing - -id_binary_to_cereal :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a -id_binary_to_cereal = \a -> - case Cer.decodeLazy (Bin.encode a) of - Right a' -> Just a' - Left _ -> Nothing - -id_cereal_to_binary :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a -id_cereal_to_binary = \a -> - case Bin.decodeOrFail (Cer.encodeLazy a) of - Right (z,_,a') | BSL.null z -> Just a' - _ -> Nothing - -#ifdef HAS_bytes -id_cereal_to_bytes :: (Cer.Serialize a, Bytes.Serial a) => a -> Maybe a -id_cereal_to_bytes = \a -> - case Bytes.runGetS Bytes.deserialize (Cer.encode a) of - Left _ -> Nothing - Right a' -> Just a' - -id_bytes_to_cereal :: (Bytes.Serial a, Cer.Serialize a) => a -> Maybe a -id_bytes_to_cereal = \a -> - case Cer.decodeLazy (Bytes.runPutL (Bytes.serialize a)) of - Right a' -> Just a' - Left _ -> Nothing -#endif -#endif - -#ifdef HAS_serialise -INSTANCETRON(Cborg.Serialise) -id_serialise :: Cborg.Serialise a => a -> Maybe a -id_serialise = \a -> - case Cborg.deserialiseOrFail (Cborg.serialise a) of - Right a' -> Just a' - Left _ -> Nothing -#endif