list-witnesses 0.1.3.2 → 0.1.4.0

raw patch · 4 files changed

+36/−26 lines, 4 filesdep +singletons-basedep ~decidabledep ~functor-productsdep ~microlensPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: singletons-base

Dependency ranges changed: decidable, functor-products, microlens, profunctors, singletons, vinyl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• list-witnesses.cabal +12/−12
• src/Data/Type/List/Edit.hs +13/−12
• src/Data/Type/List/Sublist.hs +2/−2

@@ -1,6 +1,15 @@ Changelog ========= +Version 0.1.4.0+---------------++*July 22, 2023*++<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.4.0>++*   Now requires singletons 3.0 and above, and GHC 9.2 and above.+ Version 0.1.3.2 --------------- 

@@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack------ hash: b5cd1b4dd5aa9afa7ec4fbf2fbfb27e461d5361e5bd05a2edf0ad347669f5c77  name:           list-witnesses-version:        0.1.3.2+version:        0.1.4.0 synopsis:       Witnesses for working with type-level lists description:    Collection of assorted inductive witnesses and functions for working with                 type-level lists.@@ -21,11 +19,12 @@ bug-reports:    https://github.com/mstksg/list-witnesses/issues author:         Justin Le maintainer:     justin@jle.im-copyright:      (c) Justin Le 2018+copyright:      (c) Justin Le 2023 license:        BSD3 license-file:   LICENSE-tested-with:    GHC >= 8.6 build-type:     Simple+tested-with:+    GHC >= 9.2 extra-source-files:     README.md     CHANGELOG.md@@ -45,10 +44,11 @@   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns   build-depends:       base >=4.7 && <5-    , decidable >=0.2-    , functor-products-    , microlens-    , profunctors-    , singletons-    , vinyl+    , decidable >=0.3.1 && <0.4+    , functor-products >=0.1.2 && <0.2+    , microlens <0.5+    , profunctors <5.7+    , singletons-base >=3.0 && <3.1+    , singletons >=3.0 && <3.2+    , vinyl >=0.14.3 &&  <0.15   default-language: Haskell2010

