26 import Types.Data.Bool
27 import Types.Data.List hiding (Null)
28 import Types.Data.Maybe
33 data Bin size key value left right
37 instance Map (Bin s k v l r)
41 type instance Null Tip = True
42 type instance Null (Bin s k v l r) = False
46 type instance Size Tip = D0
47 type instance Size (Bin s k v l r) = s
50 type family Lookup k m
51 type instance Lookup k Tip = Nothing
52 type instance Lookup k (Bin s k' v l r)
53 = If (IsLT (Compare k k'))
55 (If (IsGT (Compare k k'))
60 type family LookupAssoc k m
61 type instance LookupAssoc k Tip = Nothing
62 type instance LookupAssoc k (Bin s k' v l r)
63 = If (IsLT (Compare k k'))
65 (If (IsGT (Compare k k'))
70 type Member k m = IsJust (Lookup k m)
73 type NotMember k m = Not (Member k m)
76 type Find k m = FromJust (Lookup k m)
79 type FindWithDefault a k m
80 = FromMaybe a (Lookup k m)
86 type Singleton k v = Bin D1 k v Tip Tip
89 type family Insert k v m
90 type instance Insert k v Tip = Singleton k v
91 type instance Insert k v (Bin s k' v' l r)
92 = If (IsLT (Compare k k'))
93 (Balance k' v' (Insert k v l) r)
94 (If (IsGT (Compare k k'))
95 (Balance k' v' l (Insert k v r))
103 = If (Size l :+: Size r :<: 1)
104 (Bin (Size l :+: Size r :+: D1) k v l r)
105 (If (Size r :>=: Delta :*: Size l)
107 (If (Size l :>=: Delta :*: Size r)
109 (Bin (Size l :+: Size r :+: D1) k v l r)))
112 type family RotateL k v l r
113 type instance RotateL k v l (Bin s k' v' l' r')
114 = If (Size l' :<: Ratio :*: Size r')
115 (SingleL k v l (Bin s k' v' l' r'))
116 (DoubleL k v l (Bin s k' v' l' r'))
118 type family RotateR k v l r
119 type instance RotateR k v (Bin s k' v' l' r') r
120 = If (Size r' :<: Ratio :*: Size l')
121 (SingleR k v (Bin s k' v' l' r') r)
122 (DoubleR k v (Bin s k' v' l' r') r)
125 type family SingleL k v l r
126 type instance SingleL k v l (Bin s k' v' l' r')
127 = Bin' k' v' (Bin' k v l l') r'
129 type family SingleR k v l r
130 type instance SingleR k v (Bin s k' v' l r) r'
131 = Bin' k' v' l (Bin' k v r r')
133 type family DoubleL k v l r
134 type instance DoubleL k v l (Bin s k' v' (Bin s' k'' v'' l' r) r')
135 = Bin' k'' v'' (Bin' k v l l') (Bin' k' v' r r')
137 type family DoubleR k v l r
138 type instance DoubleR k v (Bin s k' v' l (Bin s' k'' v'' l' r)) r'
139 = Bin' k'' v'' (Bin' k' v' l l') (Bin' k v r r')
143 = Bin (Size l :+: Size r :+: D1) k v l r