author  wenzelm 
Wed, 21 Mar 2012 11:00:34 +0100  
changeset 47060  e2741ec9ae36 
parent 32765  3032c0308019 
permissions  rwrr 
23427  1 
(* Title: Pure/General/balanced_tree.ML 
2 
Author: Lawrence C Paulson and Makarius 

3 

4 
Balanced binary trees. 

5 
*) 

6 

7 
signature BALANCED_TREE = 

8 
sig 

9 
val make: ('a * 'a > 'a) > 'a list > 'a 

10 
val dest: ('a > 'a * 'a) > int > 'a > 'a list 

11 
val access: {left: 'a > 'a, right: 'a > 'a, init: 'a} > int > int > 'a 

12 
val accesses: {left: 'a > 'a, right: 'a > 'a, init: 'a} > int > 'a list 

13 
end; 

14 

32765  15 
structure Balanced_Tree: BALANCED_TREE = 
23427  16 
struct 
17 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
32765
diff
changeset

18 
fun make _ [] = raise List.Empty 
23427  19 
 make _ [x] = x 
20 
 make f xs = 

21 
let 

22 
val m = length xs div 2; 

23 
val (ps, qs) = chop m xs; 

24 
in f (make f ps, make f qs) end; 

25 

26 
fun dest f n x = 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
32765
diff
changeset

27 
if n <= 0 then raise List.Empty 
23427  28 
else if n = 1 then [x] 
29 
else 

30 
let 

31 
val m = n div 2; 

32 
val (left, right) = f x; 

33 
in dest f m left @ dest f (n  m) right end; 

34 

35 
(*construct something of the form f(...g(...(x)...)) for balanced access*) 

36 
fun access {left = f, right = g, init = x} len i = 

37 
let 

38 
fun acc 1 _ = x 

39 
 acc n i = 

40 
let val m = n div 2 in 

41 
if i <= m then f (acc m i) 

42 
else g (acc (n  m) (i  m)) 

43 
end; 

44 
in if 1 <= i andalso i <= len then acc len i else raise Subscript end; 

45 

46 
(*construct ALL such accesses; could try harder to share recursive calls!*) 

47 
fun accesses {left = f, right = g, init = x} len = 

48 
let 

49 
fun acc 1 = [x] 

50 
 acc n = 

51 
let 

52 
val m = n div 2; 

53 
val accs_left = acc m; 

54 
val accs_right = 

55 
if n  m = m then accs_left 

56 
else acc (n  m); 

57 
in map f accs_left @ map g accs_right end; 

58 
in if 1 <= len then acc len else raise Subscript end; 

59 

60 
end; 