src/Pure/General/balanced_tree.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23427 26202f4e663d
child 29606 fedb8be05f24
permissions -rw-r--r--
tuned signature;
     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;