Adding copy/paste.

Also copy as detached goal.

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 *)
 (*********************************)

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

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 *)

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

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

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 =

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

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 *)