selects the naive pairing algorithm when shapes are not on disk

examples/use_api/create_session.ml

@@ -63,7 +63,8 @@ let keygen ?parent () = ()
 (* create an empty session in the current directory *)
 let env_session,_,_ =
   let dummy_session : unit Session.session = Session.create_session "." in
-  Session.update_session ~keygen ~allow_obsolete:true dummy_session env config
+  Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true 
+    dummy_session env config
 
 (* adds a file in the new session *)
 let file : unit Session.file = 

src/ide/gmain.ml

@@ -805,14 +805,14 @@ let () =
 let sched =
   try
     Debug.dprintf debug "@[<hov 2>[GUI session] Opening session...@\n";
-    let session =
+    let session,use_shapes =
       if Sys.file_exists project_dir then
         S.read_session project_dir
       else
-        S.create_session project_dir
+        S.create_session project_dir, false
     in
     let env,(_:bool),(_:bool) =
-      M.update_session ~allow_obsolete:true session gconfig.env
+      M.update_session ~use_shapes ~allow_obsolete:true session gconfig.env
         gconfig.Gconfig.config
     in
     Debug.dprintf debug "@]@\n[GUI session] Opening session: update done@.  @[<hov 2>";
@@ -1959,7 +1959,8 @@ let reload () =
     (** reload the session *)
     let old_session = (env_session()).S.session in
     let new_env_session,(_:bool),(_:bool) =
-      M.update_session ~allow_obsolete:true old_session gconfig.env
+      (* use_shapes is true since session is in memory *)
+      M.update_session ~use_shapes:true ~allow_obsolete:true old_session gconfig.env
         gconfig.Gconfig.config
     in
     current_env_session := Some new_env_session

src/session/session.ml

@@ -1487,22 +1487,26 @@ let read_sum_and_shape ch =
       | Exit -> sum, Buffer.contents shape
 
 
-let fix_attributes ch name attrs =
-  if name = "goal" then
-  let sum,shape = read_sum_and_shape ch in
-  let attrs =
-    try
-      let old_sum = List.assoc "sum" attrs in
-      if sum <> old_sum then
-        begin
-          Format.eprintf "old sum = %s ; new sum = %s@." old_sum sum;
-          exit 2
-        end;
-      attrs
-    with Not_found -> ("sum", sum) :: attrs
-  in
-  ("shape",shape) :: attrs
-  else attrs
+  let use_shapes = ref true
+
+  let fix_attributes ch name attrs =
+    if name = "goal" then
+      try 
+        let sum,shape = read_sum_and_shape ch in
+        let attrs =
+          try
+            let old_sum = List.assoc "sum" attrs in
+            if sum <> old_sum then
+              begin
+                Format.eprintf "old sum = %s ; new sum = %s@." old_sum sum;
+                exit 2
+              end;
+            attrs
+          with Not_found -> ("sum", sum) :: attrs
+        in
+        ("shape",shape) :: attrs
+      with _ -> use_shapes := false; attrs
+    else attrs
 
 (*
 let rec read_shapes_goal ch g =
@@ -1546,9 +1550,11 @@ let read_shapes fn xml =
 *)
 
 let read_xml_and_shapes xml_fn compressed_fn =
+  use_shapes := true;
   let ch = C.open_in compressed_fn in
   try
-    Xml.from_file ~fixattrs:(fix_attributes ch) xml_fn
+    let xml = Xml.from_file ~fixattrs:(fix_attributes ch) xml_fn in
+    xml, !use_shapes
   with
       e -> C.close_in ch; raise e
 end
@@ -1569,7 +1575,7 @@ let read_file_session_and_shapes dir xml_filename =
       begin
         Format.eprintf "[Warning] could not read goal shapes because \
                                 Why3 was not compiled with compress support@.";
-        Xml.from_file xml_filename
+        Xml.from_file xml_filename, false
       end
   else
     let shape_filename = Filename.concat dir shape_filename in
@@ -1578,12 +1584,12 @@ let read_file_session_and_shapes dir xml_filename =
     else
       begin
         Format.eprintf "[Warning] could not find goal shapes file@.";
-        Xml.from_file xml_filename
+        Xml.from_file xml_filename, false
       end
 with e ->
   Format.eprintf "[Warning] failed to read goal shapes: %s@."
     (Printexc.to_string e);
-  Xml.from_file xml_filename
+  Xml.from_file xml_filename, false
 
 type notask = unit
 let read_session dir =
@@ -1591,30 +1597,29 @@ let read_session dir =
     raise (OpenError (Pp.sprintf "%s is not an existing directory" dir));
   let xml_filename = Filename.concat dir db_filename in
   let session = empty_session dir in
+  let use_shapes =
   (** If the xml is present we read it, otherwise we consider it empty *)
