diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,9 @@ +- 0.1.6 + - Add `boring` instances + - Add `some` (`GEq` etc) instances + - Add `deepseq` instances + - Require GHC-7.8+ + - 0.1.5 - Add `discreteBool :: Dec (a :~: b)` (GHC-7.8+) - Add `Show`, `Eq`, `Ord` `SBool b` instances. diff --git a/README.md b/README.md deleted file mode 100644 --- a/README.md +++ /dev/null @@ -1,7 +0,0 @@ -# singleton-bool - -[![Build Status](https://travis-ci.org/phadej/singleton-bool.svg?branch=master)](https://travis-ci.org/phadej/singleton-bool) -[![Hackage](https://img.shields.io/hackage/v/singleton-bool.svg)](http://hackage.haskell.org/package/singleton-bool) -[![Stackage Nightly](http://stackage.org/package/singleton-bool/badge/nightly)](http://stackage.org/nightly/package/singleton-bool) - -Type level booleans diff --git a/singleton-bool.cabal b/singleton-bool.cabal --- a/singleton-bool.cabal +++ b/singleton-bool.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: singleton-bool -version: 0.1.5 +version: 0.1.6 synopsis: Type level booleans description: Type level booleans. @@ -16,12 +16,17 @@ license: BSD3 license-file: LICENSE build-type: Simple +extra-source-files: CHANGELOG.md tested-with: - GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 || ==7.6.3 - -extra-source-files: - CHANGELOG.md - README.md + GHC ==7.8.4 + || ==7.10.3 + || ==8.0.2 + || ==8.2.2 + || ==8.4.4 + || ==8.6.5 + || ==8.8.4 + || ==8.10.4 + || ==9.0.1 source-repository head type: git @@ -31,14 +36,11 @@ hs-source-dirs: src ghc-options: -Wall build-depends: - base >=4.6 && <4.13 - - if impl(ghc >= 7.8) - build-depends: - dec >=0.0.3 && <0.1 + base >=4.7 && <4.16 + , boring >=0.2 && <0.3 + , dec >=0.0.3 && <0.1 + , deepseq >=1.3 && <1.5 + , some >=1.0.3 && <1.1 exposed-modules: Data.Singletons.Bool default-language: Haskell2010 - - if !impl(ghc >=7.8) - build-depends: tagged >=0.8.5 && <0.9 diff --git a/src/Data/Singletons/Bool.hs b/src/Data/Singletons/Bool.hs --- a/src/Data/Singletons/Bool.hs +++ b/src/Data/Singletons/Bool.hs @@ -1,7 +1,8 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -9,10 +10,6 @@ #if __GLASGOW_HASKELL__ >= 800 {-# OPTIONS_GHC -Wno-redundant-constraints #-} #endif -#if MIN_VERSION_base(4,7,0) -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE FlexibleContexts #-} -#endif -- | Additions to "Data.Type.Bool". module Data.Singletons.Bool ( SBool(..), @@ -22,31 +19,36 @@ reflectBool, reifyBool, -- * Data.Type.Dec -#if MIN_VERSION_base(4,7,0) -- | 'discreteBool' is available with @base >= 4.7@ (GHC-7.8) discreteBool, -#endif -- * Data.Type.Bool and .Equality -- | These are only defined with @base >= 4.7@ -#if MIN_VERSION_base(4,7,0) sboolAnd, sboolOr, sboolNot, eqToRefl, eqCast, sboolEqRefl, trivialRefl, -#endif ) where -#if MIN_VERSION_base(4,7,0) -import Data.Type.Bool -import Data.Type.Dec (Dec (..)) -import Data.Type.Equality -import Unsafe.Coerce (unsafeCoerce) -#endif +import Control.DeepSeq (NFData (..)) +import Data.Boring (Boring (..)) +import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..)) +import Data.GADT.DeepSeq (GNFData (..)) +import Data.GADT.Show (GRead (..), GShow (..)) +import Data.Proxy (Proxy (..)) +import Data.Type.Bool +import Data.Type.Dec (Dec (..)) +import Data.Type.Equality +import Unsafe.Coerce (unsafeCoerce) -import Data.Proxy (Proxy (..)) +import qualified Data.Some.Church as Church -- $setup -- >>> :set -XDataKinds -XTypeOperators --- >>> import Data.Type.Dec (decShow) +-- >>> import Data.Proxy (Proxy (..)) +-- >>> import Data.Type.Dec +-- >>> import Data.Some +-- >>> import Data.GADT.Compare +-- >>> import Data.GADT.Show +-- >>> import Data.Type.Equality data SBool (b :: Bool) where STrue :: SBool 'True @@ -69,6 +71,11 @@ instance Ord (SBool b) where compare _ _ = EQ +-- | @since 0.1.6 +instance NFData (SBool b) where + rnf STrue = () + rnf SFalse = () + ------------------------------------------------------------------------------- -- conversion to and from explicit SBool values ------------------------------------------------------------------------------- @@ -111,10 +118,80 @@ reflectBool _ = fromSBool (sbool :: SBool b) ------------------------------------------------------------------------------- +-- Boring +------------------------------------------------------------------------------- + +-- | @since 0.1.6 +instance SBoolI b => Boring (SBool b) where + boring = sbool + +------------------------------------------------------------------------------- +-- Data.GADT (some) +------------------------------------------------------------------------------- + +-- | +-- +-- >>> geq STrue STrue +-- Just Refl +-- +-- >>> geq STrue SFalse +-- Nothing +-- +-- @since 0.1.6 +instance GEq SBool where + geq STrue STrue = Just Refl + geq SFalse SFalse = Just Refl + geq _ _ = Nothing + +-- | +-- +-- @since 0.1.6 +instance GCompare SBool where + gcompare SFalse SFalse = GEQ + gcompare SFalse STrue = GLT + gcompare STrue SFalse = GGT + gcompare STrue STrue = GEQ + +-- | @since 0.1.6 +instance GNFData SBool where + grnf STrue = () + grnf SFalse = () + +-- | +-- +-- >>> showsPrec 0 STrue "" +-- "STrue" +-- +-- @since 0.1.6 +instance GShow SBool where + gshowsPrec = showsPrec + +-- | +-- +-- >>> readsPrec 0 "Some STrue" :: [(Some SBool, String)] +-- [(Some STrue,"")] +-- +-- >>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)] +-- [(Some SFalse,"")] +-- +-- >>> readsPrec 0 "Some Else" :: [(Some SBool, String)] +-- [] +-- +-- @since 0.1.6 +instance GRead SBool where + greadsPrec _ s = + [ (Church.mkSome STrue, t) + | ("STrue", t) <- lex s + ] + ++ + [ (Church.mkSome SFalse, t) + | ("SFalse", t) <- lex s + ] + +------------------------------------------------------------------------------- -- Discrete ------------------------------------------------------------------------------- -#if MIN_VERSION_base(4,7,0) -- | Decidable equality. -- -- >>> decShow (discreteBool :: Dec ('True :~: 'True)) @@ -127,13 +204,11 @@ (STrue, SFalse) -> No $ \p -> case p of {} (SFalse, STrue) -> No $ \p -> case p of {} (SFalse, SFalse) -> Yes Refl -#endif ------------------------------------------------------------------------------- -- Witnesses ------------------------------------------------------------------------------- -#if MIN_VERSION_base(4,7,0) -- | >>> sboolAnd STrue SFalse -- SFalse sboolAnd :: SBool a -> SBool b -> SBool (a && b) @@ -179,4 +254,3 @@ sboolEqRefl = case sbool :: SBool (a == b) of STrue -> Just eqToRefl SFalse -> Nothing -#endif