factorize the interpretation of files on command line, and the creation of controllers

no empty dir will be created with a name having an extension, eg

  why3 ide file.mlw

will now signal an error if file.mlw does not exist

side effect: Open_Session request is disabled, will see if we want it later

src/ide/why3ide.ml

@@ -182,7 +182,16 @@ let env, gconfig = try
     exit 1
 
 (* Initialization of config, provers, task_driver and controller in the server *)
-let () = Server.init_server gconfig.config env
+let () =
+  let dir =
+    try
+      Server_utils.get_session_dir ~allow_mkdir:true files
+    with Invalid_argument s ->
+      Format.eprintf "Error: %s@." s;
+      Whyconf.Args.exit_with_usage spec usage_str
+  in
+  Server.init_server gconfig.config env dir;
+  Queue.iter (fun f -> send_request (Add_file_req f)) files
 
 let () =
   Debug.dprintf debug "[GUI] Init the GTK interface...@?";
@@ -1576,9 +1585,6 @@ let (_ : GMenu.image_menu_item) =
 
 let () =
   S.timeout ~ms:100 (fun () -> List.iter treat_notification (get_notified ()); true);
-  let f = Queue.pop files in
-  send_request (Open_session_req f);
-  Queue.iter (fun f -> send_request (Add_file_req f)) files;
   (* temporary *)
   vpan222#set_position 500;
   goals_view#expand_all ();

src/ide/why3web.ml

@@ -139,10 +139,13 @@ let () =
     let config, _base_config, env =
       Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
     in
-    if Queue.is_empty files then
-      Whyconf.Args.exit_with_usage spec usage_str;
-    let f = Queue.pop files in
-    P.push_request (Open_session_req f);
+    let dir =
+      try
+        Server_utils.get_session_dir ~allow_mkdir:true files
+      with Invalid_argument s ->
+        Format.eprintf "Error: %s@." s;
+        Whyconf.Args.exit_with_usage spec usage_str
+    in
+    S.init_server config env dir;
     Queue.iter (fun f -> P.push_request (Add_file_req f)) files;
-    S.init_server config env;
     Wserver.main_loop None 6789 handler stdin_handler

src/session/controller_itp.ml

@@ -78,16 +78,18 @@ type controller =
       (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
   }
 
+(*
 let clear_proof_state c =
   Stdlib.Hstr.clear c.proof_state.file_state;
   Hid.clear c.proof_state.th_state;
   Htn.clear c.proof_state.tn_state;
   Hpn.clear c.proof_state.pn_state
+*)
 
-let create_controller config env =
+let create_controller config env ses =
   let c =
     {
-      controller_session = Session_itp.dummy_session;
+      controller_session = ses;
       proof_state = init_proof_state ();
       controller_config = config;
       controller_env = env;
@@ -108,10 +110,7 @@ let create_controller config env =
     provers;
   c
 
-
-let init_controller s c =
-  clear_proof_state c;
-  c.controller_session <- s
+let set_session cont ses = cont.controller_session <- ses
 
 let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
 let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
@@ -390,8 +389,7 @@ let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
   in
   merge_file_section
     c.controller_session ~use_shapes ~old_ses ~old_theories
-    ~env:c.controller_env file_name new_theories format;
-  reload_session_proof_state c
+    ~env:c.controller_env file_name new_theories format
 
 let reload_files (c : controller) ~use_shapes =
   let old_ses = c.controller_session in
@@ -400,7 +398,8 @@ let reload_files (c : controller) ~use_shapes =
   try
     Stdlib.Hstr.iter
       (fun f -> merge_file old_ses c ~use_shapes f)
-      (get_files old_ses)
+      (get_files old_ses);
+    reload_session_proof_state c
   with e ->
     c.controller_session <- old_ses;
     raise e

src/session/controller_itp.mli

@@ -73,12 +73,12 @@ type controller = private
     controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
   }
 
