upgrade why3session to session_itp format, first step

Makefile.in

@@ -211,9 +211,9 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 	    mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
 	    mlw_main mlw_interp
 
-LIB_SESSION = compress xml termcode session session_itp \
-              session_tools strategy strategy_parser controller_itp \
-	      session_scheduler server_utils itp_communication \
+LIB_SESSION = compress xml termcode session_itp \
+              strategy strategy_parser controller_itp \
+	      server_utils itp_communication \
 	      itp_server json_util
 
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \

src/session/itp_server.ml

@@ -367,7 +367,6 @@ let () =
   type server_data =
     { config : Whyconf.config;
       task_driver : Driver.driver;
-      sd_provers : Whyconf.config_prover Whyconf.Mprover.t;
       cont : Controller_itp.controller;
     }
 
@@ -529,7 +528,6 @@ let get_locations t =
     server_data := Some
                      { config = config;
                        task_driver = task_driver;
-                       sd_provers = provers;
                        cont = c }
 
   (* -----------------------------------   ------------------------------------- *)

src/session/server_utils.ml

@@ -10,6 +10,34 @@ open Itp_communication
 exception NotADirectory of string
 exception BadFileName of string
 
+
+let default_session_filename = "why3session.xml"
+
+let get_project_dir fname =
+  if not (Sys.file_exists fname) then raise Not_found;
+  let d =
+    if Sys.is_directory fname then fname
+    else if Filename.basename fname = default_session_filename then begin
+(*
+      Debug.dprintf debug "Info: found db file '%s'@." fname;
+*)
+      Filename.dirname fname
+    end
+    else
+      begin
+(*
+        Debug.dprintf debug "Info: found regular file '%s'@." fname;
+ *)
+        try Filename.chop_extension fname
+        with Invalid_argument _ -> fname (* ^".w3s" *)
+      end
+  in
+(*
+  Debug.dprintf debug "Info: using '%s' as directory for the project@." d;
+ *)
+  d
+
+
 (******************************)
 (* Creation of the controller *)
 (******************************)

src/session/server_utils.mli

+
+
 exception NotADirectory of string
 exception BadFileName of string
 
+val get_project_dir : string -> string
+
 (** Controller initialization *)
 
 (* Init the given controller with the session in file/directory given *)

src/session/session_itp.ml

+
+
+
+
+
 open Stdlib
 
 module Hprover = Whyconf.Hprover

src/tools/why3replay.ml

@@ -137,7 +137,7 @@ module S = Session_itp
 
 let project_dir =
   try
-    Session.get_project_dir fname
+    Server_utils.get_project_dir fname
   with Not_found -> failwith "file does not exist"
 
 let goal_statistics cont (goals,n,m) g =

src/why3session/why3session_copy.ml

@@ -12,7 +12,7 @@
 open Why3
 open Why3session_lib
 open Whyconf
