allToAny, travis update

mstksg · Nov 13, 2018 · 88487f2 · 88487f2
1 parent f978c60
commit 88487f2
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 12 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -29,9 +29,9 @@ matrix:
     compiler: ": #GHC 8.4.4"
     addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.4,happy-1.19.5,alex-3.1.7], sources: [hvr-ghc]}}
 
-  - env: BUILD=cabal GHCVER=8.6.1 CABALVER=2.4 HAPPYVER=1.19.5 ALEXVER=3.1.7
-    compiler: ": #GHC 8.6.1"
-    addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.1,happy-1.19.5,alex-3.1.7], sources: [hvr-ghc]}}
+  - env: BUILD=cabal GHCVER=8.6.2 CABALVER=2.4 HAPPYVER=1.19.5 ALEXVER=3.1.7
+    compiler: ": #GHC 8.6.2"
+    addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.2,happy-1.19.5,alex-3.1.7], sources: [hvr-ghc]}}
 
   # Build with the newest GHC and cabal-install. This is an accepted failure,
   # see below.
@@ -43,7 +43,7 @@ matrix:
   # variable, such as using --stack-yaml to point to a different file.
   - env: BUILD=stack ARGS=""
     compiler: ": #stack default"
-    addons: {apt: {packages: [ghc-8.6.1], sources: [hvr-ghc]}}
+    addons: {apt: {packages: [ghc-8.6.2], sources: [hvr-ghc]}}
 
   - env: BUILD=stack ARGS="--resolver lts-12"
     compiler: ": #stack 8.4.4"

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,15 @@
 Changelog
 =========
 
+Version 0.1.5.0
+---------------
+
+*Unreleased*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.5.0>
+
+*   Add `allToAny` to *Data.Type.Predicate.Quantification*.
+
 Version 0.1.4.0
 ---------------
 

diff --git a/package.yaml b/package.yaml
@@ -1,5 +1,5 @@
 name:                decidable
-version:             0.1.4.0
+version:             0.1.5.0
 github:              "mstksg/decidable"
 license:             BSD3
 author:              "Justin Le"

diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
@@ -20,33 +20,33 @@
 --
 module Data.Type.Predicate.Quantification (
   -- * Any
-    Any, WitAny(..), anyImpossible
+    Any, WitAny(..), None, anyImpossible
   -- ** Decision
   , decideAny, idecideAny, decideNone, idecideNone
-  -- ** Negation
-  , None, allNotNone, noneAllNot
   -- ** Entailment
   , entailAny, ientailAny, entailAnyF, ientailAnyF
   -- ** Composition
   , allComp, compAll
   -- * All
-  , All, WitAll(..)
+  , All, WitAll(..), NotAll
   -- ** Decision
   , decideAll, idecideAll
-  -- ** Negation
-  , NotAll
-  , anyNotNotAll, notAllAnyNot
   -- ** Entailment
   , entailAll, ientailAll, entailAllF, ientailAllF
   , decideEntailAll, idecideEntailAll
   -- ** Composition
   , anyComp, compAny
+  -- * Logical interplay
+  , allToAny
+  , allNotNone, noneAllNot
+  , anyNotNotAll, notAllAnyNot
   ) where
 
 import           Data.Kind
 import           Data.Singletons
 import           Data.Singletons.Decide
 import           Data.Type.Predicate
+import           Data.Type.Predicate.Logic
 import           Data.Type.Universe
 
 -- | 'decideNone', but providing an 'Elem'.
@@ -201,3 +201,10 @@ noneAllNot
     => None f p --> All f (Not p)
 noneAllNot xs vAny = elimDisproof (decide @(All f (Not p)) xs) $ \vAll ->
     vAll $ WitAll $ \i p -> vAny $ WitAny i p
+
+-- | If something is true for all xs, then it must be true for at least one
+-- x in xs, provided that xs is not empty.
+--
+-- @since 0.1.5.0
+allToAny :: (All f p &&& NotNull f) --> Any f p
+allToAny _ (a, WitAny i _) = WitAny i $ runWitAll a i