Improved copy-paste functionality

- copy from a transformation to a proof node works, adding
  the transformation below the target node

- when copied transformation as less or more subgoals, then
  only the first subgoals are copied

- explicit error message in case of invalid copy

src/session/controller_itp.ml

@@ -829,15 +829,15 @@ let mark_as_obsolete ~notification c any =
 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 rec copy_rec ~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
+  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 ~counterexmp:false
@@ -846,7 +846,7 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
       let callback x tr args st = callback_tr tr args st;
         match st with
         | TSdone tid ->
-          copy_paste c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr
+          copy_rec c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr
         | _ -> ()
       in
       List.iter (fun x -> schedule_tr_with_same_arguments c x to_pn
@@ -854,12 +854,37 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
     | 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
+        let rec iter_copy l1 l2 =
+          match l1,l2 with
+          | x::r1, y::r2 ->
+             copy_rec c (APn x) (APn y)
+                      ~notification ~callback_pa ~callback_tr;
+             iter_copy r1 r2
+          | _ -> ()
+        in iter_copy from_tn_list to_tn_list
     | _ -> raise BadCopyPaste
 
 
+let copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
+  let s = c.controller_session in
+  if is_below s from_any to_any || is_below s to_any from_any
+  then raise BadCopyPaste;
+  match from_any, to_any with
+  | APn _, APn _ ->
+     copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any
+  | ATn from_tn, APn to_pn ->
+     let callback tr args st =
+       callback_tr tr args st;
+       match st with
+       | TSdone tid ->
+          copy_rec c (ATn from_tn) (ATn tid) ~notification ~callback_pa ~callback_tr
+       | _ -> ()
+     in
+     schedule_tr_with_same_arguments c from_tn to_pn ~callback ~notification
+  | _ -> raise BadCopyPaste
+
+
+
 
 
 

src/session/controller_itp.mli

@@ -270,6 +270,8 @@ val mark_as_obsolete:
   notification:notifier ->
   controller -> any option -> unit
 
+exception BadCopyPaste
+
 (* [copy_paste c a b] try to copy subtree originating at node a to node b *)
 val copy_paste:
     notification:notifier ->

src/session/itp_server.ml

@@ -1355,10 +1355,16 @@ 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 d.cont)
-          ~callback_pa:(callback_update_tree_proof d.cont)
-          ~callback_tr:(callback_update_tree_transform)
-          d.cont from_any to_any
+        begin
+          try
+            C.copy_paste
+              ~notification:(notify_change_proved d.cont)
+              ~callback_pa:(callback_update_tree_proof d.cont)
+              ~callback_tr:(callback_update_tree_transform)
+              d.cont from_any to_any
+          with C.BadCopyPaste ->
+               P.notify (Message (Error "invalid copy"))
+        end
     | Get_file_contents f          ->
         read_and_send f
     | Save_file_req (name, text)   ->

tests/demo-itp.mlw

 
 
+module TestCopyPaste
+
+ use import int.Int
+
+ goal g1: 1=2 /\ 3=4
+
+ goal g2: 5=6 /\ 7=8 /\ 9=10
+
+end
+
 module M
   use import int.Int
 
@@ -10,11 +20,11 @@ end
 module TestWarnings
 
   use import int.Int
-  
+
   function f (x y : int) :int = x
-  
+
   axiom a : forall x:int. x*x >= 0
-  
+
   goal g1: forall z:int. 42 > 0
 
   goal g2: let z=1 in 42 > 0
@@ -30,7 +40,7 @@ module TestTaskPrinting
   goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 +
            averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0
 
-  goal g2: let x = 1 in x + 1 >= 0
+  (*goal g2: let x = 1 in x + 1 >= 0*)
 
   goal g3: let x = 1 in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0
 
@@ -66,11 +76,11 @@ end
 module TestInduction
 
   use import int.Int
-  
+
   predicate p int
-  
+
   goal g : forall n. p n
-  
+
 end
 
 module TestInfixSymbols
@@ -106,9 +116,9 @@ module TestRewritePoly
   use import int.Int
   use import list.List
   use import list.Append
-  
+
   goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil)
-  
+
 end
 
 

tests/demo-itp/why3session.xml

@@ -6,14 +6,52 @@
 <prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="4" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../demo-itp.mlw">
+<theory name="TestCopyPaste" sum="22d35cc9b3a5547f481892208f0547bc">
+ <goal name="g1">
+ <transf name="split_goal_wp" >
+  <goal name="g1.0">
+  <proof prover="6"><result status="unknown" time="0.00"/></proof>
+  </goal>
+  <goal name="g1.1">
+  <proof prover="2"><result status="unknown" time="0.00"/></proof>
+  <proof prover="3"><result status="unknown" time="0.00"/></proof>
+  <proof prover="4"><result status="unknown" time="0.01"/></proof>
+  <proof prover="6" timelimit="1"><result status="unknown" time="0.01"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="g2">
+ <transf name="split_goal_wp" >
+  <goal name="g2.0">
+  <proof prover="6"><result status="unknown" time="0.01"/></proof>
+  </goal>
+  <goal name="g2.1">
+  <proof prover="2"><result status="unknown" time="0.00"/></proof>
+  <proof prover="3"><result status="unknown" time="0.00"/></proof>
+  <proof prover="4"><result status="unknown" time="0.01"/></proof>
+  <proof prover="6" timelimit="1"><result status="unknown" time="0.01"/></proof>
+  </goal>
+  <goal name="g2.2">
+  <proof prover="5"><result status="timeout" time="4.89"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
 <theory name="M" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="TestTaskPrinting" sum="01fbd777d08f356d2f390e335249eeb9">
