src/Pure/library.ML
 changeset 16705 33f38450cab6 parent 16694 f8ca69762221 child 16721 e2427ea379a9
```     1.1 --- a/src/Pure/library.ML	Wed Jul 06 10:34:07 2005 +0200
1.2 +++ b/src/Pure/library.ML	Wed Jul 06 10:41:38 2005 +0200
1.3 @@ -298,13 +298,13 @@
1.4  fun I x = x;
1.5  fun K x = fn y => x;
1.6
1.7 -(*reverse apply*)
1.8 -fun (x |> f) = f x;
1.9 -fun ((x, y) |-> f) = f x y;
1.10 -fun ((x, y) |>> f) = (f x, y);
1.11 -fun ((x, y) ||> f) = (x, f y);
1.12 -fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;
1.13 -fun ((x, y) ||>> f) = let val (z, y') = f y in ((x, z), y') end;
1.14 +(*reverse application and structured results*)
1.15 +fun x |> f = f x;
1.16 +fun (x, y) |-> f = f x y;
1.17 +fun (x, y) |>> f = (f x, y);
1.18 +fun (x, y) ||> f = (x, f y);
1.19 +fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
1.20 +fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
1.21
1.22  (*application of (infix) operator to its left or right argument*)
1.23  fun apl (x, f) y = f (x, y);
1.24 @@ -475,21 +475,11 @@
1.25      fun fold_aux [] y = ([], y)
1.26        | fold_aux (x :: xs) y =
1.27            let
1.28 -            val (x', y') = f x y
1.29 -            val (xs', y'') = fold_aux xs y'
1.30 +            val (x', y') = f x y;
1.31 +            val (xs', y'') = fold_aux xs y';
1.32            in (x' :: xs', y'') end;
1.33    in fold_aux end;
1.34
1.35 -fun foldl_map f =
1.36 -  let
1.37 -    fun fold_aux (x, []) = (x, [])
1.38 -      | fold_aux (x, y :: ys) =
1.39 -          let
1.40 -            val (x', y') = f (x, y);
1.41 -            val (x'', ys') = fold_aux (x', ys);
1.42 -          in (x'', y' :: ys') end;
1.43 -  in fold_aux end;
1.44 -
1.45  (*the following versions of fold are designed to fit nicely with infixes*)
1.46
1.47  (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
1.48 @@ -515,6 +505,16 @@
1.49
1.50  fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
1.51
1.52 +fun foldl_map f =
1.53 +  let
1.54 +    fun fold_aux (x, []) = (x, [])
1.55 +      | fold_aux (x, y :: ys) =
1.56 +          let
1.57 +            val (x', y') = f (x, y);
1.58 +            val (x'', ys') = fold_aux (x', ys);
1.59 +          in (x'', y' :: ys') end;
1.60 +  in fold_aux end;
1.61 +
1.62
1.63  (* basic list functions *)
1.64
```