Flatten undone_proof in proof_attempt_status. Avoid producing "undone" reports.

src/ide/gmain.ml

@@ -432,11 +432,11 @@ let clear model = model#clear ()
 
 let image_of_result ~obsolete result =
   match result with
-    | Session.Undone Session.Interrupted -> !image_undone
-    | Session.Undone Session.Unedited
-    | Session.Undone Session.JustEdited -> !image_unknown
-    | Session.Undone Session.Scheduled -> !image_scheduled
-    | Session.Undone Session.Running -> !image_running
+    | Session.Interrupted -> !image_undone
+    | Session.Unedited -> !image_editor
+    | Session.JustEdited -> !image_unknown
+    | Session.Scheduled -> !image_scheduled
+    | Session.Running -> !image_running
     | Session.InternalFailure _ -> !image_failure
     | Session.Done r -> match r.Call_provers.pr_answer with
         | Call_provers.Valid ->
@@ -486,11 +486,11 @@ let set_proof_state a =
           Format.sprintf "%.2f [%d.0]" time a.S.proof_timelimit
         else
           Format.sprintf "%.2f" time
-    | S.Undone S.Unedited -> "(not yet edited)"
-    | S.Undone S.JustEdited -> "(edited)"
+    | S.Unedited -> "(not yet edited)"
+    | S.JustEdited -> "(edited)"
     | S.InternalFailure _ -> "(internal failure)"
-    | S.Undone S.Interrupted -> "(interrupted)"
-    | S.Undone (S.Scheduled | S.Running) ->
+    | S.Interrupted -> "(interrupted)"
+    | S.Scheduled | S.Running ->
         Format.sprintf "[limit=%d sec., %d M]"
           a.S.proof_timelimit a.S.proof_memlimit
   in
@@ -576,17 +576,16 @@ let update_task_view a =
     | S.Proof_attempt a ->
         let o =
           match a.S.proof_state with
-            | S.Undone S.Interrupted ->
-              "proof not yet scheduled for running"
-            | S.Undone S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button"
-            | S.Undone S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button"
+            | S.Interrupted -> "proof not yet scheduled for running"
+            | S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button"
+            | S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button"
             | S.Done ({Call_provers.pr_answer = Call_provers.HighFailure} as r) ->
               let b = Buffer.create 37 in
               bprintf b "%a" Call_provers.print_prover_result r;
               Buffer.contents b
             | S.Done r -> r.Call_provers.pr_output
-            | S.Undone S.Scheduled-> "proof scheduled but not running yet"
-            | S.Undone S.Running -> "prover currently running"
+            | S.Scheduled-> "proof scheduled but not running yet"
+            | S.Running -> "prover currently running"
             | S.InternalFailure e ->
               let b = Buffer.create 37 in
               bprintf b "%a" Exn_printer.exn_printer e;
@@ -955,10 +954,10 @@ let bisect_proof_attempt pa =
   let set_timelimit res =
     timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
   let rec callback lp pa c = function
-    | S.Undone (S.Running | S.Scheduled) -> ()
-    | S.Undone S.Interrupted ->
+    | S.Running | S.Scheduled -> ()
+    | S.Interrupted ->
       dprintf debug "Bisecting interrupted.@."
-    | S.Undone (S.Unedited | S.JustEdited) -> assert false
+    | S.Unedited | S.JustEdited -> assert false
     | S.InternalFailure exn ->
       (** Perhaps the test can be considered false in this case? *)
       dprintf debug "Bisecting interrupted by an error %a.@."
@@ -1005,10 +1004,10 @@ let bisect_proof_attempt pa =
         update the proof attempt *)
   let first_callback pa = function
     (** this pa can be different than the first pa *)
-    | S.Undone (S.Running | S.Scheduled) -> ()
-    | S.Undone S.Interrupted ->
+    | S.Running | S.Scheduled -> ()
+    | S.Interrupted ->
       dprintf debug "Bisecting interrupted.@."
-    | S.Undone (S.Unedited | S.JustEdited) -> assert false
+    | S.Unedited | S.JustEdited -> assert false
     | S.InternalFailure exn ->
         dprintf debug "proof of the initial task interrupted by an error %a.@."
           Exn_printer.exn_printer exn

src/session/session.ml

@@ -41,15 +41,12 @@ let debug = Debug.register_info_flag "session"
 
 module PHstr = Util.Hstr
 