+<theory name="TestWarnings" sum="aeca3388f2e65d42f78feba3152450b6">
  <goal name="g1">
  </goal>
  <goal name="g2">
  </goal>
+</theory>
+<theory name="TestTaskPrinting" sum="801f15aa4345fd2ac2cb9efbcefa4d4b">
+ <goal name="g1">
+ </goal>
  <goal name="g3">
  </goal>
  <goal name="g4">
@@ -26,6 +64,8 @@
  </goal>
  <goal name="g8">
  </goal>
+ <goal name="g2">
+ </goal>
 </theory>
 <theory name="TestAutomaticIntro" sum="6566463f1ee0314d808add53aa21307c">
  <goal name="g">
@@ -34,9 +74,9 @@
 <theory name="TestInduction" sum="7cd4f889593553a3efe96040db1cbe94">
  <goal name="g">
  <transf name="induction" arg1="n">
-  <goal name="g.0">
+  <goal name="g.0" expl="base case">
   </goal>
-  <goal name="g.1">
+  <goal name="g.1" expl="recursive case">
   </goal>
  </transf>
  </goal>
@@ -75,32 +115,32 @@
  </goal>
  <goal name="power_sum" proved="true">
  <transf name="induction" proved="true" arg1="n">
-  <goal name="power_sum.0" proved="true">
+  <goal name="power_sum.0" expl="base case" proved="true">
   <proof prover="1"><result status="valid" time="0.01"/></proof>
   <proof prover="2"><result status="unknown" time="1.00"/></proof>
   </goal>
-  <goal name="power_sum.1" proved="true">
+  <goal name="power_sum.1" expl="recursive case" proved="true">
   <proof prover="0" obsolete="true"><result status="valid" time="0.87" steps="15"/></proof>
   <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
   <proof prover="2" obsolete="true"><result status="unknown" time="1.01"/></proof>
   <transf name="case" proved="true" arg1="(n=0)">
-   <goal name="power_sum.1.0" proved="true">
+   <goal name="power_sum.1.0" expl="true case (recursive case)" proved="true">
    <proof prover="1"><result status="valid" time="0.01"/></proof>
    <proof prover="2"><result status="unknown" time="1.00"/></proof>
    </goal>
-   <goal name="power_sum.1.1" proved="true">
+   <goal name="power_sum.1.1" expl="false case (recursive case)" proved="true">
    <proof prover="0"><result status="timeout" time="1.00"/></proof>
    <proof prover="1"><result status="timeout" time="1.00"/></proof>
    <proof prover="2"><result status="unknown" time="1.10"/></proof>
    <proof prover="3"><result status="unknown" time="0.00"/></proof>
    <transf name="instantiate" proved="true" arg1="Hrec" arg2="(n-1)">
-    <goal name="power_sum.1.1.0" proved="true">
+    <goal name="power_sum.1.1.0" expl="false case (recursive case)" proved="true">
     <proof prover="0"><result status="timeout" time="1.01"/></proof>
     <proof prover="1"><result status="timeout" time="1.00"/></proof>
     <proof prover="2"><result status="timeout" time="1.00"/></proof>
     <proof prover="3"><result status="unknown" time="0.00"/></proof>
     <transf name="replace" proved="true" arg1="(n+m)" arg2="((n-1)+m+1)">
-     <goal name="power_sum.1.1.0.0" proved="true">
+     <goal name="power_sum.1.1.0.0" expl="false case (recursive case)" proved="true">
      <proof prover="0"><result status="valid" time="0.08" steps="14"/></proof>
      <proof prover="1"><result status="timeout" time="1.00"/></proof>
      <proof prover="2"><result status="timeout" time="1.00"/></proof>
@@ -114,9 +154,9 @@
    </goal>
   </transf>
   <transf name="instantiate" proved="true" arg1="Hrec" arg2="(n-1)">
-   <goal name="power_sum.1.0" proved="true">
+   <goal name="power_sum.1.0" expl="recursive case" proved="true">
    <transf name="replace" proved="true" arg1="(n+m)" arg2="((n-1)+m+1)">
-    <goal name="power_sum.1.0.0" proved="true">
+    <goal name="power_sum.1.0.0" expl="recursive case" proved="true">
     <proof prover="0"><result status="valid" time="0.22" steps="29"/></proof>
     <proof prover="1"><result status="timeout" time="1.00"/></proof>
     <proof prover="2"><result status="timeout" time="1.00"/></proof>
@@ -128,7 +168,7 @@
    </goal>
   </transf>
   <transf name="replace" arg1="(n+m)" arg2="((n-1)+m+1)">
-   <goal name="power_sum.1.0">
+   <goal name="power_sum.1.0" expl="recursive case">
    <proof prover="0"><result status="timeout" time="1.00"/></proof>
    <proof prover="1"><result status="timeout" time="1.00"/></proof>
    <proof prover="2"><result status="unknown" time="1.74"/></proof>