-val create_controller: Whyconf.config -> Env.env -> controller
-(** creates a controller with an empty session.
+val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
+(** creates a controller for the given session.
     The config and env is used to load the drivers for the provers. *)
 
-val init_controller: Session_itp.session -> controller -> unit
-(** adds a session to a controller *)
+(* TEMPORARY *)
+val set_session : controller -> Session_itp.session -> unit
 
 (** Used to find if a proof/trans node or theory is proved or not *)
 val tn_proved: controller -> Session_itp.transID -> bool

src/session/itp_communication.ml

@@ -92,7 +92,9 @@ type ide_request =
   | Prove_req               of node_ID * prover * Call_provers.resource_limit
   | Transform_req           of node_ID * transformation * string list
   | Strategy_req            of node_ID * strategy
+(*
   | Open_session_req        of string
+ *)
   | Add_file_req            of string
   | Set_max_tasks_req       of int
   | Get_file_contents       of string
@@ -118,7 +120,8 @@ let modify_session (r: ide_request) =
   | Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
   | Replay_req | Clean_req | Mark_obsolete_req _ -> true
 
-  | Open_session_req _ | Set_max_tasks_req _ | Get_file_contents _
+  (*| Open_session_req _ *)
+  | Set_max_tasks_req _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
   | Get_Session_Tree_req | Save_req | Reload_req | Exit_req
   | Interrupt_req -> false

src/session/itp_communication.mli

@@ -98,7 +98,9 @@ type ide_request =
   | Prove_req               of node_ID * prover * Call_provers.resource_limit
   | Transform_req           of node_ID * transformation * string list
   | Strategy_req            of node_ID * strategy
+(*
   | Open_session_req        of string
+ *)
   | Add_file_req            of string
   | Set_max_tasks_req       of int
   | Get_file_contents       of string

src/session/itp_server.ml

@@ -247,7 +247,9 @@ let print_request fmt r =
   | Prove_req (_nid, prover, _rl)   -> fprintf fmt "prove with %s" prover
   | Transform_req (_nid, tr, _args) -> fprintf fmt "transformation :%s" tr
   | Strategy_req (_nid, st)         -> fprintf fmt "strategy %s" st
+(*
   | Open_session_req f              -> fprintf fmt "open session file %s" f
+*)
   | Add_file_req f                  -> fprintf fmt "open file %s" f
   | Set_max_tasks_req i             -> fprintf fmt "set max tasks %i" i
   | Get_file_contents _f            -> fprintf fmt "get file contents"
@@ -323,7 +325,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
 
   module C = Controller_itp.Make(S)
 
-  let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
+let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
 
 
 (****************)
@@ -509,13 +511,6 @@ let get_locations t =
   let get_prover_list (config: Whyconf.config) =
     Mstr.fold (fun x _ acc -> x :: acc) (Whyconf.get_prover_shortcuts config) []
 
-  let init_server config env =
-    let c = create_controller config env in
-    let task_driver = task_driver config env in
-    server_data := Some
-                     { task_driver = task_driver;
-                       cont = c }
-
   (* -----------------------------------   ------------------------------------- *)
 
   let get_node_type (node: any) =
@@ -835,13 +830,18 @@ let get_locations t =
       P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
 
 
-  (* ------------ init controller ------------ *)
+  (* ------------ init server ------------ *)
 
-  (* Init cont on file or directory. It is called only when an
-     Open_session_req is requested *)
-  let init_cont f =
+  let init_server config env f =
+    Debug.dprintf debug "[ITP server] loading session %s@." f;
+    let ses,use_shapes = Session_itp.load_session f in
+    Debug.dprintf debug "[ITP server] creating controller@.";
+    let c = create_controller config env ses in
+    let task_driver = task_driver config env in
+    server_data := Some
+                     { task_driver = task_driver;
+                       cont = c };
     let d = get_server_data () in
-    let config = d.cont.controller_config in
     let prover_list = get_prover_list config in
     let transformation_list = List.map fst (list_transforms ()) in
     let strategies_list =
@@ -857,20 +857,15 @@ let get_locations t =
           Hstr.fold (fun c _ acc -> c :: acc) commands_table []
       }
     in
