Merge branch 'master' of gitlab.inria.fr:why3/why3 into improve_elim_let

examples/bts/231_destruct/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../231_destruct.mlw">
+<file>
+<path name=".."/>
+<path name="231_destruct.mlw"/>
 <theory name="T">
  <goal name="G">
  <transf name="destruct" arg1="H">

examples/isqrt/why3session.xml

@@ -5,14 +5,15 @@
 <prover id="0" name="Z3" version="4.6.0" timelimit="11" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.5" timelimit="11" steplimit="0" memlimit="1000"/>
-<file  proved="true">
+<file proved="true">
 <path name=".."/>
 <path name="isqrt.mlw"/>
 <theory name="Square" proved="true">
  <goal name="sqr_non_neg" proved="true">
- <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.00" steps="2"/></proof>
  </goal>
  <goal name="sqr_increasing" proved="true">
  <proof prover="0"><result status="valid" time="0.01"/></proof>

src/core/term.mli

@@ -171,6 +171,9 @@ val t_open_branch : term_branch -> pattern * term
 val t_open_quant : term_quant -> vsymbol list * trigger * term
 
 val t_open_bound_with : term -> term_bound -> term
+(** [t_open_bound_with t tb] opens the binding [tb] and immediately
+    replaces the corresponding bound variable with [t] *)
+
 val t_clone_bound_id : term_bound -> preid
 
 (** open bindings with optimized closing callbacks *)

src/core/trans.mli

@@ -58,25 +58,43 @@ val fold_map   : (task_hd -> 'a * 'b -> ('a * 'b)     ) -> 'a -> 'b -> 'b trans
 val fold_map_l : (task_hd -> 'a * 'b -> ('a * 'b) list) -> 'a -> 'b -> 'b tlist
 
 val decl   : (decl -> decl list     ) -> task -> task trans
-(** [decl f t1 t2] adds to task [t1] the declarations [f d] for each
-    declaration [d] of task [t2]. (similar to a "flat_map"
-    operation) *)
+(** [decl f t1 t2] appends to task [t1] the set of declarations [f d]
+    for each declaration [d] of task [t2], similarly to a "flat_map"
+    operation on lists.
+
+    For example, if [t2] is made of the two declarations [d1] and [d2]
+    in that order, if [f d1 = [d11;d12]] and [f d2 = [d21;d22]], then
+    the resulting task contains the declarations of [t1] followed by
+    [d11;d12;d21;d22] *)
 
 val decl_l : (decl -> decl list list) -> task -> task tlist
