removed usage of phantom type "notask" in sessions. Added detached old goals.

(no yet displayed in IDE)

src/ide/gmain.ml

@@ -812,7 +812,7 @@ let sched =
     Debug.dprintf debug "@[<hov 2>[GUI session] Opening session...@\n";
     let session,use_shapes =
       if Sys.file_exists project_dir then
-        S.read_session project_dir
+        S.read_session ~keygen:MA.create project_dir
       else
         S.create_session project_dir, false
     in

src/session/session.ml

@@ -189,8 +189,12 @@ and 'a transf =
       mutable transf_goals : 'a goal list;
       (** Not mutated after the creation of the session *)
       mutable transf_expanded : bool;
+      mutable transf_detached : 'a detached option;
     }
 
+and 'a detached =
+    { detached_goals: 'a goal list; }
+
 and 'a theory =
     { mutable theory_key : 'a;
       theory_name : Ident.ident;
@@ -200,6 +204,7 @@ and 'a theory =
       mutable theory_verified : float option;
       mutable theory_expanded : bool;
       mutable theory_task : Theory.theory hide;
+      mutable theory_detached : 'a detached option;
     }
 
 and 'a file =
@@ -1053,6 +1058,7 @@ let raw_add_transformation ~(keygen:'a keygen) ~(expanded:bool) g name =
              transf_key = key;
              transf_goals = [];
              transf_expanded = expanded;
+             transf_detached = None;
            }
   in
   PHstr.replace g.goal_transformations name tr;
@@ -1085,6 +1091,7 @@ let raw_add_theory ~(keygen:'a keygen) ~(expanded:bool)
               theory_verified = None;
               theory_expanded = expanded;
               theory_task = None;
+              theory_detached = None;
             }
   in
   mth
@@ -1152,8 +1159,6 @@ let string_attribute field r =
       field r.Xml.name;
     assert false
 
-let dummy_keygen ?parent:_ () = ()
-
 let load_result r =
   match r.Xml.name with
     | "result" ->
@@ -1215,11 +1220,9 @@ let load_ident elt =
       Ident.id_fresh ~label name in
   Ident.id_register preid
 
-type load_ctxt = {
+type 'key load_ctxt = {
   old_provers : (Whyconf.prover * int * int) Mint.t ;
-(*
-  shapes : ((string, Tc.shape) Hashtbl.t) option
-*)
+  keygen : 'key keygen;
 }
 
 let rec load_goal ctxt parent acc g =
@@ -1232,19 +1235,10 @@ let rec load_goal ctxt parent acc g =
         let shape =
           try Tc.shape_of_string (List.assoc "shape" g.Xml.attributes)
           with Not_found -> Tc.shape_of_string ""
-(*
-            match ctxt.shapes with
-              | None -> Tc.shape_of_string ""
-              | Some h ->
-                try Hashtbl.find h csum
-                with Not_found ->
-                  Format.eprintf "[Warning] shape not found for goal %s@." csum;
-                  Tc.shape_of_string ""
-*)
         in
         let expanded = bool_attribute "expanded" g false in
         let mg =
-          raw_add_no_task ~keygen:dummy_keygen ~expanded parent gname expl sum shape
+          raw_add_no_task ~keygen:ctxt.keygen ~expanded parent gname expl sum shape
         in
         List.iter (load_proof_or_transf ctxt mg) g.Xml.elements;
         mg.goal_verified <- goal_verified mg;
@@ -1284,7 +1278,7 @@ and load_proof_or_transf ctxt mg a =
           end;
         *)
           let (_ : 'a proof_attempt) =
-            add_external_proof ~keygen:dummy_keygen ~archived ~obsolete
+            add_external_proof ~keygen:ctxt.keygen ~archived ~obsolete
               ~timelimit ~memlimit ~edit mg p res
           in
           ()
@@ -1295,7 +1289,7 @@ and load_proof_or_transf ctxt mg a =
     | "transf" ->
         let trname = string_attribute "name" a in
         let expanded = bool_attribute "expanded" a false in
-        let mtr = raw_add_transformation ~keygen:dummy_keygen ~expanded mg trname in
+        let mtr = raw_add_transformation ~keygen:ctxt.keygen ~expanded mg trname in
         mtr.transf_goals <-
           List.rev
           (List.fold_left
@@ -1413,7 +1407,7 @@ and load_metas ctxt mg a =
   let metas_args =
     List.fold_left load_meta Mstr.empty metas_args in
   let expanded = bool_attribute "expanded" a false in
-  let metas = raw_add_metas ~keygen:dummy_keygen ~expanded mg metas_args idpos in
+  let metas = raw_add_metas ~keygen:ctxt.keygen ~expanded mg metas_args idpos in
   let goal = match goal with
     | [] -> raise (LoadError (a,"No subgoal for this metas"))
     | [goal] -> goal
@@ -1435,7 +1429,7 @@ let load_theory ctxt mf acc th =
         let expanded = bool_attribute "expanded" th false in
         let csum = string_attribute_opt "sum" th in
         let checksum = Opt.map Tc.checksum_of_string csum in
-        let mth = raw_add_theory ~keygen:dummy_keygen ~expanded ~checksum mf thname in
+        let mth = raw_add_theory ~keygen:ctxt.keygen ~expanded ~checksum mf thname in
         mth.theory_goals <-
           List.rev
           (List.fold_left
@@ -1447,17 +1441,18 @@ let load_theory ctxt mf acc th =
         eprintf "[Warning] Session.load_theory: unexpected element '%s'@." s;
         acc
 
-let load_file session old_provers f =
+let load_file ~keygen session old_provers f =
   match f.Xml.name with
     | "file" ->
+       let ctxt = { old_provers = old_provers ; keygen = keygen } in
         let fn = string_attribute "name" f in
         let fmt = load_option "format" f in
         let expanded = bool_attribute "expanded" f false in
-        let mf = raw_add_file ~keygen:dummy_keygen ~expanded session fn fmt in
+        let mf = raw_add_file ~keygen:ctxt.keygen ~expanded session fn fmt in
         mf.file_theories <-
           List.rev
           (List.fold_left
-             (load_theory { old_provers = old_provers } mf) [] f.Xml.elements);
+             (load_theory ctxt mf) [] f.Xml.elements);
         mf.file_verified <- file_verified mf;
         old_provers
     | "prover" ->
@@ -1483,14 +1478,7 @@ let load_file session old_provers f =
         eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
         old_provers
 
-(*
-let old_provers = ref Mstr.empty
-*)
-(* dead code
-let get_old_provers () = !old_provers
-*)
-
-let load_session session xml =
+let load_session ~keygen session xml =
   match xml.Xml.name with
     | "why3session" ->
       let shape_version = int_attribute_def "shape_version" xml 1 in
@@ -1498,7 +1486,7 @@ let load_session session xml =
       Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
       (** just to keep the old_provers somewhere *)
       let old_provers =
-        List.fold_left (load_file session) Mint.empty xml.Xml.elements
+        List.fold_left (load_file ~keygen session) Mint.empty xml.Xml.elements
       in
       Mint.iter
         (fun id (p,_,_) ->
@@ -1612,8 +1600,7 @@ with e ->
     (Printexc.to_string e);
   Xml.from_file xml_filename, false
 
-type notask = unit
-let read_session dir =
+let read_session ~keygen dir =
   if not (Sys.file_exists dir && Sys.is_directory dir) then
     raise (SessionFileError (Pp.sprintf "%s is not an existing directory" dir));
   let xml_filename = Filename.concat dir db_filename in
@@ -1625,7 +1612,7 @@ let read_session dir =
         Tc.reset_dict ();
         let xml,use_shapes = read_file_session_and_shapes dir xml_filename in
         try
-          load_session session xml.Xml.content;
+          load_session ~keygen session xml.Xml.content;
           use_shapes
         with Sys_error msg ->
           failwith ("Open session: sys error " ^ msg)
@@ -1640,6 +1627,7 @@ let read_session dir =
   in
   session, use_shapes
 
+let read_session_no_keys = read_session ~keygen:(fun ?parent:_ () -> ())
 
 (*******************************)
 (* Session modification        *)
@@ -2038,7 +2026,7 @@ module AssoGoals : sig
   val set_use_shapes : bool -> unit
   val associate :
     'a goal list -> 'b goal list ->
-    ('b goal * ('a goal * bool) option) list
+    ('b goal * ('a goal * bool) option) list * 'a goal list
 end = struct
 (** When Why3 will require 3.12 put all of that in a function using
     explicit type argument "(type t)" and remove all the Obj.magic *)
@@ -2071,16 +2059,18 @@ end = struct
 
   let associate
       (from_goals: 'ffrom goal list) (to_goals: 'tto goal list) :
-      ('tto goal * ('ffrom goal * bool) option) list =
+      ('tto goal * ('ffrom goal * bool) option) list * 'ffrom goal list =
     let from_goals : ffrom goal list =
       Obj.magic (from_goals : 'ffrom goal list) in
     let to_goals   : tto goal list =
       Obj.magic (to_goals : 'tto goal list) in
-    let associated : (tto goal * (ffrom goal * bool) option) list =
+    let associated :
+          (tto goal * (ffrom goal * bool) option) list * ffrom goal list =
       AssoGoals.associate
         ~use_shapes:!use_shapes from_goals to_goals
     in
-    (Obj.magic associated : ('tto goal * ('ffrom goal * bool) option) list)
+    (Obj.magic associated : 
+       ('tto goal * ('ffrom goal * bool) option) list * ('ffrom goal list))
 
 end
 
@@ -2335,7 +2325,7 @@ and merge_trans ~ctxt ~theories env to_goal _ from_transf =
         raise Exit
     in
     set_transf_expanded to_transf from_transf.transf_expanded;
-    let associated =
+    let associated,detached =
       Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
         env.session.session_shape_version;
       AssoGoals.associate
@@ -2346,7 +2336,9 @@ and merge_trans ~ctxt ~theories env to_goal _ from_transf =
         merge_any_goal ~ctxt ~theories env obsolete  from_goal to_goal
       | (_, None) ->
         found_missed_goals_in_theory := true)
-      associated
+      associated;
+    if detached <> [] then
+    to_transf.transf_detached <- Some { detached_goals = detached }
   with Exit -> ()
 
 (** convert the ident from the old task to the ident at the same
@@ -2668,7 +2660,7 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
         from_transf_name Exn_printer.exn_printer exn;
       raise Paste_error
   in
-  let associated =
+  let associated,detached =
     Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
       env.session.session_shape_version;
     AssoGoals.associate
@@ -2678,6 +2670,8 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
     add_goal_to_parent ~keygen env from_goal to_goal
   | (_, None) -> ()
   ) associated;
+  if detached <> [] then
+    to_transf.transf_detached <- Some { detached_goals = detached };
   to_transf
 
 let get_project_dir fname =

src/session/session.mli

@@ -127,8 +127,12 @@ and 'a transf = private
       mutable transf_goals : 'a goal list;
       (** Not mutated after the creation *)
       mutable transf_expanded : bool;
+      mutable transf_detached : 'a detached option;
     }
 
