# HG changeset patch
# User wenzelm
# Date 1350385600 -7200
# Node ID 52da6a736c320251c1d47a950732863b0e044d6f
# Parent  4a15873c4ec915cc50b3e3602fdcc3a338f0fcb5
more informative error messages of initial/terminal proof methods;
more systematic support for sequences with embedded errors;
tuned Seq.maps;

diff -r 4a15873c4ec9 -r 52da6a736c32 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*)
 
diff -r 4a15873c4ec9 -r 52da6a736c32 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 15 19:03:02 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 13:06:40 2012 +0200
@@ -514,20 +514,16 @@
       | recover_result _ _ = lost_structure ();
   in recover_result propss results end;
 
-fun the_finished_goal results =
-  (case Seq.pull results of
-    SOME ((f1, state1), rest) =>
-      let val (ctxt1, (_, goal1)) = get_goal state1 in
-        if Thm.no_prems goal1 then f1 state1
-        else
-          (case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of
-            SOME ((f, state), _) => f state
-          | NONE =>
-              error ("Failed to finish proof:\n" ^
-                Pretty.string_of
-                  (Goal_Display.pretty_goal {main = true, limit = false} ctxt1 goal1)))
-      end
-  | NONE => error "Failed to finish proof");
+val finished_goal_error = "Failed to finish proof";
+
+fun finished_goal state =
+  let val (ctxt, (_, goal)) = get_goal state in
+    if Thm.no_prems goal then Seq.Result state
+    else
+      Seq.Error (fn () =>
+        finished_goal_error ^ ":\n" ^
+          Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal))
+  end;
 
 
 (* goal views -- corresponding to methods *)
@@ -833,7 +829,8 @@
   |> assert_current_goal true
   |> using_facts []
   |> `before_qed |-> (refine o the_default Method.succeed_text)
-  |> Seq.maps (refine (Method.finish_text txt));
+  |> Seq.maps (refine (Method.finish_text txt))
+  |> Seq.map finished_goal;
 
 fun check_result msg sq =
   (case Seq.pull sq of
@@ -954,10 +951,10 @@
 
 fun local_qeds txt =
   end_proof false txt
-  #> Seq.map (pair (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results)));
+  #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
+    (fn ((after_qed, _), results) => after_qed results));
 
-fun local_qed txt = local_qeds txt #> the_finished_goal;
+fun local_qed txt = local_qeds txt #> Seq.the_result finished_goal_error;
 
 
 (* global goals *)
@@ -975,33 +972,34 @@
 
 fun global_qeds txt =
   end_proof true txt
-  #> Seq.map (pair (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state))));
+  #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+    after_qed results (context_of state)));
 
-fun global_qed txt = global_qeds txt #> the_finished_goal;
+fun global_qed txt = global_qeds txt #> Seq.the_result finished_goal_error;
 
 
 (* concluding steps *)
 
-local
-
-fun failure_initial state =
+fun method_error name state = Seq.Error (fn () =>
   let
     val (ctxt, (facts, goal)) = get_goal state;
+    val pr_header =
+      "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method on goal state:\n";
     val pr_facts =
       if null facts then ""
       else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n";
     val pr_goal =
       "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal);
-  in error ("Failure of initial proof method on goal state:\n" ^ pr_facts ^ pr_goal) end;
+  in pr_header ^ pr_facts ^ pr_goal end);
 
-fun failure_terminal _ = error "Failure of terminal proof method";
+local
 
-val op ORELSE = Seq.ORELSE;
+val op APPEND = Seq.APPEND;
 
 fun terminal_proof qeds initial terminal =
-  (((proof (SOME initial) ORELSE failure_initial)
-    #> Seq.maps (qeds terminal)) ORELSE failure_terminal) #> the_finished_goal;
+  ((proof (SOME initial) #> Seq.map Seq.Result) APPEND (Seq.single o method_error "initial"))
+  #> Seq.maps_results (qeds terminal APPEND (Seq.single o method_error "terminal"))
+  #> Seq.the_result "";
 
 in