eliminators 0.4 → 0.4.1

raw patch · 3 files changed

+12/−6 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Data.Eliminator: elimVoid :: forall (p_alp3 :: (~>) Void Type) (s_alp4 :: Void). Sing s_alp4 -> (@@) p_alp3 s_alp4

- Data.Eliminator: elimBool :: forall (p_alri :: (~>) Bool Type) (s_alrj :: Bool). Sing s_alrj -> (@@) p_alri False -> (@@) p_alri True -> (@@) p_alri s_alrj

+ Data.Eliminator: elimBool :: forall (p_alnV :: (~>) Bool Type) (s_alnW :: Bool). Sing s_alnW -> (@@) p_alnV False -> (@@) p_alnV True -> (@@) p_alnV s_alnW

- Data.Eliminator: elimEither :: forall (a_aiQ7 :: Type) (b_aiQ8 :: Type) (p_alru :: (~>) (Either a_aiQ7 b_aiQ8) Type) (s_alrv :: Either a_aiQ7 b_aiQ8). Sing s_alrv -> (forall (f0_alrw :: a_aiQ7). Sing f0_alrw -> (@@) p_alru (Left f0_alrw)) -> (forall (f0_alrx :: b_aiQ8). Sing f0_alrx -> (@@) p_alru (Right f0_alrx)) -> (@@) p_alru s_alrv

+ Data.Eliminator: elimEither :: forall (a_aiOT :: Type) (b_aiOU :: Type) (p_alo7 :: (~>) (Either a_aiOT b_aiOU) Type) (s_alo8 :: Either a_aiOT b_aiOU). Sing s_alo8 -> (forall (f0_alo9 :: a_aiOT). Sing f0_alo9 -> (@@) p_alo7 (Left f0_alo9)) -> (forall (f0_aloa :: b_aiOU). Sing f0_aloa -> (@@) p_alo7 (Right f0_aloa)) -> (@@) p_alo7 s_alo8

- Data.Eliminator: elimList :: forall (a_11 :: Type) (p_alD7 :: (~>) ([] a_11) Type) (s_alD8 :: [] a_11). Sing s_alD8 -> (@@) p_alD7 [] -> (forall (f0_alD9 :: a_11). Sing f0_alD9 -> forall (f1_alDa :: [a_11]). Sing f1_alDa -> (@@) p_alD7 f1_alDa -> (@@) p_alD7 ((:) f0_alD9 f1_alDa)) -> (@@) p_alD7 s_alD8

+ Data.Eliminator: elimList :: forall (a_11 :: Type) (p_alAe :: (~>) ([] a_11) Type) (s_alAf :: [] a_11). Sing s_alAf -> (@@) p_alAe [] -> (forall (f0_alAg :: a_11). Sing f0_alAg -> forall (f1_alAh :: [a_11]). Sing f1_alAh -> (@@) p_alAe f1_alAh -> (@@) p_alAe ((:) f0_alAg f1_alAh)) -> (@@) p_alAe s_alAf

- Data.Eliminator: elimMaybe :: forall (a_11 :: Type) (p_alrI :: (~>) (Maybe a_11) Type) (s_alrJ :: Maybe a_11). Sing s_alrJ -> (@@) p_alrI Nothing -> (forall (f0_alrK :: a_11). Sing f0_alrK -> (@@) p_alrI (Just f0_alrK)) -> (@@) p_alrI s_alrJ

+ Data.Eliminator: elimMaybe :: forall (a_11 :: Type) (p_alol :: (~>) (Maybe a_11) Type) (s_alom :: Maybe a_11). Sing s_alom -> (@@) p_alol Nothing -> (forall (f0_alon :: a_11). Sing f0_alon -> (@@) p_alol (Just f0_alon)) -> (@@) p_alol s_alom

- Data.Eliminator: elimNat :: forall (p_alrT :: (~>) Nat Type) (s_alrU :: Nat). Sing s_alrU -> (@@) p_alrT Z -> (forall (f0_alrV :: Nat). Sing f0_alrV -> (@@) p_alrT f0_alrV -> (@@) p_alrT (S f0_alrV)) -> (@@) p_alrT s_alrU

+ Data.Eliminator: elimNat :: forall (p_alow :: (~>) Nat Type) (s_alox :: Nat). Sing s_alox -> (@@) p_alow Z -> (forall (f0_aloy :: Nat). Sing f0_aloy -> (@@) p_alow f0_aloy -> (@@) p_alow (S f0_aloy)) -> (@@) p_alow s_alox

