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