gmain.ml 67.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14


open Format

15
open Why3
16 17
open Whyconf
open Gconfig
18
open Stdlib
François Bobot's avatar
François Bobot committed
19
open Debug
20

21
module C = Whyconf
François Bobot's avatar
François Bobot committed
22

23 24 25 26 27 28 29 30 31 32 33
external reset_gc : unit -> unit = "ml_reset_gc"

(* Setting a Gc.alarm is pointless; the function has to be called manually
   before each lablgtk operation. Indeed, each major slice resets
   caml_extra_heap_resources to zero, but alarms are executed only at
   finalization time, that is, after a full collection completes. Note that
   manual calls can fail to prevent extraneous collections too, if a major
   slice happens right in the middle of a sequence of lablgtk operations due
   to memory starvation. Hopefully, it seldom happens. *)
let () = reset_gc ()

34
let debug = Debug.lookup_flag "ide_info"
35 36 37 38 39

(************************)
(* parsing command line *)
(************************)

40
let files = Queue.create ()
41
let opt_parser = ref None
42 43

let spec = Arg.align [
44
  "-F", Arg.String (fun s -> opt_parser := Some s),
45
      "<format> select input format (default: \"why\")";
46 47
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
48
(*
49
  "-f",
50
   Arg.String (fun s -> input_files := s :: !input_files),
51
   "<file> add file to the project (ignored if it is already there)";
52 53 54 55
*)
]

let usage_str = sprintf
56
  "Usage: %s [options] [<file.why>|<project directory>]..."
57 58
  (Filename.basename Sys.argv.(0))

59 60 61 62 63 64
let gconfig = try
  let config, base_config, env =
    Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in
  if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
  Gconfig.load_config config base_config env;
  Gconfig.config ()
65

66 67 68
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
69

70
let () =
MARCHE Claude's avatar
MARCHE Claude committed
71
  Debug.dprintf debug "[GUI] Init the GTK interface...@?";
72 73 74 75
  ignore (GtkMain.Main.init ());
  Debug.dprintf debug " done.@.";
  Gconfig.init ()

76
let (why_lang, any_lang) =
77
  let main = Gconfig.get_main () in
78 79 80 81 82 83
  let load_path = Filename.concat (datadir main) "lang" in
  let languages_manager =
    GSourceView2.source_language_manager ~default:true
  in
  languages_manager#set_search_path
    (load_path :: languages_manager#search_path);
84
  let why_lang =
85
    match languages_manager#language "why3" with
86
    | None ->
87
        eprintf "language file for 'why3' not found in directory %s@."
88 89
          load_path;
        exit 1
90 91 92 93 94 95
    | Some _ as l -> l in
  let any_lang filename =
    match languages_manager#guess_language ~filename () with
    | None -> why_lang
    | Some _ as l -> l in
  (why_lang, any_lang)
96

97
(* Borrowed from Frama-C src/gui/source_manager.ml:
98 99 100 101 102 103 104 105 106 107 108 109 110
Try to convert a source file either as UTF-8 or as locale. *)
let try_convert s =
  try
    if Glib.Utf8.validate s then s else Glib.Convert.locale_to_utf8 s
  with Glib.Convert.Error _ ->
    try
      Glib.Convert.convert_with_fallback
        ~fallback:"#neither UTF-8 nor locale nor ISO-8859-15#"
        ~to_codeset:"UTF-8"
        ~from_codeset:"ISO_8859-15"
        s
    with Glib.Convert.Error _ as e -> Printexc.to_string e

111
let source_text fname =
112 113 114 115 116 117 118 119 120
  try
    let ic = open_in fname in
    let size = in_channel_length ic in
    let buf = String.create size in
    really_input ic buf 0 size;
    close_in ic;
    try_convert buf
  with e when not (Debug.test_flag Debug.stack_trace) ->
    "Error while opening or reading file '" ^ fname ^ "':\n" ^ (Printexc.to_string e)
121 122 123 124 125 126 127 128 129

(***************)
(* Main window *)
(***************)

let w = GWindow.window
  ~allow_grow:true ~allow_shrink:true
  ~width:gconfig.window_width
  ~height:gconfig.window_height
MARCHE Claude's avatar
MARCHE Claude committed
130
  ~title:"Why3 Interactive Proof Session" ()
131

MARCHE Claude's avatar
MARCHE Claude committed
132 133 134
let () =
  w#set_icon (Some !Gconfig.why_icon)

135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
let (_ : GtkSignal.id) =
  w#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=w;Gtk.height=h} ->
       gconfig.window_height <- h;
       gconfig.window_width <- w)

let vbox = GPack.vbox ~packing:w#add ()

(* Menu *)

let menubar = GMenu.menu_bar ~packing:vbox#pack ()

let factory = new GMenu.factory menubar

let accel_group = factory#accel_group

MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156 157 158 159 160
let hb = GPack.hbox ~packing:vbox#add ()

