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 


18 
fun make _ [] = raise Empty


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 =


27 
if n <= 0 then raise Empty


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;
