type instance Size (Bin s k v l r) = s
-- CompCase
-type CompCase a b ifLT ifGT ifEQ
- = If (IsLT (Compare a b))
- ifLT
- (If (IsGT (Compare a b))
- ifGT
- ifEQ)
+type family CompCase o ifLT ifGT ifEQ
+type instance CompCase LT ifLT ifGT ifEQ = ifLT
+type instance CompCase GT ifLT ifGT ifEQ = ifGT
+type instance CompCase EQ ifLT ifGT ifEQ = ifEQ
-- Lookup
type family Lookup k m
type instance Lookup k Tip = Nothing
type instance Lookup k (Bin s k' v l r)
- = CompCase k k'
+ = CompCase (Compare k k')
(Lookup k l)
(Lookup k r)
(Just v)
type family LookupAssoc k m
type instance LookupAssoc k Tip = Nothing
type instance LookupAssoc k (Bin s k' v l r)
- = CompCase k k'
+ = CompCase (Compare k k')
(LookupAssoc k l)
(LookupAssoc k r)
(Just (Cons k v))
type family Insert k v m
type instance Insert k v Tip = Singleton k v
type instance Insert k v (Bin s k' v' l r)
- = CompCase k k'
+ = CompCase (Compare k k')
(Balance k' v' (Insert k v l) r)
(Balance k' v' l (Insert k v r))
(Bin s k v l r)
type family Delete k m
type instance Delete k Tip = Tip
type instance Delete k (Bin s k' v l r)
- = CompCase k k'
+ = CompCase (Compare k k')
(Balance k' v (Delete k l) r)
(Balance k' v l (Delete k r))
(Glue l r)
type Balance k v l r
= If ((Size l :+: Size r) :<=: D1)
- (Bin (Size l :+: Size r :+: D1) k v l r)
+ (Bin (SizeX l r) k v l r)
(If (Size r :>=: (Delta :*: Size l))
(RotateL k v l r)
(If (Size l :>=: (Delta :*: Size r))
(RotateR k v l r)
- (Bin (Size l :+: Size r :+: D1) k v l r)))
+ (Bin (SizeX l r) k v l r)))
+
+type SizeX l r = Size l :+: Size r :+: D1
-- Rotate
type family RotateL k v l r
type family UpdateWithKey f k m
type instance UpdateWithKey f k Tip = Tip
type instance UpdateWithKey f k (Bin s k' v l r)
- = CompCase k k'
+ = CompCase (Compare k k')
(Balance k' v (UpdateWithKey f k l) r)
(Balance k' v l (UpdateWithKey f k r))
- (If (IsJust (App2 f k' v))
- (Bin s k' (FromJust (App2 f k' v)) l r)
- (Glue l r))
+ (UpdateWithKey' s k' (App2 f k' v) l r)
+
+type family UpdateWithKey' s k mv l r
+type instance UpdateWithKey' s k (Just v) l r = Bin s k v l r
+type instance UpdateWithKey' s k Nothing l r = Glue l r
-- Map
type MapValue f m = MapWithKey (MapValue' f) m