haskus-utils-types 1.4.1 → 1.5

raw patch · 4 files changed

+60/−41 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• haskus-utils-types.cabal +7/−8
• src/lib/Haskus/Utils/Types.hs +2/−0
• src/lib/Haskus/Utils/Types/Bool.hs +2/−2
• src/lib/Haskus/Utils/Types/List.hs +49/−31

@@ -1,13 +1,13 @@ name:                haskus-utils-types-version:             1.4.1+version:             1.5 synopsis:            Haskus types utility modules license:             BSD3 license-file:        LICENSE author:              Sylvain Henry maintainer:          sylvain@haskus.fr-homepage:            http://www.haskus.org-copyright:           Sylvain Henry 2018-category:            System+homepage:            https://www.haskus.org+copyright:           Sylvain Henry 2020+category:            Type build-type:          Simple cabal-version:       1.20 @@ -33,9 +33,8 @@   other-modules:    build-depends:       -         base                      >= 4.9 && < 5+         base >= 4.9 && < 5 -  build-tools:    ghc-options:          -Wall   default-language:     Haskell2010   hs-source-dirs:       src/lib@@ -48,5 +47,5 @@    default-language:    Haskell2010     build-depends:-         base-      ,  doctest                 >= 0.16+         base >= 4.9 && < 5+      ,  doctest >= 0.16

@@ -1,6 +1,7 @@ -- | Type-level utils module Haskus.Utils.Types    ( module X+   , Type    ) where @@ -11,3 +12,4 @@ import Haskus.Utils.Types.List       as X import Haskus.Utils.Types.Proxy      as X import Haskus.Utils.Types.Constraint as X+import Data.Kind (Type)