-type undone_proof =
+type proof_attempt_status =
+    | Unedited (** editor not yet run for interactive proof *)
+    | JustEdited (** edited but not run yet *)
+    | Interrupted (** external proof has never completed *)
     | Scheduled (** external proof attempt is scheduled *)
-    | Interrupted
     | Running (** external proof attempt is in progress *)
-    | Unedited
-    | JustEdited
-
-type proof_attempt_status =
-    | Undone of undone_proof
     | Done of Call_provers.prover_result (** external proof done *)
     | InternalFailure of exn (** external proof aborted by internal error *)
 
@@ -491,9 +488,9 @@ let save_result fmt r =
 
 let save_status fmt s =
   match s with
-    | Undone Unedited ->
+    | Unedited ->
         fprintf fmt "@\n<unedited/>"
-    | Undone _ ->
+    | Scheduled | Running | Interrupted | JustEdited ->
         fprintf fmt "@\n<undone/>"
     | InternalFailure msg ->
         fprintf fmt "@\n<internalfailure reason=\"%a\"/>"
@@ -1025,11 +1022,11 @@ let load_result r =
           Call_provers.pr_output = "";
           Call_provers.pr_status = Unix.WEXITED 0
         }
-    | "undone" -> Undone Interrupted
-    | "unedited" -> Undone Unedited
+    | "undone" -> Interrupted
+    | "unedited" -> Unedited
     | s ->
         eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
-        Undone Interrupted
+        Interrupted
 
 let load_option attr g =
   try Some (List.assoc attr g.Xml.attributes)
@@ -1091,7 +1088,7 @@ and load_proof_or_transf ~old_provers mg a =
         in
         let res = match a.Xml.elements with
           | [r] -> load_result r
-          | [] -> Undone Interrupted
+          | [] -> Interrupted
           | _ ->
             eprintf "[Error] Too many result elements@.";
             raise (LoadError (a,"too many result elements"))
@@ -1753,10 +1750,9 @@ let update_edit_external_proof env_session a =
         let file = Sysutil.uniquify file in
         let file = Sysutil.relativize_filename session_dir file in
         set_edited_as (Some file) a;
-        if a.proof_state = Undone Unedited
+        if a.proof_state = Unedited
         then set_proof_state ~notify ~obsolete:a.proof_obsolete
-          ~archived:a.proof_archived
-          (Undone Interrupted) a;
+          ~archived:a.proof_archived Interrupted a;
         file
       | Some f -> f
   in
@@ -1781,7 +1777,12 @@ let update_edit_external_proof env_session a =
   file
 
 let print_attempt_status fmt = function
-  | Undone _ -> pp_print_string fmt "Undone"
+  | Scheduled | Running ->
+    pp_print_string fmt "Running"
+  | JustEdited | Interrupted ->
+    pp_print_string fmt "Not yet run"
+  | Unedited ->
+    pp_print_string fmt "Not yet edited"
   | Done pr -> Call_provers.print_prover_result fmt pr
   | InternalFailure _ -> pp_print_string fmt "Failure"
 

src/session/session.mli

@@ -35,18 +35,13 @@ module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover
 
 (** {2 Proof attempts} *)
 
-(** State of proof without result *)
-type undone_proof =
-    | Scheduled (** external proof attempt is scheduled *)
-    | Interrupted (** external proof has been interrupted or
-                      has never been scheduled*)
-    | Running (** external proof attempt is in progress *)
-    | Unedited (** unedited but editable *)
-    | JustEdited (** edited but not run yet *)
-
 (** State of a proof *)
 type proof_attempt_status =
-    | Undone of undone_proof
+    | Unedited (** editor not yet run for interactive proof *)
+    | JustEdited (** edited but not run yet *)
+    | Interrupted (** external proof has never completed *)
+    | Scheduled (** external proof attempt is scheduled *)
+    | Running (** external proof attempt is in progress *)
     | Done of Call_provers.prover_result (** external proof done *)
     | InternalFailure of exn (** external proof aborted by internal error *)
 

src/session/session_scheduler.ml

@@ -87,9 +87,9 @@ let goals t = t.theory_goals
 let theory_expanded t = t.theory_expanded
 *)
 
-let running a = match a.proof_state with
-  | Undone (Scheduled | Running) -> true
-  | Undone (Unedited | JustEdited | Interrupted)
+let running = function
+  | Scheduled | Running -> true
+  | Unedited | JustEdited | Interrupted
   | Done _ | InternalFailure _ -> false
 
 (*************************)
@@ -170,7 +170,7 @@ let timeout_handler t =
     if List.length l < t.maximum_running_proofs then
       begin try
         let (callback,pre_call) = Queue.pop t.proof_attempts_queue in
