# HG changeset patch
# User haftmann
# Date 1120571359 -7200
# Node ID 539b9cc282fa1ebc74738c8ee24b1f8da42edadf
# Parent  b8b2579a2509e6b28bc4e0c87b2a5d0151dff878
added combinatros '||>' and '||>>' and fold_map fitting nicely to ST combinator '|->'

diff -r b8b2579a2509 -r 539b9cc282fa src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 05 15:39:48 2005 +0200
+++ b/src/Pure/library.ML	Tue Jul 05 15:49:19 2005 +0200
@@ -8,7 +8,7 @@
 tables, balanced trees, orders, current directory, misc.
 *)
 
-infix |> |-> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
+infix |> |-> |>> ||> |>>> ||>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
   mem mem_int mem_string union union_int union_string inter inter_int
   inter_string subset subset_int subset_string;
 
@@ -22,9 +22,11 @@
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
   val |> : 'a * ('a -> 'b) -> 'b
-  val |-> : ('a * 'c) * ('c -> 'a -> 'b) -> 'b
-  val |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b
-  val |>>> : ('a * 'b) * ('a -> 'c * 'd) -> 'c * ('b * 'd)
+  val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
+  val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
+  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
+  val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
+  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
@@ -85,6 +87,7 @@
   val apply: ('a -> 'a) list -> 'a -> 'a
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
@@ -297,9 +300,11 @@
 
 (*reverse apply*)
 fun (x |> f) = f x;
-fun ((x, v) |-> f) = f v x;
+fun ((x, y) |-> f) = f x y;
 fun ((x, y) |>> f) = (f x, y);
+fun ((x, y) ||> f) = (x, f y);
 fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;
+fun ((x, y) ||>> f) = let val (z, y') = f y in ((x, z), y') end;
 
 (*application of (infix) operator to its left or right argument*)
 fun apl (x, f) y = f (x, y);
@@ -465,6 +470,16 @@
       | fold_aux (x :: xs) y = f x (fold_aux xs y);
   in fold_aux end;
 
+fun fold_map f = 
+  let
+    fun fold_aux [] y = ([], y)
+      | fold_aux (x :: xs) y =
+          let
+            val (x', y') = f x y
+            val (xs', y'') = fold_aux xs y'
+          in (x' :: xs', y'') end;
+  in fold_aux end;
+
 fun foldl_map f =
   let
     fun fold_aux (x, []) = (x, [])