-  if Sys.file_exists xml_filename then begin
-    try
-      Tc.reset_dict ();
-      let xml = read_file_session_and_shapes dir xml_filename in
-(*
-      let xml = Xml.from_file xml_filename in
-      let xml = import_shapes dir xml in
-*)
+    if Sys.file_exists xml_filename then 
       try
-        load_session session xml.Xml.content;
-      with Sys_error msg ->
-        failwith ("Open session: sys error " ^ msg)
-    with
-      | Sys_error msg ->
-      (* xml does not exist yet *)
-        raise (OpenError msg)
-      | Xml.Parse_error s ->
-        Format.eprintf "XML database corrupted, ignored (%s)@." s;
-      (* failwith
-         ("Open session: XML database corrupted (%s)@." ^ s) *)
-        raise (OpenError "XML corrupted")
-  end;
-  session
+        Tc.reset_dict ();
+        let xml,use_shapes = read_file_session_and_shapes dir xml_filename in
+        try
+          load_session session xml.Xml.content;
+          use_shapes
+        with Sys_error msg ->
+          failwith ("Open session: sys error " ^ msg)
+      with
+        | Sys_error msg ->
+        (* xml does not exist yet *)
+          raise (OpenError msg)
+        | Xml.Parse_error s ->
+          Format.eprintf "XML database corrupted, ignored (%s)@." s;
+        (* failwith
+           ("Open session: XML database corrupted (%s)@." ^ s) *)
+          raise (OpenError "XML corrupted")
+  else false
+  in
+  session, use_shapes
 
 
 (*******************************)
@@ -2011,6 +2016,7 @@ let print_external_proof fmt p =
 (** Pairing *)
 
 module AssoGoals : sig
+  val set_use_shapes : bool -> unit
   val associate : 'a goal list -> 'b goal list ->
     ('b goal * ('a goal * bool) option) list
 end = struct
@@ -2040,6 +2046,9 @@ end = struct
   open ToGoal
   open FromGoal
 
+  let use_shapes = ref true
+  let set_use_shapes b = use_shapes := b
+
   let associate (from_goals: 'ffrom goal list) (to_goals: 'tto goal list) :
       ('tto goal * ('ffrom goal * bool) option) list =
     let from_goals : ffrom goal list =
@@ -2047,7 +2056,7 @@ end = struct
     let to_goals   : tto goal list =
       Obj.magic (to_goals : 'tto goal list) in
     let associated : (tto goal * (ffrom goal * bool) option) list =
-      AssoGoals.associate from_goals to_goals in
+      AssoGoals.associate ~use_shapes:!use_shapes from_goals to_goals in
     (Obj.magic associated : ('tto goal * ('ffrom goal * bool) option) list)
 
 end
@@ -2423,10 +2432,11 @@ let recompute_all_shapes ~release session =
   session.session_shape_version <- Termcode.current_shape_version;
   iter_session (recompute_all_shapes_file ~release) session
 
-let update_session
+let update_session ~use_shapes
     ?(release=false) ~keygen ~allow_obsolete old_session env whyconf =
   Debug.dprintf debug "[Info] update_session: shape_version = %d@\n"
     old_session.session_shape_version;
+  AssoGoals.set_use_shapes use_shapes;
   let new_session =
     create_session ~shape_version:old_session.session_shape_version
       old_session.session_dir

src/session/session.mli

@@ -186,9 +186,11 @@ type notask
 (** A phantom type which is used for sessions which don't contain any task. The
     only such sessions are sessions that come from {!read_session} *)
 
-val read_session : string -> notask session
+val read_session : string -> notask session * bool
 (** Read a session stored on the disk. It returns a session without any
-    task attached to goals *)
+    task attached to goals.
+    the returned boolean is set when there was shapes read from disk.
+*)
 
 val save_session : Whyconf.config -> 'key session -> unit
 (** Save a session on disk *)
@@ -230,6 +232,7 @@ type 'key keygen = ?parent:'key -> unit -> 'key
 exception OutdatedSession
 
 val update_session :
+  use_shapes:bool ->
   ?release:bool (* default false *)  ->
   keygen:'a keygen ->
   allow_obsolete:bool -> 'b session ->

src/session/session_scheduler.ml

@@ -313,10 +313,10 @@ let rec init_any any = O.init (key_any any) any; iter init_any any
 
 let init_session session = session_iter init_any session
 
-let update_session ?release ~allow_obsolete old_session env whyconf  =
+let update_session ~use_shapes ?release ~allow_obsolete old_session env whyconf  =
   O.reset ();
   let (env_session,_,_) as res =
-    update_session ?release
+    update_session ~use_shapes ?release
       ~keygen:O.create ~allow_obsolete old_session env whyconf
   in
   Debug.dprintf debug "Init_session@\n";

