Skip to content

GitLab

why3
why3
Commit 05164df4 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

Should allow file to be opened in two ways. 

Also do following changes:
Changed printer to allow printing from label again.
changed callback of transformation so that creating node is always done
before updating it.
Added a root for coherence and easy
Clear the message zone for a demo.
parent fb82fe5e
Hide whitespace changes
Inline Side-by-side
Showing with 246 additions and 193 deletions
src/ide/why3ide.ml
View file @ 05164df4
......@@ -161,7 +161,6 @@ let try_convert s =
s
with Glib.Convert.Error _ as e -> Printexc.to_string e
(**********************)
(* Graphical elements *)
(**********************)
......@@ -215,18 +214,6 @@ let exit_function ~destroy () =
let (_ : GtkSignal.id) = main_window#connect#destroy
~callback:(exit_function ~destroy:true)
let (_ : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._S "_Save session"
~callback:(fun () -> send_request Save_req)
let (replay_menu_item : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._R "_Replay all"
let (_ : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
~callback:(exit_function ~destroy:false)
(* 1.2 "View" menu
the entries in that menu are defined later
......@@ -304,6 +291,96 @@ let goals_model,goals_view =
Debug.dprintf debug " done@.";
model,view
(***********************************)
(* Mapping session to the GTK tree *)
(***********************************)
type pa_status = Controller_itp.proof_attempt_status
* bool (* obsolete or not *) (* TODO *)
* Call_provers.resource_limit
let node_id_type : node_type Hint.t = Hint.create 17
let node_id_proved : bool Hint.t = Hint.create 17
let node_id_pa : pa_status Hint.t = Hint.create 17
let get_node_type id = Hint.find node_id_type id
let get_node_proved id = Hint.find node_id_proved id
let get_node_id_pa id = Hint.find node_id_pa id
let get_obs (pa_st: pa_status) = match pa_st with
| _, b, _ -> b
let get_proof_attempt (pa_st: pa_status) = match pa_st with
| pa, _, _ -> pa
let get_limit (pa_st: pa_status) = match pa_st with
| _, _, l -> l
let get_node_obs id = get_obs (get_node_id_pa id)
let get_node_proof_attempt id = get_proof_attempt (get_node_id_pa id)
let get_node_limit id = get_limit (get_node_id_pa id)
let get_node_id iter = goals_model#get ~row:iter ~column:node_id_column
(* To each node we have the corresponding row_reference *)
let node_id_to_gtree : GTree.row_reference Hint.t = Hint.create 42
(* TODO exception for those: *)
let get_node_row id = Hint.find node_id_to_gtree id
(******************************)
(* Initialization of the tree *)
(******************************)
(* TODO root node is convenient. Symmetry with session and parent of a node can
always be found. Can be removed. *)
(* Creating the root of the tree. *)
let create_root () =
let root_iter = goals_model#append () in
let root_ref = goals_model#get_row_reference
(goals_model#get_path root_iter) in
Hint.add node_id_to_gtree root_node root_ref
let remove_tree goals_model =
Hint.iter (fun _x i ->
try ignore(goals_model#remove (i#iter)) with _ -> ())
node_id_to_gtree
let clear_tree_and_table goals_model =
remove_tree goals_model;
Hint.clear node_id_to_gtree;
Hint.clear node_id_type;
Hint.clear node_id_proved;
Hint.clear node_id_pa
(* Actually creating root *)
let _ = create_root ()
(**************)
(* Menu items *)
(**************)
let (_ : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._S "_Save session"
~callback:(fun () -> send_request Save_req)
let (replay_menu_item : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._R "_Replay all"
let (_ : GMenu.menu_item) =
file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
~callback:(exit_function ~destroy:false)
(* TODO key stroked to be decided *)
let reload_menu_item : GMenu.menu_item =
file_factory#add_item ~key:GdkKeysyms._E "_Reload session"
~callback:(fun () ->
(* Clearing the tree *)
clear_tree_and_table goals_model;
(* Adding the root again *)
create_root ();
send_request Reload_req)
(* vpan222 contains:
2.2.2.1 a view of the current task
2.2.2.2 a vertiacal pan which contains
......@@ -442,45 +519,19 @@ let (_ : GtkSignal.id) =
replay_menu_item#connect#activate
~callback:(fun () -> send_request Replay_req)
(***********************************)
(* Mapping session to the GTK tree *)
(***********************************)
type pa_status = Controller_itp.proof_attempt_status
* bool (* obsolete or not *) (* TODO *)
* Call_provers.resource_limit
let node_id_type : node_type Hint.t = Hint.create 17
let node_id_proved : bool Hint.t = Hint.create 17
let node_id_pa : pa_status Hint.t = Hint.create 17
let get_node_type id = Hint.find node_id_type id
let get_node_proved id = Hint.find node_id_proved id
let get_node_id_pa id = Hint.find node_id_pa id
let get_obs (pa_st: pa_status) = match pa_st with
| _, b, _ -> b
let get_proof_attempt (pa_st: pa_status) = match pa_st with
| pa, _, _ -> pa
let get_limit (pa_st: pa_status) = match pa_st with
| _, _, l -> l
let get_node_obs id = get_obs (get_node_id_pa id)
let get_node_proof_attempt id = get_proof_attempt (get_node_id_pa id)
let get_node_limit id = get_limit (get_node_id_pa id)
let get_node_id iter = goals_model#get ~row:iter ~column:node_id_column
(* To each node we have the corresponding row_reference *)
let node_id_to_gtree : GTree.row_reference Hint.t = Hint.create 42
(* TODO exception for those: *)
let get_node_row id = Hint.find node_id_to_gtree id
(**************************)
(* Graphical proof status *)
(**************************)
let image_of_pa_status ~obsolete pa =
match pa with
| Controller_itp.Unedited -> !image_scheduled (* TODO !image_unedited *)
| Controller_itp.JustEdited -> !image_scheduled (* TODO !image_edited *)
| Controller_itp.Interrupted -> !image_scheduled (* TODO !image_interrrupted *)
| Controller_itp.Scheduled -> !image_scheduled
| Controller_itp.Running -> !image_running
| Controller_itp.InternalFailure _e -> !image_failure
| Controller_itp.Uninstalled _p -> !image_failure (* TODO !image_uninstalled *)
(* | None -> !image_undone*)
| Controller_itp.Done r ->
let pr_answer = r.Call_provers.pr_answer in
......@@ -504,7 +555,6 @@ let image_of_pa_status ~obsolete pa =
| Call_provers.HighFailure ->
if obsolete then !image_failure_obs else !image_failure
end
| _ -> !image_undone
let set_status_column iter =
let id = get_node_id iter in
......@@ -525,6 +575,11 @@ let set_status_column iter =
in
goals_model#set ~row:iter ~column:status_column image
let new_node ?parent ?(collapse=false) id name typ proved =
if not (Hint.mem node_id_to_gtree id) then begin
Hint.add node_id_type id typ;
......@@ -674,7 +729,8 @@ let interp cmd =
let (_ : GtkSignal.id) =
command_entry#connect#activate
~callback:(fun () -> add_command list_commands command_entry#text; interp command_entry#text)
~callback:(fun () -> add_command list_commands command_entry#text;
interp command_entry#text)
let on_selected_row r =
try
......@@ -698,6 +754,10 @@ let (_ : GtkSignal.id) =
(* Notification Handling *)
(*************************)
(* Function used to print stuff on the message_zone *)
let print_message s =
message_zone#buffer#set_text s
let add_to_msg_zone s =
let s = message_zone#buffer#get_text () ^ "\n" ^ s in
message_zone#buffer#set_text s;
......@@ -705,21 +765,22 @@ let add_to_msg_zone s =
let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> add_to_msg_zone s
| Transf_error (_id, s) -> add_to_msg_zone s
| Strat_error (_id, s) -> add_to_msg_zone s
| Replay_Info s -> add_to_msg_zone s
| Query_Info (_id, s) -> add_to_msg_zone s
| Query_Error (_id, s) -> add_to_msg_zone s
| Help s -> add_to_msg_zone s
| Information s -> add_to_msg_zone s
| Proof_error (_id, s) -> print_message s
| Transf_error (_id, s) -> print_message s
| Strat_error (_id, s) -> print_message s
| Replay_Info s -> print_message s
| Query_Info (_id, s) -> print_message s
| Query_Error (_id, s) -> print_message s
| Help s -> print_message s
| Information s -> print_message s
| Task_Monitor (t, s, r) -> update_monitor t s r
| Open_File_Error s -> print_message s
(* TODO do not print this particular error *)
| Error s ->
if Debug.test_flag debug then
add_to_msg_zone s
print_message s
else
add_to_msg_zone "Request failed."
print_message "Request failed."
let treat_notification n = match n with
| Node_change (id, uinfo) ->
......@@ -750,12 +811,12 @@ let treat_notification n = match n with
if typ = NGoal then goals_view#selection#select_iter row_ref#iter);
end
| Remove _id -> (* TODO *)
add_to_msg_zone "got a Remove notification not yet supported\n"
print_message "got a Remove notification not yet supported\n"
| Initialized g_info ->
(* TODO: treat other *)
init_completion g_info.provers g_info.transformations g_info.commands;
| Saved -> (* TODO *)
add_to_msg_zone "got a Saved notification not yet supported\n"
print_message "got a Saved notification not yet supported\n"
| Message (msg) -> treat_message_notification msg
(* | Proof_update (id, pa) -> (* TODO *)
let r = get_node_row id in
......@@ -766,7 +827,7 @@ let treat_notification n = match n with
goals_model#set ~row:r#iter ~column:status_column
(image_of_pa_status ~obsolete pa) *)
| Dead _s -> (* TODO *)
add_to_msg_zone "got a Dead notification not yet supported\n"
print_message "got a Dead notification not yet supported\n"
| Task (_id, s) ->
(* TODO: check that the id is the current one *)
task_view#source_buffer#set_text s;
......
src/printer/why3printer.ml
View file @ 05164df4
......@@ -28,7 +28,7 @@ let debug_print_labels = Debug.register_info_flag "print_labels"
let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let id_unique tables id = id_unique tables.printer id
let id_unique tables id = id_unique_label tables.printer id
(*
let forget_tvs () =
......
src/session/controller_itp.ml
View file @ 05164df4
......@@ -518,7 +518,7 @@ let schedule_transformation_r c id name args ~callback =
callback TSscheduled
let schedule_transformation c id name args ~callback ~notification =
let callback s = (match s with
let callback s = callback s; (match s with
| TSdone tid ->
let has_subtasks =
match get_sub_tasks c.controller_session tid with
......@@ -527,7 +527,7 @@ let schedule_transformation c id name args ~callback ~notification =
in
update_trans_node notification c tid has_subtasks
| TSfailed _e -> ()
| _ -> ()); callback s in
| _ -> ()) in
schedule_transformation_r c id name args ~callback
open Strategy
......
src/session/itp_server.ml
View file @ 05164df4
......@@ -3,12 +3,14 @@ open Call_provers
open Session_itp
open Controller_itp
exception NotADirectory of string
exception BadFileName of string
let cont_from_session_dir cont dir =
(* create project directory if needed *)
if Sys.file_exists dir then
begin
if not (Sys.is_directory dir) then failwith "not a directory"
(* TODO: raise (NotADirectory dir) *)
if not (Sys.is_directory dir) then raise (NotADirectory dir)
end
else
begin
......@@ -24,57 +26,11 @@ let cont_from_session_dir cont dir =
(* update the session *)
Controller_itp.reload_files cont ~use_shapes
(*
(* TODO: raise exceptions instead of using explicit eprintf/exit *)
let cont_from_files cont spec usage_str env files provers =
if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
let fname = Queue.peek files in
(* extract project directory, and create it if needed *)
let dir =
if Filename.check_suffix fname ".why" ||
Filename.check_suffix fname ".mlw"
then Filename.chop_extension fname
else let _ = Queue.pop files in fname
in
if Sys.file_exists dir then
begin
if not (Sys.is_directory dir) then
begin
Format.eprintf
"[Error] @[When@ more@ than@ one@ file@ is@ given@ on@ the@ \
command@ line@ the@ first@ one@ must@ be@ the@ directory@ \
of@ the@ session.@]@.";
Arg.usage spec usage_str; exit 1
end
end
else
begin
eprintf "[GUI] '%s' does not exist. \
Creating directory of that name for the project@." dir;
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = load_session dir in
eprintf "using shapes: %a@." pp_print_bool use_shapes;
(* create the controller *)
Controller_itp.init_controller ses cont;
(* update the session *)
Controller_itp.reload_files cont ~use_shapes;
(* add files to controller *)
Queue.iter (fun fname -> Controller_itp.add_file cont fname) files;
(* load provers drivers *)
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver env p.Whyconf.driver [] in
Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
with e ->
let p = p.Whyconf.prover in
eprintf "Failed to load driver for %s %s: %a@."
p.Whyconf.prover_name p.Whyconf.prover_version
Exn_printer.exn_printer e)
provers
*)
(* If we have a file we chop it and return new session based on the directory *)
let cont_from_file cont f =
let dir = try (Filename.chop_extension f) with
| Invalid_argument _ -> raise (BadFileName f) in
cont_from_session_dir cont dir
(**********************************)
(* list unproven goal and related *)
......@@ -710,6 +666,8 @@ let bypass_pretty s id =
let get_exception_message ses id fmt e =
match e with
| Controller_itp.Noprogress ->
Format.fprintf fmt "Transformation made no progress\n"
| Case.Arg_trans_type (s, ty1, ty2) ->
Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %a \n %a"
s (print_type ses id) ty1 (print_type ses id) ty2
......@@ -753,16 +711,17 @@ type global_information =
}
type message_notification =
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Error of string
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Error of string
| Open_File_Error of string
type node_type =
| NRoot
......@@ -842,11 +801,12 @@ let print_msg fmt m =
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Error s -> fprintf fmt "%s" s
| Open_File_Error s -> fprintf fmt "%s" s
let print_notify fmt n =
match n with
| Node_change (_ni, _nf) -> fprintf fmt "node change"
| New_node (_ni, _pni, _nt, _nf) -> fprintf fmt "new node"
| New_node (ni, _pni, _nt, _nf) -> fprintf fmt "new node %d" ni
| Remove _ni -> fprintf fmt "remove"
| Initialized _gi -> fprintf fmt "initialized"
| Saved -> fprintf fmt "saved"
......@@ -907,12 +867,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
List.map (fun (c,_,_) -> c) commands
}
(* Controller is not initialized: we cannot process any request *)
let init_controller = ref false
(* Create_controller creates a dummy controller *)
let cont =
init_controller := false;
try
create_controller env provers
with LoadDriverFailure (p, e) -> P.notify (Message (
......@@ -921,16 +877,32 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* ------------ init controller ------------ *)
(* Init cont is called only when an Open is requested *)
let init_cont dir =
try
cont_from_session_dir cont dir;
init_controller := true;
P.notify (Initialized infos)
with e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
P.notify (Dead (Pp.string_of Exn_printer.exn_printer e));
exit 1
(* Init cont on file or directory. It is called only when an
Open_session_req is requested *)
let init_cont f =
try (
if (Sys.file_exists f) then
begin
if (Sys.is_directory f) then
begin
cont_from_session_dir cont f;
P.notify (Initialized infos)
end
else
begin
cont_from_file cont f;
P.notify (Initialized infos)
end
end
else
P.notify (Message (Open_File_Error ("Not a file: " ^ f))))
with
| NotADirectory f -> P.notify (Message (Open_File_Error ("Not a directory: " ^ f)))
| BadFileName f -> P.notify (Message (Open_File_Error ("Bad file name: " ^ f)))
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
P.notify (Dead (Pp.string_of Exn_printer.exn_printer e));
exit 1
(* ----------------------------------- ------------------------------------- *)
......@@ -1065,21 +1037,6 @@ exception Bad_prover_name of prover
with the notification corresponding to a "root node" creation (root of the
files)
*)
(* TODO remove this unnecessary
let build_the_tree () : unit =
let ses = cont.controller_session in
let files = get_files ses in
P.notify (New_node (0, 0, Root, root_info));
let l = Stdlib.Hstr.fold
(fun _file_key file acc ->
let file_node_ID = node_ID_from_file file in
let pos_ID = pos_from_node file_node_ID in
let node_type, node_info = get_info_and_type ses (AFile file) in
let l = List.fold_left (fun acc th ->
build_subtree_from_theory ses th :: acc) [] file.file_theories in
Node (file_node_ID, pos_ID, node_type, node_info, l) :: acc
) files [] in
*)
(* ----------------- init the tree --------------------------- *)
(* Iter on the session tree with a function [f parent current] with type
......@@ -1144,6 +1101,7 @@ exception Bad_prover_name of prover
root f
let init_and_send_the_tree (): unit =
P.notify (New_node (0, 0, NRoot, "root"));
iter_the_files (fun ~parent id -> ignore (new_node ~parent id)) root
let resend_the_tree (): unit =
......@@ -1169,6 +1127,28 @@ exception Bad_prover_name of prover
| _ ->
P.notify (Task (nid, "can not associate a task to a node that is not a goal."))
(* -------------------- *)
(* Add a file into the session when (Add_file_req f) is sent *)
(* Note that f is the path from execution directory to the file and fn is the
path from the session directory to the file. *)
let add_file_to_session cont f =
let fn = Sysutil.relativize_filename
(Session_itp.get_dir cont.controller_session) f in
let files = get_files cont.controller_session in
if (not (Stdlib.Hstr.mem files fn)) then
if (Sys.file_exists f) then
begin
Controller_itp.add_file cont f;
let file = Stdlib.Hstr.find files fn in
init_and_send_file file
end
else
P.notify (Message (Open_File_Error ("Not a file: " ^ f)))
else
P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
(* ----------------- Schedule proof attempt -------------------- *)
(* Callback of a proof_attempt *)
......@@ -1297,7 +1277,6 @@ exception Bad_prover_name of prover
init_and_send_the_tree ()
let replay_session () : unit =
clear_tables ();
let callback = fun lr ->
P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in
(* TODO make replay print *)
......@@ -1316,7 +1295,9 @@ exception Bad_prover_name of prover
let rec treat_request r =
try (
match r with
| Prove_req (nid,p,limit) -> schedule_proof_attempt nid (get_prover p) limit
| Prove_req (nid,p,limit) ->
(try (schedule_proof_attempt nid (get_prover p) limit) with
| Bad_prover_name p -> P.notify (Message (Proof_error (nid, "Bad prover name" ^ p))))
| Transform_req (nid, t, args) -> apply_transform nid t args
| Strategy_req (nid, st) -> run_strategy_on_task nid st
| Save_req -> save_session ()
......@@ -1338,19 +1319,24 @@ exception Bad_prover_name of prover
P.notify (Message (Information ("Unknown command"^s)))
end
| Add_file_req f ->
begin
Controller_itp.add_file cont f;
let f = Sysutil.relativize_filename
(Session_itp.get_dir cont.controller_session) f in
add_file_to_session cont f
(*
let fn = Sysutil.relativize_filename
(Session_itp.get_dir cont.controller_session) f in
let files = get_files cont.controller_session in
let file = Stdlib.Hstr.find files f in
init_and_send_file file
end
| Open_session_req file_name ->
init_cont file_name;
init_and_send_the_tree ()
if (not (Hstr.mem files fn)) then
begin
add_file_to_session cont f;
(*Controller_itp.add_file cont f;*)
let file = Stdlib.Hstr.find files fn in
init_and_send_file file
end
*)
| Open_session_req file_or_dir_name ->
init_cont file_or_dir_name;
reload_session ()
| Set_max_tasks_req i -> C.set_max_tasks i
| Exit_req -> exit 0 (* TODO *)
| Exit_req -> exit 0
)
with e -> P.notify (Message (Error (Pp.string_of
(fun fmt (r,e) -> Format.fprintf fmt
......
src/session/itp_server.mli
View file @ 05164df4
......@@ -29,7 +29,7 @@ type global_information =
provers : prover list;
transformations : transformation list;
strategies : strategy list;
commands : string list;
commands : string list
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
(* session_mem_limit : int; *)
......@@ -39,19 +39,20 @@ type global_information =
}
type message_notification =
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string