@@ -17,7 +17,7 @@  -- | -- Module      : Data.Type.List.Edit--- Copyright   : (c) Justin Le 2018+-- Copyright   : (c) Justin Le 2023 -- License     : BSD3 -- -- Maintainer  : justin@jle.im@@ -68,10 +68,11 @@   , SubstituteIndexSym0, SubstituteIndexSym   ) where +import           Data.Function.Singletons (IdSym0) import           Data.Kind+import           Data.List.Singletons (SList(..)) import           Data.Singletons import           Data.Singletons.Decide-import           Data.Singletons.Prelude import           Data.Singletons.Sigma import           Data.Type.Functor.Product import           Data.Type.Predicate@@ -198,7 +199,7 @@ autoInsert = auto @_ @(IsInsert as bs) @x  -- | Kind-indexed singleton for 'Insert'.-data SInsert as bs x :: Insert as bs x -> Type where+data SInsert (as :: [k]) (bs :: [k]) (x :: k) :: Insert as bs x -> Type where     SInsZ :: SInsert as (x ': as) x 'InsZ     SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x ('InsS ins) @@ -286,7 +287,7 @@ autoDelete = auto @_ @(IsDelete as bs) @x  -- | Kind-indexed singleton for 'Delete'.-data SDelete as bs x :: Delete as bs x -> Type where+data SDelete (as :: [k]) (bs :: [k]) (x :: k) :: Delete as bs x -> Type where     SDelZ :: SDelete (x ': as) as x 'DelZ     SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x ('DelS del) @@ -347,7 +348,7 @@ autoSubstitute = auto @_ @(IsSubstitute as bs x) @y  -- | Kind-indexed singleton for 'Substitute'.-data SSubstitute as bs x y :: Substitute as bs x y -> Type where+data SSubstitute (as :: [k]) (bs :: [k]) (x :: k) (y :: k) :: Substitute as bs x y -> Type where     SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ     SSubS :: SSubstitute as bs x y sub           -> SSubstitute (c ': as) (c ': bs) x y ('SubS sub)@@ -594,7 +595,7 @@ -- | Type-level version of 'insertIndex'.  Because of how GADTs and type -- families interact, the type-level lists and kinds of the insertion and -- index must be provided.-type family InsertIndex as bs x y (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where+type family InsertIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where     InsertIndex as        (x ': as) x y 'InsZ       i       = 'IS i     InsertIndex (y ': as) (y ': bs) x y ('InsS ins) 'IZ     = 'IZ     InsertIndex (a ': as) (a ': bs) x y ('InsS ins) ('IS i) = 'IS (InsertIndex as bs x y ins i)@@ -623,14 +624,14 @@  -- | Helper type family for the implementation of 'DeleteIndex', to get -- around the lack of case statements at the type level.-type family SuccDeletedIx b bs x y (del :: DeletedIx bs x y) :: DeletedIx (b ': bs) x y where+type family SuccDeletedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (del :: DeletedIx bs x y) :: DeletedIx (b ': bs) x y where     SuccDeletedIx b bs x x 'GotDeleted = 'GotDeleted     SuccDeletedIx b bs x y ('NotDeleted i) = 'NotDeleted ('IS i)  -- | Type-level version of 'deleteIndex'.  Because of how GADTs and type -- families interact, the type-level lists and kinds of the insertion and -- index must be provided.-type family DeleteIndex as bs x y (del :: Delete as bs x) (i :: Index as y) :: DeletedIx bs x y where+type family DeleteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (del :: Delete as bs x) (i :: Index as y) :: DeletedIx bs x y where     DeleteIndex (x ': bs) bs         x x 'DelZ       'IZ     = 'GotDeleted     DeleteIndex (x ': bs) bs         x y 'DelZ       ('IS i) = 'NotDeleted i     DeleteIndex (y ': as) (y ': bs)  x y ('DelS del) 'IZ     = 'NotDeleted 'IZ@@ -648,7 +649,7 @@ type instance Apply (DeleteIndexSym as bs x y del) i = DeleteIndex as bs x y del i  -- | Kind-indexed singleton for 'DeletedIx'.-data SDeletedIx bs x y :: DeletedIx bs x y -> Type where+data SDeletedIx (bs :: [k]) (x :: k) (y :: k) :: DeletedIx bs x y -> Type where     SGotDeleted :: SDeletedIx bs x x 'GotDeleted     SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i) @@ -669,14 +670,14 @@  -- | Helper type family for the implementation of 'SubstituteIndex', to get -- around the lack of case statements at the type level.-type family SuccSubstitutedIx b bs x y z (s :: SubstitutedIx bs x y z) :: SubstitutedIx (b ': bs) x y z where+type family SuccSubstitutedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: SubstitutedIx bs x y z) :: SubstitutedIx (b ': bs) x y z where     SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)     SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)  -- | Type-level version of 'substituteIndex'.  Because of how GADTs and -- type families interact, the type-level lists and kinds of the insertion -- and index must be provided.-type family SubstituteIndex as bs x y z (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where+type family SubstituteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where     SubstituteIndex (z ': as) (y ': as) z y z 'SubZ     'IZ     = 'GotSubbed 'IZ     SubstituteIndex (x ': as) (y ': as) x y z 'SubZ     ('IS i) = 'NotSubbed ('IS i)     SubstituteIndex (z ': as) (z ': bs) x y z ('SubS s) 'IZ     = 'NotSubbed 'IZ@@ -694,7 +695,7 @@ type instance Apply (SubstituteIndexSym as bs x y z s) i = SubstituteIndex as bs x y z s i  -- | Kind-indexed singleton for 'SubstitutedIx'.-data SSubstitutedIx bs x y z :: SubstitutedIx bs x y z -> Type where+data SSubstitutedIx (bs :: [k]) (x :: k) (y :: k) (z :: k) :: SubstitutedIx bs x y z -> Type where     SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)     SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i) 

@@ -17,7 +17,7 @@  -- | -- Module      : Data.Type.List.Sublist--- Copyright   : (c) Justin Le 2018+-- Copyright   : (c) Justin Le 2023 -- License     : BSD3 -- -- Maintainer  : justin@jle.im@@ -73,10 +73,10 @@ import           Data.Bifunctor import           Data.Functor.Compose import           Data.Kind+import           Data.List.Singletons (SList(..), type (++)) import           Data.Profunctor import           Data.Singletons import           Data.Singletons.Decide-import           Data.Singletons.Prelude.List import           Data.Singletons.Sigma import           Data.Type.Functor.Product import           Data.Type.Predicate