-open Session
+open Session_itp
 open Format
 
 (**

src/why3session/why3session_csv.ml

@@ -14,7 +14,7 @@ open Why3session_lib
 open Format
 
 module Hprover = Whyconf.Hprover
-module S = Session
+module S = Session_itp
 
 let orig_dir = Sys.getcwd ()
 
@@ -96,29 +96,29 @@ let spec =
 (** Normal *)
 
 let print_cell fmt pa =
-  match pa.Session.proof_state with
-  | Session.Done {Call_provers.pr_answer = Call_provers.Valid;
+  match pa.S.proof_state with
+  | S.Done {Call_provers.pr_answer = Call_provers.Valid;
                   pr_time = time} -> fprintf fmt "%f" time
   | _ -> fprintf fmt "%s" !opt_value_not_valid
 
 let rec print_line fmt provers a =
   begin match a with
-  | Session.Goal a ->
-    fprintf fmt "\"%s\"" a.Session.goal_name.Ident.id_string;
+  | S.Goal a ->
+    fprintf fmt "\"%s\"" a.S.goal_name.Ident.id_string;
     Whyconf.Sprover.iter (fun p ->
       try
-        let pa = Session.PHprover.find a.Session.goal_external_proofs p in
+        let pa = S.PHprover.find a.S.goal_external_proofs p in
         fprintf fmt ",%a" print_cell pa
       with Not_found ->
         fprintf fmt ",") provers;
     fprintf fmt "\n@?" (* no @\n since we use Pp.wnl *)
   | _ -> () end;
-  Session.iter (print_line fmt provers) a
+  S.iter (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 provers = Session.get_used_provers session in
+  let project_dir = S.get_project_dir fname in
+  let session,_use_shapes = S.read_session project_dir in
+  let provers = S.get_used_provers session in
   let provers =
     match filter_provers with
     | [] -> provers
@@ -130,7 +130,7 @@ let run_one_normal filter_provers fmt fname =
   fprintf fmt ",%a\n@?"
     (Pp.print_iter1 Whyconf.Sprover.iter Pp.comma (Pp.asd Whyconf.print_prover))
     provers;
-  Session.session_iter (print_line fmt provers) session
+  S.session_iter (print_line fmt provers) session
 
 
 let run_normal dir filter_provers =
@@ -157,19 +157,19 @@ let print_float_list =
   Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.semi Pp.float
 
 let grab_valid_time provers_time provers pa =
-  let prover = pa.Session.proof_prover in
+  let prover = pa.S.proof_prover in
   if Whyconf.Sprover.mem prover provers then
-    match pa.Session.proof_state with
-    | Session.Done {Call_provers.pr_answer = Call_provers.Valid;
+    match pa.S.proof_state with
+    | S.Done {Call_provers.pr_answer = Call_provers.Valid;
                     pr_time = time} ->
       let l = Whyconf.Hprover.find_def provers_time [] prover in
       Whyconf.Hprover.replace provers_time prover (time::l)
   | _ -> ()
 
 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 provers = Session.get_used_provers session in
+  let project_dir = S.get_project_dir fname in
+  let session,_use_shapes = S.read_session project_dir in
+  let provers = S.get_used_provers session in
   let provers =
     match filter_provers with
     | [] -> provers
@@ -178,7 +178,7 @@ let run_one_by_time provers_time filter_provers fname =
         (fun p ->
           List.exists
           (fun f -> Whyconf.filter_prover f p) filter_provers) provers in
-  Session.session_iter_proof_attempt
+  S.session_iter_proof_attempt
     (grab_valid_time provers_time provers) session
 
 

src/why3session/why3session_html.ml

@@ -14,7 +14,7 @@ open Why3
 open Why3session_lib
 
 module Hprover = Whyconf.Hprover
-module S = Session
+module S = Session_itp
 
 let output_dir = ref ""
 let opt_context = ref false
@@ -61,7 +61,7 @@ let spec =
   " use coqdoc to print Coq proofs") ::
   common_options
 
-open Session
+open Session_itp
 
 type context =
     (string ->
@@ -69,8 +69,8 @@ type context =
      -> 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 project_dir = S.get_project_dir fname in
+  let session,_use_shapes = S.read_session project_dir in
   let output_dir =
     if !output_dir = "" then project_dir else !output_dir
   in

src/why3session/why3session_info.ml

@@ -18,7 +18,7 @@ open Why3
 open Why3session_lib
 open Whyconf
 open Format
-open Session
+open Session_itp
 open Stdlib
 
 let opt_print_provers = ref false
@@ -352,9 +352,9 @@ let print_stats r0 r1 stats =
 
 
 let run_one stats r0 r1 fname =
-  let project_dir = Session.get_project_dir fname in
+  let project_dir = Server_utils.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 = S.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

@@ -14,7 +14,7 @@ open Why3session_lib
 open Format
 
 module Hprover = Whyconf.Hprover
-module S = Session
+module S = Session_itp
 
 let opt_style = ref 1
 let opt_output_dir = ref ""
@@ -123,7 +123,7 @@ let print_result_prov proofs prov fmt=
     let pr = S.PHprover.find proofs p in
     let s = pr.S.proof_state in
       match s with
-	| Session.Done res ->
+	| S.Done res ->
 	    begin
 	      match res.Call_provers.pr_answer with
 		| Call_provers.Valid ->
@@ -146,11 +146,11 @@ let print_result_prov proofs prov fmt=
                   fprintf fmt "& \\highfailure "
 
 	    end
-	| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
-	| Session.Interrupted -> fprintf fmt "& Not yet run"
-	| Session.Unedited -> fprintf fmt "& Not yet edited"
-	| Session.Scheduled | Session.Running
-	| Session.JustEdited -> assert false
+	| S.InternalFailure _ -> fprintf fmt "& Internal Failure"
+	| S.Interrupted -> fprintf fmt "& Not yet run"
+	| S.Unedited -> fprintf fmt "& Not yet edited"
+	| S.Scheduled | S.Running
+	| S.JustEdited -> assert false
   with Not_found -> fprintf fmt "& \\noresult") prov;
   fprintf fmt "\\\\ @."
 
@@ -460,8 +460,8 @@ let print_latex_statistics n table dir session =
 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 project_dir = S.get_project_dir fname in
+  let session,_use_shapes = S.read_session project_dir in
   let dir = if !opt_output_dir = "" then project_dir else
       !opt_output_dir
   in

src/why3session/why3session_lib.ml

@@ -11,7 +11,7 @@
 
 open Why3
 
-module S = Session
+module S = Session_itp
 module C = Whyconf
 
 let verbose = Debug.register_info_flag "verbose"
@@ -72,14 +72,26 @@ let read_env_spec () =
   env,config,read_simple_spec ()
 
 let read_update_session ~allow_obsolete env config fname =
-  let project_dir = S.get_project_dir fname in
-  let session,use_shapes = S.read_session project_dir in
+  let project_dir = Server_utils.get_project_dir fname in
+  let session,use_shapes = S.load_session project_dir in
+(*
   let ctxt = S.mk_update_context
     ~allow_obsolete_goals:allow_obsolete
     ~use_shapes_for_pairing_sub_goals:use_shapes
     (fun ?parent:_ () -> ())
   in
   S.update_session ~ctxt session env config
+ *)
+  let found_obs, some_merge_miss =
+    try
+      Controller_itp.reload_files cont ~use_shapes;
+      true, false (* TODO *)
+    with
+    | e ->
+       Format.eprintf "%a@." Exn_printer.exn_printer e;
+       exit 1
+  in
+  ()
 
 (** filter *)
 type filter_prover =

src/why3session/why3session_lib.mli

@@ -47,7 +47,7 @@ val read_env_spec : unit -> Env.env * Whyconf.config * bool
 val read_update_session :
   allow_obsolete:bool -> Env.env ->
   Whyconf.config -> string ->
-  unit Session.env_session * bool * bool
+  Controller_itp.controller * bool * bool
 
 (** {2 Spec for filtering } *)
 type filter_prover
@@ -64,10 +64,11 @@ val read_filter_spec : Whyconf.config -> filters * bool
 
 val theory_iter_proof_attempt_by_filter :
   filters ->
-  ('key Session.proof_attempt -> unit) -> 'key Session.theory -> unit
+  (Session_itp.proof_attempt_node -> unit) -> Session_itp.theory -> unit
+
 val session_iter_proof_attempt_by_filter :
   filters ->
-  ('key Session.proof_attempt -> unit) -> 'key Session.session -> unit
+  (Session_itp.proof_attempt_node -> unit) -> Session_itp.session -> unit
 
 
 (* quite ad-hoc *)

src/why3session/why3session_output.ml

@@ -11,7 +11,7 @@
 
 open Why3
 open Why3session_lib
-open Session
+open Session_itp
 open Format
 
 (**

src/why3session/why3session_rm.ml

@@ -11,7 +11,7 @@
 
 open Why3
 open Why3session_lib
-open Session
+open Session_itp
 open Format
 
 type filter_prover =

src/why3session/why3session_run.ml

@@ -9,10 +9,11 @@
 (*                                                                  *)
 (********************************************************************)
 
+(*
 open Why3
 open Why3session_lib
 open Whyconf
-open Session
+open Session_itp
 open Format
 open Debug
 module Todo = Session_scheduler.Todo
@@ -363,3 +364,4 @@ let cmd =
     cmd_name     = "run";
     cmd_run      = run;
   }
+ *)