rearranged burrow_split to fold_burrow to allow composition with fold_map
authorhaftmann
Tue Jan 03 11:31:15 2006 +0100 (2006-01-03)
changeset 185495308a6ea3b96
parent 18548 cb8e8fb9e52d
child 18550 59b89f625d68
rearranged burrow_split to fold_burrow to allow composition with fold_map
NEWS
src/Pure/library.ML
     1.1 --- a/NEWS	Tue Jan 03 00:06:30 2006 +0100
     1.2 +++ b/NEWS	Tue Jan 03 11:31:15 2006 +0100
     1.3 @@ -228,14 +228,13 @@
     1.4  * Pure/library:
     1.5  
     1.6    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     1.7 -  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
     1.8 +  val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
     1.9  
    1.10  The semantics of "burrow" is: "take a function with *simulatanously*
    1.11  transforms a list of value, and apply it *simulatanously* to a list of
    1.12  list of values of the appropriate type". Confer this with "map" which
    1.13  would *not* apply its argument function simulatanously but in
    1.14 -sequence. "burrow_split" allows the transformator function to yield an
    1.15 -additional side result.
    1.16 +sequence. "fold_burrow" has an additional context.
    1.17  
    1.18  Both actually avoid the usage of "unflat" since they hide away
    1.19  "unflat" from the user.
     2.1 --- a/src/Pure/library.ML	Tue Jan 03 00:06:30 2006 +0100
     2.2 +++ b/src/Pure/library.ML	Tue Jan 03 11:31:15 2006 +0100
     2.3 @@ -101,7 +101,7 @@
     2.4    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     2.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     2.6    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     2.7 -  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
     2.8 +  val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
     2.9    val splitAt: int * 'a list -> 'a list * 'a list
    2.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    2.11    val nth: 'a list -> int -> 'a
    2.12 @@ -607,8 +607,8 @@
    2.13  fun burrow f xss =
    2.14    unflat xss ((f o flat) xss);
    2.15  
    2.16 -fun burrow_split f xss =
    2.17 -  apsnd (unflat xss) ((f o flat) xss);
    2.18 +fun fold_burrow f xss s =
    2.19 +  apfst (unflat xss) (f (flat xss) s);
    2.20  
    2.21  (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
    2.22    (proc x1; ...; proc xn) for side effects*)