src/Pure/General/balanced_tree.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 32765 3032c0308019
child 47060 e2741ec9ae36
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     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 
    15 structure Balanced_Tree: BALANCED_TREE =
    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;