-        callback (Undone Running);
+        callback Running;
         dprintf debug "[Sched] proof attempts started@.";
         let call = pre_call () in
         (Check_prover(callback,call))::l
@@ -271,7 +271,7 @@ let cancel_scheduled_proofs t =
       match Queue.pop t.actions_queue with
         | Action_proof_attempt(_timelimit,_memlimit,_old,_inplace,_command,
                                _driver,callback,_goal) ->
-            callback (Undone Interrupted)
+            callback Interrupted
         | Action_delayed _ as a->
             Queue.push a new_queue
     done
@@ -280,7 +280,7 @@ let cancel_scheduled_proofs t =
     try
       while true do
         let (callback,_) = Queue.pop t.proof_attempts_queue in
-        callback (Undone Interrupted)
+        callback Interrupted
       done
     with
       | Queue.Empty ->
@@ -292,7 +292,7 @@ let schedule_proof_attempt ~timelimit ~memlimit ?old ~inplace
   dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@."
     (fun fmt g -> Format.pp_print_string fmt
       (Task.task_goal g).Decl.pr_name.Ident.id_string) goal;
-  callback (Undone Scheduled);
+  callback Scheduled;
   Queue.push
     (Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
                         callback,goal))
@@ -305,7 +305,7 @@ let schedule_edition t command filename callback =
     Call_provers.call_on_file ~command ~regexps:[] ~timeregexps:[]
       ~exitcodes:[(0,Call_provers.Unknown "")] filename
   in
-  callback (Undone Running);
+  callback Running;
   t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
   run_timeout_handler t
 
@@ -413,7 +413,7 @@ let adapt_timelimit a =
 let run_external_proof eS eT ?callback a =
   (* check that the state is not Scheduled or Running *)
   (* Perhaps this test, a.proof_archived, should be done somewhere else *)
-  if a.proof_archived || running a then ()
+  if a.proof_archived || running a.proof_state then ()
   else
     match find_prover eS a with
       | None ->
@@ -457,7 +457,7 @@ let run_external_proof eS eT ?callback a =
           npc.prover_config.Whyconf.interactive then
           begin
             set_proof_state ~notify ~obsolete:false ~archived:false
-              (Undone Unedited) a;
+              Unedited a;
             Util.apply_option2 () callback a a.proof_state
           end
         else
@@ -467,7 +467,7 @@ let run_external_proof eS eT ?callback a =
           let memlimit = a.proof_memlimit in
           let callback result =
             begin match result with
-              | Undone Interrupted ->
+              | Interrupted ->
                   set_proof_state ~notify
                     ~obsolete:previous_obs ~archived:false previous_result a
               | _ ->
@@ -510,7 +510,7 @@ let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
     with Not_found ->
       let ep = add_external_proof ~keygen:O.create ~obsolete:false
         ~archived:false ~timelimit ~memlimit 
-        ~edit:None g p (Undone Interrupted) in
+        ~edit:None g p Interrupted in
       O.init ep.proof_key (Proof_attempt ep);
       ep
   in
@@ -558,7 +558,7 @@ let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
 let proof_successful_or_just_edited a =
   match a.proof_state with
     | Done { Call_provers.pr_answer = Call_provers.Valid }
-    | Undone JustEdited -> true
+    | JustEdited -> true
     | _ -> false
 
 let rec replay_on_goal_or_children eS eT
@@ -674,7 +674,7 @@ let check_external_proof eS eT todo a =
   dprintf debug "[Sched] Check external proof : %a@."
     (fun fmt g -> pp_print_string fmt g.goal_name.Ident.id_string) g;
   (* check that the state is not Scheduled or Running *)
-  if a.proof_archived || running a then ()
+  if a.proof_archived || running a.proof_state then ()
   else
     begin
       Todo.todo todo;
@@ -704,8 +704,8 @@ let check_external_proof eS eT todo a =
             let memlimit = a.proof_memlimit in
             let callback result =
               match result with
-                | Undone Scheduled | Undone Running | Undone Interrupted -> ()
-                | Undone (Unedited | JustEdited) -> assert false
+                | Scheduled | Running -> ()
+                | Unedited | Interrupted | JustEdited -> assert false
                 | InternalFailure msg ->
                   Todo._done todo (g,ap,timelimit,(CallFailed msg));
                   set_proof_state ~notify ~obsolete:false ~archived:false
@@ -758,12 +758,7 @@ let check_all eS eT ~callback =
 
 let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
   let callback _key status =