- Data.Eliminator: elimNonEmpty :: forall (a_ac6N :: Type) (p_als3 :: (~>) (NonEmpty a_ac6N) Type) (s_als4 :: NonEmpty a_ac6N). Sing s_als4 -> (forall (f0_als5 :: a_ac6N). Sing f0_als5 -> forall (f1_als6 :: [a_ac6N]). Sing f1_als6 -> (@@) p_als3 ((:|) f0_als5 f1_als6)) -> (@@) p_als3 s_als4

+ Data.Eliminator: elimNonEmpty :: forall (a_ac3J :: Type) (p_aloG :: (~>) (NonEmpty a_ac3J) Type) (s_aloH :: NonEmpty a_ac3J). Sing s_aloH -> (forall (f0_aloI :: a_ac3J). Sing f0_aloI -> forall (f1_aloJ :: [a_ac3J]). Sing f1_aloJ -> (@@) p_aloG ((:|) f0_aloI f1_aloJ)) -> (@@) p_aloG s_aloH

- Data.Eliminator: elimOrdering :: forall (p_alsf :: (~>) Ordering Type) (s_alsg :: Ordering). Sing s_alsg -> (@@) p_alsf LT -> (@@) p_alsf EQ -> (@@) p_alsf GT -> (@@) p_alsf s_alsg

+ Data.Eliminator: elimOrdering :: forall (p_aloS :: (~>) Ordering Type) (s_aloT :: Ordering). Sing s_aloT -> (@@) p_aloS LT -> (@@) p_aloS EQ -> (@@) p_aloS GT -> (@@) p_aloS s_aloT

- Data.Eliminator: elimTuple0 :: forall (p_alH8 :: (~>) () Type) (s_alH9 :: ()). Sing s_alH9 -> (@@) p_alH8 () -> (@@) p_alH8 s_alH9

+ Data.Eliminator: elimTuple0 :: forall (p_alEf :: (~>) () Type) (s_alEg :: ()). Sing s_alEg -> (@@) p_alEf () -> (@@) p_alEf s_alEg

- Data.Eliminator: elimTuple2 :: forall (a_11 :: Type) (b_12 :: Type) (p_alHd :: (~>) ((,) a_11 b_12) Type) (s_alHe :: (,) a_11 b_12). Sing s_alHe -> (forall (f0_alHf :: a_11). Sing f0_alHf -> forall (f1_alHg :: b_12). Sing f1_alHg -> (@@) p_alHd ((,) f0_alHf f1_alHg)) -> (@@) p_alHd s_alHe

+ Data.Eliminator: elimTuple2 :: forall (a_11 :: Type) (b_12 :: Type) (p_alEk :: (~>) ((,) a_11 b_12) Type) (s_alEl :: (,) a_11 b_12). Sing s_alEl -> (forall (f0_alEm :: a_11). Sing f0_alEm -> forall (f1_alEn :: b_12). Sing f1_alEn -> (@@) p_alEk ((,) f0_alEm f1_alEn)) -> (@@) p_alEk s_alEl

- Data.Eliminator: elimTuple3 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (p_alHp :: (~>) ((,,) a_11 b_12 c_13) Type) (s_alHq :: (,,) a_11 b_12 c_13). Sing s_alHq -> (forall (f0_alHr :: a_11). Sing f0_alHr -> forall (f1_alHs :: b_12). Sing f1_alHs -> forall (f2_alHt :: c_13). Sing f2_alHt -> (@@) p_alHp ((,,) f0_alHr f1_alHs f2_alHt)) -> (@@) p_alHp s_alHq

+ Data.Eliminator: elimTuple3 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (p_alEw :: (~>) ((,,) a_11 b_12 c_13) Type) (s_alEx :: (,,) a_11 b_12 c_13). Sing s_alEx -> (forall (f0_alEy :: a_11). Sing f0_alEy -> forall (f1_alEz :: b_12). Sing f1_alEz -> forall (f2_alEA :: c_13). Sing f2_alEA -> (@@) p_alEw ((,,) f0_alEy f1_alEz f2_alEA)) -> (@@) p_alEw s_alEx

