boring 0.1.1 → 0.1.2

raw patch · 3 files changed

+90/−14 lines, 3 filesdep +decdep +singleton-booldep ~basedep ~base-compatdep ~constraintsPVP ok

version bump matches the API change (PVP)

Dependencies added: dec, singleton-bool

Dependency ranges changed: base, base-compat, constraints, fin, generics-sop, semigroups, vec

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• boring.cabal +9/−7
• src/Data/Boring.hs +76/−7

@@ -1,5 +1,10 @@ # Revision history for boring +## 0.1.2++- Add instances for 'Boring' instances for 'SBool', 'SNat' and 'LE'.+- Add 'Boring (Dec a)', 'boringYes' and 'boringNo'.+ ## 0.1.1  - Add `GHC.Generics` instances

@@ -1,5 +1,5 @@ name:               boring-version:            0.1.1+version:            0.1.2 synopsis:           Boring and Absurd types description:   * @Boring@ types are isomorphic to @()@.@@ -14,7 +14,7 @@ license-file:       LICENSE author:             Oleg Grenrus <oleg.grenrus@iki.fi> maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:          (c) 2017 Oleg Grenrus+copyright:          (c) 2017-2019 Oleg Grenrus category:           Data build-type:         Simple extra-source-files: ChangeLog.md@@ -31,10 +31,12 @@   build-depends:       adjunctions          >=4.4     && <4.5     , base                 >=4.7     && <4.13-    , base-compat          >=0.10.5 && <0.11-    , constraints          ==0.4.1.3 || >=0.10 && <0.11-    , fin                  >=0.0.1   && <0.1-    , generics-sop         >=0.3.2.0 && <0.5+    , base-compat          >=0.10.5  && <0.11+    , constraints          ==0.4.1.3 || >=0.10 && <0.12+    , dec                  >=0.0.3   && <0.1+    , fin                  >=0.0.3   && <0.1+    , generics-sop         >=0.3.2.0 && <0.6+    , singleton-bool       >=0.1.4   && <0.2     , streams              >=3.3     && <3.4     , tagged               >=0.8.6   && <0.9     , transformers         >=0.3     && <0.6@@ -42,7 +44,7 @@     , vec                  >=0.1     && <0.2    if !impl(ghc >=8.0)-    build-depends: semigroups >=0.18.5 && <0.19+    build-depends: semigroups >=0.18.5 && <0.20    if !impl(ghc >=7.10)     build-depends: void >=0.7.2 && <0.8

@@ -5,6 +5,7 @@ {-# LANGUAGE GADTs            #-} {-# LANGUAGE TypeOperators    #-} {-# LANGUAGE ConstraintKinds  #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} -- | 'Boring' and 'Absurd' classes. One approach. --@@ -54,12 +55,17 @@     -- * Classes     Boring (..),     Absurd (..),-    -- * More integeresting stuff+    -- * More interesting stuff     vacuous,     boringRep,     untainted,     devoid,     united,+    -- ** Dec+    --+    -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'.+    boringYes,+    absurdNo,     ) where  import Prelude ()@@ -75,15 +81,20 @@ import Data.List.NonEmpty    (NonEmpty (..)) import Data.Proxy            (Proxy (..)) import Data.Tagged           (Tagged (..))+import Data.Type.Dec         (Dec (..), Decidable (..)) import Data.Stream.Infinite  (Stream (..)) import GHC.Generics   hiding (Rep) -import qualified Data.Fin      as Fin-import qualified Data.Nat      as Nat-import qualified Data.Vec.Lazy as Vec-import qualified Data.Vec.Pull as Vec.Pull-import qualified Data.Void     as V-import qualified Generics.SOP  as SOP+import qualified Data.Fin                  as Fin+import qualified Data.Nat                  as Nat+import qualified Data.Singletons.Bool      as Bool+import qualified Data.Type.Nat             as Nat+import qualified Data.Type.Nat.LE          as ZeroSucc+import qualified Data.Type.Nat.LE.ReflStep as ReflStep+import qualified Data.Vec.Lazy             as Vec+import qualified Data.Vec.Pull             as Vec.Pull+import qualified Data.Void                 as V+import qualified Generics.SOP              as SOP  #if MIN_VERSION_base(4,7,0) import qualified Data.Coerce        as Co@@ -199,6 +210,10 @@ # endif #endif +-------------------------------------------------------------------------------+-- vec + fin + singleton-bool+-------------------------------------------------------------------------------+ instance n ~ 'Nat.Z => Boring (Vec.Vec n a) where     boring = Vec.empty @@ -208,6 +223,28 @@ instance n ~ ('Nat.S 'Nat.Z) => Boring (Fin.Fin n) where     boring = Fin.boring +-- singletons are boring++-- | @since 0.1.3+instance Nat.SNatI n => Boring (Nat.SNat n) where+    boring = Nat.snat++-- | @since 0.1.3+instance Bool.SBoolI b => Boring (Bool.SBool b) where+    boring = Bool.sbool++-- | @since 0.1.3+instance ZeroSucc.LE n m => Boring (ZeroSucc.LEProof n m) where+    boring = ZeroSucc.leProof++-- | @since 0.1.3+instance (ZeroSucc.LE n m, Nat.SNatI m) => Boring (ReflStep.LEProof n m) where+    boring = ReflStep.fromZeroSucc ZeroSucc.leProof++-------------------------------------------------------------------------------+-- Generics+-------------------------------------------------------------------------------+ instance Boring (U1 p) where     boring = U1 @@ -280,6 +317,16 @@ instance n ~ 'Nat.Z => Absurd (Fin.Fin n) where     absurd = Fin.absurd +instance (ZeroSucc.LE m n, n' ~ 'Nat.S n) => Absurd (ZeroSucc.LEProof n' m) where+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof++instance (ZeroSucc.LE m n, n' ~ 'Nat.S n, Nat.SNatI n) => Absurd (ReflStep.LEProof n' m) where+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof . ReflStep.toZeroSucc++-------------------------------------------------------------------------------+-- Generics+-------------------------------------------------------------------------------+ instance Absurd (V1 p) where     absurd v = case v of {} @@ -337,3 +384,25 @@ -- @ united :: (Boring a, Functor f) => (a -> f a) -> s -> f s united f v = v <$ f boring++-------------------------------------------------------------------------------+-- Dec+-------------------------------------------------------------------------------++-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense.+--+-- @since 0.1.3+instance Decidable a => Boring (Dec a) where+    boring = decide++-- | 'Yes', it's 'boring'.+--+-- @since 0.1.3+boringYes :: Boring a => Dec a+boringYes = Yes boring++-- | 'No', it's 'absurd'.+--+-- @since 0.1.3+absurdNo :: Absurd a => Dec a+absurdNo = No absurd