+and 'a detached = private
+    { detached_goals: 'a goal list; }
+
 and 'a theory = private
     { mutable theory_key : 'a;
       theory_name : Ident.ident;
@@ -139,6 +143,7 @@ and 'a theory = private
       mutable theory_verified : float option;
       mutable theory_expanded : bool;
       mutable theory_task : Theory.theory hide;
+      mutable theory_detached : 'a detached option;
     }
 
 and 'a file = private
@@ -180,14 +185,13 @@ val get_project_dir : string -> string
 
 (** {2 Read/Write} *)
 
-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} *)
+type 'key keygen = ?parent:'key -> unit -> 'key
+(** type of functions which can generate keys *)
 
 exception ShapesFileError of string
 exception SessionFileError of string
 
-val read_session : string -> notask session * bool
+val read_session : keygen:'key keygen -> string -> 'key session * bool
 (** Read a session stored on the disk. It returns a session without any
     task attached to goals.
 
@@ -201,6 +205,8 @@ val read_session : string -> notask session * bool
 
 *)
 
+val read_session_no_keys: string -> unit session * bool
+
 val save_session : Whyconf.config -> 'key session -> unit
 (** Save a session on disk *)
 
@@ -235,9 +241,6 @@ val unload_provers : 'a env_session -> unit
 
 (** {2 Update session} *)
 
