# HG changeset patch
# User wenzelm
# Date 1192556754 -7200
# Node ID d8d8bac48031a0d32f5fd0ab304dba1d5eef9c22
# Parent  021fcbe2aaa5d945d7a6c9f5d459f33a5122e33c
added perhaps_apply/loop;

diff -r 021fcbe2aaa5 -r d8d8bac48031 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 16 18:34:51 2007 +0200
+++ b/src/Pure/library.ML	Tue Oct 16 19:45:54 2007 +0200
@@ -72,6 +72,8 @@
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
   val apply: ('a -> 'a) list -> 'a -> 'a
+  val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
+  val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val flat: 'a list list -> 'a list
@@ -357,6 +359,23 @@
 fun apply [] x = x
   | apply (f :: fs) x = apply fs (f x);
 
+fun perhaps_apply funs arg =
+  let
+    fun app [] res = res
+      | app (f :: fs) (changed, x) =
+          (case f x of
+            NONE => app fs (changed, x)
+          | SOME x' => app fs (true, x'));
+  in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
+
+fun perhaps_loop f arg =
+  let
+    fun loop (changed, x) =
+      (case f x of
+        NONE => (changed, x)
+      | SOME x' => loop (true, x'));
+  in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
+
 
 (* fold -- old versions *)