# HG changeset patch # User wenzelm # Date 1182287754 -7200 # Node ID d0580634f128624bd8e4e1293125d201013f7b29 # Parent b2d64f86d21b66b8b98694846bba395740d96b5c moved balanced tree operations to General/balanced_tree.ML; diff -r b2d64f86d21b -r d0580634f128 src/Pure/library.ML --- a/src/Pure/library.ML Tue Jun 19 23:15:51 2007 +0200 +++ b/src/Pure/library.ML Tue Jun 19 23:15:54 2007 +0200 @@ -4,7 +4,7 @@ Author: Markus Wenzel, TU Muenchen Basic library: functions, options, pairs, booleans, lists, integers, -strings, lists as sets, balanced trees, orders, current directory, misc. +strings, lists as sets, orders, current directory, misc. See also General/basics.ML for the most fundamental concepts. *) @@ -194,12 +194,6 @@ val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool - (*balanced trees*) - exception Balance - val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a - val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a - val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list - (*orders*) val is_equal: order -> bool val rev_order: order -> order @@ -920,39 +914,6 @@ -(** balanced trees **) - -exception Balance; (*indicates non-positive argument to balancing fun*) - -(*balanced folding; avoids deep nesting*) -fun fold_bal f [x] = x - | fold_bal f [] = raise Balance - | fold_bal f xs = - let val (ps, qs) = chop (length xs div 2) xs - in f (fold_bal f ps, fold_bal f qs) end; - -(*construct something of the form f(...g(...(x)...)) for balanced access*) -fun access_bal (f, g, x) n i = - let fun acc n i = (*1<=i<=n*) - if n=1 then x else - let val n2 = n div 2 - in if i<=n2 then f (acc n2 i) - else g (acc (n-n2) (i-n2)) - end - in if 1<=i andalso i<=n then acc n i else raise Balance end; - -(*construct ALL such accesses; could try harder to share recursive calls!*) -fun accesses_bal (f, g, x) n = - let fun acc n = - if n=1 then [x] else - let val n2 = n div 2 - val acc2 = acc n2 - in if n-n2=n2 then map f acc2 @ map g acc2 - else map f acc2 @ map g (acc (n-n2)) end - in if 1<=n then acc n else raise Balance end; - - - (** orders **) fun is_equal EQUAL = true