src/Pure/library.ML
changeset 16691 539b9cc282fa
parent 16688 e3de7ea24c23
child 16694 f8ca69762221
     1.1 --- a/src/Pure/library.ML	Tue Jul 05 15:39:48 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 05 15:49:19 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  tables, balanced trees, orders, current directory, misc.
     1.5  *)
     1.6  
     1.7 -infix |> |-> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
     1.8 +infix |> |-> |>> ||> |>>> ||>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
     1.9    mem mem_int mem_string union union_int union_string inter inter_int
    1.10    inter_string subset subset_int subset_string;
    1.11  
    1.12 @@ -22,9 +22,11 @@
    1.13    val I: 'a -> 'a
    1.14    val K: 'a -> 'b -> 'a
    1.15    val |> : 'a * ('a -> 'b) -> 'b
    1.16 -  val |-> : ('a * 'c) * ('c -> 'a -> 'b) -> 'b
    1.17 -  val |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b
    1.18 -  val |>>> : ('a * 'b) * ('a -> 'c * 'd) -> 'c * ('b * 'd)
    1.19 +  val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    1.20 +  val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    1.21 +  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.22 +  val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.23 +  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    1.24    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.25    val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    1.26    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.27 @@ -85,6 +87,7 @@
    1.28    val apply: ('a -> 'a) list -> 'a -> 'a
    1.29    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.30    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.31 +  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    1.32    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.33    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.34    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.35 @@ -297,9 +300,11 @@
    1.36  
    1.37  (*reverse apply*)
    1.38  fun (x |> f) = f x;
    1.39 -fun ((x, v) |-> f) = f v x;
    1.40 +fun ((x, y) |-> f) = f x y;
    1.41  fun ((x, y) |>> f) = (f x, y);
    1.42 +fun ((x, y) ||> f) = (x, f y);
    1.43  fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;
    1.44 +fun ((x, y) ||>> f) = let val (z, y') = f y in ((x, z), y') end;
    1.45  
    1.46  (*application of (infix) operator to its left or right argument*)
    1.47  fun apl (x, f) y = f (x, y);
    1.48 @@ -465,6 +470,16 @@
    1.49        | fold_aux (x :: xs) y = f x (fold_aux xs y);
    1.50    in fold_aux end;
    1.51  
    1.52 +fun fold_map f = 
    1.53 +  let
    1.54 +    fun fold_aux [] y = ([], y)
    1.55 +      | fold_aux (x :: xs) y =
    1.56 +          let
    1.57 +            val (x', y') = f x y
    1.58 +            val (xs', y'') = fold_aux xs y'
    1.59 +          in (x' :: xs', y'') end;
    1.60 +  in fold_aux end;
    1.61 +
    1.62  fun foldl_map f =
    1.63    let
    1.64      fun fold_aux (x, []) = (x, [])