- Data.Eliminator: elimTuple4 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (p_alHF :: (~>) ((,,,) a_11 b_12 c_13 d_14) Type) (s_alHG :: (,,,) a_11 b_12 c_13 d_14). Sing s_alHG -> (forall (f0_alHH :: a_11). Sing f0_alHH -> forall (f1_alHI :: b_12). Sing f1_alHI -> forall (f2_alHJ :: c_13). Sing f2_alHJ -> forall (f3_alHK :: d_14). Sing f3_alHK -> (@@) p_alHF ((,,,) f0_alHH f1_alHI f2_alHJ f3_alHK)) -> (@@) p_alHF s_alHG

+ Data.Eliminator: elimTuple4 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (p_alEM :: (~>) ((,,,) a_11 b_12 c_13 d_14) Type) (s_alEN :: (,,,) a_11 b_12 c_13 d_14). Sing s_alEN -> (forall (f0_alEO :: a_11). Sing f0_alEO -> forall (f1_alEP :: b_12). Sing f1_alEP -> forall (f2_alEQ :: c_13). Sing f2_alEQ -> forall (f3_alER :: d_14). Sing f3_alER -> (@@) p_alEM ((,,,) f0_alEO f1_alEP f2_alEQ f3_alER)) -> (@@) p_alEM s_alEN

- Data.Eliminator: elimTuple5 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (p_alHZ :: (~>) ((,,,,) a_11 b_12 c_13 d_14 e_15) Type) (s_alI0 :: (,,,,) a_11 b_12 c_13 d_14 e_15). Sing s_alI0 -> (forall (f0_alI1 :: a_11). Sing f0_alI1 -> forall (f1_alI2 :: b_12). Sing f1_alI2 -> forall (f2_alI3 :: c_13). Sing f2_alI3 -> forall (f3_alI4 :: d_14). Sing f3_alI4 -> forall (f4_alI5 :: e_15). Sing f4_alI5 -> (@@) p_alHZ ((,,,,) f0_alI1 f1_alI2 f2_alI3 f3_alI4 f4_alI5)) -> (@@) p_alHZ s_alI0

+ Data.Eliminator: elimTuple5 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (p_alF6 :: (~>) ((,,,,) a_11 b_12 c_13 d_14 e_15) Type) (s_alF7 :: (,,,,) a_11 b_12 c_13 d_14 e_15). Sing s_alF7 -> (forall (f0_alF8 :: a_11). Sing f0_alF8 -> forall (f1_alF9 :: b_12). Sing f1_alF9 -> forall (f2_alFa :: c_13). Sing f2_alFa -> forall (f3_alFb :: d_14). Sing f3_alFb -> forall (f4_alFc :: e_15). Sing f4_alFc -> (@@) p_alF6 ((,,,,) f0_alF8 f1_alF9 f2_alFa f3_alFb f4_alFc)) -> (@@) p_alF6 s_alF7

- Data.Eliminator: elimTuple6 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (p_alIn :: (~>) ((,,,,,) a_11 b_12 c_13 d_14 e_15 f_16) Type) (s_alIo :: (,,,,,) a_11 b_12 c_13 d_14 e_15 f_16). Sing s_alIo -> (forall (f0_alIp :: a_11). Sing f0_alIp -> forall (f1_alIq :: b_12). Sing f1_alIq -> forall (f2_alIr :: c_13). Sing f2_alIr -> forall (f3_alIs :: d_14). Sing f3_alIs -> forall (f4_alIt :: e_15). Sing f4_alIt -> forall (f5_alIu :: f_16). Sing f5_alIu -> (@@) p_alIn ((,,,,,) f0_alIp f1_alIq f2_alIr f3_alIs f4_alIt f5_alIu)) -> (@@) p_alIn s_alIo

+ Data.Eliminator: elimTuple6 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (p_alFu :: (~>) ((,,,,,) a_11 b_12 c_13 d_14 e_15 f_16) Type) (s_alFv :: (,,,,,) a_11 b_12 c_13 d_14 e_15 f_16). Sing s_alFv -> (forall (f0_alFw :: a_11). Sing f0_alFw -> forall (f1_alFx :: b_12). Sing f1_alFx -> forall (f2_alFy :: c_13). Sing f2_alFy -> forall (f3_alFz :: d_14). Sing f3_alFz -> forall (f4_alFA :: e_15). Sing f4_alFA -> forall (f5_alFB :: f_16). Sing f5_alFB -> (@@) p_alFu ((,,,,,) f0_alFw f1_alFx f2_alFy f3_alFz f4_alFA f5_alFB)) -> (@@) p_alFu s_alFv