-type 'key keygen = ?parent:'key -> unit -> 'key
-(** type of functions which can generate keys *)
-
 exception OutdatedSession
 
 type 'key update_context =
@@ -247,7 +250,7 @@ type 'key update_context =
     keygen : 'key keygen;
   }
 
-val update_session : ctxt:'key update_context -> 'a session ->
+val update_session : ctxt:'key update_context -> 'key session ->
   Env.env -> Whyconf.config -> 'key env_session * bool * bool
 (** reload the given session with the given environnement :
     - the files are reloaded

src/session/session_scheduler.mli

@@ -113,7 +113,7 @@ module Make(O: OBSERVER) : sig
     allow_obsolete:bool ->
     release:bool ->
     use_shapes:bool ->
-    'key session ->
+    O.key session ->
     Env.env -> Whyconf.config ->
     O.key env_session * bool * bool
   (**

src/session/termcode.ml

@@ -791,12 +791,23 @@ module Pairing(Old: S)(New: S) = struct
         end
       done
     end;
-    Array.to_list result
+    let detached =
+      List.fold_left
+        (fun acc x ->
+         if x.valid then
+           match x.elt with
+           | Old g -> g :: acc
+           | New _ -> acc
+         else acc)
+        [] allgoals
+    in
+    Debug.dprintf debug "[assoc] %d detached goals@." (List.length detached);
+    Array.to_list result, detached
 
-  let simple_associate (* ~obsolete *) oldgoals newgoals =
+  let simple_associate oldgoals newgoals =
     let rec aux acc o n =
       match o,n with
-        | _, [] -> acc
+        | old, [] -> acc,old
         | [], 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

src/session/termcode.mli

@@ -61,8 +61,8 @@ end
 
 module Pairing(Old: S)(New: S) : sig
   val associate:
-    use_shapes:bool ->
-    Old.t list -> New.t list -> (New.t * (Old.t * bool) option) list
+    use_shapes:bool -> Old.t list -> New.t list ->
+    (New.t * (Old.t * bool) option) list * Old.t list
     (** Associate new goals to (possibly) old goals
         Each new goal is mapped either to
         - [None]: no old goal associated
@@ -73,6 +73,10 @@ module Pairing(Old: S)(New: S) : sig
         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] *)
+        Note: in the output, goals appear in the same order as in [newgoals]
+
+        the second list returned is the list of non-associated old goals.
+
+     *)
 
 end

