Commit 4c744eba authored by Johannes Kanig's avatar Johannes Kanig

Allow to keep unmatched theories

When Why3 is run on a file where some theories have been suppressed, it
will delete the corresponding theories from the session file.  We now
add an option keep_unmatched_theories to Session.update_session, which
keeps all theories. In this commit, this option is always disabled.

This is useful for SPARK, which sometimes only generates part of the
Why3 file for efficiency reasons, but doesn't want the session file to
be damaged because of that.

* session.ml
(import_theory)
(import_goal)
(import_proof_attempt)
(import_transf): new functions to copy a session tree from an old
  session file
(merge_file): keep old theories when keep_unmatched_theories is true
* session_scheduler.ml
(update_session): pass keep_unmatched_theories
* why3session_lib.ml
(read_update_session): pass keep_unmatched_theories
parent 1cfa4147
......@@ -61,6 +61,7 @@ let env_session,_,_ =
let dummy_session : unit Session.session = Session.create_session "." in
let ctxt = {
Session.allow_obsolete_goals = true;
Session.keep_unmatched_theories = false;
Session.release_tasks = false;
Session.use_shapes_for_pairing_sub_goals = false;
Session.keygen = dummy_keygen;
......
......@@ -2067,6 +2067,62 @@ module AssoGoals = Tc.Pairing(Goal)(Goal)
(* merge a file into another *)
(**********************************)
(* the import_* functions can be used to copy session items from one 'b session
into another 'b session. The two sessions will have different keys. This is
different from the copy_* functions where we have 'a = 'b. Most import
functions import the entire subtree, but do not include the subtree into the
parent. For example, [import_theory keygen file theory] will return a new
theory whose parent is [file], but it will not modify [file.file_theories]
to contain the new theory. This is left to the caller. An exception to this
rule is [import_proof_attempt], because of its usage of
[add_external_proof]. *)
let rec import_theory ~keygen file th =
let new_th =
raw_add_theory
~keygen
~expanded:th.theory_expanded
~checksum:th.theory_checksum
file th.theory_name in
let goals =
List.map (import_goal ~keygen (Parent_theory new_th)) th.theory_goals in
new_th.theory_goals <- goals;
new_th
and import_goal ~keygen parent g =
let new_goal =
raw_add_no_task
~keygen
~expanded:g.goal_expanded
parent g.goal_name g.goal_expl g.goal_checksum g.goal_shape in
PHprover.iter (fun _ v -> import_proof_attempt ~keygen new_goal v)
g.goal_external_proofs;
PHstr.iter (fun k v ->
let tf = import_transf ~keygen new_goal v in
PHstr.add new_goal.goal_transformations k tf) g.goal_transformations;
new_goal
and import_proof_attempt ~keygen goal pa =
ignore (add_external_proof
~keygen
~obsolete:pa.proof_obsolete
~archived:pa.proof_archived
~limit:pa.proof_limit
~edit:pa.proof_edited_as
goal pa.proof_prover pa.proof_state)
and import_transf ~keygen goal tf =
let new_tf =
raw_add_transformation
~keygen
~expanded:tf.transf_expanded
goal
tf.transf_name in
let goals =
List.map (import_goal ~keygen (Parent_transf new_tf)) tf.transf_goals in
new_tf.transf_goals <- goals;
new_tf
let found_obsolete = ref false
let found_missed_goals = ref false
let found_missed_goals_in_theory = ref false
......@@ -2235,6 +2291,7 @@ type 'key update_context =
release_tasks : bool;
use_shapes_for_pairing_sub_goals : bool;
keygen : 'key keygen;
keep_unmatched_theories : bool;
}
let rec recover_sub_tasks ~theories env_session task g =
......@@ -2446,21 +2503,32 @@ let merge_file ~ctxt ~theories env from_f to_f =
(fun acc t -> Mstr.add t.theory_name.Ident.id_string t acc)
Mstr.empty from_f.file_theories
in
List.iter
(fun to_th ->
try
let from_th =
let name = to_th.theory_name.Ident.id_string in
try Mstr.find name from_theories
(* TODO: remove this later when all sessions are updated *)
with Not_found -> Mstr.find ("WP "^name) from_theories
in
merge_theory ~ctxt ~theories env from_th to_th
with
| Not_found when ctxt.allow_obsolete_goals -> ()
| Not_found -> raise OutdatedSession
)
to_f.file_theories;
let find_remove k map =
let elt = Mstr.find k map in
let acc = Mstr.remove k map in
elt, acc in
let remaining_theories =
List.fold_left
(fun acc to_th ->
try
let from_th, acc =
let name = to_th.theory_name.Ident.id_string in
try find_remove name acc
(* TODO: remove this later when all sessions are updated *)
with Not_found -> find_remove ("WP "^name) acc
in
merge_theory ~ctxt ~theories env from_th to_th;
acc
with
| Not_found when ctxt.allow_obsolete_goals -> acc
| Not_found -> raise OutdatedSession
)
from_theories to_f.file_theories in
if ctxt.keep_unmatched_theories then
Mstr.iter (fun _ v ->
to_f.file_theories <-
(import_theory ~keygen:ctxt.keygen to_f v) :: to_f.file_theories)
remaining_theories;
Debug.dprintf debug "[Info] merge_file, done@\n"
let rec recompute_all_shapes_goal ~release g =
......
......@@ -245,10 +245,14 @@ type 'key update_context =
release_tasks : bool;
use_shapes_for_pairing_sub_goals : bool;
keygen : 'key keygen;
keep_unmatched_theories : bool;
}
val update_session : ctxt:'key update_context -> 'oldkey session ->
Env.env -> Whyconf.config -> 'key env_session * bool * bool
val update_session :
ctxt:'key update_context ->
'oldkey session ->
Env.env -> Whyconf.config ->
'key env_session * bool * bool
(** reload the given session with the given environnement :
- the files are reloaded
- apply again the transformation
......@@ -262,6 +266,9 @@ val update_session : ctxt:'key update_context -> 'oldkey session ->
the second result.
If the merge generated new unpaired goals is indicated by
the third result.
Theories in the session that don't correspond to new theories are dropped,
unless keep_unmatched_theories is set to true. In this case, the theories
will be kept, but the goals will not contain tasks.
raises [OutdatedSession] if the session is obsolete and
[allow_obsolete] is false
......
......@@ -295,6 +295,7 @@ let update_session ~allow_obsolete ~release ~use_shapes
old_session env whyconf =
O.reset ();
let ctxt = {
keep_unmatched_theories = false;
allow_obsolete_goals = allow_obsolete;
release_tasks = release;
use_shapes_for_pairing_sub_goals = use_shapes;
......
......@@ -76,6 +76,7 @@ let read_update_session ~allow_obsolete env config fname =
let session,use_shapes = S.read_session project_dir in
let ctxt = {
S.allow_obsolete_goals = allow_obsolete;
S.keep_unmatched_theories = false;
S.release_tasks = false;
S.use_shapes_for_pairing_sub_goals = use_shapes;
S.keygen = (fun ?parent:_ () -> ());
......
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