-    match status with
-      | Undone Running | Undone Scheduled -> ()
-      |  _ ->
-        Todo._done todo ();
-        (* eprintf "todo decreased to %d@." todo.Todo.todo *)
-  in
+    if not (running status) then Todo._done todo () in
   List.iter
     (fun p ->
       Todo.todo todo;
@@ -868,7 +863,7 @@ let rec transform eS sched ~context_unproved_goals_only ?callback tr a =
 
 let edit_proof eS sched ~default_editor a =
   (* check that the state is not Scheduled or Running *)
-  if a.proof_archived || running a then ()
+  if a.proof_archived || running a.proof_state then ()
 (*
     info_window `ERROR "Edition already in progress"
 *)
@@ -910,7 +905,7 @@ let edit_proof eS sched ~default_editor a =
             match res with
               | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
                 set_proof_state ~notify ~obsolete:true ~archived:false
-                  (Undone JustEdited) a
+                  JustEdited a
               | _ ->
                   set_proof_state ~notify ~obsolete:false ~archived:false
                     res a

src/session/session_tools.ml

@@ -80,7 +80,7 @@ let transform_proof_attempt ?notify ~keygen env_session tr_name =
     let add_pa sg =
       if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
         ignore (copy_external_proof ~keygen ~goal:sg
-                  ~attempt_status:(Undone Interrupted) pr) 
+                  ~attempt_status:Interrupted pr)
     in
     List.iter add_pa tr.transf_goals in
   let proofs = all_proof_attempts env_session.session in

src/why3session/why3session_html.ml

@@ -154,10 +154,13 @@ let print_results fmt provers proofs =
 		| Call_provers.HighFailure ->
                   fprintf fmt "FF8000\">High Failure"
 	    end
-	  | S.Undone _ -> fprintf fmt "E0E0E0\">Undone"
 	  | S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
+          | S.Interrupted -> fprintf fmt "E0E0E0\">Not yet run"
+          | S.Unedited -> fprintf fmt "E0E0E0\">Not yet edited"
+          | S.Scheduled | S.Running
+          | S.JustEdited -> assert false
         end;
-        if pr.S.proof_obsolete then fprintf fmt "(obsolete)"
+        if pr.S.proof_obsolete then fprintf fmt " (obsolete)"
       with Not_found -> fprintf fmt "E0E0E0\">---"
     end;
     fprintf fmt "</td>") provers
@@ -264,10 +267,12 @@ struct
   let print_prover = Whyconf.print_prover
 
   let print_proof_status fmt = function
-    | Undone _ -> fprintf fmt "Undone"
-    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
+    | Interrupted -> fprintf fmt "Not yet run"
+    | Unedited -> fprintf fmt "Not yet edited"
+    | JustEdited | Scheduled | Running -> assert false
+    | Done pr -> fprintf fmt "Done: %a" Call_provers.print_prover_result pr
     | InternalFailure exn ->
-      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
+      fprintf fmt "Failure: %a"Exn_printer.exn_printer exn
 
   let print_proof_attempt fmt pa =
     fprintf fmt "<li>%a : %a</li>"
@@ -334,11 +339,13 @@ struct
   let print_prover = Whyconf.print_prover
 
   let print_proof_status fmt = function
-    | Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
-    | Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
+    | Interrupted -> fprintf fmt "<span class='notverified'>Not yet run</span>"
+    | Unedited -> fprintf fmt "<span class='notverified'>Not yet edited</span>"
+    | JustEdited | Scheduled | Running -> assert false
+    | Done pr -> fprintf fmt "<span class='verified'>Done: %a</span>"
       Call_provers.print_prover_result pr
     | InternalFailure exn ->
-      fprintf fmt "<span class='notverified'>Failure : %a</span>"
+      fprintf fmt "<span class='notverified'>Failure: %a</span>"
         Exn_printer.exn_printer exn
 
   let cmd_regexp = Str.regexp "%\\(.\\)"

src/why3session/why3session_latex.ml

@@ -145,7 +145,10 @@ let print_result_prov proofs prov fmt=
 
 	    end
 	| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
-	| Session.Undone _ -> fprintf fmt "& Undone"
+	| Session.Interrupted -> fprintf fmt "& Not yet run"
+	| Session.Unedited -> fprintf fmt "& Not yet edited"
+	| Session.Scheduled | Session.Running
+	| Session.JustEdited -> assert false
   with Not_found -> fprintf fmt "& \\noresult") prov;
   fprintf fmt "\\\\ @."