- Data.Eliminator: elimTuple7 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (g_17 :: Type) (p_alIP :: (~>) ((,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17) Type) (s_alIQ :: (,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17). Sing s_alIQ -> (forall (f0_alIR :: a_11). Sing f0_alIR -> forall (f1_alIS :: b_12). Sing f1_alIS -> forall (f2_alIT :: c_13). Sing f2_alIT -> forall (f3_alIU :: d_14). Sing f3_alIU -> forall (f4_alIV :: e_15). Sing f4_alIV -> forall (f5_alIW :: f_16). Sing f5_alIW -> forall (f6_alIX :: g_17). Sing f6_alIX -> (@@) p_alIP ((,,,,,,) f0_alIR f1_alIS f2_alIT f3_alIU f4_alIV f5_alIW f6_alIX)) -> (@@) p_alIP s_alIQ

+ Data.Eliminator: elimTuple7 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (g_17 :: Type) (p_alFW :: (~>) ((,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17) Type) (s_alFX :: (,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17). Sing s_alFX -> (forall (f0_alFY :: a_11). Sing f0_alFY -> forall (f1_alFZ :: b_12). Sing f1_alFZ -> forall (f2_alG0 :: c_13). Sing f2_alG0 -> forall (f3_alG1 :: d_14). Sing f3_alG1 -> forall (f4_alG2 :: e_15). Sing f4_alG2 -> forall (f5_alG3 :: f_16). Sing f5_alG3 -> forall (f6_alG4 :: g_17). Sing f6_alG4 -> (@@) p_alFW ((,,,,,,) f0_alFY f1_alFZ f2_alG0 f3_alG1 f4_alG2 f5_alG3 f6_alG4)) -> (@@) p_alFW s_alFX

Files

CHANGELOG.md +3/−0
eliminators.cabal +5/−5
src/Data/Eliminator.hs +4/−1

CHANGELOG.md view

@@ -1,3 +1,6 @@+### 0.4.1 [2018.02.13]+* Add `elimVoid` to `Data.Eliminator`.+ ## 0.4 [2018.01.09] * Require `singletons-2.4` and GHC 8.4.

eliminators.cabal view

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.4+version:             0.4.1 synopsis:            Dependently typed elimination functions using singletons description:         This library provides eliminators for inductive data types,                      leveraging the power of the @singletons@ library to allow@@ -28,8 +28,8 @@                        Data.Eliminator.TypeNats   build-depends:       base             >= 4.11    && < 4.12                      , extra            >= 1.4.2   && < 1.7-                     , singletons       >= 2.4     && < 2.5-                     , singleton-nats   >= 0.4.0.3 && < 0.5+                     , singletons       >= 2.4.1   && < 2.5+                     , singleton-nats   >= 0.4.0.4 && < 0.5                      , template-haskell >= 2.13    && < 2.14                      , th-abstraction   >= 0.2.3   && < 0.3                      , th-desugar       >= 1.8     && < 1.9@@ -51,8 +51,8 @@   build-depends:       base           >= 4.11    && < 4.12                      , eliminators                      , hspec          >= 2       && < 3-                     , singletons     >= 2.4     && < 2.5-                     , singleton-nats >= 0.4.0.3 && < 0.5+                     , singletons     >= 2.4.1   && < 2.5+                     , singleton-nats >= 0.4.0.4 && < 0.5   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests   default-language:    Haskell2010

src/Data/Eliminator.hs view

@@ -1,5 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE EmptyCase #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-}@@ -37,6 +38,7 @@   , elimTuple5   , elimTuple6   , elimTuple7+  , elimVoid   ) where  import Control.Monad.Extra@@ -46,6 +48,7 @@ import Data.Nat import Data.Singletons.Prelude import Data.Singletons.Prelude.List.NonEmpty (Sing(..))+import Data.Void (Void)  import Language.Haskell.TH.Desugar (tupleNameDegree_maybe) @@ -65,7 +68,7 @@   with @~>@ prepended. -} -$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering])+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering, ''Void]) $(deriveElimNamed "elimList" ''[]) $(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n                     in deriveElimNamed ("elimTuple" ++ show deg) n)