src/tools/why3replay.ml

@@ -401,7 +401,7 @@ let () =
     Debug.dprintf debug "Opening session...@?";
     O.verbose := Debug.test_flag debug;
     let env_session,found_obs,some_merge_miss =
-      let session, use_shapes = S.read_session project_dir in
+      let session, use_shapes = S.read_session ~keygen:O.create project_dir in
       M.update_session ~allow_obsolete:true ~release:false ~use_shapes
         session env config
     in

src/why3session/why3session_csv.ml

@@ -117,7 +117,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,_use_shapes = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session_no_keys project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with
@@ -168,7 +168,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,_use_shapes = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session_no_keys project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with

src/why3session/why3session_html.ml

@@ -66,12 +66,12 @@ open Session
 
 type context =
     (string ->
-     (formatter -> notask session -> unit) -> notask session
+     (formatter -> unit session -> unit) -> unit session
      -> unit, formatter, unit) format
 
 let run_file (context : context) print_session fname =
   let project_dir = Session.get_project_dir fname in
-  let session,_use_shapes = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session_no_keys project_dir in
   let output_dir =
     if !output_dir = "" then project_dir else !output_dir
   in

src/why3session/why3session_info.ml

@@ -203,7 +203,7 @@ type 'a goal_stat =
   | No of ('a transf * ('a goal * 'a goal_stat) list) list
   | Yes of (prover * float) list * ('a transf * ('a goal * 'a goal_stat) list) list
 
-let rec stats2_of_goal ~nb_proofs g : notask goal_stat =
+let rec stats2_of_goal ~nb_proofs g : 'a goal_stat =
   let proof_list =
     PHprover.fold
       (fun prover proof_attempt acc ->
@@ -235,7 +235,7 @@ let rec stats2_of_goal ~nb_proofs g : notask goal_stat =
     | _ -> assert false
       then Yes(proof_list,l) else No(l)
 
-and stats2_of_transf ~nb_proofs tr : (notask goal * notask goal_stat) list =
+and stats2_of_transf ~nb_proofs tr : ('a goal * 'a goal_stat) list =
   List.fold_left
     (fun acc g ->
       match stats2_of_goal ~nb_proofs g with
@@ -354,7 +354,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,_use_shapes = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session_no_keys 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

@@ -456,7 +456,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,_use_shapes = Session.read_session project_dir in
+  let session,_use_shapes = Session.read_session_no_keys project_dir in
   let dir = if !opt_output_dir = "" then project_dir else
       !opt_output_dir
   in

src/why3session/why3session_lib.ml

@@ -71,18 +71,17 @@ let read_env_spec () =
   let env = Env.create_env loadpath in
   env,config,read_simple_spec ()
 
-
 let read_update_session ~allow_obsolete env config fname =
-  let project_dir = Session.get_project_dir fname in
-  let session,use_shapes = Session.read_session project_dir in
+  let project_dir = S.get_project_dir fname in
+  let session,use_shapes = S.read_session_no_keys project_dir in
   let ctxt = {
     S.allow_obsolete_goals = allow_obsolete;
     S.release_tasks = false;
     S.use_shapes_for_pairing_sub_goals = use_shapes;
-    S.keygen = fun ?parent:_ _ -> ();
+    S.keygen = (fun ?parent:_ () -> ());
   }
   in
-  Session.update_session ~ctxt session env config
+  S.update_session ~ctxt session env config
 
 (** filter *)
 type filter_prover =
@@ -216,7 +215,7 @@ let iter_proof_attempt_by_filter iter filters f session =
   let f = three_value f filters.verified_goal
     (fun a -> Opt.inhabited a.S.proof_parent.S.goal_verified) in
   (** verified *)
-  let f = three_value f filters.verified 
+  let f = three_value f filters.verified
     (fun p -> Opt.inhabited (S.proof_verified p)) in
   (** status *)
   let f = if filters.status = [] then f else

tests/test_merge.mlw

 
 
-module M
-  
+theory T
+
   use import int.Int
 
-  lemma l1: 1 = 1
+  predicate p int
 
-  let f (x:int) : int 
-    ensures { result > 0 } 
-  =
-    (* assert { x > 0 }; *)
-    42
+  goal g: p 3 /\ p 4 /\ p 5
 
 end
\ No newline at end of file

tests/test_merge/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
- <prover
-  id="0"
-  name="Alt-Ergo"
-  version="0.95.2"/>
- <file
-  name="../test_merge.mlw"
-  verified="true"
-  expanded="true">
-  <theory
-   name="M"
-   locfile="../test_merge.mlw"
-   loclnum="3" loccnumb="7" loccnume="8"
-   verified="true"
-   expanded="true">
-   <goal
-    name="l1"
-    locfile="../test_merge.mlw"
-    loclnum="7" loccnumb="8" loccnume="10"
-    sum="41600830d468d02ad00fa968a56cacde"
-    proved="true"
-    expanded="true"
-    shape="ainfix =c1c1">
-    <proof
-     prover="0"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.01"/>
-    </proof>
-   </goal>
-   <goal
-    name="WP_parameter f"
-    locfile="../test_merge.mlw"
-    loclnum="9" loccnumb="6" loccnume="7"
-    expl="VC for f"
-    sum="98b7bd9a4c152591f929c11204735fb8"
-    proved="true"
-    expanded="true"
-    shape="ainfix &gt;c42c0">
-    <label
-     name="expl:VC for f"/>
-    <transf
-     name="split_goal_wp"
-     proved="true"
-     expanded="true">
-     <goal
-      name="WP_parameter f.1"
-      locfile="../test_merge.mlw"
-      loclnum="9" loccnumb="6" loccnume="7"
-      expl="1. postcondition"
-      sum="98b7bd9a4c152591f929c11204735fb8"
-      proved="true"
-      expanded="true"
-      shape="postconditionainfix &gt;c42c0">
-      <label
-       name="expl:VC for f"/>
-      <proof
-       prover="0"
-       timelimit="5"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="0.01"/>
-      </proof>
-     </goal>
-    </transf>
-   </goal>
-  </theory>
- </file>
+<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<file name="../test_merge.mlw" expanded="true">
+<theory name="T" sum="482715b3f8aff6f001dcbc75c5a14e89" expanded="true">
+ <goal name="g" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="g.1" expl="1." expanded="true">
+  <proof prover="2"><result status="unknown" time="0.01"/></proof>
+  </goal>
+  <goal name="g.2" expl="2." expanded="true">
+  <proof prover="0"><result status="unknown" time="0.00"/></proof>
+  </goal>
+  <goal name="g.3" expl="3." expanded="true">
+  <proof prover="1"><result status="unknown" time="0.00"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
 </why3session>