tuned;
authorwenzelm
Wed Jul 06 10:41:38 2005 +0200 (2005-07-06)
changeset 1670533f38450cab6
parent 16704 89cc9172f0be
child 16706 3a7eee8cc0ff
tuned;
Admin/profiling_report
src/Pure/library.ML
     1.1 --- a/Admin/profiling_report	Wed Jul 06 10:34:07 2005 +0200
     1.2 +++ b/Admin/profiling_report	Wed Jul 06 10:41:38 2005 +0200
     1.3 @@ -14,6 +14,8 @@
     1.4      if (m,^([ 0-9]{10}) (\S+$|GARBAGE COLLECTION.*$),) {
     1.5  	my $count = $1;
     1.6  	my $fun = $2;
     1.7 +	$fun =~ s,-?\(\d+\).*$,,g;
     1.8 +	$fun =~ s,/\d+$,,g;
     1.9  	if ($count =~ m,^\s*(\d)+$,) {
    1.10  	    if (defined($log{$fun})) {
    1.11  		$log{$fun} += $count;
     2.1 --- a/src/Pure/library.ML	Wed Jul 06 10:34:07 2005 +0200
     2.2 +++ b/src/Pure/library.ML	Wed Jul 06 10:41:38 2005 +0200
     2.3 @@ -298,13 +298,13 @@
     2.4  fun I x = x;
     2.5  fun K x = fn y => x;
     2.6  
     2.7 -(*reverse apply*)
     2.8 -fun (x |> f) = f x;
     2.9 -fun ((x, y) |-> f) = f x y;
    2.10 -fun ((x, y) |>> f) = (f x, y);
    2.11 -fun ((x, y) ||> f) = (x, f y);
    2.12 -fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;
    2.13 -fun ((x, y) ||>> f) = let val (z, y') = f y in ((x, z), y') end;
    2.14 +(*reverse application and structured results*)
    2.15 +fun x |> f = f x;
    2.16 +fun (x, y) |-> f = f x y;
    2.17 +fun (x, y) |>> f = (f x, y);
    2.18 +fun (x, y) ||> f = (x, f y);
    2.19 +fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    2.20 +fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    2.21  
    2.22  (*application of (infix) operator to its left or right argument*)
    2.23  fun apl (x, f) y = f (x, y);
    2.24 @@ -475,21 +475,11 @@
    2.25      fun fold_aux [] y = ([], y)
    2.26        | fold_aux (x :: xs) y =
    2.27            let
    2.28 -            val (x', y') = f x y
    2.29 -            val (xs', y'') = fold_aux xs y'
    2.30 +            val (x', y') = f x y;
    2.31 +            val (xs', y'') = fold_aux xs y';
    2.32            in (x' :: xs', y'') end;
    2.33    in fold_aux end;
    2.34  
    2.35 -fun foldl_map f =
    2.36 -  let
    2.37 -    fun fold_aux (x, []) = (x, [])
    2.38 -      | fold_aux (x, y :: ys) =
    2.39 -          let
    2.40 -            val (x', y') = f (x, y);
    2.41 -            val (x'', ys') = fold_aux (x', ys);
    2.42 -          in (x'', y' :: ys') end;
    2.43 -  in fold_aux end;
    2.44 -
    2.45  (*the following versions of fold are designed to fit nicely with infixes*)
    2.46  
    2.47  (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
    2.48 @@ -515,6 +505,16 @@
    2.49  
    2.50  fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
    2.51  
    2.52 +fun foldl_map f =
    2.53 +  let
    2.54 +    fun fold_aux (x, []) = (x, [])
    2.55 +      | fold_aux (x, y :: ys) =
    2.56 +          let
    2.57 +            val (x', y') = f (x, y);
    2.58 +            val (x'', ys') = fold_aux (x', ys);
    2.59 +          in (x'', y' :: ys') end;
    2.60 +  in fold_aux end;
    2.61 +
    2.62  
    2.63  (* basic list functions *)
    2.64