diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index 2dd6d521a4b7fd5a3372d2008d6e6e7990175b98..b5916fe19cce26af85f1449e3b7d05ec4f068ec9 100644 --- a/src/ide/why3ide.ml +++ b/src/ide/why3ide.ml @@ -428,7 +428,6 @@ let reload_menu_item : GMenu.menu_item = 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 @@ -811,6 +810,53 @@ let remove_item: GMenu.menu_item = | [r] -> let id = get_node_id r#iter in send_request (Remove_subtree id) | _ -> print_message "Select only one node to perform this action") + + + +(*************************************) +(* Commands of the Experimental menu *) +(*************************************) + +let exp_menu = factory#add_submenu "_Experimental" +let exp_factory = new GMenu.factory exp_menu ~accel_group + + +(* Current copied node *) +let saved_copy = ref None + +let copy () = + match get_selected_row_references () with + | [r] -> let n = get_node_id r#iter in + saved_copy := Some n + | _ -> () + +let paste () = + match get_selected_row_references () with + | [r] -> + let m = get_node_id r#iter in + (match !saved_copy with + | Some n -> send_request (Copy_paste (n, m)) + | None -> ()) + | _ -> () + +let detached_copy () = + match get_selected_row_references () with + | [r] -> let n = get_node_id r#iter in + send_request (Copy_detached n) + | _ -> () + +let (_ : GMenu.menu_item) = + exp_factory#add_item ~key:GdkKeysyms._C + ~callback:copy "Copy" + +let (_ : GMenu.menu_item) = + exp_factory#add_item ~key:GdkKeysyms._V + ~callback:paste "Paste" + +let (_ : GMenu.menu_item) = + exp_factory#add_item ~key:GdkKeysyms._D + ~callback:detached_copy "Detached copy" + (*********************************) (* add a new file in the project *) (*********************************) diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index 950403b24aef21669dd9feca306f494c4e0a4f0b..716916d8f0ad0c26d3b01bf4b69031d437d4081b 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -461,7 +461,7 @@ let schedule_proof_attempt_r c id pr ~limit ~callback = run_timeout_handler () let schedule_proof_attempt c id pr ~limit ~callback ~notification = - let callback panid s = callback panid s; + let callback panid s = callback panid s; (match s with | Done pr -> update_proof_node notification c id (pr.Call_provers.pr_answer == Call_provers.Valid) | Interrupted | InternalFailure _ -> update_proof_node notification c id false @@ -567,6 +567,65 @@ let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback ~notific in exec_strategy 0 strat id +let schedule_pa_with_same_arguments c (pa: proof_attempt_node) (pn: proofNodeID) ~callback ~notification = + let prover = pa.prover in + let limit = pa.limit in + schedule_proof_attempt c pn prover ~limit ~callback ~notification + +let schedule_tr_with_same_arguments c (tr: transID) (pn: proofNodeID) ~callback ~notification = + let s = c.controller_session in + let args = get_transf_args s tr in + let name = get_transf_name s tr in + schedule_transformation c pn name args ~callback ~notification + +exception BadCopyPaste + +(* Reproduce the transformation made on node on an other one *) +let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any = + let s = c.controller_session in + if (not (is_below s from_any to_any) && + not (is_below s to_any from_any)) then + match from_any, to_any with + | AFile _, AFile _ -> + raise BadCopyPaste + | ATh _from_th, ATh _to_th -> + raise BadCopyPaste + | APn from_pn, APn to_pn -> + let from_pa_list = get_proof_attempts s from_pn in + List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn + ~callback:callback_pa ~notification) from_pa_list; + let from_tr_list = get_transformations s from_pn in + let callback x st = callback_tr st; + match st with + | TSdone tid -> copy_paste c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr + | _ -> () + in + List.iter (fun x -> schedule_tr_with_same_arguments c x to_pn + ~callback:(callback x) ~notification) from_tr_list + | ATn from_tn, ATn to_tn -> + let from_tn_list = get_sub_tasks s from_tn in + let to_tn_list = get_sub_tasks s to_tn in + if (List.length from_tn_list = List.length to_tn_list) then + List.iter2 (fun x y -> copy_paste c (APn x) (APn y) + ~notification ~callback_pa ~callback_tr) from_tn_list to_tn_list + | _ -> raise BadCopyPaste + + +let copy_detached ~copy c from_any = + match from_any with + | APn from_pn -> + begin + let pn_id = copy_proof_node_as_detached c.controller_session from_pn in + let parent = get_any_parent c.controller_session from_any in + match parent with + | None -> raise BadCopyDetached + | Some parent -> + copy ~parent (APn pn_id); + copy_structure ~notification:copy c.controller_session (APn from_pn) (APn pn_id) + end + | _ -> raise BadCopyDetached (* Only goal can be detached *) + + let replay_proof_attempt c pr limit (id: proofNodeID) ~callback = (* The replay can be done on a different machine so we need diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index 159a6cf93e0ac9601ec5a247464d0cf8f7724a09..30c790072082f1705284463f6a04058154199fe6 100644 --- a/src/session/controller_itp.mli +++ b/src/session/controller_itp.mli @@ -206,6 +206,16 @@ type report = | No_former_result of Call_provers.prover_result (** Type for the reporting of a replayed call *) +(* [copy_paste c a b] try to copy subtree originating at node a to node b *) +val copy_paste: + notification:(any -> bool -> unit) -> + callback_pa:(proofAttemptID -> proof_attempt_status -> unit) -> + callback_tr:(transformation_status -> unit) -> + controller -> any -> any -> unit + +val copy_detached: + copy:(parent:any -> any -> unit) -> + controller -> any -> unit (* Callback for the report printing of replay TODO to be removed when we have a better way to print the result of replay *) diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 682d5ab3ae241aaf929fd59c503baa80f1a4c381..ac9a0e59c9e2eeff8d2749316f7c23de8701f5ed 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -372,6 +372,8 @@ type ide_request = | Set_max_tasks_req of int | Get_task of node_ID | Remove_subtree of node_ID + | Copy_paste of node_ID * node_ID + | Copy_detached of node_ID | Get_Session_Tree_req | Save_req | Reload_req @@ -390,6 +392,8 @@ let print_request fmt r = | Set_max_tasks_req i -> fprintf fmt "set max tasks %i" i | Get_task _nid -> fprintf fmt "get task" | Remove_subtree _nid -> fprintf fmt "remove subtree" + | Copy_paste _ -> fprintf fmt "copy paste" + | Copy_detached _ -> fprintf fmt "copy detached" | Get_Session_Tree_req -> fprintf fmt "get session tree" | Save_req -> fprintf fmt "save" | Reload_req -> fprintf fmt "reload" @@ -465,7 +469,6 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct 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 provers = Whyconf.get_provers config in let c = create_controller env in @@ -539,10 +542,10 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct let get_node_type (node: any) = match node with | AFile _ -> NFile - | ATh _ -> NTheory - | ATn _ -> NTransformation - | APn _ -> NGoal - | APa _ -> NProofAttempt + | ATh _ -> NTheory + | ATn _ -> NTransformation + | APn _ -> NGoal + | APa _ -> NProofAttempt let get_node_name (node: any) = let d = get_server_data () in @@ -944,7 +947,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct | Transform_req (nid, t, args) -> apply_transform nid t args | Strategy_req (nid, st) -> run_strategy_on_task nid st | Save_req -> save_session () - | Reload_req -> reload_session (); + | Reload_req -> reload_session () | Get_Session_Tree_req -> resend_the_tree () | Remove_subtree nid -> let n = any_from_node_ID nid in @@ -956,6 +959,21 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct with RemoveError -> (* TODO send an error instead of information *) P.notify (Message (Information "Cannot remove a proof node or theory")) end + | Copy_paste (from_id, to_id) -> + let from_any = any_from_node_ID from_id in + let to_any = any_from_node_ID to_id in + C.copy_paste ~notification:notify_change_proved + ~callback_pa:(callback_update_tree_proof d.cont) + ~callback_tr:(callback_update_tree_transform) + d.cont from_any to_any + + | Copy_detached from_id -> + let from_any = any_from_node_ID from_id in + let copy ~parent p = + let parent = node_ID_from_any parent in + ignore (new_node ~parent p) + in + C.copy_detached ~copy d.cont from_any | Get_task nid -> send_task nid | Replay_req -> replay_session (); resend_the_tree () | Command_req (nid, cmd) -> @@ -969,7 +987,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct | Help_message s -> P.notify (Message (Help s)) | QError s -> P.notify (Message (Query_Error (nid, s))) | Other (s, _args) -> - P.notify (Message (Information ("Unknown command"^s))) + P.notify (Message (Information ("Unknown command: "^s))) end | Add_file_req f -> add_file_to_session d.cont f diff --git a/src/session/itp_server.mli b/src/session/itp_server.mli index 718698edc3736a16f196b4e89bb48cd6fcde0d6a..411a2c568379938210a17c4c01d973d2a86ab7a5 100644 --- a/src/session/itp_server.mli +++ b/src/session/itp_server.mli @@ -86,6 +86,8 @@ type ide_request = | Set_max_tasks_req of int | Get_task of node_ID | Remove_subtree of node_ID + | Copy_paste of node_ID * node_ID + | Copy_detached of node_ID | Get_Session_Tree_req | Save_req | Reload_req diff --git a/src/session/json_util.ml b/src/session/json_util.ml index 8021c851a5ba46bb2966685668b81f2f169c3f39..adddb1beb2f397790b669183318ee5f48a1acd72 100644 --- a/src/session/json_util.ml +++ b/src/session/json_util.ml @@ -123,6 +123,8 @@ let convert_request_constructor (r: ide_request) = | Set_max_tasks_req _ -> String "Set_max_tasks_req" | Get_task _ -> String "Get_task" | Remove_subtree _ -> String "Remove_subtree" + | Copy_paste _ -> String "Copy_paste" + | Copy_detached _ -> String "Copy_detached" | Get_Session_Tree_req -> String "Get_Session_Tree_req" | Save_req -> String "Save_req" | Reload_req -> String "Reload_req" @@ -165,6 +167,13 @@ let print_request_to_json (r: ide_request): json_object = | Remove_subtree n -> Assoc ["ide_request", cc r; "node_ID", Int n] + | Copy_paste (from_id, to_id) -> + Assoc ["ide_request", cc r; + "node_ID", Int from_id; + "node_ID", Int to_id] + | Copy_detached from_id -> + Assoc ["ide_request", cc r; + "node_ID", Int from_id] | Get_Session_Tree_req -> Assoc ["ide_request", cc r] | Save_req -> @@ -339,18 +348,22 @@ let parse_request (constr: string) l = Set_max_tasks_req n | "Get_task", ["node_ID", Int n] -> Get_task n - | "Remove_subtree", ["node_ID", Int n] -> + | "Remove_subtree", ["node_ID", Int n] -> Remove_subtree n + | "Copy_paste", ["node_ID", Int from_id; "node_ID", Int to_id] -> + Copy_paste (from_id, to_id) + | "Copy_detached", ["node_ID", Int n] -> + Copy_detached n | "Get_Session_Tree_req", [] -> - Get_Session_Tree_req + Get_Session_Tree_req | "Save_req", [] -> - Save_req + Save_req | "Reload_req", [] -> - Reload_req + Reload_req | "Replay_req", [] -> - Replay_req + Replay_req | "Exit_req", [] -> - Exit_req + Exit_req | _ -> raise (NotRequest "") let parse_request (j: json_object): ide_request = diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index 12b76f33b02afc2ffc8856edfe0f4a5ac64a005a..c8c3f9bf93ec1d17f97ae1bf6ee772e53f582776 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -368,6 +368,29 @@ let theory_iter_proof_attempt s f th = f pan) pn.proofn_attempts) th +(**************) +(* Copy/Paste *) +(**************) + +let get_any_parent s a = + match a with + | AFile _f -> None + | ATh th -> Some (AFile (theory_parent s th)) + | ATn tr -> Some (APn (get_trans_parent s tr)) + | APn pn -> + (match (get_proofNode s pn).proofn_parent with + | Theory th -> Some (ATh th) + | Trans tr -> Some (ATn tr)) + | APa pa -> + Some (APn (get_proof_attempt_node s pa).parent) + +(* True if bid is an ancestor of aid, false if not *) +let rec is_below s (aid: any) (bid: any) = + aid = bid || + match (get_any_parent s aid) with + | None -> false + | Some pid -> is_below s pid bid + open Format open Ident @@ -495,6 +518,25 @@ let mk_proof_node_no_task (s : session) (n : Ident.ident) proofn_transformations = [] } in Hint.add s.proofNode_table node_id pn +(* Detach a new proof to a proof_parent *) +let graft_detached_proof_on_parent s (pn: proofNodeID) (parent: proof_parent) = + match parent with + | Theory th -> + th.theory_detached_goals <- th.theory_detached_goals @ [pn] + | Trans tr_id -> + let tr = get_transfNode s tr_id in + tr.transf_detached_subtasks <- tr.transf_detached_subtasks @ [pn] + +(* Intended as a feature to save a proof (also for testing detached stuff) *) +let copy_proof_node_as_detached (s: session) (pn_id: proofNodeID) = + let pn = get_proofNode s pn_id in + let new_pn_id = gen_proofNodeID s in + let parent = pn.proofn_parent in + let new_goal_name = Ident.id_register (Ident.id_clone pn.proofn_name) in + let _new_pn = mk_proof_node_no_task s new_goal_name parent new_pn_id pn.proofn_checksum pn.proofn_shape in + graft_detached_proof_on_parent s new_pn_id parent; + new_pn_id + let _mk_proof_node_task (s : session) (t : Task.task) (parent : proof_parent) (node_id : proofNodeID) = let name,_,_ = Termcode.goal_expl_task ~root:false t in @@ -524,6 +566,41 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID) Hint.add s.trans_table node_id tn; pn.proofn_transformations <- node_id::pn.proofn_transformations +exception BadCopyDetached + +let rec copy_structure ~notification s from_any to_any : unit = + match from_any, to_any with + | APn from_id, APn to_id -> + let transformations = get_transformations s from_id in + let new_transformations = + List.map (fun x -> + let tr_id = gen_transID s in + let old_tr = get_transfNode s x in + mk_transf_node s to_id tr_id old_tr.transf_name old_tr.transf_args []; + notification ~parent:to_any (ATn tr_id); + copy_structure ~notification s (ATn x) (ATn tr_id); + tr_id) transformations in + (get_proofNode s to_id).proofn_transformations <- new_transformations; + Hprover.iter (fun _k old_pa -> + let old_pa = get_proof_attempt_node s old_pa in + let pa_id = add_proof_attempt s old_pa.prover old_pa.limit None true None to_id in + notification ~parent:to_any (APa pa_id)) (get_proofNode s from_id).proofn_attempts + | ATn from_tn, ATn to_tn -> + let sub_tasks = get_sub_tasks s from_tn in + let new_sub_tasks = + List.map (fun old_pn_id -> + let old_pn = get_proofNode s old_pn_id in + let pn_id = gen_proofNodeID s in + let new_id = Ident.id_register (Ident.id_clone old_pn.proofn_name) in + mk_proof_node_no_task s new_id (Trans to_tn) + pn_id old_pn.proofn_checksum old_pn.proofn_shape; + notification ~parent:to_any (APn pn_id); + copy_structure ~notification s (APn old_pn_id) (APn pn_id); + pn_id) sub_tasks in + let tr = get_transfNode s to_tn in + tr.transf_detached_subtasks <- new_sub_tasks + | _ -> raise BadCopyDetached + let graft_transf (s : session) (id : proofNodeID) (name : string) (args : string list) (tl : Task.task list) = let tid = gen_transID s in diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index f93c95a409d54cb233f4f15d3472250384cb4f4e..ea15774c1199527198163de490141ac4cab0da21 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -67,6 +67,9 @@ type proof_attempt_node = { val session_iter_proof_attempt: (proofNodeID -> proof_attempt_node -> unit) -> session -> unit +(* [is_below s a b] true if a is below b in the session tree *) +val is_below: session -> any -> any -> bool + type proof_parent = Trans of transID | Theory of theory val get_task : session -> proofNodeID -> Task.task @@ -89,6 +92,14 @@ val get_proof_name : session -> proofNodeID -> Ident.ident val get_proof_parent : session -> proofNodeID -> proof_parent val get_trans_parent : session -> transID -> proofNodeID +val get_any_parent: session -> any -> any option + +exception BadCopyDetached + +(** [copy s pn] copy pn and add the copy as detached subgoal of its parent *) +val copy_proof_node_as_detached: session -> proofNodeID -> proofNodeID +val copy_structure: notification:(parent:any -> any -> unit) -> session -> any -> any -> unit + val empty_session : ?shape_version:int -> string -> session (** create an empty_session in the directory specified by the argument *)