eliminators 0.3 → 0.4

raw patch · 9 files changed

+38/−37 lines, 9 filesdep ~basedep ~singleton-natsdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, singleton-nats, singletons, template-haskell, th-desugar

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• eliminators.cabal +9/−8
• src/Data/Eliminator/TH.hs +10/−6
• tests/DecideSpec.hs +3/−4
• tests/DecideTypes.hs +2/−8
• tests/ListSpec.hs +3/−3
• tests/ListTypes.hs +1/−1
• tests/VecSpec.hs +4/−4
• tests/VecTypes.hs +3/−3

@@ -1,3 +1,6 @@+## 0.4 [2018.01.09]+* Require `singletons-2.4` and GHC 8.4.+ ## 0.3 [2017-11-07] * Migrate the old `elimNat` from `Data.Eliminator` (which worked over the `Nat`   from `GHC.TypeNats`) to `Data.Eliminator.TypeNats`. There `elimNat` that now

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.3+version:             0.4 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@@ -16,7 +16,7 @@ build-type:          Simple extra-source-files:  CHANGELOG.md, README.md cabal-version:       >=1.10-tested-with:         GHC == 8.2.1+tested-with:         GHC == 8.4.1  source-repository head   type:                git@@ -26,13 +26,13 @@   exposed-modules:     Data.Eliminator                        Data.Eliminator.TH                        Data.Eliminator.TypeNats-  build-depends:       base             >= 4.10    && < 4.11+  build-depends:       base             >= 4.11    && < 4.12                      , extra            >= 1.4.2   && < 1.7-                     , singletons       >= 2.3     && < 2.4+                     , singletons       >= 2.4     && < 2.5                      , singleton-nats   >= 0.4.0.3 && < 0.5-                     , template-haskell >= 2.12    && < 2.13+                     , template-haskell >= 2.13    && < 2.14                      , th-abstraction   >= 0.2.3   && < 0.3-                     , th-desugar       >= 1.7     && < 1.8+                     , th-desugar       >= 1.8     && < 1.9   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors@@ -48,11 +48,12 @@                        ListTypes                        VecTypes                        VecSpec-  build-depends:       base           >= 4.10    && < 4.11+  build-depends:       base           >= 4.11    && < 4.12                      , eliminators                      , hspec          >= 2       && < 3-                     , singletons     >= 2.3     && < 2.4+                     , singletons     >= 2.4     && < 2.5                      , singleton-nats >= 0.4.0.3 && < 0.5+  build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts

@@ -346,14 +346,18 @@   | nm == '(:)                                     = 'SCons   | Just degree <- tupleNameDegree_maybe nm        = mkTupleDataName degree   | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree-  | otherwise                                      = prefixUCName "S" ":%" nm+  | otherwise                                      = prefixConName "S" "%" nm  mkTupleDataName :: Int -> Name mkTupleDataName n = mkName $ "STuple" ++ (show n) --- put an uppercase prefix on a name. Takes two prefixes: one for identifiers--- and one for symbols-prefixUCName :: String -> String -> Name -> Name-prefixUCName pre tyPre n = case (nameBase n) of-    (':' : rest) -> mkName (tyPre ++ rest)+-- Put an uppercase prefix on a constructor name. Takes two prefixes:+-- one for identifiers and one for symbols.+--+-- This is different from 'prefixName' in that infix constructor names always+-- start with a colon, so we must insert the prefix after the colon in order+-- for the new name to be syntactically valid.+prefixConName :: String -> String -> Name -> Name+prefixConName pre tyPre n = case (nameBase n) of+    (':' : rest) -> mkName (':' : tyPre ++ rest)     alpha -> mkName (pre ++ alpha)

@@ -39,8 +39,7 @@       show (decEqNatList (SCons (sLit @0) SNil) SNil)                   `shouldBe` disproved       show (decEqNatList SNil                   (SCons (sLit @0) SNil)) `shouldBe` disproved       show (decEqNatList (SCons (sLit @0) SNil) (SCons (sLit @0) SNil)) `shouldBe` proved-      -- TODO: Try this in the next version of singletons-      -- show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved+      show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved  ----- @@ -86,14 +85,14 @@   where     left :: forall (x :: n :~: j).             Sing x -> Decision (S n :~: S j)-    left yes = Proved $ cong @Nat @Nat @(TyCon1 S) @n @j (fromSing yes)+    left yes = Proved $ cong @Nat @Nat @(TyCon S) @n @j (fromSing yes)      right :: forall (r :: (n :~: j) ~> Void).              Sing r -> Decision (S n :~: S j)     right no = Disproved $ fromSing no . sInjective @n @j sn  decEqNat :: forall (n :: Nat) (j :: Nat). Sing n -> Sing j -> Decision (n :~: j)-decEqNat sn = runWhyDecEqNat (elimNat @(TyCon1 WhyDecEqNat) @n sn base step)+decEqNat sn = runWhyDecEqNat (elimNat @(TyCon WhyDecEqNat) @n sn base step)   where     base :: WhyDecEqNat Z     base = WhyDecEqNat decEqZ

