From c3aa905c6c13b134c5ff01624450816ca3dc0147 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Mon, 1 Oct 2018 06:17:36 +0200
Subject: [PATCH] always save sessions using the current shape version
---
examples/stdlib/array/why3session.xml | 2 +-
src/session/controller_itp.ml | 8 +-
src/session/controller_itp.mli | 21 +--
src/session/itp_server.ml | 12 +-
src/session/session_itp.ml | 178 +++++++++++++++-----------
src/session/session_itp.mli | 9 +-
src/tools/why3replay.ml | 4 +-
src/why3session/why3session_lib.ml | 4 +-
src/why3session/why3session_lib.mli | 5 +-
9 files changed, 139 insertions(+), 104 deletions(-)
diff --git a/examples/stdlib/array/why3session.xml b/examples/stdlib/array/why3session.xml
index 842b827f9..ea77f929a 100644
--- a/examples/stdlib/array/why3session.xml
+++ b/examples/stdlib/array/why3session.xml
@@ -1,7 +1,7 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="4">
+<why3session shape_version="5">
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="6" steplimit="0" memlimit="1000"/>
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index c2eb78850..c522ab49e 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -223,18 +223,18 @@ let print_session fmt c =
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
-let reload_files (c : controller) ~use_shapes =
+let reload_files (c : controller) ~shape_version =
let old_ses = c.controller_session in
c.controller_env <- Env.create_env (Env.get_loadpath c.controller_env);
Whyconf.Hprover.reset c.controller_provers;
load_drivers c;
c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
- merge_files ~use_shapes c.controller_env c.controller_session old_ses
+ merge_files ~shape_version c.controller_env c.controller_session old_ses
exception Errors_list of exn list
-let reload_files (c: controller) ~use_shapes =
- let errors, b1, b2 = reload_files c ~use_shapes in
+let reload_files (c: controller) ~shape_version =
+ let errors, b1, b2 = reload_files c ~shape_version in
match errors with
| [] -> b1, b2
| _ -> raise (Errors_list errors)
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 3cebd5486..85bd76b4a 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -110,8 +110,17 @@ val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list
-val reload_files : controller -> use_shapes:bool -> bool * bool
-(** reload the files of the given session:
+val reload_files : controller -> shape_version:int option -> bool * bool
+(** [reload_files] returns a pair [(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 returned.
+
+ If parsing or typing errors occurs, a list of errors is raised
+ inside exception Errors_list.
+
+ The detailed process of reloading the files of the given session is
+ as follows.
- each file is parsed again and theories/goals extracted from it. If
some syntax error or parsing error occurs, then the corresponding
@@ -155,13 +164,7 @@ val reload_files : controller -> use_shapes:bool -> bool * bool
it, neither to its subgoals.
- [reload_files] It returns a pair (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 returned.
- If parsing or typing errors occurs, a list of errors is raised inside
- exception Errors_list.
-
-*)
+ *)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 51a859245..8406dc29b 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -595,10 +595,10 @@ 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 =
+ let reload_files cont ~shape_version =
capture_parse_or_type_errors
(fun c ->
- try let (_,_) = reload_files ~use_shapes c in [] with
+ try let (_,_) = reload_files ~shape_version c in [] with
| Errors_list le -> le) cont
let add_file cont ?format fname =
@@ -971,7 +971,7 @@ end
let init_server ?(send_source=true) config env f =
Debug.dprintf debug "loading session %s@." f;
- let ses,use_shapes = Session_itp.load_session f in
+ let ses,shape_version = Session_itp.load_session f in
Debug.dprintf debug "creating controller@.";
let c = create_controller config env ses in
let shortcuts =
@@ -1011,7 +1011,7 @@ end
};
Debug.dprintf debug "reloading source files@.";
let d = get_server_data () in
- let x = reload_files d.cont ~use_shapes in
+ let x = reload_files d.cont ~shape_version in
reset_and_send_the_whole_tree ();
(* After initial sending, we don't check anymore that there is a need to
focus on a specific node. *)
@@ -1273,7 +1273,9 @@ end
let _old_focus = !focused_node in
unfocus ();
clear_tables ();
- let l = reload_files d.cont ~use_shapes:true in
+ let l = reload_files d.cont
+ ~shape_version:(Some Termcode.current_shape_version)
+ in
reset_and_send_the_whole_tree ();
match l with
| [] ->
diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml
index 40653805b..249c13ae0 100644
--- a/src/session/session_itp.ml
+++ b/src/session/session_itp.ml
@@ -65,8 +65,6 @@ type proof_node = {
proofn_name : Ident.ident;
proofn_expl : string;
proofn_parent : proof_parent;
- proofn_checksum : Termcode.checksum;
- proofn_shape : Termcode.shape;
proofn_attempts : proofAttemptID Hprover.t;
mutable proofn_transformations : transID list;
}
@@ -118,7 +116,7 @@ type session = {
mutable next_transID : int;
session_dir : string; (** Absolute path *)
session_files : file Hstr.t;
- mutable session_shape_version : int;
+ session_sum_shape_table : (Termcode.checksum * Termcode.shape) Hpn.t;
session_prover_ids : int Hprover.t;
(* tasks *)
session_raw_tasks : Task.task Hpn.t;
@@ -470,6 +468,7 @@ let print_proof_attempt fmt pa =
let rec print_proof_node s (fmt: Format.formatter) p =
let pn = get_proofNode s p in
+ let sum,_ = Hpn.find s.session_sum_shape_table p in
let parent = match pn.proofn_parent with
| Theory t -> t.theory_name.id_string
| Trans id -> (get_transfNode s id).transf_name
@@ -477,7 +476,7 @@ let rec print_proof_node s (fmt: Format.formatter) p =
fprintf fmt
"@[<hv 1> Goal %s;@ parent %s;@ sum %s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@]@]"
pn.proofn_name.id_string parent
- (Termcode.string_of_checksum pn.proofn_checksum)
+ (Termcode.string_of_checksum sum)
(Pp.print_list Pp.semi print_proof_attempt)
(Hprover.fold (fun _key e l ->
let e = get_proof_attempt_node s e in
@@ -512,10 +511,10 @@ let _print_session fmt s =
let empty_session ?from dir =
- let prover_ids, shape_version =
+ let prover_ids =
match from with
- | Some v -> v.session_prover_ids, v.session_shape_version
- | None -> Hprover.create 7, Termcode.current_shape_version
+ | Some v -> v.session_prover_ids
+ | None -> Hprover.create 7
in
{ proofAttempt_table = Hint.create 97;
next_proofAttemptID = 0;
@@ -525,10 +524,10 @@ let empty_session ?from dir =
next_transID = 0;
session_dir = dir;
session_files = Hstr.create 3;
- session_shape_version = shape_version;
session_prover_ids = prover_ids;
session_raw_tasks = Hpn.create 97;
session_task_tables = Hpn.create 97;
+ session_sum_shape_table = Hpn.create 97;
file_state = Hstr.create 3;
th_state = Ident.Hid.create 7;
tn_state = Htn.create 97;
@@ -576,41 +575,39 @@ let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.pro
(* [mk_proof_node s n t p id] register in the session [s] a proof node
of proofNodeID [id] of parent [p] of task [t] *)
-let mk_proof_node ~version ~expl (s : session) (n : Ident.ident) (t : Task.task)
+let mk_proof_node ~shape_version ~expl (s : session) (n : Ident.ident) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
- (* let tables = Args_wrapper.build_naming_tables t in *)
- let sum = Termcode.task_checksum ~version t in
- let shape = Termcode.t_shape_task ~version ~expl t in
let pn = { proofn_name = n;
proofn_expl = expl;
proofn_parent = parent;
- proofn_checksum = sum;
- proofn_shape = shape;
proofn_attempts = Hprover.create 7;
proofn_transformations = [] } in
+ Hint.add s.proofNode_table node_id pn;
Hpn.add s.session_raw_tasks node_id t;
- Hint.add s.proofNode_table node_id pn
+ let sum = Termcode.task_checksum ~version:shape_version t in
+ let shape = Termcode.t_shape_task ~version:shape_version ~expl t in
+ Hpn.add s.session_sum_shape_table node_id (sum,shape)
+
+let mk_new_proof_node = mk_proof_node ~shape_version:Termcode.current_shape_version
let mk_proof_node_no_task (s : session) (n : Ident.ident)
(parent : proof_parent) (node_id : proofNodeID) sum shape proved =
let pn = { proofn_name = n;
proofn_expl = "";
proofn_parent = parent;
- proofn_checksum = sum;
- proofn_shape = shape;
proofn_attempts = Hprover.create 7;
proofn_transformations = [] } in
Hint.add s.proofNode_table node_id pn;
+ Hpn.add s.session_sum_shape_table node_id (sum,shape);
Hint.add s.pn_state node_id proved
-let mk_transf_proof_node (s : session) (parent_name : string)
+let mk_new_transf_proof_node (s : session) (parent_name : string)
(tid : transID) (index : int) (t : Task.task) =
let id = gen_proofNodeID s in
let gid,expl,_ = Termcode.goal_expl_task ~root:false t in
let goal_name = parent_name ^ "." ^ string_of_int index in
let goal_name = Ident.id_register (Ident.id_derive goal_name gid) in
- mk_proof_node ~version:s.session_shape_version ~expl
- s goal_name t (Trans tid) id;
+ mk_new_proof_node ~expl s goal_name t (Trans tid) id;
id
let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
@@ -633,7 +630,7 @@ let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : string list) (tl : Task.task list) =
let tid = gen_transID s in
let parent_name = (get_proofNode s id).proofn_name.Ident.id_string in
- let sub_tasks = List.mapi (mk_transf_proof_node s parent_name tid) tl in
+ let sub_tasks = List.mapi (mk_new_transf_proof_node s parent_name tid) tl in
let proved = sub_tasks = [] in
mk_transf_node s id tid name args ~proved sub_tasks ~detached:false;
tid
@@ -1140,7 +1137,6 @@ let build_session (s : session) xml =
match xml.Xml.name with
| "why3session" ->
let shape_version = int_attribute_def "shape_version" xml 1 in
- s.session_shape_version <- shape_version;
Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
(* just to keep the old_provers somewhere *)
let old_provers =
@@ -1151,10 +1147,12 @@ let build_session (s : session) xml =
Debug.dprintf debug "prover %d: %a@." id Whyconf.print_prover p;
Hprover.replace s.session_prover_ids p id)
old_provers;
- Debug.dprintf debug "[Info] load_session: done@\n"
+ Debug.dprintf debug "[Info] load_session: done@\n";
+ shape_version
| s ->
Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
- s
+ s;
+ Termcode.current_shape_version
exception ShapesFileError of string
@@ -1193,7 +1191,7 @@ let read_sum_and_shape ch =
| Exit -> Bytes.unsafe_to_string sum, Buffer.contents shape
- let use_shapes = ref true
+ let has_shapes = ref true
let fix_attributes ch name attrs =
if name = "goal" then
@@ -1213,16 +1211,16 @@ let read_sum_and_shape ch =
with Not_found -> ("sum", sum) :: attrs
in
("shape",shape) :: attrs
- with _ -> use_shapes := false; attrs
+ with _ -> has_shapes := false; attrs
else attrs
let read_xml_and_shapes xml_fn compressed_fn =
- use_shapes := true;
+ has_shapes := true;
try
let ch = C.open_in compressed_fn in
let xml = Xml.from_file ~fixattrs:(fix_attributes ch) xml_fn in
C.close_in ch;
- xml, !use_shapes
+ xml, !has_shapes
with Sys_error msg ->
raise (ShapesFileError ("cannot open shapes file for reading: " ^ msg))
end
@@ -1262,18 +1260,18 @@ with e ->
let load_session (dir : string) =
let session = empty_session dir in
let file = Filename.concat dir db_filename in
- let use_shapes =
+ let shape_version =
(* If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists file then
try
(*
Termcode.reset_dict ();
*)
- let xml,use_shapes =
+ let xml,has_shapes =
read_file_session_and_shapes dir file in
try
- build_session session xml.Xml.content;
- use_shapes
+ let shape_version = build_session session xml.Xml.content in
+ if has_shapes then Some shape_version else None
with Sys_error msg ->
failwith ("Open session: sys error " ^ msg)
with
@@ -1283,9 +1281,9 @@ let load_session (dir : string) =
| Xml.Parse_error s ->
Warning.emit "XML database corrupted, ignored (%s)@." s;
raise (SessionFileError "XML corrupted")
- else false
+ else None
in
- session, use_shapes
+ session, shape_version
(* -------------------- merge/update session --------------------------- *)
@@ -1293,8 +1291,8 @@ let load_session (dir : string) =
module Goal = struct
type 'a t = proofNodeID * session
- let checksum (id,s) = Some (get_proofNode s id).proofn_checksum
- let shape (id,s) = (get_proofNode s id).proofn_shape
+ let checksum (id,s) = Some (fst (Hpn.find s.session_sum_shape_table id))
+ let shape (id,s) = snd (Hpn.find s.session_sum_shape_table id)
let name (id,s) = (get_proofNode s id).proofn_name
end
@@ -1311,9 +1309,9 @@ let save_detached_proof s parent old_pa_n =
parent)
let rec save_detached_goal old_s s parent detached_goal_id id =
- let detached_goal = get_proofNode old_s detached_goal_id in
- mk_proof_node_no_task s detached_goal.proofn_name parent id detached_goal.proofn_checksum
- detached_goal.proofn_shape false;
+ let detached_goal = get_proofNode old_s detached_goal_id in
+ let (sum,shape) = Hpn.find old_s.session_sum_shape_table detached_goal_id in
+ mk_proof_node_no_task s detached_goal.proofn_name parent id sum shape false;
Hprover.iter (fun _ pa ->
let pa = get_proof_attempt_node old_s pa in
save_detached_proof s id pa) detached_goal.proofn_attempts;
@@ -1398,19 +1396,19 @@ let add_registered_transformation s env old_tr goal_id =
in
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
-let rec merge_goal ~use_shapes env new_s old_s ~goal_obsolete old_goal new_goal_id =
+let rec merge_goal ~shape_version env new_s old_s ~goal_obsolete old_goal new_goal_id =
Hprover.iter (fun k pa ->
let pa = get_proof_attempt_node old_s pa in
merge_proof new_s ~goal_obsolete new_goal_id k pa)
old_goal.proofn_attempts;
List.iter
- (merge_trans ~use_shapes env old_s new_s new_goal_id)
+ (merge_trans ~shape_version env old_s new_s new_goal_id)
old_goal.proofn_transformations;
let new_goal_node = get_proofNode new_s new_goal_id in
new_goal_node.proofn_transformations <- List.rev new_goal_node.proofn_transformations;
update_goal_node (fun _ -> ()) new_s new_goal_id
-and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
+and merge_trans ~shape_version env old_s new_s new_goal_id old_tr_id =
let old_tr = get_transfNode old_s old_tr_id in
let old_subtasks = List.map (fun id -> id,old_s)
old_tr.transf_subtasks in
@@ -1426,12 +1424,13 @@ and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
let new_subtasks = List.map (fun id -> id,new_s)
new_tr.transf_subtasks in
let associated,detached =
- AssoGoals.associate ~use_shapes old_subtasks new_subtasks
+ AssoGoals.associate ~use_shapes:(shape_version <> None)
+ old_subtasks new_subtasks
in
List.iter
(function
| ((new_goal_id,_), Some ((old_goal_id,_), goal_obsolete)) ->
- merge_goal ~use_shapes env new_s old_s ~goal_obsolete
+ merge_goal ~shape_version env new_s old_s ~goal_obsolete
(get_proofNode old_s old_goal_id) new_goal_id
| ((id,s), None) ->
Debug.dprintf debug "[merge_trans] missed new subgoal: %s@."
@@ -1459,7 +1458,7 @@ and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
exit 2
-let merge_theory ~use_shapes env old_s old_th s th : unit =
+let merge_theory ~shape_version env old_s old_th s th : unit =
let get_goal_name goal_node =
let name = goal_node.proofn_name in
try
@@ -1481,18 +1480,18 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
let new_goal = get_proofNode s ng_id in
(* look for old_goal with matching name *)
let new_goal_name = get_goal_name new_goal in
- let old_goal = get_proofNode old_s
- (Hstr.find old_goals_table new_goal_name) in
+ let old_id = Hstr.find old_goals_table new_goal_name in
+ let old_goal = get_proofNode old_s old_id in
Hstr.remove old_goals_table new_goal_name;
let goal_obsolete =
- let s1 = new_goal.proofn_checksum in
- let s2 = old_goal.proofn_checksum in
+ let s1 = fst (Hpn.find s.session_sum_shape_table ng_id) in
+ let s2 = fst (Hpn.find old_s.session_sum_shape_table old_id) in
Debug.dprintf debug "[merge_theory] goal has checksum@.";
not (Termcode.equal_checksum s1 s2)
in
if goal_obsolete then
found_obsolete := true;
- merge_goal ~use_shapes env s old_s ~goal_obsolete old_goal ng_id
+ merge_goal ~shape_version env s old_s ~goal_obsolete old_goal ng_id
with
| Not_found ->
(* if no goal of matching name is found store it to look for
@@ -1503,12 +1502,14 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
(* attach the session to the subtasks to be able to instantiate Pairing *)
let detached_goals = Hstr.fold (fun _key g tl -> (g,old_s) :: tl) old_goals_table [] in
let associated,detached =
- AssoGoals.associate ~use_shapes detached_goals !new_goals
+ AssoGoals.associate ~use_shapes:(shape_version <> None)
+ detached_goals !new_goals
in
List.iter (function
| ((new_goal_id,_), Some ((old_goal_id,_), goal_obsolete)) ->
Debug.dprintf debug "[merge_theory] pairing paired one goal, yeah !@.";
- merge_goal ~use_shapes env s old_s ~goal_obsolete (get_proofNode old_s old_goal_id) new_goal_id
+ merge_goal ~shape_version env s old_s ~goal_obsolete
+ (get_proofNode old_s old_goal_id) new_goal_id
| ((id,_), None) ->
Debug.dprintf debug "[merge_theory] pairing found missed sub goal: %s@."
(get_proofNode s id).proofn_name.Ident.id_string;
@@ -1522,10 +1523,16 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
provided in merge try to merge the new theory with the previous one *)
let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theory)
: theory =
- let add_goal parent goal id =
- let name,expl,task = Termcode.goal_expl_task ~root:true goal in
- mk_proof_node ~version:s.session_shape_version ~expl
- s name task parent id;
+ let add_goal =
+ match merge with
+ | Some(_,_,_,Some v) ->
+ fun parent goal id ->
+ let name,expl,task = Termcode.goal_expl_task ~root:true goal in
+ mk_proof_node ~shape_version:v ~expl s name task parent id
+ | _ ->
+ fun parent goal id ->
+ let name,expl,task = Termcode.goal_expl_task ~root:true goal in
+ mk_new_proof_node ~expl s name task parent id
in
let tasks = Task.split_theory th None None in
let goalsID = List.map (fun _ -> gen_proofNodeID s) tasks in
@@ -1538,8 +1545,8 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
List.iter2 (add_goal parent) tasks goalsID;
begin
match merge with
- | Some (old_s, old_th, env, use_shapes) ->
- merge_theory ~use_shapes env old_s old_th s theory
+ | Some (old_s, old_th, env, shape_version) ->
+ merge_theory ~shape_version env old_s old_th s theory
| _ -> if tasks <> [] then found_detached := true (* should be found_new_goals instead of found_detached *)
end;
theory
@@ -1568,7 +1575,7 @@ let add_file_section (s:session) (fn:string) ~file_is_detached
(* 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 ~file_is_detached ~env
+let merge_file_section ~shape_version ~old_ses ~old_theories ~file_is_detached ~env
(s:session) (fn:string) (theories:Theory.theory list) format
: unit =
Debug.dprintf debug_merge "[Session_itp.merge_file_section] fn = %s@." fn;
@@ -1587,7 +1594,8 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~file_is_detached ~env
let old_th = Hstr.find old_th_table theory_name in
Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory found: %s@." theory_name;
Hstr.remove old_th_table theory_name;
- make_theory_section ~detached:false ~merge:(old_ses,old_th,env,use_shapes) s fn th
+ make_theory_section ~detached:false
+ ~merge:(old_ses,old_th,env,shape_version) s fn th
with Not_found ->
(* if no theory was found we make a new theory section *)
Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory NOT FOUND in old session: %s@." theory_name;
@@ -1626,31 +1634,56 @@ let read_file env ?format fn =
in
List.map (fun (_,_,a) -> a) th
-let merge_file ~use_shapes env (ses : session) (old_ses : session) file =
+let merge_file ~shape_version 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
try
let new_theories = read_file env file_name ?format in
merge_file_section
- ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:false
+ ses ~shape_version ~old_ses ~old_theories ~file_is_detached:false
~env file_name new_theories format;
None
with e -> (* TODO: capture only parsing and typing errors *)
merge_file_section
- ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:true
+ ses ~shape_version ~old_ses ~old_theories ~file_is_detached:true
~env file_name [] format;
Some e
-let merge_files ~use_shapes env (ses:session) (old_ses : session) =
+let merge_files ~shape_version env (ses:session) (old_ses : session) =
let errors =
Hstr.fold
(fun _ f acc ->
- match merge_file ~use_shapes env ses old_ses f with
+ match merge_file ~shape_version env ses old_ses f with
| None -> acc
| Some e -> e :: acc)
(get_files old_ses) []
in
+ (* recompute shapes if absent or obsolete *)
+ if shape_version <> Some Termcode.current_shape_version then
+ begin
+ Hpn.clear ses.session_sum_shape_table;
+ let version = Termcode.current_shape_version in
+ fold_all_session
+ ses
+ (fun () n ->
+ match n with
+ | APn id ->
+ let sum,shape =
+ try
+ let t = get_task ses id in
+ let _,expl,_ = Termcode.goal_expl_task ~root:false t in
+ let sum = Termcode.task_checksum ~version t in
+ let shape = Termcode.t_shape_task ~version ~expl t in
+ sum, shape
+ with Not_found -> (* detached goal *)
+ Termcode.dumb_checksum, Termcode.shape_of_string ""
+ in
+ Hpn.add ses.session_sum_shape_table id (sum,shape)
+ | _ -> ()
+ )
+ ()
+ end;
(errors,!found_obsolete,!found_detached)
@@ -1659,9 +1692,6 @@ let merge_files ~use_shapes env (ses:session) (old_ses : session) =
(************************)
module Mprover = Whyconf.Mprover
-(* dead code
-module Sprover = Whyconf.Sprover
-*)
module PHprover = Whyconf.Hprover
open Format
@@ -1826,11 +1856,10 @@ let rec save_goal s ctxt fmt pnid =
save_ident pn.proofn_name
(save_string_attrib "expl") pn.proofn_expl
(save_bool_def "proved" false) (pn_proved s pnid);
- let sum = Termcode.string_of_checksum pn.proofn_checksum in
- let shape = Termcode.string_of_shape pn.proofn_shape in
- Compress.Compress_z.output_string ctxt.ch_shapes sum;
+ let (sum,shape) = Hpn.find s.session_sum_shape_table pnid in
+ Compress.Compress_z.output_string ctxt.ch_shapes (Termcode.string_of_checksum sum);
Compress.Compress_z.output_char ctxt.ch_shapes ' ';
- Compress.Compress_z.output_string ctxt.ch_shapes shape;
+ Compress.Compress_z.output_string ctxt.ch_shapes (Termcode.string_of_shape shape);
Compress.Compress_z.output_char ctxt.ch_shapes '\n';
let l = Hprover.fold
(fun _ a acc ->
@@ -1888,10 +1917,7 @@ let save fname shfname session =
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
- session.session_shape_version;
-(*
- Termcode.reset_dict ();
-*)
+ Termcode.current_shape_version;
let prover_ids = session.session_prover_ids in
let provers =
PHprover.fold (get_prover_to_save prover_ids)
diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli
index 57cee7327..5d14abdad 100644
--- a/src/session/session_itp.mli
+++ b/src/session/session_itp.mli
@@ -169,8 +169,9 @@ val read_file :
signaled with exceptions. *)
val merge_files :
- use_shapes:bool -> Env.env -> session -> session -> exn list * bool * bool
-(** [merge_files ~use_shapes env ses old_ses] merges the file sections
+ shape_version:int option ->
+ Env.env -> session -> session -> exn list * bool * bool
+(** [merge_files ~use_shape_version 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,
@@ -221,11 +222,11 @@ val mark_obsolete: session -> proofAttemptID -> unit
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
-val load_session : string -> session * bool
+val load_session : string -> session * int option
(** [load_session dir] load a session in directory [dir]; all the
tasks are initialised to None
- The returned boolean is set when there was shapes read from disk.
+ The second result is the shape version read from disk, if any
raises [SessionFileError msg] if the database file cannot be read
correctly.
diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml
index 93b8b6e0e..e9a72f973 100644
--- a/src/tools/why3replay.ml
+++ b/src/tools/why3replay.ml
@@ -384,12 +384,12 @@ let () =
Whyconf.Args.exit_with_usage option_list usage_msg;
try
Debug.dprintf debug "Opening session '%s'...@?" dir;
- let ses,use_shapes = S.load_session dir in
+ let ses,shape_version = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in
(* update the session *)
let found_obs, found_detached =
try
- Controller_itp.reload_files cont ~use_shapes
+ Controller_itp.reload_files cont ~shape_version
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
diff --git a/src/why3session/why3session_lib.ml b/src/why3session/why3session_lib.ml
index df5c61b3d..b46b47392 100644
--- a/src/why3session/why3session_lib.ml
+++ b/src/why3session/why3session_lib.ml
@@ -78,7 +78,7 @@ let read_session fname =
S.load_session project_dir
let read_update_session ~allow_obsolete env config fname =
- let session,use_shapes = read_session fname in
+ let session,shape_version = read_session fname in
(*
let ctxt = S.mk_update_context
~allow_obsolete_goals:allow_obsolete
@@ -90,7 +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
+ Controller_itp.reload_files cont ~shape_version
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
diff --git a/src/why3session/why3session_lib.mli b/src/why3session/why3session_lib.mli
index 951f4398e..1e2c4ab03 100644
--- a/src/why3session/why3session_lib.mli
+++ b/src/why3session/why3session_lib.mli
@@ -44,7 +44,10 @@ val common_options : spec_list
val read_env_spec : unit -> Env.env * Whyconf.config * bool
(** read_simple_spec also *)
-val read_session : string -> Session_itp.session * bool
+val read_session : string -> Session_itp.session * int option
+(** [read_session s] reads the session file [s] and returns a pair
+[(ses,shape_version)] where [ses] is the session structure (without
+any tasks) and [shape_version] indicates the shapes version, if any *)
val read_update_session :
allow_obsolete:bool -> Env.env ->
--
GitLab