blob: 016ac830170ac516dc76f71d97c2bd4a48064600 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
{-# LANGUAGE GADTs #-}
module ShouldCompile where
-- data RBTree = forall n. Root (SubTree Black n)
-- Kind Colour
data Red
data Black
-- Kind Nat
data Z
data S a
data SubTree c n where
Leaf :: SubTree Black Z
RNode :: SubTree Black n -> Int -> SubTree Black n -> SubTree Red n
BNode :: SubTree cL m -> Int -> SubTree cR m -> SubTree Black (S m)
Fix :: SubTree Red n -> SubTree Black n
ins :: Int -> SubTree c n -> SubTree c n
ins n Leaf = (Fix (RNode Leaf n Leaf))
ins n (BNode x m y) | n <= m = black (ins n x) m y
ins n (BNode x m y) | n > m = black x m (ins n y)
ins n (RNode x m y) | n <= m = RNode (ins n x) m y
ins n (RNode x m y) | n > m = RNode x m (ins n y)
black :: SubTree c n -> Int -> SubTree d n -> SubTree Black (S n)
black (RNode (Fix u) v c) w (x@(RNode _ _ _)) = Fix(RNode (blacken u) v (BNode c w x))
black (RNode (Fix u) v c) w (x@(BNode _ _ _)) = BNode u v (RNode c w x)
black (RNode a v (Fix (RNode b u c))) w (x@(BNode _ _ _)) = BNode (RNode a v b) u (RNode c w x)
black (Fix x) n (Fix y) = BNode x n y
black x n (Fix y) = BNode x n y
black (Fix x) n y = BNode x n y
black x n y = BNode x n y
blacken :: SubTree Red n -> SubTree Black (S n)
blacken (RNode l e r) = (BNode l e r)
|