@@ -51,11 +51,11 @@    boolValue :: Bool  instance KnownBool 'True where-   {-# INLINE boolValue #-}+   {-# INLINABLE boolValue #-}    boolValue = True  instance KnownBool 'False where-   {-# INLINE boolValue #-}+   {-# INLINABLE boolValue #-}    boolValue = False  

@@ -25,6 +25,7 @@    , NubHead    -- * Sublist    , Head+   , Last    , Tail    , Init    , Take@@ -122,6 +123,11 @@ type family Head (xs :: [k]) :: k where    Head (x ': xs) = x +-- | Last of a list+type family Last (xs :: [k]) :: k where+   Last '[x]      = x+   Last (x ': xs) = Last xs+ -- | Concat two type lists type family Concat (xs :: [k]) (ys :: [k]) :: [k] where    Concat '[] '[]      = '[]@@ -202,33 +208,32 @@  -- | Check that a type is member of a type list type family CheckMember (a :: k) (l :: [k]) :: Constraint where-   CheckMember a l = CheckMember' l a l+   CheckMember a l = CheckMember' (MaybeIndexOf a l) a l  -- | Helper for CheckMember-type family CheckMember' (i :: [k]) (a :: k) (l :: [k]) :: Constraint where-   CheckMember' i a (a ': l) = ()-   CheckMember' i a (b ': l) = CheckMember' i a l-   CheckMember' i a '[]      = TypeError ( 'Text "`"-                                     ':<>: 'ShowType a-                                     ':<>: 'Text "'"-                                     ':<>: 'Text " is not a member of "-                                     ':<>: 'ShowType i)+type family CheckMember' (i :: Nat) (a :: k) (l :: [k]) :: Constraint where+   CheckMember' 0 a l = TypeError ( 'Text "`"+                              ':<>: 'ShowType a+                              ':<>: 'Text "'"+                              ':<>: 'Text " is not a member of "+                              ':<>: 'ShowType l)+   CheckMember' _ _ _ = ()   -- | Check that a list is a subset of another type family CheckMembers (l1 :: [k]) (l2 :: [k]) :: Constraint where-   CheckMembers l1 l1 = ()-   CheckMembers l1 l2 = CheckMembers' l2 '[] l1 l2+   CheckMembers '[]       l1 = ()+   CheckMembers (x ': xs) l2 = CheckMembers' (MaybeIndexOf x l2) x xs (x ': xs) l2  -- | Helper for CheckMembers-type family CheckMembers' (i :: [k]) (e :: [k]) (l1 :: [k]) (l2 :: [k]) :: Constraint where-   CheckMembers' i e '[] '[] = TypeError (   'ShowType e-                                       ':$$: 'Text "is not a subset of"-                                       ':$$: 'ShowType i)-   CheckMembers' i e '[] l2  = ()-   CheckMembers' i e (l ': ls) '[]       = CheckMembers' i (l ': e) ls i-   CheckMembers' i e (x ': xs) (x ': ys) = CheckMembers' i e xs i-   CheckMembers' i e (x ': xs) (y ': ys) = CheckMembers' i e (x ': xs) ys+type family CheckMembers' (i :: Nat) (x :: k) (xs :: [k]) (l1 :: [k]) (l2 :: [k]) :: Constraint where+   CheckMembers' 0 x _ l1 l2 = TypeError (     'ShowType l1+                                         ':$$: 'Text "is not a subset of"+                                         ':$$: 'ShowType l2+                                         ':$$: 'ShowType x+                                         ':<>: 'Text " is missing from the latter.")+   CheckMembers' _ _ '[] _ _ = ()+   CheckMembers' _ _ (x ': xs) l1 l2 = CheckMembers' (MaybeIndexOf x l2) x xs l1 l2  -- | Get list indexes type family Indexes (l :: [k]) :: [Nat] where@@ -270,13 +275,15 @@    NubHead (x ': xs) = x ': Remove x xs  -- | Get the first index of a type-type family IndexOf (a :: k) (l :: [k]) :: Nat where-   IndexOf x xs = IndexOf' x xs xs+type IndexOf (x :: k) (xs :: [k]) = IndexOf' (MaybeIndexOf x xs) x xs  -- | Get the first index of a type-type family IndexOf' (a :: k) (l :: [k]) (l2 :: [k]) :: Nat where-   IndexOf' x (x ': xs) l2 = 0-   IndexOf' y (x ': xs) l2 = 1 + IndexOf' y xs l2+type family IndexOf' (i :: Nat) (a :: k) (l :: [k]) :: Nat where+   IndexOf' 0 x l = TypeError ( 'ShowType x+                          ':<>: 'Text " not found in list:"+                          ':$$: 'Text " "+                          ':<>: 'ShowType l )+   IndexOf' i _ _ = i - 1  -- | Get all the indexes of a type type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where@@ -295,14 +302,22 @@ -- | Helper for MaybeIndexOf type family MaybeIndexOf' (n :: Nat) (a :: k) (l :: [k]) where    MaybeIndexOf' n x '[]       = 0-   MaybeIndexOf' n x (x ': xs) = 1 + n+   MaybeIndexOf' n x (x ': xs) = n + 1    MaybeIndexOf' n x (y ': xs) = MaybeIndexOf' (n+1) x xs  -- | Indexed access into the list-type family Index (n :: Nat) (l :: [k]) :: k where-   Index 0 (x ': xs) = x-   Index n (x ': xs) = Index (n-1) xs+type Index (n :: Nat) (l :: [k]) = Index' n l l +-- | Indexed access into the list+type family Index' (n :: Nat) (l :: [k]) (l2 :: [k]) = (r :: k) where+   Index' 0 (x ': _ ) _  = x+   Index' n (_ ': xs) l2 = Index' (n-1) xs l2+   Index' n '[]       l2 = TypeError ( 'Text "Index "+                                ':<>: 'ShowType n+                                ':<>: 'Text " out of bounds for list:"+                                ':$$: 'Text " "+                                ':<>: 'ShowType l2 )+ -- | List membership test type family Elem (t :: b) (f :: b) (x :: k) (xs :: [k]) :: b where    Elem t f x '[]       = f@@ -348,9 +363,12 @@ --------------------------------------  -- | Constraint: x member of xs-type Member x xs =-   ( x ~ Index (IndexOf x xs) xs-   , KnownNat (IndexOf x xs)+type family Member x xs :: Constraint where+   Member x xs = MemberAtIndex (IndexOf x xs) x xs+   +type MemberAtIndex i x xs =+   ( x ~ Index i xs+   , KnownNat i    )  -- | Constraint: all the xs are members of ys