added perhaps_apply/loop;
authorwenzelm
Tue Oct 16 19:45:54 2007 +0200 (2007-10-16)
changeset 25058d8d8bac48031
parent 25057 021fcbe2aaa5
child 25059 e6e0ee56a672
added perhaps_apply/loop;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Oct 16 18:34:51 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Oct 16 19:45:54 2007 +0200
     1.3 @@ -72,6 +72,8 @@
     1.4    val the_single: 'a list -> 'a
     1.5    val singleton: ('a list -> 'b list) -> 'a -> 'b
     1.6    val apply: ('a -> 'a) list -> 'a -> 'a
     1.7 +  val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
     1.8 +  val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
     1.9    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.10    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.11    val flat: 'a list list -> 'a list
    1.12 @@ -357,6 +359,23 @@
    1.13  fun apply [] x = x
    1.14    | apply (f :: fs) x = apply fs (f x);
    1.15  
    1.16 +fun perhaps_apply funs arg =
    1.17 +  let
    1.18 +    fun app [] res = res
    1.19 +      | app (f :: fs) (changed, x) =
    1.20 +          (case f x of
    1.21 +            NONE => app fs (changed, x)
    1.22 +          | SOME x' => app fs (true, x'));
    1.23 +  in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
    1.24 +
    1.25 +fun perhaps_loop f arg =
    1.26 +  let
    1.27 +    fun loop (changed, x) =
    1.28 +      (case f x of
    1.29 +        NONE => (changed, x)
    1.30 +      | SOME x' => loop (true, x'));
    1.31 +  in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
    1.32 +
    1.33  
    1.34  (* fold -- old versions *)
    1.35