Commit 7b17e4bf authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Continued changes on server_data.

parent f04a5a8c
...@@ -907,25 +907,6 @@ module Args = struct ...@@ -907,25 +907,6 @@ module Args = struct
let lp = List.rev_append !opt_loadpath (loadpath main) in let lp = List.rev_append !opt_loadpath (loadpath main) in
config, base_config, Env.create_env lp config, base_config, Env.create_env lp
let parse ?(extra_help=Format.pp_print_newline) options default usage =
let options = align_options options in
Arg.parse options default usage;
if !opt_help then begin
Format.printf "@[%s%a@]" (Arg.usage_string options usage) extra_help ();
exit 0
end;
Debug.Args.set_flags_selected ();
if Debug.Args.option_list () then exit 0
let init () =
let base_config = read_config !opt_config in
let config = List.fold_left merge_config base_config !opt_extra in
let main = get_main config in
load_plugins main;
let lp = List.rev_append !opt_loadpath (loadpath main) in
Debug.Args.set_flags_selected ();
config, base_config, Env.create_env lp
let exit_with_usage options usage = let exit_with_usage options usage =
Arg.usage (align_options options) usage; Arg.usage (align_options options) usage;
exit 1 exit 1
......
...@@ -258,13 +258,6 @@ module Args : sig ...@@ -258,13 +258,6 @@ module Args : sig
(string -> unit) -> string -> (string -> unit) -> string ->
config * config * Env.env config * config * Env.env
val init : unit -> config * config * Env.env
val parse :
?extra_help : (Format.formatter -> unit -> unit) ->
(string * Arg.spec * string) list ->
(string -> unit) -> string -> unit
val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a
end end
...@@ -77,6 +77,8 @@ module S = struct ...@@ -77,6 +77,8 @@ module S = struct
() ()
end end
module Server = Itp_server.Make (S) (Protocol_why3ide)
(************************) (************************)
(* parsing command line *) (* parsing command line *)
(************************) (************************)
...@@ -101,22 +103,20 @@ let usage_str = sprintf ...@@ -101,22 +103,20 @@ let usage_str = sprintf
"Usage: %s [options] [<file.why>|<project directory>]..." "Usage: %s [options] [<file.why>|<project directory>]..."
(Filename.basename Sys.argv.(0)) (Filename.basename Sys.argv.(0))
let gconfig = try let env, gconfig = try
= Server.get_configs () in let config, base_config, env =
let config,base_config, env = Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str;
if Queue.is_empty files then if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str; Whyconf.Args.exit_with_usage spec usage_str;
Gconfig.load_config config base_config; Gconfig.load_config config base_config;
Gconfig.config () env, Gconfig.config ()
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
exit 1 exit 1
module Server = Itp_server.Make (S) (Protocol_why3ide) (* Initialization of config, provers, task_driver and controller in the server *)
let () = Server.init_server gconfig.config env
let () = Server.init_controller config base_config env
let () = let () =
Debug.dprintf debug "[GUI] Init the GTK interface...@?"; Debug.dprintf debug "[GUI] Init the GTK interface...@?";
......
...@@ -131,8 +131,11 @@ let usage_str = sprintf ...@@ -131,8 +131,11 @@ let usage_str = sprintf
let () = let () =
Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str; let config, base_config, env =
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
in
if Queue.is_empty files then if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str; Whyconf.Args.exit_with_usage spec usage_str;
Queue.iter (fun f -> P.push_request (Itp_server.Open_session_req f)) files; Queue.iter (fun f -> P.push_request (Itp_server.Open_session_req f)) files;
S.init_server config env;
Wserver.main_loop None 6789 handler stdin_handler Wserver.main_loop None 6789 handler stdin_handler
...@@ -440,7 +440,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -440,7 +440,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let server_data = ref None let server_data = ref None
let d () = let get_server_data () =
match !server_data with match !server_data with
| None -> | None ->
Format.eprintf "[ITP server] not yet initialized@."; Format.eprintf "[ITP server] not yet initialized@.";
...@@ -490,7 +490,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -490,7 +490,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* Init cont on file or directory. It is called only when an (* Init cont on file or directory. It is called only when an
Open_session_req is requested *) Open_session_req is requested *)
let init_cont f = let init_cont f =
let d = d () in let d = get_server_data () in
let prover_list = get_prover_list d.config in let prover_list = get_prover_list d.config in
let transformation_list = List.map fst (list_transforms ()) in let transformation_list = List.map fst (list_transforms ()) in
let strategies_list = let strategies_list =
...@@ -543,7 +543,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -543,7 +543,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| APa _ -> NProofAttempt | APa _ -> NProofAttempt
let get_node_name (node: any) = let get_node_name (node: any) =
let d = d () in let d = get_server_data () in
match node with match node with
| AFile file -> | AFile file ->
file.file_name file.file_name
...@@ -631,7 +631,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -631,7 +631,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let get_prover p = let get_prover p =
let d = d () in let d = get_server_data () in
match return_prover p d.config with match return_prover p d.config with
| None -> raise (Bad_prover_name p) | None -> raise (Bad_prover_name p)
| Some c -> c | Some c -> c
...@@ -665,14 +665,15 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -665,14 +665,15 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
node_ID -> any -> unit *) node_ID -> any -> unit *)
let iter_subtree_proof_attempt_from_goal let iter_subtree_proof_attempt_from_goal
(f: parent:node_ID -> any -> unit) parent id = (f: parent:node_ID -> any -> unit) parent id =
let d = d () in let d = get_server_data () in
Whyconf.Hprover.iter Whyconf.Hprover.iter
(fun _pa panid -> f ~parent (APa panid)) (fun _pa panid -> f ~parent (APa panid))
(get_proof_attempt_ids d.cont.controller_session id) (get_proof_attempt_ids d.cont.controller_session id)
let rec iter_subtree_from_goal let rec iter_subtree_from_goal
(f: parent:node_ID -> any -> unit) parent id = (f: parent:node_ID -> any -> unit) parent id =
let ses = cont.controller_session in let d = get_server_data () in
let ses = d.cont.controller_session in
f ~parent (APn id); f ~parent (APn id);
let nid = node_ID_from_pn id in let nid = node_ID_from_pn id in
List.iter List.iter
...@@ -682,7 +683,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -682,7 +683,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
and iter_subtree_from_trans and iter_subtree_from_trans
(f: parent:node_ID -> any -> unit) parent trans_id = (f: parent:node_ID -> any -> unit) parent trans_id =
let ses = cont.controller_session in let d = get_server_data () in
let ses = d.cont.controller_session in
f ~parent (ATn trans_id); f ~parent (ATn trans_id);
let nid = node_ID_from_tn trans_id in let nid = node_ID_from_tn trans_id in
List.iter List.iter
...@@ -704,7 +706,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -704,7 +706,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
file.file_theories file.file_theories
let iter_the_files (f: parent:node_ID -> any -> unit) parent : unit = let iter_the_files (f: parent:node_ID -> any -> unit) parent : unit =
let ses = cont.controller_session in let d = get_server_data () in
let ses = d.cont.controller_session in
let files = get_files ses in let files = get_files ses in
Stdlib.Hstr.iter Stdlib.Hstr.iter
(fun _ file -> (fun _ file ->
...@@ -742,12 +745,13 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -742,12 +745,13 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* -- send the task -- *) (* -- send the task -- *)
let send_task nid = let send_task nid =
let d = get_server_data () in
match any_from_node_ID nid with match any_from_node_ID nid with
| APn id -> | APn id ->
let task = get_task cont.controller_session id in let task = get_task d.cont.controller_session id in
let tables = get_tables cont.controller_session id in let tables = get_tables d.cont.controller_session id in
let s = Pp.string_of let s = Pp.string_of
(fun fmt -> Driver.print_task ~cntexample:false ?name_table:tables task_driver fmt) (fun fmt -> Driver.print_task ~cntexample:false ?name_table:tables d.task_driver fmt)
task in task in
P.notify (Task (nid,s)) P.notify (Task (nid,s))
| _ -> | _ ->
...@@ -810,22 +814,23 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -810,22 +814,23 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
with Not_found -> () with Not_found -> ()
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit = let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
let d = get_server_data () in
let prover = p.Whyconf.prover in let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof cont in let callback = callback_update_tree_proof d.cont in
let goals = let goals =
match any_from_node_ID nid with match any_from_node_ID nid with
| APn pnid -> [pnid] | APn pnid -> [pnid]
| APa panid -> | APa panid ->
let ses = cont.controller_session in let ses = d.cont.controller_session in
[get_proof_attempt_parent ses panid] [get_proof_attempt_parent ses panid]
| ATn tn -> | ATn tn ->
List.rev (unproven_goals_below_tn cont [] tn) List.rev (unproven_goals_below_tn d.cont [] tn)
| AFile file -> | AFile file ->
List.rev (unproven_goals_below_file cont file) List.rev (unproven_goals_below_file d.cont file)
| ATh th -> | ATh th ->
List.rev (unproven_goals_below_th cont [] th) List.rev (unproven_goals_below_th d.cont [] th)
in in
List.iter (fun id -> C.schedule_proof_attempt cont id prover List.iter (fun id -> C.schedule_proof_attempt d.cont id prover
~limit ~callback ~notification:notify_change_proved) ~limit ~callback ~notification:notify_change_proved)
goals goals
...@@ -833,26 +838,28 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -833,26 +838,28 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* Callback of a transformation *) (* Callback of a transformation *)
let callback_update_tree_transform status = let callback_update_tree_transform status =
let d = get_server_data () in
match status with match status with
| TSdone trans_id -> | TSdone trans_id ->
let ses = cont.controller_session in let ses = d.cont.controller_session in
let id = get_trans_parent ses trans_id in let id = get_trans_parent ses trans_id in
let nid = node_ID_from_pn id in let nid = node_ID_from_pn id in
init_and_send_subtree_from_trans nid trans_id init_and_send_subtree_from_trans nid trans_id
| TSfailed (id, e) -> | TSfailed (id, e) ->
let msg = let msg =
Pp.sprintf "%a" (get_exception_message cont.controller_session id) e Pp.sprintf "%a" (get_exception_message d.cont.controller_session id) e
in in
P.notify (Message (Strat_error(node_ID_from_pn id, msg))) P.notify (Message (Strat_error(node_ID_from_pn id, msg)))
| _ -> () | _ -> ()
let rec apply_transform nid t args = let rec apply_transform nid t args =
let d = get_server_data () in
match any_from_node_ID nid with match any_from_node_ID nid with
| APn id -> | APn id ->
let callback = callback_update_tree_transform in let callback = callback_update_tree_transform in
C.schedule_transformation cont id t args ~callback ~notification:notify_change_proved C.schedule_transformation d.cont id t args ~callback ~notification:notify_change_proved
| APa panid -> | APa panid ->
let parent_id = get_proof_attempt_parent cont.controller_session panid in let parent_id = get_proof_attempt_parent d.cont.controller_session panid in
let parent = node_ID_from_pn parent_id in let parent = node_ID_from_pn parent_id in
apply_transform parent t args apply_transform parent t args
| ATn _ | AFile _ | ATh _ -> | ATn _ | AFile _ | ATh _ ->
...@@ -862,9 +869,10 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -862,9 +869,10 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* ----------------- run strategy -------------------- *) (* ----------------- run strategy -------------------- *)
let run_strategy_on_task nid s = let run_strategy_on_task nid s =
let d = get_server_data () in
match any_from_node_ID nid with match any_from_node_ID nid with
| APn id -> | APn id ->
let l = strategies cont.controller_env config loaded_strategies in let l = strategies d.cont.controller_env d.config loaded_strategies in
let st = List.filter (fun (_,c,_,_) -> c=s) l in let st = List.filter (fun (_,c,_,_) -> c=s) l in
begin begin
match st with match st with
...@@ -873,16 +881,17 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -873,16 +881,17 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let callback sts = let callback sts =
Format.printf "Strategy status: %a@." print_strategy_status sts Format.printf "Strategy status: %a@." print_strategy_status sts
in in
let callback_pa = callback_update_tree_proof cont in let callback_pa = callback_update_tree_proof d.cont in
let callback_tr st = callback_update_tree_transform st in let callback_tr st = callback_update_tree_transform st in
C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback ~notification:notify_change_proved C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:notify_change_proved
| _ -> Format.printf "Strategy '%s' not found@." s | _ -> Format.printf "Strategy '%s' not found@." s
end end
| _ -> () | _ -> ()
(* ----------------- Save session --------------------- *) (* ----------------- Save session --------------------- *)
let save_session () = let save_session () =
Session_itp.save_session cont.controller_session; let d = get_server_data () in
Session_itp.save_session d.cont.controller_session;
P.notify Saved P.notify Saved
(* ----------------- Reload session ------------------- *) (* ----------------- Reload session ------------------- *)
...@@ -896,15 +905,17 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -896,15 +905,17 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
Hstr.clear file_to_node_ID Hstr.clear file_to_node_ID
let reload_session () : unit = let reload_session () : unit =
let d = get_server_data () in
clear_tables (); clear_tables ();
reload_files cont ~use_shapes:true; reload_files d.cont ~use_shapes:true;
init_and_send_the_tree () init_and_send_the_tree ()
let replay_session () : unit = let replay_session () : unit =
let d = get_server_data () in
let callback = fun lr -> let callback = fun lr ->
P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in
(* TODO make replay print *) (* TODO make replay print *)
C.replay ~use_steps:false cont ~callback:callback ~remove_obsolete:false C.replay ~use_steps:false d.cont ~callback:callback ~remove_obsolete:false
(* ----------------- treat_request -------------------- *) (* ----------------- treat_request -------------------- *)
...@@ -917,6 +928,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -917,6 +928,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
Not_found -> None Not_found -> None
let rec treat_request r = let rec treat_request r =
let d = get_server_data () in
try ( try (
match r with match r with
| Prove_req (nid,p,limit) -> | Prove_req (nid,p,limit) ->
...@@ -937,7 +949,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -937,7 +949,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| Command_req (nid, cmd) -> | Command_req (nid, cmd) ->
begin begin
let snid = get_proof_node_id nid in let snid = get_proof_node_id nid in
match (interp commands commands_table config cont snid cmd) with match (interp commands commands_table d.config d.cont snid cmd) with
| Transform (s, _t, args) -> treat_request (Transform_req (nid, s, args)) | Transform (s, _t, args) -> treat_request (Transform_req (nid, s, args))
| Query s -> P.notify (Message (Query_Info (nid, s))) | Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) -> schedule_proof_attempt nid p limit | Prove (p, limit) -> schedule_proof_attempt nid p limit
...@@ -948,7 +960,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -948,7 +960,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
P.notify (Message (Information ("Unknown command"^s))) P.notify (Message (Information ("Unknown command"^s)))
end end
| Add_file_req f -> | Add_file_req f ->
add_file_to_session cont f add_file_to_session d.cont f
| Open_session_req file_or_dir_name -> | Open_session_req file_or_dir_name ->
init_cont file_or_dir_name; init_cont file_or_dir_name;
reload_session () reload_session ()
......
...@@ -108,6 +108,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig ...@@ -108,6 +108,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
(* (*
val get_configs: unit -> Whyconf.config * Whyconf.config val get_configs: unit -> Whyconf.config * Whyconf.config
*) *)
(* Initialize server_data *)
val init_server: Whyconf.config -> Env.env -> unit
(* Nothing ! *) (* Nothing ! *)
......
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