Commit 035a91c6 authored by Sylvain Dailler's avatar Sylvain Dailler

[WIP] This is ongoing experimental work.

Change the way shapes are saved. The shape files is now organized as
follow:
- first, the shapes of all declarations that were converted to shape
- second, checksum followed by a string representing the succession of
variables declarations.
Example:
"(* Recording of all shape variable declarations *)
left case
a=axc0
a=a+a+a+a+a+a+a+axaxaxaxaxaxaxaxc0
Na=axc0Oa=axc0
right case
Na=axc0

(* Checksum then concatenated variables representing a task shape *)
956169bfb451ee6459ffdc4df18de7fd H3H2H3
4dceea9c71fce658291b3212396973a6 H1H2H3
566331d4fbc568133c5beace068734c6 H0H1H2H1
bf3e0320b4b7af8d182c9aaa24ff2ee7 H5H2H3
03fe7b1734fc43b78ef069c15b8ceef0 H4H5H2H5
"

Other changes:
- Transform to shape only the local declarations
- The shape size limit is now per declarations

Effect:
- It seems to reduce the size of the shapes a little

TODO:
- We read the session Xml twice just to be able to get the version of the
shape before reading them
- Data structure to record correspondence between shape and variable index
seems inefficient (GShape)
- At saving, the shapes need to be recomputed in order to not save useless
shape variables (or temporary goals that were removed). This does not seem
to be too inefficient: To be decided.
- shapes should now be saved as a list of integer instead of strings
- Pairing is under change. Proposed measure during brainstorming with
Claude -> lcp measure replaced by the lexicographic order on:
(number of same hypotheses, lcp on explanations, lcp on goal shape)
- hyp_sep is "H". To be decided
- all remaining TODO in the code
parent 963e1996
use int.Int
constant x : int
axiom h : x = 0 \/ x <> 0
axiom k : x + x + x + x + x = 0
goal g : x = 0 \/ x <> 0
axiom h : x = 1 \/ x <> 1
axiom k : x + x + x + x + x = 985
goal g : x = 1 \/ x <> 1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="7">
<why3session shape_version="8">
<file proved="true">
<path name=".."/>
<path name="276_shape.mlw"/>
......
......@@ -1227,6 +1227,25 @@ let read_sum_and_shape ch =
raise (ShapesFileError "shapes files corrupted (premature end of file), ignored");
| Exit -> Bytes.unsafe_to_string sum, Buffer.contents shape
(* Read the first part of the shapes: a list of shapes which are then referred
as H1 ... Hn in the shape corresponding to tasks *)
let rec read_global_buffer ch =
Buffer.clear shape;
try
while true do
let c = C.input_char ch in
if c = '\n' then raise Exit;
Buffer.add_char shape c
done;
assert false
with
| End_of_file ->
raise (ShapesFileError "shapes files corrupted (premature end of file), ignored");
| Exit ->
let g_shape = Buffer.contents shape in
Buffer.clear shape;
if g_shape <> "" then
(Termcode.add_to_global_buffer g_shape; read_global_buffer ch)
let has_shapes = ref true
......@@ -1251,10 +1270,26 @@ let read_sum_and_shape ch =
with _ -> has_shapes := false; attrs
else attrs
let get_version (xml: Xml.t) =
match xml.Xml.content.Xml.name with
| "why3session" ->
let shape_version = int_attribute_def "shape_version" xml.Xml.content 1 in
shape_version
| s ->
Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
s;
Termcode.current_shape_version
let read_xml_and_shapes xml_fn compressed_fn =
has_shapes := true;
try
let ch = C.open_in compressed_fn in
(* We need to parse the file first to get the shape version *)
let shape_version =
let xml = Xml.from_file xml_fn in
get_version xml in
if shape_version >= 8 then read_global_buffer ch;
let xml = Xml.from_file ~fixattrs:(fix_attributes ch) xml_fn in
C.close_in ch;
xml, !has_shapes
......@@ -1997,6 +2032,13 @@ let save fname shfname session =
provers Mint.empty
in
Mint.iter (save_prover fmt) provers_to_save;
if Termcode.current_shape_version >= 8 then
begin
(* In version higher than 8, first save the list of variables that are
referenced in shapes. *)
Compress.Compress_z.output_string chsh (Buffer.contents Termcode.global_buffer);
Compress.Compress_z.output_string chsh "\n";
end;
let ctxt = { prover_ids = prover_ids; provers = provers; ch_shapes = chsh } in
Hfile.iter (save_file session ctxt fmt) session.session_files;
fprintf fmt "@]@\n</why3session>";
......@@ -2006,6 +2048,28 @@ let save fname shfname session =
let save_session (s : session) =
(* TODO this is inefficient. Think about trying to change the datastructure of
global maps in shapes *)
let uniformize_shape () =
Termcode.clear_global_hyp_shape ();
fold_all_session s (fun () any ->
match any with
| APn g ->
let t = get_task s g in
let (_, expl, _) =
let root =
match get_proof_parent s g with
| Trans _ -> false | Theory _ -> true in
Termcode.goal_expl_task ~root t in
let version = Termcode.current_shape_version in
let shape = Termcode.t_shape_task ~expl ~version t in
let (checksum, _) = Hpn.find s.session_sum_shape_table g in
Hpn.replace s.session_sum_shape_table g (checksum, shape)
| _ -> ()) () in
(* Used here so that shape do not save artifacts of the old saved shapes or
removed goals (making them grow). It also ensures the order of hypothesis
is deterministic between two runs of Why3. *)
uniformize_shape ();
let f = Filename.concat s.session_dir db_filename in
Sysutil.backup_file f;
let fs = Filename.concat s.session_dir shape_filename in
......
This diff is collapsed.
......@@ -45,6 +45,10 @@ val print_shape: Format.formatter -> shape -> unit
val t_shape_task: ?version:int -> expl:string -> Task.task -> shape
(** returns the shape of a given task *)
val global_buffer: Buffer.t
val add_to_global_buffer: string -> unit
val clear_global_hyp_shape: unit -> unit
(** Checksums *)
type checksum
......
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