|
1 (* Title: Pure/General/balanced_tree.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Makarius |
|
4 |
|
5 Balanced binary trees. |
|
6 *) |
|
7 |
|
8 signature BALANCED_TREE = |
|
9 sig |
|
10 val make: ('a * 'a -> 'a) -> 'a list -> 'a |
|
11 val dest: ('a -> 'a * 'a) -> int -> 'a -> 'a list |
|
12 val access: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> int -> 'a |
|
13 val accesses: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> 'a list |
|
14 end; |
|
15 |
|
16 structure BalancedTree: BALANCED_TREE = |
|
17 struct |
|
18 |
|
19 fun make _ [] = raise Empty |
|
20 | make _ [x] = x |
|
21 | make f xs = |
|
22 let |
|
23 val m = length xs div 2; |
|
24 val (ps, qs) = chop m xs; |
|
25 in f (make f ps, make f qs) end; |
|
26 |
|
27 fun dest f n x = |
|
28 if n <= 0 then raise Empty |
|
29 else if n = 1 then [x] |
|
30 else |
|
31 let |
|
32 val m = n div 2; |
|
33 val (left, right) = f x; |
|
34 in dest f m left @ dest f (n - m) right end; |
|
35 |
|
36 (*construct something of the form f(...g(...(x)...)) for balanced access*) |
|
37 fun access {left = f, right = g, init = x} len i = |
|
38 let |
|
39 fun acc 1 _ = x |
|
40 | acc n i = |
|
41 let val m = n div 2 in |
|
42 if i <= m then f (acc m i) |
|
43 else g (acc (n - m) (i - m)) |
|
44 end; |
|
45 in if 1 <= i andalso i <= len then acc len i else raise Subscript end; |
|
46 |
|
47 (*construct ALL such accesses; could try harder to share recursive calls!*) |
|
48 fun accesses {left = f, right = g, init = x} len = |
|
49 let |
|
50 fun acc 1 = [x] |
|
51 | acc n = |
|
52 let |
|
53 val m = n div 2; |
|
54 val accs_left = acc m; |
|
55 val accs_right = |
|
56 if n - m = m then accs_left |
|
57 else acc (n - m); |
|
58 in map f accs_left @ map g accs_right end; |
|
59 in if 1 <= len then acc len else raise Subscript end; |
|
60 |
|
61 end; |