type-sets 0.1.0.0 → 0.1.1.0

raw patch · 5 files changed

+791/−8 lines, 5 filesdep ~cmptypePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: cmptype

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−1
• README.md +2/−2
• src/Type/RBSet.hs +583/−0
• test/Spec.hs +196/−1
• type-sets.cabal +5/−4

@@ -1,7 +1,11 @@ # Changelog for type-sets +## 0.1.1.0 --- 2019-08-11++- Added `Type.RBSet` for a red-black-tree-backed set (thanks to @danidiaz)+ ## 0.1.0.0 --- 2019-08-07 -Initial release!+- Initial release!  ## Unreleased changes

@@ -1,7 +1,7 @@ # type-sets  [![Build Status](https://api.travis-ci.org/isovector/type-sets.svg?branch=master)](https://travis-ci.org/isovector/type-sets)-[![Hackage](https://img.shields.io/hackage/v/cmptype.svg?logo=haskell&label=cmptype)](https://hackage.haskell.org/package/cmptype)+[![Hackage](https://img.shields.io/hackage/v/type-sets.svg?logo=haskell&label=type-sets)](https://hackage.haskell.org/package/type-sets)   ## Dedication@@ -31,7 +31,7 @@ test1 = id  -- Bool is a member :)  test2 :: Proxy (Member Char MySet) -> Proxy 'False-test2 = id  -- False is not a member :(+test2 = id  -- Char is not a member :( ```  See the `Type.Set` module for more operations.