let left_scrollview =
  try
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
      ~packing:(hb#pack ~expand:false) ()
  with Gtk.Error _ -> assert false

let () = left_scrollview#set_shadow_type `OUT
161 162 163

let tools_window_vbox =
  try
MARCHE Claude's avatar
MARCHE Claude committed
164
    GPack.vbox ~packing:left_scrollview#add_with_viewport ()
165 166 167
  with Gtk.Error _ -> assert false

let context_frame =
MARCHE Claude's avatar
MARCHE Claude committed
168
  GBin.frame ~label:"Context" ~shadow_type:`ETCHED_OUT
169 170 171 172 173 174 175 176 177 178 179 180
    ~packing:(tools_window_vbox#pack ~expand:false) ()

let context_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
    ~packing:context_frame#add ()

let context_unproved_goals_only = ref true

let () =
  let b1 = GButton.radio_button
    ~packing:context_box#add ~label:"Unproved goals" ()
  in
François Bobot's avatar
François Bobot committed
181 182
  b1#misc#set_tooltip_markup
    "When selected, tools below are applied only to <b>unproved</b> goals";
183 184 185 186 187 188 189
  let (_ : GtkSignal.id) =
    b1#connect#clicked
      ~callback:(fun () -> context_unproved_goals_only := true)
  in
  let b2 = GButton.radio_button
    ~group:b1#group ~packing:context_box#add ~label:"All goals" ()
  in
François Bobot's avatar
François Bobot committed
190 191
  b2#misc#set_tooltip_markup
    "When selected, tools below are applied to all goals";
192 193 194 195 196 197
  let (_ : GtkSignal.id) =
    b2#connect#clicked
      ~callback:(fun () -> context_unproved_goals_only := false)
  in ()


198 199 200 201 202 203 204 205
let strategies_frame =
  GBin.frame ~label:"Strategies" ~shadow_type:`ETCHED_OUT
    ~packing:(tools_window_vbox#pack ~expand:false) ()

let strategies_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:strategies_frame#add ()

206
let provers_frame =
MARCHE Claude's avatar
MARCHE Claude committed
207
  GBin.frame ~label:"Provers" ~shadow_type:`ETCHED_OUT
208 209
    ~packing:(tools_window_vbox#pack ~expand:false) ()

MARCHE Claude's avatar
MARCHE Claude committed
210

211 212 213 214 215 216 217
let provers_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:provers_frame#add ()

let () = provers_frame#set_resize_mode `PARENT

let tools_frame =
MARCHE Claude's avatar
MARCHE Claude committed
218
  GBin.frame ~label:"Tools" ~shadow_type:`ETCHED_OUT
219 220 221 222 223 224
    ~packing:(tools_window_vbox#pack ~expand:false) ()

let tools_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:tools_frame#add ()

225
let monitor_frame =
MARCHE Claude's avatar
MARCHE Claude committed
226
  GBin.frame ~label:"Proof monitoring" ~shadow_type:`ETCHED_OUT
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
    ~packing:(tools_window_vbox#pack ~expand:false) ()

let monitor_box =
  GPack.vbox ~homogeneous:false ~packing:monitor_frame#add ()

let monitor_waiting =
  GMisc.label ~text:"  Waiting: 0" ~packing:monitor_box#add ()

let monitor_scheduled =
  GMisc.label ~text:"Scheduled: 0" ~packing:monitor_box#add ()

let monitor_running =
  GMisc.label ~text:"  Running: 0" ~packing:monitor_box#add ()


242 243 244 245 246 247 248 249 250 251

(* horizontal paned *)

let hp = GPack.paned `HORIZONTAL ~packing:hb#add ()


(* tree view *)
let scrollview =
  try
    GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
MARCHE Claude's avatar
MARCHE Claude committed
252
      ~width:gconfig.tree_width ~shadow_type:`ETCHED_OUT
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
      ~packing:hp#add ()
  with Gtk.Error _ -> assert false

let (_ : GtkSignal.id) =
  scrollview#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=w;Gtk.height=_h} ->
       gconfig.tree_width <- w)




(****************)
(* goals widget *)
(****************)

let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let icon_column = cols#add Gobject.Data.gobject
let status_column = cols#add Gobject.Data.gobject
let time_column = cols#add Gobject.Data.string
274
let index_column = cols#add Gobject.Data.int
275

276 277 278 279
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
let image_renderer = GTree.cell_renderer_pixbuf [ ]
let icon_renderer = GTree.cell_renderer_pixbuf [ ]
280

281 282
let view_name_column =
  GTree.view_column ~title:"Theories/Goals" ()
283

284 285 286 287 288 289
let () =
  view_name_column#pack icon_renderer ;
  view_name_column#add_attribute icon_renderer "pixbuf" icon_column ;
  view_name_column#pack name_renderer;
  view_name_column#add_attribute name_renderer "text" name_column;
  view_name_column#set_resizable true;
290 291 292 293
  view_name_column#set_max_width 800;
(*
  view_name_column#set_alignment 1.0;
*)
294
  ()
295

296 297 298 299
let view_status_column =
  GTree.view_column ~title:"Status"
    ~renderer:(image_renderer, ["pixbuf", status_column])
    ()
300

301 302 303
let view_time_column =
  GTree.view_column ~title:"Time"
    ~renderer:(renderer, ["text", time_column]) ()
304

305 306 307 308 309
let () =
  view_status_column#set_resizable false;
  view_status_column#set_visible true;
  view_time_column#set_resizable false;
  view_time_column#set_visible true
310

311
let goals_model,goals_view =
MARCHE Claude's avatar
MARCHE Claude committed
312
  Debug.dprintf debug "[GUI] Creating tree model...@?";
313 314
  let model = GTree.tree_store cols in
  let view = GTree.view ~model ~packing:scrollview#add () in
315
  let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
316 317 318 319
  let () = view#set_rules_hint true in
  ignore (view#append_column view_name_column);
  ignore (view#append_column view_status_column);
  ignore (view#append_column view_time_column);
320
  Debug.dprintf debug " done@.";
321
  model,view
322

323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359

(******************************)
(* vertical paned on the right*)
(******************************)

let right_vb = GPack.vbox ~packing:hp#add ()

let vp =
  try
    GPack.paned `VERTICAL ~packing:right_vb#add ()
  with Gtk.Error _ -> assert false

let right_hb = GPack.hbox ~packing:(right_vb#pack ~expand:false) ()

(******************)
(* goal text view *)
(******************)

let scrolled_task_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT ~packing:vp#add ()

let (_ : GtkSignal.id) =
  scrolled_task_view#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=_w;Gtk.height=h} ->
       gconfig.task_height <- h)

let task_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ~height:gconfig.task_height
    ()

360 361
let modifiable_sans_font_views = ref [goals_view#misc]
let modifiable_mono_font_views = ref [task_view#misc]
362 363 364 365
let () = task_view#source_buffer#set_language why_lang
let () = task_view#set_highlight_current_line true


366 367 368 369
let clear model = model#clear ()

let image_of_result ~obsolete result =
  match result with
370 371 372 373 374
    | Session.Interrupted -> !image_undone
    | Session.Unedited -> !image_editor
    | Session.JustEdited -> !image_unknown
    | Session.Scheduled -> !image_scheduled
    | Session.Running -> !image_running
375 376
    | Session.InternalFailure _ -> !image_failure
    | Session.Done r -> match r.Call_provers.pr_answer with
377 378 379 380 381 382
        | Call_provers.Valid ->
            if obsolete then !image_valid_obs else !image_valid
        | Call_provers.Invalid ->
            if obsolete then !image_invalid_obs else !image_invalid
        | Call_provers.Timeout ->
            if obsolete then !image_timeout_obs else !image_timeout
383 384
        | Call_provers.OutOfMemory ->
            if obsolete then !image_outofmemory_obs else !image_outofmemory
385 386 387 388 389 390
        | Call_provers.Unknown _ ->
            if obsolete then !image_unknown_obs else !image_unknown
        | Call_provers.Failure _ ->
            if obsolete then !image_failure_obs else !image_failure
        | Call_provers.HighFailure ->
            if obsolete then !image_failure_obs else !image_failure
391

392
(* connecting to the Session model *)
393

394 395 396 397 398 399 400 401
let fan n =
  match n mod 4 with
    | 0 -> "|"
    | 1 | -3 -> "\\"
    | 2 | -2 -> "-"
    | 3 | -1 -> "/"
    | _ -> assert false

François Bobot's avatar
François Bobot committed
402
module S = Session
MARCHE Claude's avatar
MARCHE Claude committed
403

404 405
let session_needs_saving = ref false

MARCHE Claude's avatar
MARCHE Claude committed
406 407
let set_row_status row b =
  if b then
408
    goals_model#set ~row:row#iter ~column:status_column !image_yes
MARCHE Claude's avatar
MARCHE Claude committed
409
  else
410
    goals_model#set ~row:row#iter ~column:status_column !image_unknown
MARCHE Claude's avatar
MARCHE Claude committed
411

412 413
let set_proof_state a =
  let obsolete = a.S.proof_obsolete in
François Bobot's avatar
François Bobot committed
414 415
  let row = a.S.proof_key in
  let res = a.S.proof_state in
416
  goals_model#set ~row:row#iter ~column:status_column
MARCHE Claude's avatar
MARCHE Claude committed
417 418
    (image_of_result ~obsolete res);
  let t = match res with
François Bobot's avatar
François Bobot committed
419 420 421
    | S.Done { Call_provers.pr_time = time } ->
        if gconfig.show_time_limit then
          Format.sprintf "%.2f [%d.0]" time a.S.proof_timelimit
MARCHE Claude's avatar
MARCHE Claude committed
422 423
        else
          Format.sprintf "%.2f" time
424 425
    | S.Unedited -> "(not yet edited)"
    | S.JustEdited -> "(edited)"
François Bobot's avatar
François Bobot committed
426
    | S.InternalFailure _ -> "(internal failure)"
427 428
    | S.Interrupted -> "(interrupted)"
    | S.Scheduled | S.Running ->
429
        Format.sprintf "[limit=%d sec., %d M]"
430
          a.S.proof_timelimit a.S.proof_memlimit
MARCHE Claude's avatar
MARCHE Claude committed
431 432
  in
  let t = if obsolete then t ^ " (obsolete)" else t in
433 434
  (* TODO find a better way to signal arhived row *)
  let t = if a.S.proof_archived then t ^ " (archived)" else t in
435
  goals_model#set ~row:row#iter ~column:time_column t
MARCHE Claude's avatar
MARCHE Claude committed
436

437
let model_index = Hint.create 17
438

439
let get_any_from_iter row =
MARCHE Claude's avatar
MARCHE Claude committed
440
  try
441
    let idx = goals_model#get ~row ~column:index_column in
442
    Hint.find model_index idx
443 444
  with Not_found -> invalid_arg "Gmain.get_any_from_iter"

445
(*
446 447
let get_any (row:Gtk.tree_path) : M.any =
  get_any_from_iter (goals_model#get_iter row)
448 449 450 451 452 453 454 455
*)

let get_any_from_row_reference r = get_any_from_iter r#iter

let get_selected_row_references () =
  List.map
    (fun path -> goals_model#get_row_reference path)
    goals_view#selection#get_selected_rows
456

457
let row_expanded b iter _path =
458
  session_needs_saving := true;
459 460 461
  let expand_g g = goals_view#expand_row g.S.goal_key#path in
  let expand_tr _ tr = goals_view#expand_row tr.S.transf_key#path in
  let expand_m _ m = goals_view#expand_row m.S.metas_key#path in
462
  match get_any_from_iter iter with
François Bobot's avatar
François Bobot committed
463 464 465 466 467
    | S.File f ->
        S.set_file_expanded f b
    | S.Theory t ->
        S.set_theory_expanded t b
    | S.Goal g ->
468 469 470 471 472
        S.set_goal_expanded g b;
        if b then begin
          Session.PHstr.iter expand_tr g.S.goal_transformations;
          Session.Mmetas_args.iter expand_m g.S.goal_metas
        end
François Bobot's avatar
François Bobot committed
473
    | S.Transf tr ->
474 475 476 477 478
        S.set_transf_expanded tr b;
        if b then begin match tr.S.transf_goals with
          | [g] -> expand_g g
          | _ -> ()
        end
François Bobot's avatar
François Bobot committed
479
    | S.Proof_attempt _ -> ()
François Bobot's avatar
François Bobot committed
480
    | S.Metas m ->
481 482
        S.set_metas_expanded m b;
        if b then expand_g m.S.metas_goal
483

484 485 486 487 488 489 490
let current_selected_row = ref None
let current_env_session = ref None
let env_session () =
  match !current_env_session with
    | None -> assert false
    | Some e -> e

491 492
let task_text t =
  Pp.string_of ~max_boxes:42 Pretty.print_task t
493

494
let split_transformation = "split_goal_wp"
495 496 497 498
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"

let update_task_view a =
Andrei Paskevich's avatar
Andrei Paskevich committed
499
  let text =
500 501 502 503
  match a with
    | S.Goal g ->
      if (Gconfig.config ()).intro_premises then
        let trans =
504
          Trans.lookup_transform intro_transformation (env_session()).S.env
505
        in
506
        task_text (try Trans.apply trans (S.goal_task g) with
507
          e -> eprintf "@.%a@." Exn_printer.exn_printer e; raise e)
508
      else
509 510 511
        task_text (S.goal_task g)
    | S.Theory th -> "Theory " ^ th.S.theory_name.Ident.id_string
    | S.File file -> "File " ^ file.S.file_name
512
    | S.Proof_attempt a ->
513
        begin
514
          match a.S.proof_state with
515
            | S.Interrupted -> "proof not yet scheduled for running"
François Bobot's avatar
François Bobot committed
516 517 518 519 520 521
            | S.Unedited ->
              "Interactive proof, not yet edited. Edit with \"Edit\" button"
            | S.JustEdited ->
              "Edited interactive proof. Run it with \"Replay\" button"
            | S.Done
                ({Call_provers.pr_answer = Call_provers.HighFailure} as r) ->
522 523 524
              let b = Buffer.create 37 in
              bprintf b "%a" Call_provers.print_prover_result r;
              Buffer.contents b
Andrei Paskevich's avatar
Andrei Paskevich committed
525
            | S.Done r ->
526 527 528 529 530 531 532 533 534
              let out = r.Call_provers.pr_output in
              begin
                let env = env_session () in
                match S.get_edited_as_abs env.S.session a with
                | None -> out
                | Some f -> (source_text f) ^
                  "\n----------------------------------------------\n\n"
                  ^ out
              end
535 536
            | S.Scheduled-> "proof scheduled but not running yet"
            | S.Running -> "prover currently running"
537 538 539 540
            | S.InternalFailure e ->
              let b = Buffer.create 37 in
              bprintf b "%a" Exn_printer.exn_printer e;
              Buffer.contents b
541 542 543
        end
    | S.Transf tr ->
        "transformation \"" ^ tr.S.transf_name ^ "\""
François Bobot's avatar
François Bobot committed
544 545 546 547 548 549 550 551
   | S.Metas m ->
     let print_meta_args =
       Pp.hov 2 (Pp.print_list Pp.space Pretty.print_meta_arg) in
     let print =
       Pp.print_iter2 Mstr.iter Pp.newline2 Pp.newline Pp.string
         (Pp.indent 2
            (Pp.print_iter1 S.Smeta_args.iter Pp.newline print_meta_args))
     in
552 553 554 555
     (Pp.string_of (Pp.hov 2 print) m.S.metas_added)
 in
 task_view#source_buffer#set_text text;
 task_view#scroll_to_mark `INSERT
François Bobot's avatar
François Bobot committed
556 557


558

François Bobot's avatar
François Bobot committed
559 560

module MA = struct
François Bobot's avatar
François Bobot committed
561 562 563
     type key = GTree.row_reference

     let create ?parent () =
564
       reset_gc ();
565
       session_needs_saving := true;
François Bobot's avatar
François Bobot committed
566 567 568 569 570 571 572 573
       let parent = match parent with
         | None -> None
         | Some r -> Some r#iter
       in
       let iter = goals_model#append ?parent () in
       goals_model#set ~row:iter ~column:index_column (-1);
       goals_model#get_row_reference (goals_model#get_path iter)

François Bobot's avatar
François Bobot committed
574
     let keygen = create
François Bobot's avatar
François Bobot committed
575 576

     let remove row =
577
       session_needs_saving := true;
François Bobot's avatar
François Bobot committed
578 579
       let (_:bool) = goals_model#remove row#iter in ()

580
     let reset () =
581 582
       session_needs_saving := true;
       goals_model#clear ()
François Bobot's avatar
François Bobot committed
583 584 585 586 587 588 589 590 591 592 593

     let idle f =
       let (_ : GMain.Idle.id) = GMain.Idle.add f in ()

     let timeout ~ms f =
       let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
       ()

     let notify_timer_state =
       let c = ref 0 in
       fun t s r ->
594
         reset_gc ();
François Bobot's avatar
François Bobot committed
595 596 597 598 599 600 601
         incr c;
         monitor_waiting#set_text ("Waiting: " ^ (string_of_int t));
         monitor_scheduled#set_text ("Scheduled: " ^ (string_of_int s));
         monitor_running#set_text
           (if r=0 then "Running: 0" else
              "Running: " ^ (string_of_int r)^ " " ^ (fan (!c / 10)))

MARCHE Claude's avatar
MARCHE Claude committed
602
let notify any =
603
  reset_gc ();
604
  session_needs_saving := true;
605
  let row,expanded =
606
    match any with
607
      | S.Goal g -> g.S.goal_key, g.S.goal_expanded
François Bobot's avatar
François Bobot committed
608 609 610
      | S.Theory t -> t.S.theory_key, t.S.theory_expanded
      | S.File f -> f.S.file_key, f.S.file_expanded
      | S.Proof_attempt a -> a.S.proof_key,false
MARCHE Claude's avatar
MARCHE Claude committed
611
      | S.Transf tr ->
612
        tr.S.transf_key,tr.S.transf_expanded
François Bobot's avatar
François Bobot committed
613
      | S.Metas m -> m.S.metas_key,m.S.metas_expanded
614
  in
615 616 617 618 619 620 621 622 623
  (* name is set by notify since upgrade policy may update the prover name *)
  goals_model#set ~row:row#iter ~column:name_column
    (match any with
      | S.Goal g -> S.goal_expl g
      | S.Theory th -> th.S.theory_name.Ident.id_string
      | S.File f -> Filename.basename f.S.file_name
      | S.Proof_attempt a ->
        let p = a.S.proof_prover in
        Pp.string_of_wnl C.print_prover p
François Bobot's avatar
François Bobot committed
624 625 626
      | S.Transf tr -> tr.S.transf_name
      | S.Metas _m -> "Metas..."
   );
627 628 629 630 631 632
  let ind = goals_model#get ~row:row#iter ~column:index_column in
  begin
    match !current_selected_row with
      | Some r when r == ind ->
        update_task_view any
      | _ -> ()
633
  end;
634
  if expanded then goals_view#expand_to_path row#path else
635
    goals_view#collapse_row row#path;
MARCHE Claude's avatar
MARCHE Claude committed
636
  match any with
François Bobot's avatar
François Bobot committed
637 638 639 640 641 642 643
    | S.Goal g ->
        set_row_status row g.S.goal_verified
    | S.Theory th ->
        set_row_status row th.S.theory_verified
    | S.File file ->
        set_row_status row file.S.file_verified
    | S.Proof_attempt a ->
644
        set_proof_state a
François Bobot's avatar
François Bobot committed
645 646
    | S.Transf tr ->
        set_row_status row tr.S.transf_verified
647
    | S.Metas m ->
François Bobot's avatar
François Bobot committed
648
        set_row_status row m.S.metas_verified
649

MARCHE Claude's avatar
MARCHE Claude committed
650 651
let init =
  let cpt = ref (-1) in
652
  fun row any ->
653
    reset_gc ();
MARCHE Claude's avatar
MARCHE Claude committed
654 655 656 657
    let ind = goals_model#get ~row:row#iter ~column:index_column in
    if ind < 0 then
      begin
        incr cpt;
658
        Hint.add model_index !cpt any;
MARCHE Claude's avatar
MARCHE Claude committed
659 660 661 662
        goals_model#set ~row:row#iter ~column:index_column !cpt
      end
    else
      begin
663
        Hint.replace model_index ind any;
MARCHE Claude's avatar
MARCHE Claude committed
664
      end;
665
    (* useless since it has no child: goals_view#expand_row row#path; *)
MARCHE Claude's avatar
MARCHE Claude committed
666
    goals_model#set ~row:row#iter ~column:icon_column
667
      (match any with
MARCHE Claude's avatar
MARCHE Claude committed
668 669 670
         | S.Goal _ -> !image_goal
         | S.Theory _ -> !image_theory
         | S.File _ -> !image_file
François Bobot's avatar
François Bobot committed
671
         | S.Proof_attempt _ -> !image_prover
François Bobot's avatar
François Bobot committed
672 673
         | S.Transf _ -> !image_transf
         | S.Metas _ -> !image_metas);
MARCHE Claude's avatar
MARCHE Claude committed
674
    notify any
MARCHE Claude's avatar
MARCHE Claude committed
675

François Bobot's avatar
François Bobot committed
676 677 678 679
let rec init_any any =
  init (S.key_any any) any;
  S.iter init_any any

680
let uninstalled_prover = Gconfig.uninstalled_prover gconfig
681

François Bobot's avatar
François Bobot committed
682 683 684 685
end

module M = Session_scheduler.Make(MA)

686

MARCHE Claude's avatar
MARCHE Claude committed
687 688
let () = w#add_accel_group accel_group
let () = w#show ()
689

690 691 692 693
(********************)
(* opening database *)
(********************)

694
(** TODO remove that should done only in session *)
695 696 697
let project_dir =
  let fname = Queue.pop files in
  (** The remaining files in [files] are going to be open *)
698 699 700 701
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
702
          Debug.dprintf debug
MARCHE Claude's avatar
MARCHE Claude committed
703
            "[GUI] found directory '%s' for the project@." fname;
704
          fname
705 706
        end
      else
707
        if Queue.is_empty files then (* that was the only file *) begin
MARCHE Claude's avatar
MARCHE Claude committed
708
          Debug.dprintf debug "[GUI] found regular file '%s'@." fname;
709 710 711 712
          let d =
            try Filename.chop_extension fname
            with Invalid_argument _ -> fname
          in
713
          Debug.dprintf debug
MARCHE Claude's avatar
MARCHE Claude committed
714
            "[GUI] using '%s' as directory for the project@." d;
715 716 717 718 719 720 721 722 723 724 725
          Queue.push fname files; (** we need to open [fname] *)
          d
        end
        else begin
          (** The first argument is not a directory and it's not the
              only file *)
          Format.eprintf
            "[Error] @[When@ more@ than@ one@ file@ is@ given@ on@ the@ \
             command@ line@ the@ first@ one@ must@ be@ the@ directory@ \
             of@ the@ session.@]@.";
          Arg.usage spec usage_str; exit 1
726 727 728
        end
    end
  else
729
    fname
730 731 732 733

let () =
  if not (Sys.file_exists project_dir) then
    begin
MARCHE Claude's avatar
MARCHE Claude committed
734
      Debug.dprintf debug "[GUI] '%s' does not exist. \
735
        Creating directory of that name for the project@." project_dir;
736 737 738 739 740 741 742 743 744 745 746 747
      Unix.mkdir project_dir 0o777
    end

let info_window ?(callback=(fun () -> ())) mt s =
  let buttons = match mt with
    | `INFO -> GWindow.Buttons.close
    | `WARNING -> GWindow.Buttons.close
    | `QUESTION -> GWindow.Buttons.ok_cancel
    | `ERROR -> GWindow.Buttons.close
  in
  let d = GWindow.message_dialog
    ~message:s
748
    ~message_type:(mt :> Gtk.Tags.message_type)
749
    ~buttons
750
    ~title:"Why3IDE"
751
    ~icon:(!Gconfig.why_icon)
752
    ~modal:true
753 754 755 756
    ~show:true ()
  in
  let (_ : GtkSignal.id) =
    d#connect#response
757
      ~callback:(function x ->
758 759
                   d#destroy ();
                   if mt <> `QUESTION || x = `OK then callback ())
760 761
  in ()

762 763 764
let file_info = GMisc.label ~text:""
  ~packing:(right_hb#pack ~fill:true) ()

765
let warnings = Queue.create ()
MARCHE Claude's avatar
MARCHE Claude committed
766

767
let record_warning ?loc msg = Queue.push (loc,msg) warnings
MARCHE Claude's avatar
MARCHE Claude committed
768

769 770 771 772 773
let () = Warning.set_hook record_warning

let display_warnings () =
  if Queue.is_empty warnings then () else
    begin
Andrei Paskevich's avatar
Andrei Paskevich committed
774
      Queue.iter
775 776 777 778 779 780 781 782 783 784 785 786 787 788 789
        (fun (loc,msg) ->
          match loc with
            | None ->
              Format.fprintf Format.str_formatter "%s@\n" msg
            | Some l ->
            (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
              Format.fprintf Format.str_formatter "%a: %s@\n"
                Loc.gen_report_position l msg)
        warnings;
      Queue.clear warnings;
      let msg =
        Format.flush_str_formatter ()
      in
  (* file_info#set_text msg; *)
      info_window `WARNING msg
Andrei Paskevich's avatar
Andrei Paskevich committed
790
    end
MARCHE Claude's avatar
MARCHE Claude committed
791

792 793
(* check if provers are present *)
let () =
794
  if C.Mprover.is_empty (C.get_provers gconfig.Gconfig.config) then
795
    begin
François Bobot's avatar
François Bobot committed
796 797
      info_window `ERROR
        "No prover configured.\nPlease run 'why3config --detect-provers' first"
798 799 800 801 802
        ~callback:GMain.quit;
      GMain.main ();
      exit 2;
    end

803
let sched =
804
  try
MARCHE Claude's avatar
MARCHE Claude committed
805
    Debug.dprintf debug "@[<hov 2>[GUI session] Opening session...@\n";
806
    let session,use_shapes =
MARCHE Claude's avatar
MARCHE Claude committed
807 808 809
      if Sys.file_exists project_dir then
        S.read_session project_dir
      else
810
        S.create_session project_dir, false
MARCHE Claude's avatar
MARCHE Claude committed
811
    in
812
    let env,(_:bool),(_:bool) =
813 814
      M.update_session ~allow_obsolete:true ~release:false ~use_shapes
        session gconfig.env gconfig.Gconfig.config
815
    in
MARCHE Claude's avatar
MARCHE Claude committed
816
    Debug.dprintf debug "@]@\n[GUI session] Opening session: update done@.  @[<hov 2>";
817
    let sched = M.init (gconfig.session_nb_processes)
818
    in
MARCHE Claude's avatar
MARCHE Claude committed
819
    Debug.dprintf debug "@]@\n[GUI session] Opening session: done@.";
820
    session_needs_saving := false;
821 822
    current_env_session := Some env;
    sched
823
  with e when not (Debug.test_flag Debug.stack_trace) ->
824 825 826 827 828
    eprintf "@[Error while opening session:@ %a@.@]"
      Exn_printer.exn_printer e;
    exit 1


829 830 831 832
(**********************************)
(* add new file from command line *)
(**********************************)

833
let open_file ?(start=false) f =
834
  let f = Sysutil.relativize_filename project_dir f in
MARCHE Claude's avatar
MARCHE Claude committed
835
  Debug.dprintf debug "[GUI session] Adding file '%s'@." f;
836
  if S.PHstr.mem (env_session()).S.session.S.session_files f then
MARCHE Claude's avatar
MARCHE Claude committed
837
    Debug.dprintf debug "[GUI] file %s already in database@." f
838 839
  else
    try
MARCHE Claude's avatar
MARCHE Claude committed
840
      Debug.dprintf debug "[GUI] adding file %s in database@." f;
841 842
      ignore (M.add_file (env_session()) ?format:!opt_parser f);
    with e ->
843 844 845 846 847 848 849 850 851 852 853
      if start
      then begin
        eprintf "@[Error while reading file@ '%s':@ %a@]@." f
          Exn_printer.exn_printer e;
        exit 1
      end
      else
        let msg =
          Pp.sprintf_wnl "@[Error while reading file@ '%s':@ %a@]" f
            Exn_printer.exn_printer e in
        info_window `ERROR msg
854

855
let () = Queue.iter (open_file ~start:true) files
856 857 858 859 860 861

(*****************************************************)
(* method: run a given prover on each unproved goals *)
(*****************************************************)

let prover_on_selected_goals pr =
862 863
  let timelimit = gconfig.session_time_limit in
  let memlimit = gconfig.session_mem_limit in
864
  List.iter
865
    (fun row ->
MARCHE Claude's avatar
MARCHE Claude committed
866
      try
867
       let a = get_any_from_row_reference row in
MARCHE Claude's avatar
MARCHE Claude committed
868
       M.run_prover
869
         (env_session()) sched
MARCHE Claude's avatar
MARCHE Claude committed
870
         ~context_unproved_goals_only:!context_unproved_goals_only
871
         ~timelimit ~memlimit
MARCHE Claude's avatar
MARCHE Claude committed
872 873 874 875
         pr a
      with e ->
        eprintf "@[Exception raised while running a prover:@ %a@.@]"
          Exn_printer.exn_printer e)
876
    (get_selected_row_references ())
877 878 879 880 881 882 883

(**********************************)
(* method: replay obsolete proofs *)
(**********************************)

let replay_obsolete_proofs () =
  List.iter
884 885
    (fun r ->
       let a = get_any_from_row_reference r in
886
       M.replay (env_session()) sched ~obsolete_only:true
887
         ~context_unproved_goals_only:!context_unproved_goals_only a)
888
    (get_selected_row_references ())
889

890 891 892 893 894 895 896 897 898 899
(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)

let cancel_proofs () =
  List.iter
    (fun r ->
       let a = get_any_from_row_reference r in
       M.cancel a)
    (get_selected_row_references ())
900

901 902 903 904 905 906 907 908 909 910
(*****************************************)
(* method: Set or unset the archive flag *)
(*****************************************)

let set_archive_proofs b () =
  List.iter
    (fun r ->
       let a = get_any_from_row_reference r in
       S.iter_proof_attempt (fun a -> M.set_archive a b) a)
    (get_selected_row_references ())
911 912

(*****************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
913
(* method: apply strategy on selected goals *)
914 915 916
(*****************************************************)


917
let apply_trans_on_selection tr =
918
  List.iter
919 920
    (fun r ->
       let a = get_any_from_row_reference r in
921
        M.transform (env_session()) sched
922
          ~context_unproved_goals_only:!context_unproved_goals_only
923
          tr a)
924
    (get_selected_row_references ())
925

MARCHE Claude's avatar
MARCHE Claude committed
926 927 928 929 930

let apply_strategy_on_selection str =
  List.iter
    (fun r ->
      let a = get_any_from_row_reference r in
931 932 933
      M.run_strategy (env_session()) sched
        ~context_unproved_goals_only:!context_unproved_goals_only
        str a)
MARCHE Claude's avatar
MARCHE Claude committed
934 935 936
    (get_selected_row_references ())


François Bobot's avatar
François Bobot committed
937 938 939 940 941 942 943 944 945 946
(*****************************************************)
(* method: bisect goal *)
(*****************************************************)

let bisect_proof_attempt pa =
  let eS = env_session () in
  let timelimit = ref (-1) in
  let set_timelimit res =
    timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
  let rec callback lp pa c = function
947 948
    | S.Running | S.Scheduled -> ()
    | S.Interrupted ->
François Bobot's avatar
François Bobot committed
949
      dprintf debug "Bisecting interrupted.@."
950
    | S.Unedited | S.JustEdited -> assert false
François Bobot's avatar
François Bobot committed
951 952 953 954 955 956 957 958 959 960 961
    | S.InternalFailure exn ->
      (** Perhaps the test can be considered false in this case? *)
      dprintf debug "Bisecting interrupted by an error %a.@."
        Exn_printer.exn_printer exn
    | S.Done res ->
      let b = res.Call_provers.pr_answer = Call_provers.Valid in
      dprintf debug "Bisecting: %a.@."
        Call_provers.print_prover_result res;
      if b then set_timelimit res;
      let r = c b in
      match r with
962 963 964
      | Eliminate_definition.BSdone [] ->
        dprintf debug "Bisecting doesn't reduced the task.@."
      | Eliminate_definition.BSdone reml ->
François Bobot's avatar
François Bobot committed
965 966 967 968
        dprintf debug "Bisecting done.@.";
        begin try
        let keygen = MA.keygen in
        let notify = MA.notify in
969 970
        let reml = List.map (fun (m,l) -> m.Theory.meta_name,l) reml in
        let metas = S.add_registered_metas ~keygen eS reml pa.S.proof_parent in
François Bobot's avatar
François Bobot committed
971 972 973 974 975 976 977 978 979 980
        let trans = S.add_registered_transformation ~keygen
          eS "eliminate_builtin" metas.S.metas_goal in
        let goal = List.hd trans.S.transf_goals in (* only one *)
        let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
          ~goal ~env_session:eS pa in
        MA.init_any (S.Metas metas);
        M.run_external_proof eS sched npa
        with e ->
          dprintf debug "Bisecting error:@\n%a@."
            Exn_printer.exn_printer e end
981 982
      | Eliminate_definition.BSstep (t,c) ->
        assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
François Bobot's avatar
François Bobot committed
983 984 985 986
        M.schedule_proof_attempt
          ~timelimit:!timelimit
          ~memlimit:pa.S.proof_memlimit
          ?old:(S.get_edited_as_abs eS.S.session pa)
987
          (** It is dangerous, isn't it? to be in place for bisecting? *)
François Bobot's avatar
François Bobot committed
988 989 990 991 992 993 994 995 996
          ~inplace:lp.S.prover_config.C.in_place
          ~command:(C.get_complete_command lp.S.prover_config)
          ~driver:lp.S.prover_driver
          ~callback:(callback lp pa c) sched t
  in
    (** Run once the complete goal in order to verify its validity and
        update the proof attempt *)
  let first_callback pa = function
    (** this pa can be different than the first pa *)
997 998
    | S.Running | S.Scheduled -> ()
    | S.Interrupted ->
François Bobot's avatar
François Bobot committed
999
      dprintf debug "Bisecting interrupted.@."
1000