added ? combinator for conditional transformations
authorhaftmann
Thu Aug 25 09:23:40 2005 +0200 (2005-08-25)
changeset 171414b0dc89de43b
parent 17140 5be3a21ec949
child 17142 76a5a2cc3171
added ? combinator for conditional transformations
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Aug 25 09:23:13 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Aug 25 09:23:40 2005 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    union_string inter inter_int inter_string subset subset_int
     1.5    subset_string;
     1.6  
     1.7 +infix 2 ?;
     1.8 +
     1.9  infix 3 oo ooo oooo;
    1.10  
    1.11  signature BASIC_LIBRARY =
    1.12 @@ -30,6 +32,7 @@
    1.13    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.14    val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.15    val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    1.16 +  val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
    1.17    val ` : ('b -> 'a) -> 'b -> 'a * 'b
    1.18    val tap: ('b -> 'a) -> 'b -> 'b
    1.19    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.20 @@ -320,6 +323,9 @@
    1.21  fun f #> g = g o f;
    1.22  fun f #-> g = uncurry g o f;
    1.23  
    1.24 +(*conditional application*)
    1.25 +fun b ? f = fn x => if b x then f x else x
    1.26 +
    1.27  (*view results*)
    1.28  fun `f = fn x => (f x, x);
    1.29  fun tap f x = (f x; x);