@@ -0,0 +1,583 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}++-- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for+-- the original term-level code by Stefan Kahrs.+--+-- @since 0.1.1.0+module Type.RBSet+  ( -- * Core type+    TypeSet (..)+  , Empty+    -- * Set operations+  , Member+  , Insertable(Insert)+  , InsertAll+  , FromList+  , Removable(Remove)+  , Merge+  ) where++import Type.Compare+import GHC.TypeLits++-- | The color of a node.+data Color = R+           | B+    deriving (Show,Eq)++-- | A Red-Black tree.+--+-- @since 0.1.1.0+data TypeSet a = E+               | N Color (TypeSet a) a (TypeSet a)+    deriving (Show,Eq)++-- | A map without entries.+type Empty = E++--+--+-- Insertion++{- | Insert a list of type level key / value pairs into a type-level map.+-}+type family InsertAll (es :: [k]) (t :: TypeSet k) :: TypeSet k where+    InsertAll '[] t = t+    InsertAll ( v ': es ) t = Insert v (InsertAll es t)++{- | Build a type-level map out of a list of type level key / value pairs.+-}+type FromList (es :: [k]) = InsertAll es Empty++{- | The associated type family 'Insert' produces the resulting map.++ -}+class Insertable (k :: ki) (t :: TypeSet ki) where+    type Insert k t :: TypeSet ki++-- insert x s =+--  T B a z b+--  where+--  T _ a z b = ins s+instance (InsertableHelper1 k t, Insert1 k t ~ inserted, CanMakeBlack inserted) => Insertable k t where+    type Insert k t = MakeBlack (Insert1 k t)++class CanMakeBlack (t :: TypeSet ki) where+    type MakeBlack t :: TypeSet ki++instance CanMakeBlack (N color left k right) where+    type MakeBlack (N color left k right) = N B left k right++instance CanMakeBlack E where+    type MakeBlack E = E++class InsertableHelper1 (k :: ki)+                        (t :: TypeSet ki) where+    type Insert1 k t :: TypeSet ki++instance InsertableHelper1 k E where+    type Insert1 k E = N R E k E++instance (CmpType k k' ~ ordering,+          InsertableHelper2 ordering k color left k' right+         )+         => InsertableHelper1 k (N color left k' right) where+    -- FIXME possible duplicate work with CmpType: both in constraint and in associated type family.+    -- Is that bad? How to avoid it?+    type Insert1 k (N color left k' right) = Insert2 (CmpType k k') k color left k' right++class InsertableHelper2 (ordering :: Ordering)+                        (k :: ki)+                        (color :: Color)+                        (left :: TypeSet ki)+                        (k' :: ki)+                        (right :: TypeSet ki) where+    type Insert2 ordering k color left k' right :: TypeSet ki++--  ins s@(T B a y b)+--      | x<y = balance (ins a) y b+instance (InsertableHelper1 k left, Insert1 k left ~ inserted,+          Balanceable inserted k' right+         )+         => InsertableHelper2 LT k B left k' right where+    type Insert2              LT k B left k' right = Balance (Insert1 k left) k' right++--  ins s@(T B a y b)+--      | x<y = balance (ins a) y b+instance (InsertableHelper1 k left, Insert1 k left ~ inserted,+          Balanceable inserted k' right+         )+         => InsertableHelper2 LT k R left k' right where+    type Insert2              LT k R left k' right = N R (Insert1 k left) k' right+++instance InsertableHelper2 EQ k color left k right where+    type Insert2           EQ k color left k right = N color left k right++--  ins s@(T B a y b)+--      | ...+--      | x>y = balance a y (ins b)+instance (InsertableHelper1 k right, Insert1 k right ~ inserted,+          Balanceable left  k' inserted+         )+         => InsertableHelper2 GT k B left k' right where+    type Insert2              GT k B left k' right = Balance left  k' (Insert1 k right)++--  ins s@(T R a y b)+--      | ...+--      | x>y = T R a y (ins b)+instance (InsertableHelper1 k right, Insert1 k right ~ inserted,+          Balanceable left  k' inserted+         )+         => InsertableHelper2 GT k R left k' right where+    type Insert2              GT k R left k' right = N R left k' (Insert1 k right)++data BalanceAction = BalanceSpecial+                   | BalanceLL+                   | BalanceLR+                   | BalanceRL+                   | BalanceRR+                   | DoNotBalance+                   deriving Show++type family ShouldBalance (left :: TypeSet ki) (right :: TypeSet ki) :: BalanceAction where+    ShouldBalance (N R _ _ _) (N R _ _ _) = BalanceSpecial+    ShouldBalance (N R (N R _ _ _) _ _) _ = BalanceLL+    ShouldBalance (N R _ _ (N R _ _ _)) _ = BalanceLR+    ShouldBalance _ (N R (N R _ _ _) _ _) = BalanceRL+    ShouldBalance _ (N R _ _ (N R _ _ _)) = BalanceRR+    ShouldBalance _ _                     = DoNotBalance++class Balanceable (left :: TypeSet ki) (k :: ki) (right :: TypeSet ki) where+    type Balance left k right :: TypeSet ki++instance (ShouldBalance left right ~ action,+          BalanceableHelper action left k right+         )+         => Balanceable left k right where+    -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family.+    -- Is that bad? How to avoid it?+    type Balance left k right = Balance' (ShouldBalance left right) left k right++class BalanceableHelper (action :: BalanceAction)+                        (left :: TypeSet ki)+                        (k :: ki)+                        (right :: TypeSet ki) where+    type Balance' action left k right :: TypeSet ki++-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)+instance BalanceableHelper BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) where+    type Balance'          BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) =+                                      N R (N B left1 k1 right1) kx (N B left2 k2 right2)++-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+instance BalanceableHelper BalanceLL (N R (N R a k1 b) k2 c) k3 d where+    type Balance'          BalanceLL (N R (N R a k1 b) k2 c) k3 d =+                                 N R (N B a k1 b) k2 (N B c k3 d)++-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+instance BalanceableHelper BalanceLR (N R a k1 (N R b k2 c)) k3 d where+    type Balance'          BalanceLR (N R a k1 (N R b k2 c)) k3 d =+                                 N R (N B a k1 b) k2 (N B c k3 d)++-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+instance BalanceableHelper BalanceRL a k1 (N R (N R b k2 c) k3 d) where+    type Balance'          BalanceRL a k1 (N R (N R b k2 c) k3 d) =+                                 N R (N B a k1 b) k2 (N B c k3 d)+++-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+instance BalanceableHelper BalanceRR a k1(N R b k2 (N R c k3 d)) where+    type Balance'          BalanceRR a k1(N R b k2 (N R c k3 d)) =+                                 N R (N B a k1 b) k2 (N B c k3 d)++-- balance a x b = T B a x b+instance BalanceableHelper DoNotBalance a k b where+    type Balance'          DoNotBalance a k b = N B a k b+++--- Member+---+---+------------------------------------------------------------------------------+-- | /O(log n)/. Determine membership in the 'TypeSet.'+type family Member (t :: k) (bst :: TypeSet k)  :: Bool where+  Member t 'E = 'False+  Member t ('N _ lbst a rbst) = MemberImpl (CmpType t a) t lbst rbst++type family MemberImpl (ord :: Ordering)+                       (t :: k)+                       (lbst :: TypeSet k)+                       (rbst :: TypeSet k) :: Bool where+  MemberImpl 'EQ t lbst rbst = 'True+  MemberImpl 'LT t lbst rbst = Member t lbst+  MemberImpl 'GT t lbst rbst = Member t rbst++------------------------------------------------------------------------------+-- | /O(m log n)/ for @Merge m n@; put your smaller set on the left side. Merge+-- two 'TypeSet's together.+type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k where+  Merge Empty big   = big+  Merge small Empty = small+  Merge ('N _ lbst a rbst) big = Merge rbst (Merge lbst (Insert a big))+++--+--+--+-- deletion+--+--+--++type family DiscriminateBalL (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where+    DiscriminateBalL (N R _ _ _) _ = False+    DiscriminateBalL _           _ = True++class BalanceableL (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where+    type BalL l k r :: TypeSet ki++class BalanceableHelperL (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where+    type BalL' b l k r :: TypeSet ki++instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k r) => BalanceableL l k r where+    type BalL l k r = BalL' (DiscriminateBalL l r) l k r++-- balleft :: RB a -> a -> RB a -> RB a+-- balleft (T R a x b) y c = T R (T B a x b) y c+instance BalanceableHelperL False (N R left1 k1 right1) k2 right2 where+    type BalL'              False (N R left1 k1 right1) k2 right2 =+                             (N R (N B left1 k1 right1) k2 right2)++-- balleft bl x (T B a y b) = balance bl x (T R a y b)+-- the @(N B in the call to balance tree is misleading, as it is ingored...+instance (N R t2 z t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y g) =>+    BalanceableHelperL True t1 y (N B t2 z t3) where+    type BalL'         True t1 y (N B t2 z t3)+                 =  Balance t1 y (N R t2 z t3)++-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))+instance (N R l k r ~ g, BalanceableHelper    (ShouldBalance t3 g) t3 z g) =>+    BalanceableHelperL True t1 y (N R (N B t2 u t3) z (N B l k r)) where+    type BalL'         True t1 y (N R (N B t2 u t3) z (N B l k r)) =+                             N R (N B t1 y t2) u (Balance t3 z (N R l k r))+++-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+-- balright (T B a x b) y bl = balance (T R a x b) y bl+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+type family DiscriminateBalR (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where+    DiscriminateBalR _ (N R _ _ _) = False+    DiscriminateBalR _ _           = True++class BalanceableR (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where+    type BalR l k r :: TypeSet ki++class BalanceableHelperR (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where+    type BalR' b l k r :: TypeSet ki++instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k r) => BalanceableR l k r where+    type BalR l k r = BalR' (DiscriminateBalR l r) l k r++-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+instance BalanceableHelperR False right2 k2 (N R left1 k1 right1) where+    type BalR'              False right2 k2 (N R left1 k1 right1) =+                                  (N R right2 k2 (N B left1 k1 right1))++-- balright (T B a x b) y bl = balance (T R a x b) y bl+instance (N R t2 z t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y t1) =>+    BalanceableHelperR True (N B t2 z t3) y t1 where+    type BalR'         True (N B t2 z t3) y t1+             =  Balance (N R t2 z t3) y t1++-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+instance (N R t2 u t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z l) =>+    BalanceableHelperR True (N R (N B t2 u t3) z (N B l k r)) y t1 where+    type BalR'         True (N R (N B t2 u t3) z (N B l k r)) y t1 =+                             N R (Balance (N R t2 u t3) z l) k (N B r y t1)+-- app :: RB a -> RB a -> RB a+-- app E x = x+-- app x E = x+-- app (T R a x b) (T R c y d) =+--  case app b c of+--      T R b' z c' -> T R(T R a x b') z (T R c' y d)+--      bc -> T R a x (T R bc y d)+-- app (T B a x b) (T B c y d) =+--  case app b c of+--      T R b' z c' -> T R(T B a x b') z (T B c' y d)+--      bc -> balleft a x (T B bc y d)+-- app a (T R b x c) = T R (app a b) x c+-- app (T R a x b) c = T R a x (app b c)+++class Fuseable (l :: TypeSet ki) (r :: TypeSet ki) where+    type Fuse l r :: TypeSet ki++instance Fuseable E E where+    type Fuse E E = E++-- app E x = x+instance Fuseable E (N color left k right) where+    type Fuse E (N color left k right) = N color left k right++-- app x E = x+instance Fuseable (N color left k right) E where+    type Fuse (N color left k right) E = N color left k right++-- app a (T R b x c) = T R (app a b) x c+instance Fuseable (N B left1 k1 right1) left2+    => Fuseable (N B left1 k1 right1) (N R left2 k2 right2) where+    type Fuse   (N B left1 k1 right1) (N R left2 k2 right2) = N R (Fuse (N B left1 k1 right1) left2) k2 right2+++-- app (T R a x b) c = T R a x (app b c)+instance Fuseable right1 (N B left2 k2 right2)+    => Fuseable (N R left1 k1 right1) (N B left2 k2 right2) where+    type Fuse   (N R left1 k1 right1) (N B left2 k2 right2) = N R left1 k1 (Fuse right1 (N B left2 k2 right2))+++-- app (T R a x b) (T R c y d) =+instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 right1) (N R left2 k2 right2))+    => Fuseable (N R left1 k1 right1) (N R left2 k2 right2) where+    type Fuse   (N R left1 k1 right1) (N R left2 k2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 right1) (N R left2 k2 right2)++class FuseableHelper1 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where+    type Fuse1 fused l r :: TypeSet ki++-- app (T R a x b) (T R c y d) =+--  case app b c of+--      T R b' z c' -> T R (T R a x b') z (T R c' y d)+-- FIXME: The Fuseable constraint is repeated from avobe :(+instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)+    => FuseableHelper1 (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where+    type Fuse1         (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R (N R left1 k1 s1) z (N R s2 k2 right2)+++-- app (T R a x b) (T R c y d) =+--  case app b c of+--      ...+--      bc -> T R a x (T R bc y d)+-- FIXME: The Fuseable constraint is repeated from above :(+instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2)+    => FuseableHelper1 (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where+    type Fuse1         (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R left1 k1 (N R (N B s1 z s2) k2 right2)++-- app (T R a x b) (T R c y d) =+--  case app b c of+--      ...+--      bc -> T R a x (T R bc y d)+instance FuseableHelper1 E (N R left1 k1 E) (N R E k2 right2) where+    type Fuse1           E (N R left1 k1 E) (N R E k2 right2) = N R left1 k1 (N R E k2 right2)++-- app (T B a x b) (T B c y d) =+instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 right1) (N B left2 k2 right2))+    => Fuseable (N B left1 k1 right1) (N B left2 k2 right2) where+    type Fuse   (N B left1 k1 right1) (N B left2 k2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 right1) (N B left2 k2 right2)++-- could FuseableHelper1 and FuseableHelper2 be, well... fused?+class FuseableHelper2 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where+    type Fuse2 fused l r :: TypeSet ki++-- app (T B a x b) (T B c y d) =+--  case app b c of+--      T R b' z c' -> T R (T B a x b') z (T B c' y d)+instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)+    => FuseableHelper2 (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where+    type Fuse2         (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = N R (N B left1 k1 s1) z (N B s2 k2 right2)++-- app (T B a x b) (T B c y d) =+--  case app b c of+--      ...+--      bc -> balleft a x (T B bc y d)+instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2, BalanceableL left1 k1 (N B (N B s1 z s2) k2 right2))+    => FuseableHelper2 (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where+    type Fuse2         (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = BalL left1 k1 (N B (N B s1 z s2) k2 right2)++-- app (T B a x b) (T B c y d) =+--  case app b c of+--      ...+--      bc -> balleft a x (T B bc y d)+instance (BalanceableL left1 k1 (N B E k2 right2))+    => FuseableHelper2 E (N B left1 k1 E) (N B E k2 right2) where+    type Fuse2         E (N B left1 k1 E) (N B E k2 right2) = BalL left1 k1 (N B E k2 right2)+++--  del E = E+--  del (T _ a y b)+--      | x<y = delformLeft a y b+--      | x>y = delformRight a y b+--      | otherwise = app a b+class Delable (k :: ki) (t :: TypeSet ki) where+    type Del k t :: TypeSet ki++--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b+--  delformLeft a y b = T R (del a) y b+--  In the term-level code, the k to delete is already on the environment.+class DelableL (k :: ki) (l :: TypeSet ki) (kx :: ki)  (r :: TypeSet ki) where+    type DelL k l kx r :: TypeSet ki++--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b+instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableL deleted kx right)+    => DelableL k (N B leftz kz rightz) kx right where+    type DelL   k (N B leftz kz rightz) kx right = BalL (Del k (N B leftz kz rightz)) kx right++--  delformLeft a y b = T R (del a) y b+instance (Delable k (N R leftz kz rightz))+    => DelableL k (N R leftz kz rightz) kx right where+    type DelL   k (N R leftz kz rightz) kx right = N R (Del k (N R leftz kz rightz)) kx right++--  delformLeft a y b = T R (del a) y b+instance DelableL k E kx right where+    type DelL     k E kx right = N R E kx right++--  delformRight a y b@(T B _ _ _) = balright a y (del b)+--  delformRight a y b = T R a y (del b)+class DelableR (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where+    type DelR k l kx r :: TypeSet ki++--  delformRight a y b@(T B _ _ _) = balright a y (del b)+instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableR left kx deleted)+    => DelableR k left kx (N B leftz kz rightz) where+    type DelR   k left kx (N B leftz kz rightz) = BalR left kx (Del k (N B leftz kz rightz))+++--  delformRight a y b = T R a y (del b)+instance (Delable k (N R leftz kz rightz))+    => DelableR k left kx (N R leftz kz rightz) where+    type   DelR k left kx (N R leftz kz rightz) = N R left kx (Del k (N R leftz kz rightz))++--  delformRight a y b = T R a y (del b)+instance DelableR k left kx E where+    type DelR     k left kx E = N R left kx E++--  del E = E+instance Delable k E where+    type Del     k E = E++-- the color is discarded+--  del (T _ a y b)+--      | x<y = delformLeft a y b+--      | x>y = delformRight a y b+--      | otherwise = app a b+instance (CmpType kx k ~ ordering, DelableHelper ordering k left kx right) => Delable k (N color left kx right) where+    type Del k (N color left kx right) = Del' (CmpType kx k) k left kx right++class DelableHelper (ordering :: Ordering) (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where+    type Del' ordering k l kx r :: TypeSet ki++--      | x<y = delformLeft a y b+instance DelableL k left kx right => DelableHelper GT k left kx right where+    type Del'                                      GT k left kx right = DelL k left kx right++--      | otherwise = app a b+instance Fuseable left right => DelableHelper EQ k left k right where+    type Del'                                 EQ k left k right = Fuse left right++--      | x>y = delformRight a y b+instance DelableR k left kx right => DelableHelper LT k left kx right where+    type Del'                                      LT k left kx right = DelR k left kx right++{- | The associated type family 'Remove' produces the resulting map.++ -}+class Removable (k :: ki) (t :: TypeSet ki) where+    type Remove k t :: TypeSet ki++instance (Delable k t, Del k t ~ deleted, CanMakeBlack deleted) => Removable k t where+    type Remove k t = MakeBlack (Del k t)++++-- The original term-level code, taken from:+-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html+--+-- {- Version 1, 'untyped' -}+-- data Color = R | B deriving Show+-- data RB a = E | T Color (RB a) a (RB a) deriving Show+--+-- {- Insertion and membership test as by Okasaki -}+-- insert :: Ord a => a -> RB a -> RB a+-- insert x s =+--  T B a z b+--  where+--  T _ a z b = ins s+--  ins E = T R E x E+--  ins s@(T B a y b)+--      | x<y = balance (ins a) y b+--      | x>y = balance a y (ins b)+--      | otherwise = s+--  ins s@(T R a y b)+--      | x<y = T R (ins a) y b+--      | x>y = T R a y (ins b)+--      | otherwise = s+--+--+-- {- balance: first equation is new,+--    to make it work with a weaker invariant -}+-- balance :: RB a -> a -> RB a -> RB a+-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)+-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+-- balance a x b = T B a x b+--+-- member :: Ord a => a -> RB a -> Bool+-- member x E = False+-- member x (T _ a y b)+--  | x<y = member x a+--  | x>y = member x b+--  | otherwise = True+--+-- {- deletion a la SMK -}+-- delete :: Ord a => a -> RB a -> RB a+-- delete x t =+--  case del t of {T _ a y b -> T B a y b; _ -> E}+--  where+--  del E = E+--  del (T _ a y b)+--      | x<y = delformLeft a y b+--      | x>y = delformRight a y b+--             | otherwise = app a b+--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b+--  delformLeft a y b = T R (del a) y b+--+--  delformRight a y b@(T B _ _ _) = balright a y (del b)+--  delformRight a y b = T R a y (del b)+--+-- balleft :: RB a -> a -> RB a -> RB a+-- balleft (T R a x b) y c = T R (T B a x b) y c+-- balleft bl x (T B a y b) = balance bl x (T R a y b)+-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))+--+-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+-- balright (T B a x b) y bl = balance (T R a x b) y bl+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+--+-- sub1 :: RB a -> RB a+-- sub1 (T B a x b) = T R a x b+-- sub1 _ = error "invariance violation"+--+-- app :: RB a -> RB a -> RB a+-- app E x = x+-- app x E = x+-- app (T R a x b) (T R c y d) =+--  case app b c of+--      T R b' z c' -> T R (T R a x b') z (T R c' y d)+--      bc -> T R a x (T R bc y d)+-- app (T B a x b) (T B c y d) =+--  case app b c of+--      T R b' z c' -> T R(T B a x b') z (T B c' y d)+--      bc -> balleft a x (T B bc y d)+-- app a (T R b x c) = T R (app a b) x c+-- app (T R a x b) c = T R a x (app b c)+

@@ -1,10 +1,13 @@ {-# LANGUAGE DataKinds #-}  {-# OPTIONS_GHC -fplugin=Type.Compare.Plugin      #-}-{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}+{-# OPTIONS_GHC -fconstraint-solver-iterations=0  #-} -- with iterations=10, bit sets fail in the RB tests :(  import Data.Proxy+import Data.Functor.Identity+import Data.Functor.Const import Type.Set+import qualified Type.RBSet as RB  type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty)) @@ -13,6 +16,198 @@  test2 :: Proxy (Member Char MySet) -> Proxy 'False test2 = id  -- False is not a member :(++-- RB tests+--+--+type MyRBSet = RB.FromList '[+                              Bool+                            , String+                            , String+                            , String+                            , Maybe Int+                            , Maybe Char+                            , Char+                            , Either Int Int+                            , Either Int Int+                            , Either Int Int+                            , Either Char Int+                            , Either Bool Int+                            , Maybe Bool+                            , Identity Int+                            , Identity Char+                            , Identity Bool+                            , Either Int (Identity Int)+                            , Either Int (Identity Char)+                            , Either Int (Identity Bool)+                            , Either Char (Identity Int)+                            , Either Char (Identity Char)+                            , Either Char (Identity Bool)+                            , Either Bool (Identity Int)+                            , Either Bool (Identity Char)+                            , Either Bool (Identity Bool)+                            ]++type MyReducedRBSet = RB.Remove Bool+                    ( RB.Remove String+                    ( RB.Remove (Either Int Int)+                    ( RB.Remove (Either Char Int)+                    ( RB.Remove (Either Bool (Identity Int))+                    ( RB.Remove (Either Bool (Identity Char))+                    ( RB.Remove (Either Bool (Identity Bool))+                      MyRBSet))))))++type MyReducedToEmptyRBSet =+                      RB.Remove (Maybe Int)+                    ( RB.Remove (Maybe Char)+                    ( RB.Remove Char+                    ( RB.Remove (Either Bool Int)+                    ( RB.Remove (Maybe Bool)+                    ( RB.Remove (Identity Int)+                    ( RB.Remove (Identity Char)+                    ( RB.Remove (Identity Bool)+                    ( RB.Remove (Either Int (Identity Int))+                    ( RB.Remove (Either Int (Identity Char))+                    ( RB.Remove (Either Int (Identity Bool))+                    ( RB.Remove (Either Char (Identity Int))+                    ( RB.Remove (Either Char (Identity Char))+                    ( RB.Remove (Either Char (Identity Bool))+                      MyReducedRBSet)))))))))))))++type MyMergedRBSet = RB.Merge (RB.FromList '[Const Int Bool,+                                             Const Int Char,+                                             Const Int String])+                              MyReducedRBSet++testRB1 :: Proxy (RB.Member (Bool) MyRBSet) -> Proxy 'True+testRB1 = id+testRB2 :: Proxy (RB.Member (String) MyRBSet) -> Proxy 'True+testRB2 = id+testRB3 :: Proxy (RB.Member (Maybe Int) MyRBSet) -> Proxy 'True+testRB3 = id+testRB4 :: Proxy (RB.Member (Maybe Char) MyRBSet) -> Proxy 'True+testRB4 = id+testRB5 :: Proxy (RB.Member (Char) MyRBSet) -> Proxy 'True+testRB5 = id+testRB6 :: Proxy (RB.Member (Either Int Int) MyRBSet) -> Proxy 'True+testRB6 = id+testRB7 :: Proxy (RB.Member (Either Char Int) MyRBSet) -> Proxy 'True+testRB7 = id+testRB8 :: Proxy (RB.Member (Either Bool Int) MyRBSet) -> Proxy 'True+testRB8 = id+testRB9 :: Proxy (RB.Member (Maybe Bool) MyRBSet) -> Proxy 'True+testRB9 = id+testRB10 :: Proxy (RB.Member (Identity Int) MyRBSet) -> Proxy 'True+testRB10 = id+testRB11 :: Proxy (RB.Member (Identity Char) MyRBSet) -> Proxy 'True+testRB11 = id+testRB12 :: Proxy (RB.Member (Identity Bool) MyRBSet) -> Proxy 'True+testRB12 = id+testRB13 :: Proxy (RB.Member (Either Int (Identity Int)) MyRBSet) -> Proxy 'True+testRB13 = id+testRB14 :: Proxy (RB.Member (Either Int (Identity Char)) MyRBSet) -> Proxy 'True+testRB14 = id+testRB15 :: Proxy (RB.Member (Either Int (Identity Bool)) MyRBSet) -> Proxy 'True+testRB15 = id+testRB16 :: Proxy (RB.Member (Either Char (Identity Int)) MyRBSet) -> Proxy 'True+testRB16 = id+testRB17 :: Proxy (RB.Member (Either Char (Identity Char)) MyRBSet) -> Proxy 'True+testRB17 = id+testRB18 :: Proxy (RB.Member (Either Char (Identity Bool)) MyRBSet) -> Proxy 'True+testRB18 = id+testRB19 :: Proxy (RB.Member (Either Bool (Identity Int)) MyRBSet) -> Proxy 'True+testRB19 = id+testRB20 :: Proxy (RB.Member (Either Bool (Identity Char)) MyRBSet) -> Proxy 'True+testRB20 = id+testRB21 :: Proxy (RB.Member (Either Bool (Identity Bool)) MyRBSet) -> Proxy 'True+testRB21 = id++testRB102 :: Proxy (RB.Member Float MyRBSet) -> Proxy 'False+testRB102 = id  -- False is not a member :(++--+-- Test MyReducedRBSet+testRB201 :: Proxy (RB.Member (Bool) MyReducedRBSet) -> Proxy 'False+testRB201 = id+testRB202 :: Proxy (RB.Member (String) MyReducedRBSet) -> Proxy 'False+testRB202 = id+testRB203 :: Proxy (RB.Member (Either Int Int) MyReducedRBSet) -> Proxy 'False+testRB203 = id+testRB204 :: Proxy (RB.Member (Either Char Int) MyReducedRBSet) -> Proxy 'False+testRB204 = id+testRB205 :: Proxy (RB.Member (Either Bool (Identity Int)) MyReducedRBSet) -> Proxy 'False+testRB205 = id+testRB206 :: Proxy (RB.Member (Either Bool (Identity Char)) MyReducedRBSet) -> Proxy 'False+testRB206 = id+testRB207 :: Proxy (RB.Member (Either Bool (Identity Bool)) MyReducedRBSet) -> Proxy 'False+testRB207 = id++-- the rest remain+testRB303 :: Proxy (RB.Member (Maybe Int) MyReducedRBSet) -> Proxy 'True+testRB303 = id+testRB304 :: Proxy (RB.Member (Maybe Char) MyReducedRBSet) -> Proxy 'True+testRB304 = id+testRB305 :: Proxy (RB.Member (Char) MyReducedRBSet) -> Proxy 'True+testRB305 = id+testRB308 :: Proxy (RB.Member (Either Bool Int) MyReducedRBSet) -> Proxy 'True+testRB308 = id+testRB309 :: Proxy (RB.Member (Maybe Bool) MyReducedRBSet) -> Proxy 'True+testRB309 = id+testRB310 :: Proxy (RB.Member (Identity Int) MyReducedRBSet) -> Proxy 'True+testRB310 = id+testRB311 :: Proxy (RB.Member (Identity Char) MyReducedRBSet) -> Proxy 'True+testRB311 = id+testRB312 :: Proxy (RB.Member (Identity Bool) MyReducedRBSet) -> Proxy 'True+testRB312 = id+testRB313 :: Proxy (RB.Member (Either Int (Identity Int)) MyReducedRBSet) -> Proxy 'True+testRB313 = id+testRB314 :: Proxy (RB.Member (Either Int (Identity Char)) MyReducedRBSet) -> Proxy 'True+testRB314 = id+testRB315 :: Proxy (RB.Member (Either Int (Identity Bool)) MyReducedRBSet) -> Proxy 'True+testRB315 = id+testRB316 :: Proxy (RB.Member (Either Char (Identity Int)) MyReducedRBSet) -> Proxy 'True+testRB316 = id+testRB317 :: Proxy (RB.Member (Either Char (Identity Char)) MyReducedRBSet) -> Proxy 'True+testRB317 = id+testRB318 :: Proxy (RB.Member (Either Char (Identity Bool)) MyReducedRBSet) -> Proxy 'True+testRB318 = id++-- Tests for MyMergedRBSet+testRB400 :: Proxy (RB.Member (Const Int Bool) MyMergedRBSet) -> Proxy 'True+testRB400 = id+testRB401 :: Proxy (RB.Member (Const Int Char) MyMergedRBSet) -> Proxy 'True+testRB401 = id+testRB402 :: Proxy (RB.Member (Const Int String) MyMergedRBSet) -> Proxy 'True+testRB402 = id++testRB403 :: Proxy (RB.Member (Maybe Int) MyMergedRBSet) -> Proxy 'True+testRB403 = id+testRB404 :: Proxy (RB.Member (Maybe Char) MyMergedRBSet) -> Proxy 'True+testRB404 = id+testRB405 :: Proxy (RB.Member (Char) MyMergedRBSet) -> Proxy 'True+testRB405 = id+testRB408 :: Proxy (RB.Member (Either Bool Int) MyMergedRBSet) -> Proxy 'True+testRB408 = id+testRB409 :: Proxy (RB.Member (Maybe Bool) MyMergedRBSet) -> Proxy 'True+testRB409 = id+testRB410 :: Proxy (RB.Member (Identity Int) MyMergedRBSet) -> Proxy 'True+testRB410 = id+testRB411 :: Proxy (RB.Member (Identity Char) MyMergedRBSet) -> Proxy 'True+testRB411 = id+testRB412 :: Proxy (RB.Member (Identity Bool) MyMergedRBSet) -> Proxy 'True+testRB412 = id+testRB413 :: Proxy (RB.Member (Either Int (Identity Int)) MyMergedRBSet) -> Proxy 'True+testRB413 = id+testRB414 :: Proxy (RB.Member (Either Int (Identity Char)) MyMergedRBSet) -> Proxy 'True+testRB414 = id+testRB415 :: Proxy (RB.Member (Either Int (Identity Bool)) MyMergedRBSet) -> Proxy 'True+testRB415 = id+testRB416 :: Proxy (RB.Member (Either Char (Identity Int)) MyMergedRBSet) -> Proxy 'True+testRB416 = id+testRB417 :: Proxy (RB.Member (Either Char (Identity Char)) MyMergedRBSet) -> Proxy 'True+testRB417 = id+testRB418 :: Proxy (RB.Member (Either Char (Identity Bool)) MyMergedRBSet) -> Proxy 'True+testRB418 = id  main :: IO () main = putStrLn "It compiled!"

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 60b368d526cc5cac3b6dd1535ea9d63df46fe48ac16f522464490b53a71a034b+-- hash: b462ce7243b616ca6d6a73fd65f8ead37c671611e51cbcd0c759f4cf55154214  name:           type-sets-version:        0.1.0.0+version:        0.1.1.0 synopsis:       Type-level sets description:    Please see the README on GitHub at <https://github.com/isovector/type-sets#readme> category:       Type@@ -29,6 +29,7 @@  library   exposed-modules:+      Type.RBSet       Type.Set       Type.Set.Variant   other-modules:@@ -37,7 +38,7 @@       src   build-depends:       base >=4.7 && <5-    , cmptype >=0.1.0.0 && <0.2+    , cmptype >=0.1.0.0 && <=0.3.0.0   default-language: Haskell2010  test-suite type-sets-test@@ -50,6 +51,6 @@   ghc-options: -threaded -rtsopts -with-rtsopts=-N   build-depends:       base >=4.7 && <5-    , cmptype >=0.1.0.0 && <0.2+    , cmptype >=0.1.0.0 && <=0.3.0.0     , type-sets   default-language: Haskell2010