Commit 5a92d21d authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'new_ide'

parents 240666a1 929d29c6
......@@ -17,7 +17,12 @@ open Stdlib
let debug = Debug.register_flag "python"
~desc:"mini-python plugin debug flag"
(* NO! this will be executed at plugin load, thus
disabling the warning for ALL WHY3 USERS even if they don't
use the python front-end
let () = Debug.set_flag Dterm.debug_ignore_unused_var
*)
let mk_id ~loc name =
{ id_str = name; id_lab = []; id_loc = loc }
......
......@@ -563,10 +563,12 @@ let debug_ignore_unused_var = Debug.register_info_flag "ignore_unused_vars"
~desc:"Suppress@ warnings@ on@ unused@ variables"
let check_used_var t vs =
if not (Debug.test_flag debug_ignore_unused_var) then
let s = vs.vs_name.id_string in
if (s = "" || s.[0] <> '_') && t_v_occurs vs t = 0 then
Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s
if Debug.test_noflag debug_ignore_unused_var then
begin
let s = vs.vs_name.id_string in
if (s = "" || s.[0] <> '_') && t_v_occurs vs t = 0 then
Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s
end
let check_exists_implies f = match f.t_node with
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f,{ t_node = Ttrue }) },_)
......
......@@ -1042,9 +1042,11 @@ let display_warnings () =
print_message ~kind:1 ~notif_kind:"warning" "%s" msg
end
let print_message ~kind ~notif_kind fmt =
display_warnings (); print_message ~kind ~notif_kind fmt
let () =
Warning.set_hook (fun ?loc s -> record_warning ?loc s; display_warnings ())
(**** Monitor *****)
......@@ -1420,10 +1422,10 @@ let interp_ide cmd =
let s = List.fold_left (fun acc x -> (fst x) ^ ": " ^
(snd x) ^ "\n" ^ acc) "" ide_command_list in
clear_command_entry ();
message_zone#buffer#set_text s
print_message ~kind:1 ~notif_kind:"Info" "%s" s
| _ ->
clear_command_entry ();
message_zone#buffer#set_text ("Error: " ^ cmd ^ "\nPlease report.")
print_message ~kind:1 ~notif_kind:"error" "Error: %s\nPlease report." cmd
let interp cmd =
(* TODO: do some preprocessing for queries, or leave everything to server ? *)
......@@ -1555,36 +1557,6 @@ let (_ : GtkSignal.id) =
in
goals_view#event#connect#key_press ~callback
(*************************************)
(* 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 (_ : GMenu.menu_item) = exp_factory#add_item ~callback:copy "Copy"
let (_ : GMenu.menu_item) = exp_factory#add_item ~callback:paste "Paste"
(*********************************)
(* add a new file in the project *)
(*********************************)
......@@ -2050,6 +2022,8 @@ let bisect_item =
create_menu_item tools_factory "Bisect on external proof"
"Search for a maximal set of hypotheses to remove before calling a prover"
let ( _ : GMenu.menu_item) = tools_factory#add_separator ()
let focus_item =
create_menu_item tools_factory "Focus"
"Focus on proof node"
......@@ -2058,6 +2032,14 @@ let unfocus_item =
create_menu_item tools_factory "Unfocus"
"Unfocus"
let ( _ : GMenu.menu_item) = tools_factory#add_separator ()
let copy_item = create_menu_item tools_factory "Copy" "Copy the current tree node"
let paste_item = create_menu_item tools_factory "Paste"
"Paste the copied node below the current node"
let () =
let on_selected_rows ~multiple ~notif_kind ~action f () =
match get_selected_row_references () with
......@@ -2103,6 +2085,36 @@ let () =
~callback:(fun () -> send_request Unfocus_req)
(*************************************)
(* Copy paste *)
(*************************************)
(* 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;
paste_item#misc#set_sensitive true
| _ ->
saved_copy := None;
paste_item#misc#set_sensitive false
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 () =
paste_item#misc#set_sensitive false;
connect_menu_item copy_item ~callback:copy;
connect_menu_item paste_item ~callback:paste
(* the command-line *)
......@@ -2321,5 +2333,5 @@ let () =
(fun () -> List.iter treat_notification (get_notified ()); true);
main_window#add_accel_group accel_group;
main_window#set_icon (Some !Gconfig.why_icon);
message_zone#buffer#set_text "Welcome to Why3 IDE\ntype 'help' for help";
print_message ~kind:1 ~notif_kind:"Info" "Welcome to Why3 IDE\ntype 'help' for help\n";
GMain.main ()
......@@ -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
......
......@@ -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 ->
......
......@@ -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) ->
......
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
......@@ -7,6 +17,20 @@ module M
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
end
module TestTaskPrinting
use import int.Int
......@@ -16,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
......@@ -52,11 +76,11 @@ end
module TestInduction
use import int.Int
predicate p int
goal g : forall n. p n
end
module TestInfixSymbols
......@@ -92,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
......
......@@ -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>
......
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