--- a/NEWS Tue Jan 03 00:06:30 2006 +0100
+++ b/NEWS Tue Jan 03 11:31:15 2006 +0100
@@ -228,14 +228,13 @@
* Pure/library:
val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
- val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
+ val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
The semantics of "burrow" is: "take a function with *simulatanously*
transforms a list of value, and apply it *simulatanously* to a list of
list of values of the appropriate type". Confer this with "map" which
would *not* apply its argument function simulatanously but in
-sequence. "burrow_split" allows the transformator function to yield an
-additional side result.
+sequence. "fold_burrow" has an additional context.
Both actually avoid the usage of "unflat" since they hide away
"unflat" from the user.
--- a/src/Pure/library.ML Tue Jan 03 00:06:30 2006 +0100
+++ b/src/Pure/library.ML Tue Jan 03 11:31:15 2006 +0100
@@ -101,7 +101,7 @@
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
- val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
+ val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
val splitAt: int * 'a list -> 'a list * 'a list
val dropwhile: ('a -> bool) -> 'a list -> 'a list
val nth: 'a list -> int -> 'a
@@ -607,8 +607,8 @@
fun burrow f xss =
unflat xss ((f o flat) xss);
-fun burrow_split f xss =
- apsnd (unflat xss) ((f o flat) xss);
+fun fold_burrow f xss s =
+ apfst (unflat xss) (f (flat xss) s);
(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
(proc x1; ...; proc xn) for side effects*)