23427

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;