-    match cont_from_session ~notify:P.notify d.cont f with
-    | Some false ->
-      begin
-        add_file_to_session d.cont f;
-        P.notify (Initialized infos);
-        true
-      end
-    | Some true ->
-        P.notify (Initialized infos);
-        true
-    | None ->
-        (* Even if it fails we want to load source files *)
-        load_files_session ();
-        false
+    Debug.dprintf debug "[ITP server] sending initialization infos@.";
+    P.notify (Initialized infos);
+    Debug.dprintf debug "[ITP server] reloading source files@.";
+    let b = reload_files d.cont ~use_shapes in
+    if b then
+      init_and_send_the_tree ()
+    else
+      load_files_session ()
+
 
   (* ----------------- Schedule proof attempt -------------------- *)
 
@@ -1141,12 +1136,14 @@ let get_locations t =
       let f = Sysutil.relativize_filename
           (Session_itp.get_dir d.cont.controller_session) f in
       read_and_send f
+(*
     | Open_session_req file_or_dir_name ->
         let b = init_cont file_or_dir_name in
         if b then
           reload_session ()
         else
           () (* Eventually print debug here *)
+*)
     | Set_max_tasks_req i     -> C.set_max_tasks i
     | Exit_req                -> exit 0
      )

src/session/itp_server.mli

@@ -15,12 +15,7 @@ end
 
 module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
 
-(*
-  val get_configs: unit -> Whyconf.config * Whyconf.config
- *)
-  (* Initialize server_data *)
-  val init_server: Whyconf.config -> Env.env -> unit
-
-  (* Nothing ! *)
+  (* Initialize server with the given config, env and filename for the session *)
+  val init_server: Whyconf.config -> Env.env -> string -> unit
 
 end

src/session/json_util.ml

@@ -121,7 +121,9 @@ let convert_request_constructor (r: ide_request) =
   | Prove_req _               -> String "Prove_req"
   | Transform_req _           -> String "Transform_req"
   | Strategy_req _            -> String "Strategy_req"
+(*
   | Open_session_req _        -> String "Open_session_req"
+*)
   | Add_file_req _            -> String "Add_file_req"
   | Save_file_req _           -> String "Save_file_req"
   | Set_max_tasks_req _       -> String "Set_max_tasks_req"
@@ -162,9 +164,11 @@ let print_request_to_json (r: ide_request): Json_base.json =
       convert_record ["ide_request", cc r;
            "node_ID", Int nid;
            "strategy", String str]
+(*
   | Open_session_req f ->
       convert_record ["ide_request", cc r;
            "file", String f]
+*)
   | Add_file_req f ->
       convert_record ["ide_request", cc r;
            "file", String f]
@@ -434,10 +438,11 @@ let parse_request (constr: string) j =
     let str = get_string (get_field j "strategy") in
     Strategy_req (nid, str)
 
+(*
   | "Open_session_req" ->
     let f = get_string (get_field j "file") in
     Open_session_req f
-
+*)
   | "Add_file_req" ->
     let f = get_string (get_field j "file") in
     Add_file_req f

src/session/server_utils.ml

@@ -4,11 +4,45 @@
 (* TODO: all occurences of Format.eprintf in this file should be
    replaced by proper server notifications *)
 
-open Session_itp
-open Itp_communication
+let has_extension f =
+  try
+    let _ = Filename.chop_extension f in true
+  with Invalid_argument _ -> false
+
+let get_session_dir ~allow_mkdir files =
+  if Queue.is_empty files then invalid_arg "no files given";
+  let first = Queue.pop files in
+  (* The remaining files in [files] are going to be open *)
+  let dir =
+    if Sys.file_exists first then
+      if Sys.is_directory first then
+        (* first is a directory *)
+        first
+      else
+        if Queue.is_empty files then
+          (* first was the only file *)
+          let d =
+            try Filename.chop_extension first
+            with Invalid_argument _ ->
+              invalid_arg ("'" ^ first ^ "' has no extension and is not a directory")
+          in
+          Queue.push first files; (* we need to open [first] *)
+          d
+        else
+          invalid_arg ("'" ^ first ^ "' is not a directory")
+    else
+      (* first does not exists *)
+      if has_extension first then
+        invalid_arg ("file not found: " ^ first)
+      else first
+  in
+  if not (Sys.file_exists dir) then
+    begin
+      if allow_mkdir then Unix.mkdir dir 0o777 else
+        invalid_arg ("session directory '" ^ dir ^ "' not found")
+    end;
+  dir
 
