Commit 9fcc1a85 authored by MARCHE Claude's avatar MARCHE Claude

reload_files now returns a pair of booleans giving info

it returns (o,d), o true means there are obsolete goals, d means there
are missed objects (goals, transformations, theories or files)
that are now detached in the session

Note: there are several bugs remaining to solve, such that the fact that
missed transformations or lost instead of detached.
parent 7f2a8aab
......@@ -217,60 +217,26 @@ let print_session fmt c =
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
in
List.map (fun (_,_,a) -> a) th
(** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
let format = file_format file in
let old_theories = file_theories file in
let file_name = Filename.concat (get_dir old_ses) (file_name file) in
let new_theories =
try
read_file c.controller_env file_name ?format
with e -> (* TODO: filter only syntax error and typing errors *)
raise e
in
merge_file_section
c.controller_session ~use_shapes ~old_ses ~old_theories
~env:c.controller_env file_name new_theories format
let reload_files (c : controller) ~use_shapes =
let old_ses = c.controller_session in
c.controller_session <-
empty_session ~shape_version:(get_shape_version old_ses) (get_dir old_ses);
try
Stdlib.Hstr.iter
(fun f -> merge_file old_ses c ~use_shapes f)
(get_files old_ses);
merge_files ~use_shapes c.controller_env c.controller_session old_ses
with e ->
c.controller_session <- old_ses;
raise e
let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section c.controller_session fname theories format
let theories = Session_itp.read_file c.controller_env ?format fname in
let (_ : file) = add_file_section c.controller_session fname theories format in
()
module type Scheduler = sig
......
......@@ -93,13 +93,7 @@ val print_session : Format.formatter -> controller -> unit
val goal_task_to_print :
?do_intros:bool -> controller -> proofNodeID -> Task.task * Trans.naming_table
(*
- TODO: the presence of obsolete goals should be returned somehow by
that function, as the presence of unmatch old theories or goals
*)
val reload_files : controller -> use_shapes:bool -> unit (* (bool * bool) see above *)
val reload_files : controller -> use_shapes:bool -> bool * bool
(** reload the files of the given session:
- each file is parsed again and theories/goals extracted from it. If
......
......@@ -654,7 +654,7 @@ end
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
try reload_files cont ~use_shapes; true with
try let _ = reload_files cont ~use_shapes in true with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
......
......@@ -262,9 +262,12 @@ let is_detached (s: session) (a: any) =
match a with
| AFile _file -> false
| ATh th ->
let parent_name = th.theory_parent_name in
let parent = Hstr.find s.session_files parent_name in
List.exists (fun x -> x = th) parent.file_detached_theories
let parent_name = th.theory_parent_name in
begin
try let parent = Hstr.find s.session_files parent_name in
List.exists (fun x -> x = th) parent.file_detached_theories
with Not_found -> true
end
| ATn tn ->
let pn_id = get_trans_parent s tn in
let pn = get_proofNode s pn_id in
......@@ -1309,7 +1312,7 @@ end
module AssoGoals = Termcode.Pairing(Goal)(Goal)
let found_obsolete = ref false
let found_missed_goals_in_theory = ref false
let found_detached = ref false
let save_detached_goals old_s detached_goals_id s parent =
let save_proof parent old_pa_n =
......@@ -1423,18 +1426,19 @@ and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
| ((id,s), None) ->
Debug.dprintf debug "[merge_theory] pairing found missed sub goal :( : %s @."
(get_proofNode s id).proofn_name.Ident.id_string;
found_missed_goals_in_theory := true)
found_detached := true)
associated;
(* save the detached goals *)
let detached = List.map (fun (a,_) -> a) detached in
new_tr.transf_detached_subtasks <- save_detached_goals old_s detached new_s (Trans new_tr_id))
with | _ ->
(* TODO should create a detached transformation instead *)
()
with _ ->
Debug.dprintf debug
"[Session_itp.merge_trans] transformation failed: %s@." old_tr.transf_name;
(* TODO should create a detached transformation *)
found_detached := true
let merge_theory ~use_shapes env old_s old_th s th : unit =
let found_missed_goals_in_theory = ref false in
let old_goals_table = Hstr.create 7 in
(* populate old_goals_table *)
List.iter
......@@ -1489,7 +1493,7 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
merge_goal ~use_shapes env s old_s ~goal_obsolete (get_proofNode old_s old_goal_id) new_goal_id
| (_, None) ->
Debug.dprintf debug "[merge_theory] pairing found missed sub goal :( @.";
found_missed_goals_in_theory := true)
found_detached := true)
associated;
(* store the detached goals *)
let detached = List.map (fun (a,_) -> a) detached in
......@@ -1523,30 +1527,13 @@ let make_theory_section ?merge (s:session) parent_name (th:Theory.theory)
(* add a why file to a session *)
let add_file_section (s:session) (fn:string)
(theories:Theory.theory list) format : unit =
(theories:Theory.theory list) format : file =
let fn = Sysutil.relativize_filename s.session_dir fn in
if Hstr.mem s.session_files fn then
Debug.dprintf debug "[session] file %s already in database@." fn
else
begin
let f = { file_name = fn;
file_format = format;
file_theories = [];
file_detached_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section s fn) theories in
f.file_theories <- theories
Debug.dprintf debug "[session] file %s already in database@." fn;
assert false
end
(* add a why file to a session and try to merge its theories with the
provided ones with matching names *)
let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
(s:session) (fn:string) (theories:Theory.theory list) format
: unit =
let fn = Sysutil.relativize_filename s.session_dir fn in
if Hstr.mem s.session_files fn then
Debug.dprintf debug "[session] file %s already in database@." fn
else
let f = { file_name = fn;
file_format = format;
......@@ -1554,34 +1541,87 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
file_detached_theories = [] }
in
Hstr.add s.session_files fn f;
let theories,detached =
let old_th_table = Hstr.create 7 in
List.iter
(fun th -> Hstr.add old_th_table th.theory_name.Ident.id_string th)
old_theories;
let add_theory (th: Theory.theory) =
try
(* look for a theory with same name *)
let theory_name = th.Theory.th_name.Ident.id_string in
(* if we found one, we remove it from the table and merge it *)
let old_th = Hstr.find old_th_table theory_name in
Hstr.remove old_th_table theory_name;
make_theory_section ~merge:(old_ses,old_th,env,use_shapes) s fn th
with Not_found ->
(* if no theory was found we make a new theory section *)
make_theory_section s fn th
in
let theories = List.map add_theory theories in
(* we save the remaining, detached *)
let detached = Hstr.fold
(fun _key th tl ->
(save_detached_theory fn old_ses th s) :: tl)
old_th_table [] in
theories, detached
in
let theories = List.map (make_theory_section s fn) theories in
f.file_theories <- theories;
f.file_detached_theories <- detached;
update_file_node (fun _ -> ()) s f
f
(* add a why file to a session and try to merge its theories with the
provided ones with matching names *)
let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
(s:session) (fn:string) (theories:Theory.theory list) format
: unit =
let f = add_file_section s fn [] format in
let theories,detached =
let old_th_table = Hstr.create 7 in
List.iter
(fun th -> Hstr.add old_th_table th.theory_name.Ident.id_string th)
old_theories;
let add_theory (th: Theory.theory) =
try
(* look for a theory with same name *)
let theory_name = th.Theory.th_name.Ident.id_string in
(* if we found one, we remove it from the table and merge it *)
let old_th = Hstr.find old_th_table theory_name in
Hstr.remove old_th_table theory_name;
make_theory_section ~merge:(old_ses,old_th,env,use_shapes) s fn th
with Not_found ->
(* if no theory was found we make a new theory section *)
make_theory_section s fn th
in
let theories = List.map add_theory theories in
(* we save the remaining, detached *)
let detached = Hstr.fold
(fun _key th tl ->
(save_detached_theory fn old_ses th s) :: tl)
old_th_table [] in
theories, detached
in
f.file_theories <- theories;
f.file_detached_theories <- detached;
update_file_node (fun _ -> ()) s f
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
in
List.map (fun (_,_,a) -> a) th
let merge_file ~use_shapes env (ses : session) (old_ses : session) file =
let format = file_format file in
let old_theories = file_theories file in
let file_name = Filename.concat (get_dir old_ses) (file_name file) in
let new_theories =
try
read_file env file_name ?format
with e -> (* TODO: filter only syntax error and typing errors *)
raise e
in
merge_file_section
ses ~use_shapes ~old_ses ~old_theories
~env file_name new_theories format
let merge_files ~use_shapes env (ses:session) (old_ses : session) =
Stdlib.Hstr.iter
(fun _ f -> merge_file ~use_shapes env ses old_ses f)
(get_files old_ses);
!found_obsolete,!found_detached
(************************)
(* saving state on disk *)
......@@ -1784,7 +1824,7 @@ and save_trans s ctxt fmt (tid,t) =
arg_id := !arg_id + 1;
fprintf fmt "arg%i=\"%a\"" !arg_id save_string s
in
fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\" %a%a>@]"
fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a %a>@]"
save_string t.transf_name
(save_bool_def "proved" false) (tn_proved s tid)
(Pp.print_list Pp.space save_arg) t.transf_args;
......
......@@ -146,12 +146,19 @@ val empty_session : ?shape_version:int -> string -> session
val add_file_section :
session -> string -> (Theory.theory list) ->
Env.fformat option -> unit
Env.fformat option -> file
(** [add_file_section s fn ths] adds a new
'file' section in session [s], named [fn], containing fresh theory
subsections corresponding to theories [ths]. The tasks of each
theory nodes generated are computed using [Task.split_theory]. *)
val read_file :
Env.env -> ?format:Env.fformat -> string -> Theory.theory list
(* [read_file env ~format fn] parses the source file [fn], types it
and extract its theories. Parse errors and typing errors are
signaled with exceptions. *)
(*
val merge_file_section :
use_shapes:bool -> old_ses:session -> old_theories:theory list ->
env:Env.env -> session -> string -> Theory.theory list ->
......@@ -163,6 +170,18 @@ val merge_file_section :
old_ths, it is attempted to associate the old goals,
proof_attempts and transformations to the goals of the new
theory *)
*)
val merge_files :
use_shapes:bool -> Env.env -> session -> session -> bool * bool
(** [merge_files ~use_shapes env ses old_ses] merges the file sections
of session [s] with file sections of the same name in old session
[old_ses]. Recursively, for each theory whose name is identical to
old theories, it is attempted to associate the old goals,
proof_attempts and transformations to the goals of the new theory.
Returns a pair [(o,d)] such that [o] is true when obsolete proof
attempts where found and [d] is true id detached theories, goals
or transformations were found. *)
val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
Whyconf.prover -> limit:Call_provers.resource_limit -> proofAttemptID
......
......@@ -235,8 +235,12 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
exit 1
end
in
let callback _paid _pastatus = () in
let notification _any = () in
let callback _paid _pastatus =
Debug.dprintf debug "[Replay] callback on node paid pastatus@."
in
let notification _any =
Debug.dprintf debug "[Replay] notified on node any@."
in
if !opt_provers = [] then
let () =
C.replay ~obsolete_only:false ~use_steps:!opt_use_steps ~callback ~notification ~final_callback cont
......@@ -346,17 +350,16 @@ let () =
let ses,use_shapes = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in
(* update the session *)
let found_obs, some_merge_miss =
let found_obs, found_detached =
try
Controller_itp.reload_files cont ~use_shapes;
true, false (* TODO *)
with
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
exit 1
in
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not found_obs
if !opt_obsolete_only && not found_detached
then
begin
eprintf "Session is not obsolete, hence not replayed@.";
......@@ -371,9 +374,10 @@ let () =
in
*)
if found_obs then eprintf "[Warning] session is obsolete@.";
if some_merge_miss then eprintf "[Warning] some goals were missed during merge@.";
add_to_check_no_smoke some_merge_miss found_obs cont;
Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());
if found_detached then eprintf "[Warning] found detached goals ot theories or transformations@.";
add_to_check_no_smoke found_detached found_obs cont;
Debug.dprintf debug "[Replay] starting scheduler@.";
Unix_scheduler.Unix_scheduler.main_loop ~prompt:"scheduler> " (fun _ -> ());
eprintf "main replayer loop exited unexpectedly@.";
exit 1
with
......@@ -387,6 +391,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3newreplay.byte"
compile-command: "unset LANG; make -C ../.. bin/why3replay.opt"
End:
*)
......@@ -90,8 +90,7 @@ let read_update_session ~allow_obsolete env config fname =
let cont = Controller_itp.create_controller config env session in
let found_obs, some_merge_miss =
try
Controller_itp.reload_files cont ~use_shapes;
true, false (* TODO: take allow_obsolete, return values *)
Controller_itp.reload_files cont ~use_shapes
with
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
......
......@@ -42,7 +42,8 @@
</goal>
</theory>
<theory name="Power" sum="4cc6d21f246903f98feda68da4e48c65">
<goal name="power_1">
<goal name="power_1" proved="true">
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="sqrt4_256">
</goal>
......@@ -53,6 +54,7 @@
</goal>
<goal name="power_sum.1" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="11"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......
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