db : add invalid and highfailure to the database

src/bench/bench.ml

@@ -91,11 +91,12 @@ module BenchUtil =
 struct
 
   let print_proof_status fmt = function
-    | Db.Success -> fprintf fmt "Valid"
-  (* | Invalid -> fprintf fmt "Invalid" *)
+    | Db.Valid -> fprintf fmt "Valid"
+    | Db.Invalid -> fprintf fmt "Invalid"
     | Db.Timeout -> fprintf fmt "Timeout"
     | Db.Unknown -> fprintf fmt "Unknown"
     | Db.Failure -> fprintf fmt "Failure"
+    | Db.HighFailure -> fprintf fmt "HighFailure"
     | Db.Undone  -> fprintf fmt "Undone"
 
   open Worker
@@ -221,11 +222,11 @@ struct
 
   let proof_status_to_db_result pr =
     match pr with
-      | {pr_answer = Valid} -> (Db.Success,pr.pr_time)
-      | {pr_answer = Invalid} -> (Db.Unknown,pr.pr_time)
-      (* TODO add invalid in Db *)
+      | {pr_answer = Valid} -> (Db.Valid,pr.pr_time)
+      | {pr_answer = Invalid} -> (Db.Invalid,pr.pr_time)
       | {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
-      | {pr_answer = Failure _ | HighFailure} -> (Db.Failure,pr.pr_time)
+      | {pr_answer = Failure _} -> (Db.Failure,pr.pr_time)
+      | {pr_answer = HighFailure} -> (Db.HighFailure,pr.pr_time)
       | {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
 
 
@@ -267,7 +268,7 @@ let call callback tool prob =
         Debug.dprintf debug "Database has (%a,%f) for the goal@."
           BenchUtil.print_proof_status proof_status time;
         begin
-          if proof_status = Db.Success ||
+          if proof_status = Db.Valid ||
             (proof_status = Db.Timeout && time > (float tool.ttime -. 0.1))
           then
             callback pval i task (Cached (proof_status,time))
@@ -437,12 +438,12 @@ let empty_tool_res =
     match r with
       | Done (answer,time) ->
         begin match answer with
-          | Db.Success -> {tr with valid = add_nb_avg tr.valid time}
+          | Db.Valid -> {tr with valid = add_nb_avg tr.valid time}
           | Db.Timeout -> {tr with timeout = add_nb_avg tr.timeout time}
-      (* | Db.Invalid -> {tr with invalid = add_nb_avg tr.invalid time} *)
+          | Db.Invalid -> {tr with invalid = add_nb_avg tr.invalid time}
           | Db.Undone | Db.Unknown _ ->
             {tr with unknown = add_nb_avg tr.unknown time}
-          | Db.Failure _ ->
+          | Db.Failure _ |Db.HighFailure ->
             {tr with failure = add_nb_avg tr.failure time}
         end
       | InternalFailure _ ->
@@ -453,7 +454,7 @@ let empty_tool_res =
     | InternalFailure _ -> assert false
 
   let filter_timeline l =
-    let l = List.filter (function {result = Done (Db.Success,_)} -> true
+    let l = List.filter (function {result = Done (Db.Valid,_)} -> true
       | _ -> false) l in
     let compare_valid x y =
       let c = compare (extract_time x.result)

src/bench/whybench.ml

@@ -416,7 +416,7 @@ let () =
       begin begin match res with
         | B.Runned B.Done (ans,_) -> incr nb_done;
           begin match ans with
-            | Db.Success -> incr nb_valid
+            | Db.Valid -> incr nb_valid
             | _     -> () end
         | B.Runned B.InternalFailure _ -> incr nb_done; incr nb_failure
         | B.Cached (_,_) -> incr nb_cached

src/ide/db.ml

@@ -217,10 +217,12 @@ module Htransf = Hashtbl.Make
 
 type proof_status =
   | Undone (** external proof attempt no done yet *)
-  | Success (** external proof attempt succeeded *)
+  | Valid   (** external proof attempt succeeded *)
+  | Invalid   (** external proof attempt found a counter-example *)
   | Timeout (** external proof attempt was interrupted *)
   | Unknown (** external prover answered ``don't know'' or equivalent *)
   | Failure (** external prover call failed *)
+  | HighFailure (** external prover call failed *)
 
 type proof_attempt = int64
 (*
@@ -471,14 +473,18 @@ let transf_from_name n =
   with Not_found -> TransfId.add db n
 
 
-let status_array = [| Undone; Success; Timeout; Unknown; Failure |]
+let status_array = [| Undone; Valid; Timeout; Unknown; Failure;
+                      Invalid; HighFailure |]
 
 let int64_from_status = function
   | Undone -> 0L
-  | Success -> 1L
+  | Valid -> 1L
+  | Invalid -> 5L
   | Timeout -> 2L
   | Unknown -> 3L
   | Failure -> 4L
+  | HighFailure -> 6L
+
 
 let status_from_int64 i =
   try

src/ide/db.mli

@@ -52,13 +52,16 @@ type transf
 
 
 (** status of an external proof attempt *)
+
 type proof_status =
-  | Undone
-  | Success (** external proof attempt succeeded *)
+  | Undone (** external proof attempt no done yet *)
+  | Valid   (** external proof attempt succeeded *)
+  | Invalid (** external proof attempt found a counter-example *)
   | Timeout (** external proof attempt was interrupted *)
   | Unknown (** external prover answered ``don't know'' or equivalent *)
   | Failure (** external prover call failed *)
-  
+  | HighFailure (** external prover call failed *)
+
 (** parent of a goal: either a theory (for "toplevel" goals)
     or a transformation (for "subgoals") *)
 (* useful ?

src/ide/gmain.ml

@@ -231,9 +231,11 @@ module Model = struct
   type proof_attempt_status =
     | Scheduled (** external proof attempt is scheduled *)
     | Running (** external proof attempt is in progress *)
-    | Success (** external proof attempt succeeded *)
+    | Valid (** external proof attempt succeeded *)
+    | Invalid (** external proof attempt found a counter-example *)
     | Timeout (** external proof attempt was interrupted *)
     | Unknown (** external prover answered ``don't know'' or equivalent *)
+    | Failure (** external prover call failed *)
     | HighFailure (** external prover call failed *)
 
 
@@ -538,13 +540,17 @@ module Helpers = struct
     match obsolete,result with
     | _, Scheduled -> !image_scheduled
     | _, Running -> !image_running
-    | false, Success -> !image_valid
+    | false, Valid  -> !image_valid
+    | false, Invalid  -> !image_unknown (** TODO change *)
     | false, Timeout -> !image_timeout
     | false, Unknown -> !image_unknown
+    | false, Failure -> !image_failure
     | false, HighFailure -> !image_failure
-    | true, Success -> !image_valid_obs
+    | true, Valid -> !image_valid_obs
+    | true, Invalid  -> !image_unknown (** TODO change *)
     | true, Timeout -> !image_timeout_obs
     | true, Unknown -> !image_unknown_obs
+    | true, Failure -> !image_failure_obs
     | true, HighFailure -> !image_failure_obs
 
   let set_row_status b row =
@@ -581,7 +587,7 @@ module Helpers = struct
 
   let rec check_goal_proved g =
     let b1 = Hashtbl.fold 
-      (fun _ a acc -> acc || a.status = Success) g.external_proofs false
+      (fun _ a acc -> acc || a.status = Valid) g.external_proofs false
     in
     let b = Hashtbl.fold 
       (fun _ t acc -> acc || t.transf_proved) g.transformations b1
@@ -836,7 +842,8 @@ let apply_trans t task =
 
 let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
 let inline_transformation = Trans.lookup_transform "inline_goal" gconfig.env
-let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env
+let intro_transformation = Trans.lookup_transform "introduce_premises"
+  gconfig.env
 
 let rec reimport_any_goal parent gname t db_goal goal_obsolete =
   let goal = Helpers.add_goal_row parent gname t db_goal in
@@ -852,12 +859,14 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
          let obsolete = goal_obsolete or o in
          let s = match s with
            | Db.Undone -> Model.HighFailure
-           | Db.Success ->
+           | Db.Valid ->
                if not obsolete then proved := true;
-               Model.Success
+               Model.Valid
+           | Db.Invalid -> Model.Invalid
            | Db.Unknown -> Model.Unknown
            | Db.Timeout -> Model.Timeout
-           | Db.Failure -> Model.HighFailure
+           | Db.Failure -> Model.Failure
+           | Db.HighFailure -> Model.HighFailure
          in
          let (_pa : Model.proof_attempt) =
            Helpers.add_external_proof_row ~obsolete ~edit goal p a s t
@@ -1078,11 +1087,12 @@ let callback_of_callback callback = function
     callback Model.HighFailure 0. "Prover call failed"
   | Scheduler.Done r ->
     let res = match r.Call_provers.pr_answer with
-      | Call_provers.Valid -> Model.Success
+      | Call_provers.Valid -> Model.Valid
       | Call_provers.Timeout -> Model.Timeout
-      | Call_provers.Unknown _ | Call_provers.Invalid -> Model.Unknown
-      | Call_provers.Failure _ | Call_provers.HighFailure ->
-        Model.HighFailure in
+      | Call_provers.Unknown _ -> Model.Unknown
+      | Call_provers.Invalid ->  Model.Invalid
+      | Call_provers.Failure _ -> Model.Failure
+      | Call_provers.HighFailure -> Model.HighFailure in
     callback res r.Call_provers.pr_time r.Call_provers.pr_output
 
 (* q is a queue of proof attempt where to put the new one *)
@@ -1091,14 +1101,16 @@ let redo_external_proof q g a =
   let callback result time output =
     a.Model.output <- output;
     Helpers.set_proof_status ~obsolete:false a result time ;
-    if result = Model.Success
+    if result = Model.Valid
     then Helpers.set_proved ~propagate:true a.Model.proof_goal;
     let db_res = match result with
       | Model.Scheduled | Model.Running -> Db.Undone
-      | Model.Success -> Db.Success
+      | Model.Valid -> Db.Valid
+      | Model.Invalid -> Db.Invalid
       | Model.Unknown -> Db.Unknown
       | Model.Timeout -> Db.Timeout
-      | Model.HighFailure -> Db.Failure
+      | Model.HighFailure -> Db.HighFailure
+      | Model.Failure -> Db.Failure
     in
     Db.set_status a.Model.proof_db db_res time
   in
@@ -1937,7 +1949,8 @@ let confirm_remove_row r =
 	info_window
 	  ~callback:(fun () -> remove_transf tr)
 	  `QUESTION
-	  "Do you really want to remove the selected transformation and all its subgoals?"
+	  "Do you really want to remove the selected transformation
+and all its subgoals?"
 
 let confirm_remove_selection () =
   match goals_view#selection#get_selected_rows with