-(** [decl_l f t1 t2]: on each declaration d of task [t2]
-    (with [f d] = [ld_1; ld_2; ... ld_n]), create n duplicates (newt_i)
-    of t1 with the declaration d_i replaced by ld_i.
+(** [decl_f f t1 t2] produces a set of tasks obtained by appending new
+    declarations to task [t1].  It iterates on each declaration [d]
+    appearing in [t2]: if [f d = [ld_1; ld_2; ... ld_n]] then it
+    produces [n] tasks [t'1;..;t'n], where [ld_i] is appended to [t'i].
+    The operation on remaining tasks of [t2] are then applied to each task [t'i].
+
+    For example, if [t2] is made of the two declarations [d1] and [d2]
+    in that order, if [f d1 = [[d111;d112];[d12]]] and [f d2 =
+    [[d21];[d221;d222]]], then the result is made of the 4 tasks
+    [t1;d111;d112;d21], [t1;d111;d112;d221;d222], [t1;d12;d21] and
+    [t1;d12;d221;d222] *)
 
-    Note for example that this 'decl_l (fun d -> [[d]; [d]])' will
-    duplicate the task on each declaration and probably run forever.
-*)
 
 type diff_decl =
   | Goal_decl of Decl.decl
   | Normal_decl of Decl.decl
+(* FIXME: the differenciation of goal versus normal decl should be made using
+  [is_goal d = match d.decl_node with
+  | Prop(Goal,_) -> true | _ -> false] *)
 
 val decl_goal_l: (decl -> diff_decl list list) -> task -> task tlist
-(** [decl_goal_l f t1 t2] does the same as decl_l except that it can
+(** FIXME:
+     * make this comment more comprehensible
+     * there should be no "disallowed cases": as soon as a goal is produced, no new decls should be added anymore in the resulting tasks
+
+
+    [decl_goal_l f t1 t2] does the same as decl_l except that it can
     differentiate a new axiom added to a task from a new goal added to a task.
     In case of a new axiom, everything works as in decl_l. When a new goal [ng]
     is generated, it is remembered so that it can replace the old_goal when the

src/ide/gconfig.ml

@@ -529,9 +529,10 @@ let init () =
   resize_images 20;
   Debug.dprintf debug " done.@."
 
-let show_legend_window () =
+let show_legend_window ~parent () =
   let dialog =
     GWindow.dialog
+      ~modal:true ~parent
       ~title:"Why3: legend of icons" ~icon:!why_icon
       ()
   in
@@ -597,9 +598,10 @@ let show_legend_window () =
   dialog#destroy ()
 
 
-let show_about_window () =
+let show_about_window ~parent () =
   let about_dialog =
     GWindow.about_dialog
+      ~parent
       ~name:"The Why3 Verification Platform"
       ~authors:["François Bobot";
                 "Jean-Christophe Filliâtre";
@@ -1130,9 +1132,9 @@ let editors_page c (notebook:GPack.notebook) =
   Mprover.iter add_prover (Whyconf.get_provers c.config)
 
 
-let preferences (c : t) =
+let preferences ~parent (c : t) =
   let dialog = GWindow.dialog
-    ~modal:true ~icon:(!why_icon)
+    ~modal:true ~parent ~icon:(!why_icon)
     ~title:"Why3: preferences" ()
   in
   let vbox = dialog#vbox in
@@ -1190,19 +1192,20 @@ let run_auto_detection gconfig =
 
 (*let () = Debug.dprintf debug "[config] end of configuration initialization@."*)
 
-let uninstalled_prover_dialog ~height ~callback c unknown =
+let uninstalled_prover_dialog ~parent ~callback c unknown =
   let others,names,versions =
     Whyconf.unknown_to_known_provers
       (Whyconf.get_provers c.config) unknown
   in
   let dialog = GWindow.dialog
-                 ~icon:(!why_icon) ~modal:true
+                 ~icon:(!why_icon) ~modal:true ~parent
                  ~title:"Why3: Uninstalled prover" ()
   in
   let vbox = dialog#vbox in
   let vbox_pack = vbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
   let hbox = GPack.hbox ~packing:vbox_pack () in
   let hbox_pack = hbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
+  let height = parent#misc#allocation.Gtk.height * 3 / 4 in
   let scrollview =
     GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC ~height
       ~packing:hbox_pack ()

src/ide/gconfig.mli

@@ -112,12 +112,12 @@ val image_failure_obs : GdkPixbuf.pixbuf ref
 (* miscellaneous dialogs *)
 (*************************)
 
-val show_legend_window : unit -> unit
-val show_about_window : unit -> unit
-val preferences : t -> unit
+val show_legend_window : parent:#GWindow.window_skel -> unit -> unit
+val show_about_window : parent:#GWindow.window_skel -> unit -> unit
+val preferences : parent:#GWindow.window_skel -> t -> unit
 
 val uninstalled_prover_dialog :
-  height:int ->
+  parent:#GWindow.window_skel ->
   callback: (Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit) ->
   t -> Whyconf.prover -> unit
 

src/ide/why3ide.ml

@@ -17,6 +17,8 @@ open Ide_utils
 open History
 open Itp_communication
 
+module GSourceView = GSourceView2
+
 external reset_gc : unit -> unit = "ml_reset_gc"
 
 let debug = Debug.lookup_flag "ide_info"
@@ -200,7 +202,7 @@ let (why_lang, any_lang) =
   let main = Whyconf.get_main gconfig.config in
   let load_path = Filename.concat (Whyconf.datadir main) "lang" in
   let languages_manager =
-    GSourceView2.source_language_manager ~default:true
+    GSourceView.source_language_manager ~default:true
   in
   languages_manager#set_search_path
     (load_path :: languages_manager#search_path);
@@ -238,15 +240,15 @@ let try_convert s =
 
 (* For each view, we have to recreate the tags *)
 let create_colors v =
-  let premise_tag (v: GSourceView2.source_view) = v#buffer#create_tag
+  let premise_tag (v: GSourceView.source_view) = v#buffer#create_tag
       ~name:"premise_tag" [`BACKGROUND gconfig.premise_color] in
-  let neg_premise_tag (v: GSourceView2.source_view) = v#buffer#create_tag
+  let neg_premise_tag (v: GSourceView.source_view) = v#buffer#create_tag
       ~name:"neg_premise_tag" [`BACKGROUND gconfig.neg_premise_color] in
-  let goal_tag (v: GSourceView2.source_view) = v#buffer#create_tag
+  let goal_tag (v: GSourceView.source_view) = v#buffer#create_tag
       ~name:"goal_tag" [`BACKGROUND gconfig.goal_color] in
-  let error_line_tag (v: GSourceView2.source_view) = v#buffer#create_tag
+  let error_line_tag (v: GSourceView.source_view) = v#buffer#create_tag
       ~name:"error_line_tag" [`BACKGROUND gconfig.error_line_color] in
-  let error_tag (v: GSourceView2.source_view) = v#buffer#create_tag
+  let error_tag (v: GSourceView.source_view) = v#buffer#create_tag
       ~name:"error_tag" [`BACKGROUND gconfig.error_color_bg] in
   let _ : GText.tag = premise_tag v in
   let _ : GText.tag = neg_premise_tag v in
@@ -256,7 +258,7 @@ let create_colors v =
   ()
 
 (* Erase all the source location tags in a source file *)
-let erase_color_loc (v:GSourceView2.source_view) =
+let erase_color_loc (v:GSourceView.source_view) =
   let buf = v#buffer in
   buf#remove_tag_by_name "premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
   buf#remove_tag_by_name "neg_premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
@@ -288,7 +290,7 @@ let exit_function_unsafe () =
      source has been modified
    - label_of_tab is the mutable title of the tab
 *)
-let source_view_table : (int * GSourceView2.source_view * bool ref * GMisc.label) Hstr.t =
+let source_view_table : (int * GSourceView.source_view * bool ref * GMisc.label) Hstr.t =
   Hstr.create 14
 
 (* The corresponding file does not have a source view *)
@@ -300,7 +302,7 @@ let get_source_view_table (file:string) =
   | exception Not_found -> raise (Nosourceview file)
 
 (* This returns the source_view of a file *)
-let get_source_view (file: string) : GSourceView2.source_view =
+let get_source_view (file: string) : GSourceView.source_view =
   match Hstr.find source_view_table file with
   | (_, v, _, _) -> v
   | exception Not_found -> raise (Nosourceview file)
@@ -308,7 +310,7 @@ let get_source_view (file: string) : GSourceView2.source_view =
 (* Saving function for sources *)
 let save_sources () =
   Hstr.iter
-    (fun k (_n, (s: GSourceView2.source_view), b, _l) ->
+    (fun k (_n, (s: GSourceView.source_view), b, _l) ->
       if !b then
         let text_to_save = s#source_buffer#get_text () in
         send_request (Save_file_req (k, text_to_save))
@@ -395,12 +397,8 @@ let window_title =
   | None -> "Why3 Interactive Proof Session"
 
 let main_window : GWindow.window =
-  let w = GWindow.window
-            ~allow_grow:true ~allow_shrink:true
-            ~width:gconfig.window_width
-            ~height:gconfig.window_height
-            ~title:window_title ()
-  in
+  let w = GWindow.window ~title:window_title () in
+  w#resize ~width:gconfig.window_width ~height:gconfig.window_height;
   (* callback to record the new size of the main window when changed, so
    that on restart the window size is the same as the last session *)
   let (_ : GtkSignal.id) =
@@ -467,13 +465,15 @@ let (_ : GtkSignal.id) =
 
 let hp = GPack.paned `HORIZONTAL ~packing:hb#add ()
 
-let scrollview =
+(** {2 view for the session tree} *)
+let scrolled_session_view =
   let sv =
     GBin.scrolled_window
       ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
-      ~width:gconfig.tree_width ~shadow_type:`ETCHED_OUT
+      ~shadow_type:`ETCHED_OUT
       ~packing:hp#add ()
   in
+  hp#set_position gconfig.tree_width;
   let (_ : GtkSignal.id) =
     sv#misc#connect#size_allocate
       ~callback:
@@ -481,14 +481,6 @@ let scrollview =
        gconfig.tree_width <- w)
   in sv
 
-(** {2 view for the session tree} *)
-let scrolled_session_view =
-  GBin.scrolled_window
-    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
-    ~shadow_type:`ETCHED_OUT
-    ~packing:scrollview#add_with_viewport
-    ()
-
 (* Vertical pan *)
 let vpan222 = GPack.paned `VERTICAL ~packing:hp#add ()
 
@@ -661,7 +653,7 @@ let (_ : GtkSignal.id) =
 
 
 let task_view =
-  GSourceView2.source_view
+  GSourceView.source_view
     ~editable:false
     ~cursor_visible:false
     ~show_line_numbers:true
@@ -690,7 +682,7 @@ let create_source_view =
             ~shadow_type:`ETCHED_OUT
             ~packing:scrolled_source_view#add () in
         let source_view =
-          GSourceView2.source_view
+          GSourceView.source_view
             ~auto_indent:gconfig.allow_source_editing
             ~insert_spaces_instead_of_tabs:true ~tab_width:2
             ~show_line_numbers:true
@@ -781,7 +773,7 @@ let scrolled_edited_view =
     ~shadow_type:`ETCHED_OUT ~packing:edited_tab#add ()
 
 let edited_view =
-  GSourceView2.source_view
+  GSourceView.source_view
     ~editable:false
     ~show_line_numbers:true
     ~packing:scrolled_edited_view#add
@@ -799,7 +791,7 @@ let scrolled_output_view =
     ~shadow_type:`ETCHED_OUT ~packing:output_tab#add ()
 
 let output_view =
-  GSourceView2.source_view
+  GSourceView.source_view
     ~editable:false
     ~show_line_numbers:true
     ~packing:scrolled_output_view#add
@@ -818,7 +810,7 @@ let scrolled_counterexample_view =
     ~shadow_type:`ETCHED_OUT ~packing:counterexample_tab#add ()
 
 let counterexample_view =
-  GSourceView2.source_view
+  GSourceView.source_view
     ~editable:false
     ~show_line_numbers:true
     ~packing:scrolled_counterexample_view#add
@@ -958,7 +950,7 @@ let update_monitor =
 (* Current position in the source files *)
 let current_cursor_loc = ref None
 
-let move_to_line ~yalign (v : GSourceView2.source_view) line =
+let move_to_line ~yalign (v : GSourceView.source_view) line =
   let line = max 0 (line - 1) in
   let line = min line v#buffer#line_count in
   let it = v#buffer#get_iter (`LINE line) in
@@ -1077,7 +1069,7 @@ let convert_color (color: color): string =
   | Error_line_color -> "error_line_tag"
 
 let color_line ~color loc =
-  let color_line (v:GSourceView2.source_view) ~color l =
+  let color_line (v:GSourceView.source_view) ~color l =
     let buf = v#buffer in
     let top = buf#start_iter in
     let start = top#forward_lines (l-1) in
@@ -1102,7 +1094,7 @@ let color_loc ?(ce=false) ~color loc =
 
   (* This apply a background [color] on a location given by its file view [v] line
      [l] beginning char [b] and end char [e]. *)
-  let color_loc (v:GSourceView2.source_view) ~color l b e =
+  let color_loc (v:GSourceView.source_view) ~color l b e =
     let buf = v#buffer in
     let top = buf#start_iter in
     let start = top#forward_lines (l-1) in
@@ -1795,7 +1787,7 @@ let (_: GMenu.menu_item) =
 
 let (_: GMenu.menu_item) =
   let callback () =
-    Gconfig.preferences gconfig;
+    Gconfig.preferences ~parent:main_window gconfig;
     make_sources_editable gconfig.allow_source_editing;
     send_session_config_to_server ()
   in
@@ -1908,12 +1900,12 @@ let help_factory = new menu_factory help_menu ~accel_path:"<Why3-Main>/Help/" ~a
 let (_ : GMenu.menu_item) =
   help_factory#add_item
     "Legend"
-    ~callback:show_legend_window
+    ~callback:(show_legend_window ~parent:main_window)
 
 let (_ : GMenu.menu_item) =
   help_factory#add_item
     "About"
-    ~callback:show_about_window
+    ~callback:(show_about_window ~parent:main_window)
 
 (*****************************************************************)
 (* "Tools" submenus for strategies, provers, and transformations *)
@@ -2248,11 +2240,7 @@ let check_uninstalled_prover =
       let callback p u =
         send_request (Set_prover_policy(p,u))
       in
-      (* The gconfig.window_height is always the height of the window thanks to
-         the callback to size_allocate. By default, this dialog has 3/4 the
-         height of the main window. *)
-      let height = 3 * gconfig.window_height / 4 in
-      uninstalled_prover_dialog ~height ~callback gconfig p
+      uninstalled_prover_dialog ~parent:main_window ~callback gconfig p
     end
 
 let treat_notification n =