added higher-order combinators for structured results
authorhaftmann
Mon Nov 13 15:43:13 2006 +0100 (2006-11-13)
changeset 213356b9d4a19a3a8
parent 21334 caa210551c01
child 21336 b5c7efb57b3e
added higher-order combinators for structured results
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Nov 13 15:43:12 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 13 15:43:13 2006 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  strings, lists as sets, balanced trees, orders, current directory, misc.
     1.5  *)
     1.6  
     1.7 -infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
     1.8 +infix 1 |> |-> ||> ||>> |>> #> #-> ##> ##>> #>> |>>> ;
     1.9  infix 2 ?;
    1.10  infix 3 o oo ooo oooo;
    1.11  
    1.12 @@ -27,9 +27,12 @@
    1.13    val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.14    val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    1.15    val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    1.16 -  val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.17    val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.18    val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    1.19 +  val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    1.20 +  val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    1.21 +  val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    1.22 +  val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.23    val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
    1.24    val ` : ('b -> 'a) -> 'b -> 'a * 'b
    1.25    val tap: ('b -> 'a) -> 'b -> 'b
    1.26 @@ -303,9 +306,12 @@
    1.27  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    1.28  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    1.29  
    1.30 -(*reverse composition*)
    1.31 +(*reverse composition and structured results*)
    1.32  fun f #> g = g o f;
    1.33  fun f #-> g = uncurry g o f;
    1.34 +fun (f ##> g) x = let val (y, z) = f x in (y, g z) end;
    1.35 +fun (f ##>> g) x = let val (y, z) = f x; val (w, u) = g z in ((y, w), u) end;
    1.36 +fun (f #>> g) x = let val (y, z) = f x in (g y, z) end;
    1.37  
    1.38  (*conditional application*)
    1.39  fun b ? f = fn x => if b x then f x else x;