src/session/session_scheduler.mli

@@ -111,6 +111,7 @@ module Make(O: OBSERVER) : sig
   (** {2 Save and load a state} *)
 
   val update_session :
+    use_shapes:bool ->
     ?release:bool ->
     allow_obsolete:bool ->
     'key session ->

src/session/termcode.ml

@@ -763,9 +763,16 @@ module Pairing(Old: S)(New: S) = struct
     end;
     Array.to_list result
 
-(*
-  let associate oldgoals newgoals =
-    try List.map2 (fun o n -> n, Some (o, true)) oldgoals newgoals
-    with Invalid_argument _ -> associate oldgoals newgoals
-*)
+  let simple_associate oldgoals newgoals =
+    let rec aux acc o n =
+      match o,n with
+        | _, [] -> acc
+        | [], n :: rem_n -> aux ((n,None)::acc) [] rem_n
+        | o :: rem_o, n :: rem_n -> aux ((n,Some(o,true))::acc) rem_o rem_n
+    in
+    aux [] oldgoals newgoals
+
+  let associate ~use_shapes =
+    if use_shapes then associate else simple_associate
+
 end

src/session/termcode.mli

@@ -58,13 +58,18 @@ module type S = sig
 end
 
 module Pairing(Old: S)(New: S) : sig
-  val associate:
+  val associate: use_shapes:bool ->
     Old.t list -> New.t list -> (New.t * (Old.t * bool) option) list
     (** Associate new goals to (possibly) old goals
         Each new goal is mapped either to
-        - [None]: no pairing at all
-        - [Some (h, false)]: exact matching (equal checksums)
-        - [Some (h, true)]: inexact matching (goal obsolete)
+        - [None]: no old goal associated
+        - [Some (h, false)]: the matching is exact (same checksums)
+        - [Some (h, true)]: inexact matching (thus proofs for the new goal 
+          must be assumed obsolete)
+
+        if [use_shapes] is set, the clever algorithm matching shapes is used,
+        otherwise a simple association in the given order of goals is done.
 
         Note: in the output, goals appear in the same order as in [newgoals] *)
+
 end

src/tools/why3replay.ml

@@ -400,8 +400,8 @@ let () =
     Debug.dprintf debug "Opening session...@?";
     O.verbose := Debug.test_flag debug;
     let env_session,found_obs,some_merge_miss =
-      let session = S.read_session project_dir in
-      M.update_session ~allow_obsolete:true session env config
+      let session, use_shapes = S.read_session project_dir in
+      M.update_session ~use_shapes ~allow_obsolete:true session env config
     in
     Debug.dprintf debug " done.@.";
     if !opt_obsolete_only && not found_obs

src/why3session/why3session_csv.ml

@@ -118,7 +118,7 @@ let rec print_line fmt provers a =
 
 let run_one_normal filter_provers fmt fname =
   let project_dir = Session.get_project_dir fname in
-  let session = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with
@@ -169,7 +169,7 @@ let grab_valid_time provers_time provers pa =
 
 let run_one_by_time provers_time filter_provers fname =
   let project_dir = Session.get_project_dir fname in
-  let session = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with

src/why3session/why3session_html.ml

@@ -72,7 +72,7 @@ type context =
 
 let run_file (context : context) print_session fname =
   let project_dir = Session.get_project_dir fname in
-  let session = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let output_dir =
     if !output_dir = "" then project_dir else !output_dir
   in

src/why3session/why3session_info.ml

@@ -355,7 +355,7 @@ let print_stats r0 r1 stats =
 let run_one stats r0 r1 fname =
   let project_dir = Session.get_project_dir fname in
   if !opt_project_dir then printf "%s@." project_dir;
-  let session = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let sep = if !opt_print0 then Pp.print0 else Pp.newline in
   if !opt_print_provers then
     printf "%a@."

src/why3session/why3session_latex.ml

@@ -457,7 +457,7 @@ let table () = if !opt_longtable then "longtable" else "tabular"
 
 let run_one fname =
   let project_dir = Session.get_project_dir fname in
-  let session = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let dir = if !opt_output_dir = "" then project_dir else
       !opt_output_dir
   in

src/why3session/why3session_lib.ml

@@ -74,8 +74,9 @@ let read_env_spec () =
 
 let read_update_session ~allow_obsolete env config fname =
   let project_dir = Session.get_project_dir fname in
-  let session = Session.read_session project_dir in
-  Session.update_session ~keygen:(fun ?parent:_ _ -> ())
+  let session,use_shapes = Session.read_session project_dir in
+  (* FIXME: set use_shapes depending on what was loaded from disk *)
+  Session.update_session ~use_shapes ~keygen:(fun ?parent:_ _ -> ())
     ~allow_obsolete session env config
 
 (** filter *)