src/Pure/General/seq.ML

--- a/src/Pure/General/seq.ML	Mon Oct 15 19:03:02 2012 +0200
+++ b/src/Pure/General/seq.ML	Tue Oct 16 13:06:40 2012 +0200
@@ -35,6 +35,11 @@
   val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+  datatype 'a result = Result of 'a | Error of unit -> string
+  val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq
+  val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq
+  val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq
+  val the_result: string -> 'a result seq -> 'a
   val succeed: 'a -> 'a seq
   val fail: 'a -> 'b seq
   val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
@@ -110,7 +115,7 @@
 fun of_list xs = fold_rev cons xs empty;
 
 
-(*sequence append:  put the elements of xq in front of those of yq*)
+(*sequence append: put the elements of xq in front of those of yq*)
 fun append xq yq =
   let
     fun copy s =
@@ -161,7 +166,12 @@
       NONE => NONE
     | SOME (x, xq') => SOME (f x, map f xq')));
 
-fun maps f = flat o map f;
+fun maps f xq =
+  make (fn () =>
+    (case pull xq of
+      NONE => NONE
+    | SOME (x, xq') => pull (append (f x) (maps f xq'))));
+
 fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y));
 
 fun lift f xq y = map (fn x => f x y) xq;
@@ -191,6 +201,33 @@
   in its xq end;
 
 
+(* embedded errors *)
+
+datatype 'a result = Result of 'a | Error of unit -> string;
+
+fun maps_results f xq =
+  make (fn () =>
+    (case pull xq of
+      NONE => NONE
+    | SOME (Result x, xq') => pull (append (f x) (maps_results f xq'))
+    | SOME (Error msg, xq') => SOME (Error msg, maps_results f xq')));
+
+fun maps_result f = maps_results (map Result o f);
+fun map_result f = maps_result (single o f);
+
+(*first result or first error within sequence*)
+fun the_result default_msg seq =
+  let
+    fun result opt_msg xq =
+      (case (opt_msg, pull xq) of
+        (_, SOME (Result x, _)) => x
+      | (SOME _, SOME (Error _, xq')) => result opt_msg xq'
+      | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq'
+      | (SOME msg, NONE) => error (msg ())
+      | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg));
+  in result NONE seq end;
+
+
 
 (** sequence functions **)      (*cf. Pure/tactical.ML*)