-exception NotADirectory of string
-exception BadFileName of string
 
 (******************************)
 (* Creation of the controller *)
@@ -17,6 +51,7 @@ exception BadFileName of string
 (* [cont_from_session]: returns an option to a boolean which returns None in
    case of failure, true if nothing is left to do and false if sessions was
    loaded but [f] should still be added to the session as a file. *)
+(*
 let cont_from_session ~notify cont f : bool option =
   (* If a file is given, find the corresponding directory *)
   let dir = try (Filename.chop_extension f) with
@@ -41,8 +76,8 @@ let cont_from_session ~notify cont f : bool option =
   (* we load the session *)
   let ses,use_shapes = load_session dir in
   Format.eprintf "[session server info] using shapes: %b@." use_shapes;
-  (* create the controller *)
-  Controller_itp.init_controller ses cont;
+  (* temporary, this should not be donne like this ! *)
+  Controller_itp.set_session cont ses;
   (* update the session *)
   try (Controller_itp.reload_files cont ~use_shapes;
     (* Check if the initial file given was a file or not. If it was, we return
@@ -57,7 +92,7 @@ let cont_from_session ~notify cont f : bool option =
       notify (Message (Parse_Or_Type_Error s));
       None
     end
-
+*)
 
 
 

src/session/server_utils.mli

-exception NotADirectory of string
+
+(*exception NotADirectory of string
 exception BadFileName of string
+ *)
+
+val get_session_dir : allow_mkdir:bool -> string Queue.t -> string
+(** [get_session_dir q] analyses the queue of filenames [q] and
+    returns the session directory from it.
+
+    That directory is created if it does not exists and [allow_mkdir]
+    is true.
+
+    raises [Invalid_arg s] with some appropriate explnation [s] if no
+    valid directory can be extracted.
+
+    The first element of queue [q] is removed if it is not a file to
+    load later in the session.
 
-(** Controller initialization *)
+ *)
 
-(* Init the given controller with the session in file/directory given *)
-val cont_from_session:
-    notify:(Itp_communication.notification -> unit) ->
-      Controller_itp.controller -> string -> bool option
 
 (** Simple queries *)
 

src/tools/why3replay.ml

@@ -348,9 +348,8 @@ let run_as_bench env_session =
 let () =
   try
     Debug.dprintf debug "Opening session...@?";
-    let cont = Controller_itp.create_controller config env in
     let ses,use_shapes = S.load_session project_dir in
-    Controller_itp.init_controller ses cont;
+    let cont = Controller_itp.create_controller config env ses in
     (* update the session *)
     let found_obs, some_merge_miss =
       try

src/tools/why3shell.ml

@@ -87,8 +87,6 @@ let config, base_config, env =
 
 module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
 
-(* Initialize the server *)
-let () = Server.init_server config env
 
 (*************************)
 (* Notification Handling *)
@@ -356,8 +354,15 @@ let () =
   printf "Welcome to Why3 shell. Type 'help' for help.@.";
   let chout = open_out "why3shell.out" in
   let fmt = formatter_of_out_channel chout in
-  let f = Queue.pop files in send_request (Open_session_req f);
-  (*Queue.iter (fun f -> send_request (Add_file_req f)) files;*)
+  let dir =
+    try
+      Server_utils.get_session_dir ~allow_mkdir:true files
+    with Invalid_argument s ->
+      Format.eprintf "Error: %s@." s;
+      Whyconf.Args.exit_with_usage spec usage_str
+  in
+  Server.init_server config env dir;
+  Queue.iter (fun f -> send_request (Add_file_req f)) files;
   Unix_scheduler.timeout ~ms:100
     (fun () -> List.iter
         (fun n -> treat_notification fmt n) (get_notified ()); true);