@@ -9,18 +9,12 @@ {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}--- TODO: Remove this in the next version of singletons-{-# OPTIONS_GHC -Wno-orphans #-} module DecideTypes where  import Data.Kind import Data.Nat import Data.Singletons.TH hiding (Decision(..)) --- TODO: Remove these in the next version of singletons-$(genSingletons [''Void])-$(genDefunSymbols [''(~>)])- -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work -- around these, we define a more general Decision' data type here.@@ -42,8 +36,8 @@   showsPrec p (Disproved _) =     showParen (p > 10) $ showString "Disproved <void>" -type Decision  = Decision' (TyCon2 (->))-type PDecision = Decision' (:~>$)+type Decision  = Decision' (TyCon (->))+type PDecision = Decision' (~>@#@$)  data instance Sing (z :: PDecision a) where   -- It would be lovely to not have to write those (:: PDecision a) kind

@@ -41,12 +41,12 @@             Sing s -> Sing ss          -> WhyMapPreservesLength f ss          -> WhyMapPreservesLength f (s:ss)-    step _ _ = cong @_ @_ @((:+$$) 1)+    step _ _ = cong @_ @_ @((+@#@$$) 1)  mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)                     (f :: y ~> z) (g :: x ~> y) (l :: [x]).                     SingI l-                 => Map f (Map g l) :~: Map (f :.$$$ g) l+                 => Map f (Map g l) :~: Map (f .@#@$$$ g) l mapFusion   = elimList @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step   where@@ -57,4 +57,4 @@             Sing s -> Sing ss          -> WhyMapFusion f g ss          -> WhyMapFusion f g (s:ss)-    step _ _ = cong @_ @_ @((:$$) (f @@ (g @@ s)))+    step _ _ = cong @_ @_ @((:@#@$$) (f @@ (g @@ s)))

@@ -15,5 +15,5 @@ $(genDefunSymbols [''WhyMapPreservesLength])  type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])-  = Map f (Map g l) :~: Map (f :.$$$ g) l+  = Map f (Map g l) :~: Map (f .@#@$$$ g) l $(genDefunSymbols [''WhyMapFusion])

@@ -6,7 +6,7 @@ module VecSpec where  import Data.Eliminator-import Data.Kind+import Data.Kind (Type) import Data.Nat import Data.Singletons import Data.Singletons.Prelude.Num@@ -69,7 +69,7 @@  replicateVec :: forall (e :: Type) (howMany :: Nat).                 Sing howMany -> e -> Vec e howMany-replicateVec s e = elimNat @(TyCon1 (Vec e)) @howMany s VNil step+replicateVec s e = elimNat @(TyCon (Vec e)) @howMany s VNil step   where     step :: forall (k :: Nat). Sing k -> Vec e k -> Vec e (S k)     step _ = (e :#)@@ -102,7 +102,7 @@  appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).              SingI n-          => Vec e n -> Vec e m -> Vec e (n :+ m)+          => Vec e n -> Vec e m -> Vec e (n + m) appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step   where     base :: WhyAppendVec e m Z@@ -130,7 +130,7 @@  concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).              (SingKind e, SingI j, e ~ Demote e)-          => Vec (Vec e j) n -> Vec e (n :* j)+          => Vec (Vec e j) n -> Vec e (n * j) concatVec l = withSomeSing l $ \(singL :: Sing l) ->                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step   where

@@ -11,7 +11,7 @@ {-# LANGUAGE UndecidableInstances #-} module VecTypes where -import Data.Kind+import Data.Kind (Type) import Data.Nat import Data.Singletons.Prelude.Num import Data.Singletons.TH@@ -65,7 +65,7 @@ $(genDefunSymbols [''WhyZipWithVec])  type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)-  = Vec e n -> Vec e m -> Vec e (n :+ m)+  = Vec e n -> Vec e m -> Vec e (n + m) $(genDefunSymbols [''WhyAppendVec])  type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)@@ -73,7 +73,7 @@ $(genDefunSymbols [''WhyTransposeVec])  type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)-  = Vec e (n :* j)+  = Vec e (n * j) data WhyConcatVecSym (e :: Type) (j :: Nat)   :: forall (n :: Nat). Vec (Vec e j) n ~> Type type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l