Commit 5517c9ed authored by MARCHE Claude's avatar MARCHE Claude

session: refined the "verified" boolean status into a float option

parent 90bf8fb3
......@@ -404,10 +404,14 @@ module S = Session
let session_needs_saving = ref false
let set_row_status row b =
if b then
goals_model#set ~row:row#iter ~column:status_column !image_yes
else
goals_model#set ~row:row#iter ~column:status_column !image_unknown
match b with
| Some t ->
goals_model#set ~row:row#iter ~column:status_column !image_yes;
let t = Format.sprintf "%.2f" t in
goals_model#set ~row:row#iter ~column:time_column t
| None ->
goals_model#set ~row:row#iter ~column:status_column !image_unknown;
goals_model#set ~row:row#iter ~column:time_column ""
let set_proof_state a =
let obsolete = a.S.proof_obsolete in
......@@ -1257,13 +1261,13 @@ let (_ : GMenu.image_menu_item) =
~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
let rec collapse_verified = function
| S.Goal g when g.S.goal_verified ->
| S.Goal g when Opt.inhabited g.S.goal_verified ->
let row = g.S.goal_key in
goals_view#collapse_row row#path
| S.Theory th when th.S.theory_verified ->
| S.Theory th when Opt.inhabited th.S.theory_verified ->
let row = th.S.theory_key in
goals_view#collapse_row row#path
| S.File f when f.S.file_verified ->
| S.File f when Opt.inhabited f.S.file_verified ->
let row = f.S.file_key in
goals_view#collapse_row row#path
| any -> S.iter collapse_verified any
......
......@@ -144,7 +144,7 @@ type 'a goal =
goal_parent : 'a goal_parent;
mutable goal_checksum : Tc.checksum option;
mutable goal_shape : Tc.shape;
mutable goal_verified : bool;
mutable goal_verified : float option;
mutable goal_task: task_option;
mutable goal_expanded : bool;
goal_external_proofs : 'a proof_attempt PHprover.t;
......@@ -174,7 +174,7 @@ and 'a metas =
metas_added : metas_args;
metas_idpos : idpos;
metas_parent : 'a goal;
mutable metas_verified : bool;
mutable metas_verified : float option;
mutable metas_goal : 'a goal;
(** Not mutated after the creation *)
mutable metas_expanded : bool;
......@@ -185,7 +185,7 @@ and 'a transf =
transf_name : string;
(** Why3 tranformation name *)
transf_parent : 'a goal;
mutable transf_verified : bool;
mutable transf_verified : float option;
mutable transf_goals : 'a goal list;
(** Not mutated after the creation of the session *)
mutable transf_expanded : bool;
......@@ -197,7 +197,7 @@ and 'a theory =
theory_parent : 'a file;
mutable theory_checksum : Termcode.checksum option;
mutable theory_goals : 'a goal list;
mutable theory_verified : bool;
mutable theory_verified : float option;
mutable theory_expanded : bool;
mutable theory_task : Theory.theory hide;
}
......@@ -209,7 +209,7 @@ and 'a file =
file_parent : 'a session;
mutable file_theories: 'a theory list;
(** Not mutated after the creation *)
mutable file_verified : bool;
mutable file_verified : float option;
mutable file_expanded : bool;
mutable file_for_recovery : Theory.theory Mstr.t hide;
}
......@@ -279,7 +279,7 @@ let iter_proof_attempt f = function
| Metas m -> metas_iter_proof_attempt f m
let rec goal_iter_leaf_goal ~unproved_only f g =
if not (g.goal_verified && unproved_only) then
if not (Opt.inhabited g.goal_verified && unproved_only) then
let r = ref true in
PHstr.iter
(fun _ t -> r := false;
......@@ -344,15 +344,15 @@ module PTreeT = struct
| Any t ->
let s = match t with
| File f ->
if f.file_verified
if Opt.inhabited f.file_verified
then f.file_name
else f.file_name^"?"
| Theory th ->
if th.theory_verified
if Opt.inhabited th.theory_verified
then th.theory_name.Ident.id_string
else th.theory_name.Ident.id_string^"?"
| Goal g ->
if g.goal_verified
if Opt.inhabited g.goal_verified
then g.goal_name.Ident.id_string
else g.goal_name.Ident.id_string^"?"
| Proof_attempt pr ->
......@@ -366,11 +366,11 @@ module PTreeT = struct
(if pr.proof_obsolete then "O" else "")
(if pr.proof_archived then "A" else "")
| Transf tr ->
if tr.transf_verified
if Opt.inhabited tr.transf_verified
then tr.transf_name
else tr.transf_name^"?"
| Metas metas ->
if metas.metas_verified
if Opt.inhabited metas.metas_verified
then "metas..."
else "metas..."^"?"
in
......@@ -803,38 +803,50 @@ let save_session config session =
type 'a notify = 'a any -> unit
let notify : 'a notify = fun _ -> ()
let compute_verified get l =
List.fold_left (fun acc t ->
match acc,get t with
| Some x, Some y -> Some (x +. y)
| _ -> None) (Some 0.0) l
let file_verified f =
List.for_all (fun t -> t.theory_verified) f.file_theories
compute_verified (fun t -> t.theory_verified) f.file_theories
let theory_verified t =
List.for_all (fun g -> g.goal_verified) t.theory_goals
compute_verified (fun g -> g.goal_verified) t.theory_goals
let transf_verified t =
List.for_all (fun g -> g.goal_verified) t.transf_goals
compute_verified (fun g -> g.goal_verified) t.transf_goals
let metas_verified m = m.metas_goal.goal_verified
let proof_verified a =
(not a.proof_obsolete) &&
if a.proof_obsolete then None else
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid} -> true
| _ -> false
| Done { Call_provers.pr_answer = Call_provers.Valid;
Call_provers.pr_time = t } -> Some t
| _ -> None
let goal_verified g =
try
PHprover.iter
(fun _ a ->
if proof_verified a
then raise Exit)
g.goal_external_proofs;
PHstr.iter
(fun _ t -> if t.transf_verified then raise Exit)
g.goal_transformations;
Mmetas_args.iter
(fun _ t -> if t.metas_verified then raise Exit)
g.goal_metas;
false
with Exit -> true
let acc = ref None in
let accumulate v =
match v with
| None -> ()
| Some t ->
match !acc with
| Some x -> acc := Some (x +. t)
| None -> acc := v
in
PHprover.iter
(fun _ a -> accumulate (proof_verified a))
g.goal_external_proofs;
PHstr.iter
(fun _ t -> accumulate t.transf_verified)
g.goal_transformations;
Mmetas_args.iter
(fun _ t -> accumulate t.metas_verified)
g.goal_metas;
!acc
let check_file_verified notify f =
let b = file_verified f in
......@@ -960,7 +972,7 @@ let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum sh
goal_external_proofs = PHprover.create 7;
goal_transformations = PHstr.create 3;
goal_metas = Mmetas_args.empty;
goal_verified = false;
goal_verified = None;
goal_expanded = expanded;
}
in
......@@ -986,7 +998,7 @@ let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl
goal_external_proofs = PHprover.create 7;
goal_transformations = PHstr.create 3;
goal_metas = Mmetas_args.empty;
goal_verified = false;
goal_verified = None;
goal_expanded = expanded;
}
in
......@@ -1001,7 +1013,7 @@ let raw_add_transformation ~(keygen:'a keygen) ~(expanded:bool) g name =
let key = keygen ~parent () in
let tr = { transf_name = name;
transf_parent = g;
transf_verified = false;
transf_verified = None;
transf_key = key;
transf_goals = [];
transf_expanded = expanded;
......@@ -1016,7 +1028,7 @@ let raw_add_metas ~(keygen:'a keygen) ~(expanded:bool) g added idpos =
let ms = { metas_added = added;
metas_idpos = idpos;
metas_parent = g;
metas_verified = false;
metas_verified = None;
metas_key = key;
metas_goal = g;
metas_expanded = expanded;
......@@ -1034,7 +1046,7 @@ let raw_add_theory ~(keygen:'a keygen) ~(expanded:bool)
theory_parent = mfile;
theory_checksum = checksum;
theory_goals = [];
theory_verified = false;
theory_verified = None;
theory_expanded = expanded;
theory_task = None;
}
......@@ -1047,7 +1059,7 @@ let raw_add_file ~(keygen:'a keygen) ~(expanded:bool) session f fmt =
file_key = key;
file_format = fmt;
file_theories = [];
file_verified = false;
file_verified = None;
file_expanded = expanded;
file_parent = session;
file_for_recovery = None;
......
......@@ -82,7 +82,7 @@ type 'a goal = private
goal_parent : 'a goal_parent;
mutable goal_checksum : Termcode.checksum option; (** checksum of the task *)
mutable goal_shape : Termcode.shape; (** shape of the task *)
mutable goal_verified : bool;
mutable goal_verified : float option;
mutable goal_task: task_option;
mutable goal_expanded : bool;
goal_external_proofs : 'a proof_attempt PHprover.t;
......@@ -112,7 +112,7 @@ and 'a metas =
metas_added : metas_args;
metas_idpos : idpos;
metas_parent : 'a goal;
mutable metas_verified : bool;
mutable metas_verified : float option;
mutable metas_goal : 'a goal;
(** Not mutated after the creation *)
mutable metas_expanded : bool;
......@@ -123,7 +123,7 @@ and 'a transf = private
transf_name : string;
(** Why3 transformation name *)
transf_parent : 'a goal;
mutable transf_verified : bool;
mutable transf_verified : float option;
mutable transf_goals : 'a goal list;
(** Not mutated after the creation *)
mutable transf_expanded : bool;
......@@ -136,7 +136,7 @@ and 'a theory = private
mutable theory_checksum : Termcode.checksum option;
mutable theory_goals : 'a goal list;
(** Not mutated after the creation *)
mutable theory_verified : bool;
mutable theory_verified : float option;
mutable theory_expanded : bool;
mutable theory_task : Theory.theory hide;
}
......@@ -148,7 +148,7 @@ and 'a file = private
file_parent : 'a session;
mutable file_theories: 'a theory list;
(** Not mutated after the creation *)
mutable file_verified : bool;
mutable file_verified : float option;
mutable file_expanded : bool;
mutable file_for_recovery : Theory.theory Mstr.t hide;
}
......@@ -300,9 +300,9 @@ val goal_task_option : 'key goal -> Task.task option
val goal_expl : 'key goal -> string
(** Return the explication of a goal *)
val proof_verified : 'key proof_attempt -> bool
(** Return true if the proof is not obsolete and the result is valid *)
val proof_verified : 'key proof_attempt -> float option
(** Return [Some t] if the proof is not obsolete and the result is
valid. [t] is the time needed to solved it *)
val get_used_provers : 'a session -> Whyconf.Sprover.t
(** Get the set of provers which appear in the session *)
......
......@@ -890,16 +890,16 @@ let remove_metas t =
remove_metas ~notify t
let rec clean = function
| Goal g when g.goal_verified ->
| Goal g when Opt.inhabited g.goal_verified ->
iter_goal
(fun a ->
if a.proof_obsolete || not (proof_successful_or_just_edited a) then
remove_proof_attempt a)
(fun t ->
if not t.transf_verified then remove_transformation t
if not (Opt.inhabited t.transf_verified) then remove_transformation t
else transf_iter clean t)
(fun m ->
if not m.metas_verified then remove_metas m
if not (Opt.inhabited m.metas_verified) then remove_metas m
else metas_iter clean m)
g
| Goal g ->
......@@ -913,7 +913,7 @@ let rec clean = function
*)
transf_iter clean t)
(fun m ->
if not m.metas_verified then remove_metas m
if not (Opt.inhabited m.metas_verified) then remove_metas m
else metas_iter clean m)
g
| Proof_attempt a -> clean (Goal a.proof_parent)
......
......@@ -210,7 +210,7 @@ let project_dir =
with Not_found -> failwith "file does not exist"
let goal_statistics (goals,n,m) g =
if g.S.goal_verified then (goals,n+1,m+1) else (g::goals,n,m+1)
if Opt.inhabited g.S.goal_verified then (goals,n+1,m+1) else (g::goals,n,m+1)
let theory_statistics (ths,n,m) th =
let goals,n1,m1 =
......@@ -358,8 +358,10 @@ let add_to_check config some_merge_miss found_obs =
let transform_smoke env_session =
let trans tr_name s =
Session_tools.filter_proof_attempt S.proof_verified s.S.session;
Session_tools.transform_proof_attempt ~keygen:O.create s tr_name in
Session_tools.filter_proof_attempt
(fun p -> Opt.inhabited (S.proof_verified p)) s.S.session;
Session_tools.transform_proof_attempt ~keygen:O.create s tr_name
in
match !opt_smoke with
| SD_None -> ()
| SD_Top -> trans "smoke_detector_top" env_session
......
......@@ -11,6 +11,8 @@
(* useful option combinators *)
let inhabited = function None -> false | Some _ -> true
let get = function None -> invalid_arg "Opt.get" | Some x -> x
let get_exn exn = function None -> raise exn | Some x -> x
......
......@@ -11,6 +11,8 @@
(** Useful option combinators *)
val inhabited : 'a option -> bool
val get : 'a option -> 'a
val get_exn : exn -> 'a option -> 'a
......
......@@ -139,9 +139,11 @@ let run_one ~action env config filters pk fname =
interactive
(PHprover.find pr.proof_parent.goal_external_proofs prover)
| Not_valid ->
let rm =
(PHprover.find pr.proof_parent.goal_external_proofs prover) in
not (proof_verified rm) in
let rm =
PHprover.find pr.proof_parent.goal_external_proofs prover
in
not (Opt.inhabited (proof_verified rm))
in
if not replace then raise Exit;
copy_external_proof ~keygen ~prover ~env_session pr
in
......
......@@ -167,7 +167,7 @@ let rec num_lines acc tr =
fprintf fmt "<tr>";
for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) tr.S.transf_verified
(color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified)
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" tr.transf_name ;
......@@ -187,7 +187,8 @@ let rec num_lines acc tr =
if not is_first then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) g.S.goal_verified (max_depth - depth + 1);
(color_of_status ~dark:false) (Opt.inhabited g.S.goal_verified)
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_expl g);
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
......@@ -208,8 +209,10 @@ let rec num_lines acc tr =
let provers = List.sort Whyconf.Prover.compare provers in
let name = th.S.theory_name.Ident.id_string in
fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
(color_of_status ~dark:true) th.S.theory_verified
name (if th.S.theory_verified then "fully verified" else "not fully verified")
(color_of_status ~dark:true) (Opt.inhabited th.S.theory_verified)
name
(if Opt.inhabited th.S.theory_verified
then "fully verified" else "not fully verified")
;
fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
......@@ -395,7 +398,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
fprintf fmt
"@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified tr.transf_verified
print_verified (Opt.inhabited tr.transf_verified)
tr.transf_name
(Pp.print_list Pp.newline print_goal) tr.transf_goals
......@@ -403,7 +406,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
fprintf fmt
"@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
print_verified g.goal_verified
print_verified (Opt.inhabited g.goal_verified)
g.goal_name.Ident.id_string
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
......@@ -416,7 +419,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
fprintf fmt
"@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified th.theory_verified
print_verified (Opt.inhabited th.theory_verified)
th.theory_name.Ident.id_string
(Pp.print_list Pp.newline print_goal) th.theory_goals in
......@@ -424,7 +427,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
fprintf fmt
"@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified f.file_verified
print_verified (Opt.inhabited f.file_verified)
f.file_name
(Pp.print_list Pp.newline print_theory) f.file_theories in
......
......@@ -164,7 +164,7 @@ let rec stats_of_goal ~root prefix_name stats goal =
in
List.iter (update_perf_stats stats) proof_list;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations;
if not goal.goal_verified then
if not (Opt.inhabited goal.goal_verified) then
let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
stats.no_proof <- Sstr.add goal_name stats.no_proof
else
......@@ -230,7 +230,7 @@ let rec stats2_of_goal ~nb_proofs g : notask goal_stat =
[]
in
if match nb_proofs with
| 0 -> not g.goal_verified
| 0 -> not (Opt.inhabited g.goal_verified)
| 1 -> List.length proof_list = 1
| _ -> assert false
then Yes(proof_list,l) else No(l)
......
......@@ -204,9 +204,9 @@ let iter_proof_attempt_by_filter iter filters f session =
(** three value *)
let three_value f v p =
let iter_obsolete a =
match v with
| FT_No when not (p a) -> f a
| FT_Yes when (p a) -> f a
match v, p a with
| FT_No, false -> f a
| FT_Yes, true -> f a
| _ -> () (** FT_All treated after *) in
if v = FT_All then f else iter_obsolete in
(** obsolete *)
......@@ -215,9 +215,10 @@ let iter_proof_attempt_by_filter iter filters f session =
let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
(** verified_goal *)
let f = three_value f filters.verified_goal
(fun a -> a.S.proof_parent.S.goal_verified) in
(fun a -> Opt.inhabited a.S.proof_parent.S.goal_verified) in
(** verified *)
let f = three_value f filters.verified S.proof_verified in
let f = three_value f filters.verified
(fun p -> Opt.inhabited (S.proof_verified p)) in
(** status *)
let f = if filters.status = [] then f else
(fun a -> match a.S.proof_state with
......
......@@ -65,7 +65,7 @@ let run_one env config filters fname =
let remove = match !opt_remove with
| Always -> true (*| Never -> false*)
| Interactive -> interactive pr
| Not_valid -> not (proof_verified pr) in
| Not_valid -> not (Opt.inhabited (proof_verified pr)) in
if remove then remove_external_proof pr) env_session.session;
save_session config env_session.session
......
......@@ -186,7 +186,7 @@ let is_successful env = (** means all goals proved*)
let rec iter = function
| File f -> file_iter iter f
| Theory th -> theory_iter iter th
| Goal g -> if not (g.goal_verified) then raise Exit
| Goal g -> if not (Opt.inhabited (g.goal_verified)) then raise Exit
| Proof_attempt _ | Transf _ | Metas _ -> assert false in
session_iter iter env.session;
true
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment