why3ide.ml 29.4 KB
Newer Older
1 2 3 4

open Format
open Why3
open Gconfig
5 6 7
open Stdlib
open Session_itp
open Controller_itp
8 9
open Session_user_interface
open Historic
10

11 12
external reset_gc : unit -> unit = "ml_reset_gc"

13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
let debug = Debug.lookup_flag "ide_info"

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

let files = Queue.create ()
let opt_parser = ref None

let spec = Arg.align [
  "-F", Arg.String (fun s -> opt_parser := Some s),
      "<format> select input format (default: \"why\")";
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
(*
  "-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<file> add file to the project (ignored if it is already there)";
*)
  Termcode.arg_extra_expl_prefix
]

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

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

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

50 51 52 53 54 55 56 57
let task_driver =
  let main = Whyconf.get_main gconfig.config in
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver gconfig.env d []


MARCHE Claude's avatar
MARCHE Claude committed
58 59 60 61
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers gconfig.config

let cont =
MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65 66
  try
    Session_user_interface.cont_from_files spec usage_str gconfig.env files provers
  with e ->
       eprintf "%a@." Exn_printer.exn_printer e;
       exit 1
MARCHE Claude's avatar
MARCHE Claude committed
67

68 69 70 71 72 73
let () =
  Debug.dprintf debug "[GUI] Init the GTK interface...@?";
  ignore (GtkMain.Main.init ());
  Debug.dprintf debug " done.@.";
  Gconfig.init ()

MARCHE Claude's avatar
MARCHE Claude committed
74

MARCHE Claude's avatar
MARCHE Claude committed
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
(********************************)
(* Source language highlighting *)
(********************************)

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
  in
  languages_manager#set_search_path
    (load_path :: languages_manager#search_path);
  let why_lang =
    match languages_manager#language "why3" with
    | None ->
        eprintf "language file for 'why3' not found in directory %s@."
          load_path;
        exit 1
    | 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)

(* Borrowed from Frama-C src/gui/source_manager.ml:
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



116 117 118
(**********************)
(* Graphical elements *)
(**********************)
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155

let main_window =
  let w = GWindow.window
            ~allow_grow:true ~allow_shrink:true
            ~width:gconfig.window_width
            ~height:gconfig.window_height
            ~title:"Why3 Interactive Proof Session" ()
  in
  (* 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) =
    w#misc#connect#size_allocate
      ~callback:
      (fun {Gtk.width=w;Gtk.height=h} ->
       gconfig.window_height <- h;
       gconfig.window_width <- w)
  in w

(* the main window contains a vertical box, containing:
   1. the menu
   2. an horizontal box
 *)

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

let menubar = GMenu.menu_bar
  ~packing:(vbox#pack ?from:None ?expand:None ?fill:None ?padding:None)
  ()

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

(* 1. Menu *)

let factory = new GMenu.factory menubar

let accel_group = factory#accel_group

MARCHE Claude's avatar
MARCHE Claude committed
156 157
(* 1.1 "File" menu *)

158 159 160 161 162 163 164 165 166
let file_menu = factory#add_submenu "_File"
let file_factory = new GMenu.factory file_menu ~accel_group

let exit_function ~destroy () =
  ignore(destroy); GMain.quit ()

let (_ : GtkSignal.id) = main_window#connect#destroy
  ~callback:(exit_function ~destroy:true)

167 168
let (_ : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._S "_Save session"
169
    ~callback:(fun () -> Session_itp.save_session cont.controller_session)
170 171 172 173

let (replay_menu_item : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._R "_Replay all"

174 175 176 177
let (_ : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
    ~callback:(exit_function ~destroy:false)

MARCHE Claude's avatar
MARCHE Claude committed
178 179 180 181 182 183 184

(* 1.2 "View" menu

   the entries in that menu are defined later

*)

185 186 187 188
(* 2. horizontal box contains:
   2.1 TODO: a tool box ?
   2.2 a horizontal paned containing:
     2.2.1 a scrolled window to hold the tree view of the session
Clément Fumex's avatar
Clément Fumex committed
189
     2.2.2 a vertical paned containing
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
*)

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

let scrollview =
  let sv =
    GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
      ~width:gconfig.tree_width ~shadow_type:`ETCHED_OUT
      ~packing:hp#add ()
  in
  let (_ : GtkSignal.id) =
    sv#misc#connect#size_allocate
      ~callback:
      (fun {Gtk.width=w;Gtk.height=_h} ->
       gconfig.tree_width <- w)
  in sv

Clément Fumex's avatar
Clément Fumex committed
208
let vpan222 = GPack.paned `VERTICAL ~packing:hp#add ()
209 210 211 212 213 214

(*  the scrolled window 2.2.1 contains a GTK tree

*)


MARCHE Claude's avatar
MARCHE Claude committed
215 216 217 218 219 220 221 222
(* view for the session tree *)
let scrolled_session_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
    ~packing:scrollview#add
    ()

223 224 225
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let index_column = cols#add Gobject.Data.int
226
let status_column = cols#add Gobject.Data.gobject
MARCHE Claude's avatar
MARCHE Claude committed
227

228 229 230 231
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let view_name_column = GTree.view_column ~title:"Theories/Goals" ()
let () =
  view_name_column#pack name_renderer;
232 233 234 235 236 237
  view_name_column#add_attribute name_renderer "text" name_column;
  view_name_column#set_sizing `AUTOSIZE

let status_renderer = GTree.cell_renderer_pixbuf [ ]
let view_status_column = GTree.view_column ~title:"Status"
    ~renderer:(status_renderer, ["pixbuf", status_column])()
238

239 240 241 242 243 244 245 246 247
let goals_model,goals_view =
  Debug.dprintf debug "[GUI] Creating tree model...@?";
  let model = GTree.tree_store cols in
  let view = GTree.view ~model ~packing:scrolled_session_view#add () in
(*
  let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
  let () = view#set_rules_hint true in
 *)
  ignore (view#append_column view_name_column);
248
  ignore (view#append_column view_status_column);
249 250 251 252 253 254
(*
  ignore (view#append_column view_status_column);
  ignore (view#append_column view_time_column);
*)
  Debug.dprintf debug " done@.";
  model,view
255

Clément Fumex's avatar
Clément Fumex committed
256
(* vpan222 contains:
257
   2.2.2.1 a view of the current task
Clément Fumex's avatar
Clément Fumex committed
258 259
   2.2.2.2 a vertiacal pan which contains
     2.2.2.2.1 the input field to type commands
260
     2.2.2.2.2 a scrolled window to hold the output of the commands
261 262 263 264 265 266
 *)

let scrolled_task_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
Clément Fumex's avatar
Clément Fumex committed
267
    ~packing:vpan222#add ()
268 269 270 271

let task_view =
  GSourceView2.source_view
    ~editable:false
Clément Fumex's avatar
Clément Fumex committed
272
    ~cursor_visible:false
273 274 275 276
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ()

Clément Fumex's avatar
Clément Fumex committed
277
let vbox2222 = GPack.vbox ~packing:vpan222#add  ()
278

279 280 281 282 283 284
let hbox22221 =
  GPack.hbox
    ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()

let monitor =
  GMisc.label
MARCHE Claude's avatar
MARCHE Claude committed
285 286 287
    ~text:"  0/0/0"
    ~width:80
    ~xalign:0.0
288
    ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
289

MARCHE Claude's avatar
MARCHE Claude committed
290 291
let command_entry = GEdit.entry ~packing:hbox22221#add ()

MARCHE Claude's avatar
MARCHE Claude committed
292
let message_zone =
293 294 295 296
  let sv = GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
      ~shadow_type:`ETCHED_OUT ~packing:vbox2222#add ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
297
  GText.view ~editable:false ~cursor_visible:false
298 299
    ~packing:sv#add ()

300 301 302 303 304 305 306 307 308 309 310 311 312 313 314
(**** Monitor *****)

let fan n =
  match n mod 4 with
    | 0 -> "|"
    | 1 | -3 -> "\\"
    | 2 | -2 -> "-"
    | 3 | -1 -> "/"
    | _ -> assert false

let update_monitor =
  let c = ref 0 in
  fun t s r ->
  reset_gc ();
  incr c;
MARCHE Claude's avatar
MARCHE Claude committed
315 316 317 318 319
  let f = if r=0 then "  " else fan (!c / 2) ^ " " in
  monitor#set_text
    (f ^ (string_of_int t) ^ "/" ^ (string_of_int s) ^ "/" ^ (string_of_int r))


320 321 322 323 324 325
(****************************)
(* command entry completion *)
(****************************)

let completion_cols = new GTree.column_list
let completion_col = completion_cols#add Gobject.Data.string
326
(* let text_col = completion_cols#add Gobject.Data.string *)
327 328 329 330 331 332 333
let completion_model = GTree.tree_store completion_cols

let command_entry_completion : GEdit.entry_completion =
  GEdit.entry_completion ~model:completion_model ~minimum_key_length:1 ~entry:command_entry ()

let add_completion_entry s =
  let row = completion_model#append () in
334
  (* completion_model#set ~row ~column:text_col "test"; *)
335 336
  completion_model#set ~row ~column:completion_col s

337 338 339 340 341 342 343
let match_function s iter =
  let candidate = completion_model#get ~row:iter ~column:completion_col in
  try
    ignore (Str.search_forward (Str.regexp s) candidate 0);
    true
  with Not_found -> false

344
let init_comp cont =
345 346 347 348 349 350 351
  (* add the names of all the the transformations *)
  List.iter add_completion_entry (Trans.list_trans ());
  (* add the name of the commands *)
  List.iter (fun (c,_,_) -> add_completion_entry c)
    Session_user_interface.commands;
  (* todo: add queries *)

352 353 354
  (* add provers *)
  Whyconf.Hprover.iter
      (fun p _ -> add_completion_entry (p.Whyconf.prover_name^","^p.Whyconf.prover_version))
355
      cont.controller_provers;
356 357 358 359

  add_completion_entry "auto";
  add_completion_entry "auto 2";

360
  command_entry_completion#set_text_column completion_col;
361 362 363 364 365 366 367
  command_entry_completion#set_match_func match_function;
(*  ignore (command_entry_completion#connect#match_selected
    ~callback:(fun _ iter ->
        command_entry#set_text "test";
        true));*)

    (* GTree.model_filter -> Gtk.tree_iter -> bool *)
368

369
  command_entry#set_completion command_entry_completion
370 371


MARCHE Claude's avatar
MARCHE Claude committed
372

Sylvain Dailler's avatar
Sylvain Dailler committed
373 374 375 376 377

(*********************)
(* Terminal historic *)
(*********************)

378
let list_commands = create_historic()
Sylvain Dailler's avatar
Sylvain Dailler committed
379 380 381

let _ =
  command_entry#event#connect#key_press
382 383 384
    ~callback:(fun (ev: 'a Gdk.event) ->
      match GdkEvent.Key.keyval ev with
      | k when k = GdkKeysyms._Up -> (* Arrow up *)
385 386 387 388 389
          let s = print_next_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
390
      | k when k = GdkKeysyms._Down -> (* Arrow down *)
391 392 393 394 395
          let s = print_prev_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
Sylvain Dailler's avatar
Sylvain Dailler committed
396 397 398
      | _ -> false
      )

399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414
(********************************************)
(* controller instance on the GTK scheduler *)
(********************************************)


module S = struct
    let idle ~prio f =
      let (_ : GMain.Idle.id) = GMain.Idle.add ~prio f in ()

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

module C = Controller_itp.Make(S)

415 416 417 418 419 420
let () =
  let n = gconfig.session_nb_processes in
  Debug.dprintf debug "[IDE] setting max proof tasks to %d@." n;
  C.set_max_tasks n;
  C.register_observer update_monitor

421 422 423 424 425 426
let (_ : GtkSignal.id) =
  replay_menu_item#connect#activate
    ~callback:(fun () ->
               let callback = C.replay_print in
               C.replay ~use_steps:false cont ~callback ~remove_obsolete:false)

427 428 429 430 431 432 433

(***********************************)
(* Mapping session to the GTK tree *)
(***********************************)

type index =
  | Inone
434
  | IproofAttempt of proofAttemptID
435
  | IproofNode of proofNodeID
436
  | Itransformation  of transID
437 438 439 440
  | Ifile of file
  | Itheory of theory

let model_index : index Hint.t = Stdlib.Hint.create 17
441 442 443 444
let get_index iter =
  let index = goals_model#get ~row:iter ~column:index_column in
  Hint.find model_index index

445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
(* To each node we have the corresponding row_reference *)
let file_id_to_gtree : GTree.row_reference Hstr.t = Hstr.create 3
let th_id_to_gtree   : GTree.row_reference Ident.Hid.t = Ident.Hid.create 7
let pn_id_to_gtree   : GTree.row_reference Hpn.t = Hpn.create 17
let tn_id_to_gtree   : GTree.row_reference Htn.t = Htn.create 17
let pan_id_to_gtree  : GTree.row_reference Hpan.t = Hpan.create 17

(* TODO exception for those: *)
let row_from_file file = Hstr.find file_id_to_gtree (file.file_name)
let row_from_th   th   = Ident.Hid.find th_id_to_gtree (theory_name th)
let row_from_pn   pn   = Hpn.find pn_id_to_gtree pn
let row_from_tn   tn   = Htn.find tn_id_to_gtree tn
let row_from_pan  pan  = Hpan.find pan_id_to_gtree pan

let new_node =
  let cpt = ref (-1) in
  fun ?parent ?(collapse=false) name ind ->
  incr cpt;
  Hint.add model_index !cpt ind;
  let parent = Opt.map (fun x -> x#iter) parent in
  let iter = goals_model#append ?parent () in
  goals_model#set ~row:iter ~column:name_column name;
  goals_model#set ~row:iter ~column:index_column !cpt;
  let new_ref = goals_model#get_row_reference (goals_model#get_path iter) in
  (* By default expand_path when creating a new node *)
  if not collapse then goals_view#expand_to_path (goals_model#get_path iter);
  begin
    match ind with
    | IproofAttempt panid ->
       Hpan.add pan_id_to_gtree panid new_ref
    | IproofNode pnid ->
      Hpn.add pn_id_to_gtree pnid new_ref
    | Itransformation tnid ->
      Htn.add tn_id_to_gtree tnid new_ref
    | Ifile file ->
      Hstr.add file_id_to_gtree file.file_name new_ref
    | Itheory th ->
      Ident.Hid.add th_id_to_gtree (theory_name th) new_ref
    | Inone -> ()
  end;
  new_ref


let image_of_result ~obsolete rOpt =
  match rOpt with
  | None -> !image_undone
  | Some r ->
    match r.Call_provers.pr_answer with
    | 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
    | Call_provers.OutOfMemory ->
      if obsolete then !image_outofmemory_obs else !image_outofmemory
    | Call_provers.StepLimitExceeded ->
      if obsolete then !image_steplimitexceeded_obs
      else !image_steplimitexceeded
    | 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
510

511
let set_status_column_from_cont cont iter =
512
  let index = get_index iter in
513 514 515
  let image = match index with
    | Inone -> assert false
    | IproofAttempt panid ->
516
      let pa = get_proof_attempt_node cont.controller_session panid in
517 518 519 520 521 522 523 524
      image_of_result ~obsolete:pa.proof_obsolete pa.Session_itp.proof_state
    | IproofNode pn ->
      if pn_proved cont pn
      then !image_valid
      else !image_unknown
    | Itransformation tn -> if tn_proved cont tn
      then !image_valid
      else !image_unknown
525 526 527
    | Ifile file -> if file_proved cont file
      then !image_valid
      else !image_unknown
528 529 530 531 532
    | Itheory th -> if th_proved cont th
      then !image_valid
      else !image_unknown
  in
  goals_model#set ~row:iter ~column:status_column image
533

534
let build_subtree_proof_attempt_from_goal cont row_ref id =
535 536
  Whyconf.Hprover.iter
    (fun pa panid ->
537 538 539 540
       let name = Pp.string_of Whyconf.print_prover pa in
       let r = new_node ~parent:row_ref name (IproofAttempt panid) in
       set_status_column_from_cont cont r#iter)
    (get_proof_attempt_ids cont.controller_session id)
541

542 543
let rec build_subtree_from_goal cont th_row_reference id =
  let ses = cont.controller_session in
544
  let name = get_proof_name ses id in
545
  let row_ref =
546 547
    new_node ~parent:th_row_reference name.Ident.id_string
             (IproofNode id)
MARCHE Claude's avatar
MARCHE Claude committed
548
  in
549
  set_status_column_from_cont cont row_ref#iter;
550 551
  List.iter
    (fun trans_id ->
552
      ignore (build_subtree_from_trans cont row_ref trans_id))
553
    (get_transformations ses id);
554
  build_subtree_proof_attempt_from_goal cont row_ref id
555

556 557
and build_subtree_from_trans cont goal_row_reference trans_id =
  let ses = cont.controller_session in
558 559 560
  let name = get_transf_name ses trans_id in
  let row_ref =
    new_node ~parent:goal_row_reference name (Itransformation trans_id) in
561
  set_status_column_from_cont cont row_ref#iter;
562 563
  List.iter
    (fun goal_id ->
564 565 566
      (build_subtree_from_goal cont row_ref goal_id))
    (get_sub_tasks ses trans_id);
  row_ref
567

568 569
let build_tree_from_session cont =
  let ses = cont.controller_session in
570 571 572 573
  let files = get_files ses in
  Stdlib.Hstr.iter
    (fun _ file ->
       let file_row_reference = new_node file.file_name (Ifile file) in
574
       set_status_column_from_cont cont file_row_reference#iter;
575 576 577 578 579 580
       List.iter (fun th ->
                  let th_row_reference =
                    new_node ~parent:file_row_reference
                             (theory_name th).Ident.id_string
                             (Itheory th)
                  in
581 582
                  set_status_column_from_cont cont th_row_reference#iter;
                  List.iter (build_subtree_from_goal cont th_row_reference)
583 584 585 586
                            (theory_goals th))
                 file.file_theories)
    files

587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640
(*******************************)
(* commands of the "View" menu *)
(*******************************)

let view_menu = factory#add_submenu "_View"
let view_factory = new GMenu.factory view_menu ~accel_group

(* goals view is not yet multi-selectable
let (_ : GMenu.image_menu_item) =
  view_factory#add_image_item ~key:GdkKeysyms._A
    ~label:"Select all"
    ~callback:(fun () -> goals_view#selection#select_all ()) ()
 *)

let (_ : GMenu.menu_item) =
  view_factory#add_item ~key:GdkKeysyms._plus
    ~callback:enlarge_fonts "Enlarge font"

let (_ : GMenu.menu_item) =
    view_factory#add_item ~key:GdkKeysyms._minus
      ~callback:reduce_fonts "Reduce font"

let (_ : GMenu.image_menu_item) =
  view_factory#add_image_item ~key:GdkKeysyms._E
    ~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()

let collapse_iter iter =
  let path = goals_model#get_path iter in
  goals_view#collapse_row path

let rec collapse_proven_goals_from_pn pn =
  match pn_proved cont pn with
  | true  -> collapse_iter (row_from_pn pn)#iter
  | false ->
    List.iter collapse_proven_goals_from_tn
      (get_transformations cont.controller_session pn)
and collapse_proven_goals_from_tn tn =
  match tn_proved cont tn with
  | true  -> collapse_iter (row_from_tn tn)#iter
  | false ->
    List.iter collapse_proven_goals_from_pn
      (get_sub_tasks cont.controller_session tn)

let collapse_proven_goals_from_th th =
  match th_proved cont th with
  | true  -> collapse_iter (row_from_th th)#iter
  | false -> List.iter collapse_proven_goals_from_pn (theory_goals th)

let collapse_proven_goals_from_file file =
  match file_proved cont file with
  | true  -> collapse_iter (row_from_file file)#iter
  | false -> List.iter collapse_proven_goals_from_th file.file_theories

let collapse_proven_goals_from_iter iter =
641
  let index = get_index iter in
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
  match index with
  | Inone              -> assert false
  | IproofAttempt _    -> ()
  | IproofNode pn      -> collapse_proven_goals_from_pn pn
  | Itransformation tn -> collapse_proven_goals_from_tn tn
  | Itheory th         -> collapse_proven_goals_from_th th
  | Ifile file         -> collapse_proven_goals_from_file file

let collapse_proven_goals () =
  match goals_model#get_iter_first with
  | None -> ()
  | Some root_iter -> collapse_proven_goals_from_iter root_iter

let (_ : GMenu.image_menu_item) =
  view_factory#add_image_item ~key:GdkKeysyms._C
    ~label:"Collapse proven goals" ~callback:(fun () -> collapse_proven_goals ()) ()

let () =
  Gconfig.add_modifiable_sans_font_view goals_view#misc;
  Gconfig.add_modifiable_mono_font_view monitor#misc;
  Gconfig.add_modifiable_mono_font_view task_view#misc;
  Gconfig.add_modifiable_mono_font_view command_entry#misc;
  Gconfig.add_modifiable_mono_font_view message_zone#misc;
MARCHE Claude's avatar
MARCHE Claude committed
665
  task_view#source_buffer#set_language why_lang;
666 667
  Gconfig.set_fonts ()

668 669 670 671
(******************)
(*    actions     *)
(******************)

672 673
(* TODO We currently use this for transformations etc... With strategies, we sure
   do not want to move the current index with the computing of strategy. *)
674 675
let current_selected_index = ref Inone

676 677 678 679 680 681 682 683 684 685 686 687
let image_of_pa_status ~obsolete pa_status =
  match pa_status with
    | Controller_itp.Interrupted   -> !image_undone
    | Controller_itp.Unedited      -> !image_editor
    | Controller_itp.JustEdited    -> !image_unknown
    | Controller_itp.Scheduled     -> !image_scheduled
    | Controller_itp.Running       -> !image_running
    | Controller_itp.InternalFailure _
    | Controller_itp.Uninstalled _ -> !image_failure
    | Controller_itp.Done r        -> image_of_result ~obsolete (Some r)

let rec update_status_column_from_iter cont iter =
688 689
  set_status_column_from_cont cont iter;
  match goals_model#iter_parent iter with
690
  | Some p -> update_status_column_from_iter cont p
691 692
  | None -> ()

693 694
let move_current_row_selection_up () =
  let current_view = List.hd (goals_view#selection#get_selected_rows) in
695 696 697
  ignore (GTree.Path.up current_view);
  let row_up = goals_model#get_row_reference current_view in
  goals_view#selection#select_iter row_up#iter
698 699 700 701 702 703 704 705 706 707 708 709 710

let move_current_row_selection_down () =
  let current_iter =
    try
      let current_view = List.hd (goals_view#selection#get_selected_rows) in
      let current_row = goals_model#get_row_reference current_view in
      Some current_row#iter
    with Not_found ->
      None
  in
  let child = goals_model#iter_children current_iter in
  goals_view#selection#select_iter child

711 712 713 714 715 716 717 718 719
(* Callback of a transformation *)
let callback_update_tree_transform cont status =
  match status with
  | TSdone trans_id ->
    let ses = cont.controller_session in
    let id = get_trans_parent ses trans_id in
    let row_ref = row_from_pn id in
    let r = build_subtree_from_trans cont row_ref trans_id in
    update_status_column_from_iter cont r#iter;
720 721 722 723 724 725 726 727 728 729 730 731
    (* move focus if the current index still corresponds to the
       goal *)
    let ppn = get_trans_parent cont.controller_session trans_id in
    begin match !current_selected_index with
      | IproofNode pn when pn = ppn ->
        (match Session_itp.get_sub_tasks ses trans_id with
         | first_goal :: _ ->
           (* Put the selection on the first goal *)
           goals_view#selection#select_iter (row_from_pn first_goal)#iter
         | [] -> ())
      | _ -> ()
    end;
732 733 734
  | TSfailed (id, e) ->
      message_zone#buffer#set_text
        (Pp.sprintf "%a" (get_exception_message cont.controller_session id) e)
735 736
  | _ -> ()

737
let rec apply_transform cont t args =
738 739
  match !current_selected_index with
  | IproofNode id ->
740
     let callback = callback_update_tree_transform cont in
741
     C.schedule_transformation cont id t args ~callback
742
  | IproofAttempt _ ->
743 744
    move_current_row_selection_up ();
    apply_transform cont t args
745
  | Itransformation _ | Ifile _ | Itheory _ | Inone ->
746 747 748 749
    begin try move_current_row_selection_down () with
      Not_found -> printf "no goals to apply transform"
    end;
    apply_transform cont t args
750

751 752 753 754 755 756 757 758
let go_to_nearest_unproven_goal_and_collapse pn =
  begin match get_first_unproven_goal_around_pn cont pn with
    | Some next_pn ->
      goals_view#selection#select_iter (row_from_pn next_pn)#iter
    | None -> ()
  end;
  collapse_proven_goals ()

759
(* Callback of a proof_attempt *)
760 761
let callback_update_tree_proof cont panid pa_status =
  let ses = cont.controller_session in
762
  let pa = get_proof_attempt_node ses panid in
MARCHE Claude's avatar
MARCHE Claude committed
763 764
  let prover = pa.prover in
  let name = Pp.string_of Whyconf.print_prover prover in
765 766
  let obsolete = pa.proof_obsolete in
  let r = match pa_status with
767 768 769 770 771 772 773 774 775
    | Scheduled ->
      begin
        try row_from_pan panid
        with Not_found ->
          let parent_id = get_proof_attempt_parent ses panid in
          let parent = row_from_pn parent_id in
          new_node ~parent name (IproofAttempt panid)
      end
    | Done _ ->
776 777 778 779 780 781 782 783 784 785
      let ppn = get_proof_attempt_parent cont.controller_session panid in
      let piter = (row_from_pn ppn)#iter in
      update_status_column_from_iter cont piter;
      (* move focus an collapse if the goal was proven and
         the current index still corresponds to the goal *)
      begin match !current_selected_index with
        | IproofNode pn when pn = ppn ->
          if pn_proved cont pn then
            go_to_nearest_unproven_goal_and_collapse pn
        | _ -> ()
786
      end;
787
      row_from_pan panid
788
    | _  -> row_from_pan panid (* TODO ? *)
789 790 791 792
  in
  goals_model#set ~row:r#iter ~column:status_column
    (image_of_pa_status ~obsolete pa_status)

793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811
let test_schedule_proof_attempt cont (p: Whyconf.config_prover) limit =
  let prover = p.Whyconf.prover in
  let callback = callback_update_tree_proof cont in
  let rec get_goals () =
    match !current_selected_index with
    | IproofNode id -> [id]
    | IproofAttempt _ ->
      move_current_row_selection_up ();
      get_goals ()
    | Itransformation tn ->
      List.rev (unproven_goals_below_tn cont [] tn)
    | Ifile file ->
      List.rev (unproven_goals_below_file cont file)
    | Itheory th ->
      List.rev (unproven_goals_below_th cont [] th)
    | Inone -> []
  in
  List.iter (fun id -> C.schedule_proof_attempt cont id prover ~limit ~callback)
    (get_goals ())
MARCHE Claude's avatar
MARCHE Claude committed
812 813 814 815 816 817 818 819 820 821 822 823 824 825 826

let run_strategy_on_task s =
  match !current_selected_index with
  | IproofNode id ->
     let l = Session_user_interface.strategies
               cont.controller_env gconfig.config
     in
     let st = List.filter (fun (_,c,_,_) -> c=s) l in
     begin
       match st with
       | [(n,_,_,st)] ->
          printf "running strategy '%s'@." n;
          let callback sts =
            printf "Strategy status: %a@." print_strategy_status sts
          in
MARCHE Claude's avatar
MARCHE Claude committed
827
          let callback_pa =
828
            callback_update_tree_proof cont
MARCHE Claude's avatar
MARCHE Claude committed
829 830
          in
          let callback_tr st =
831
            callback_update_tree_transform cont st
MARCHE Claude's avatar
MARCHE Claude committed
832 833
          in
          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
MARCHE Claude's avatar
MARCHE Claude committed
834 835
    | _ -> printf "Strategy '%s' not found@." s
     end
836
  | _ -> ()
MARCHE Claude's avatar
MARCHE Claude committed
837

838
let clear_command_entry () = command_entry#set_text ""
MARCHE Claude's avatar
MARCHE Claude committed
839 840

let interp cmd =
MARCHE Claude's avatar
MARCHE Claude committed
841 842 843 844 845
  let id =
    match !current_selected_index with
    | IproofNode id -> Some id
    | _ -> None
  in
846 847
  try
  match interp cont id cmd with
848 849
    | Transform(s,_t,args) ->
       clear_command_entry ();
850
       apply_transform cont s args
851
    | Query s ->
MARCHE Claude's avatar
MARCHE Claude committed
852
       clear_command_entry ();
853
       message_zone#buffer#set_text s
854 855 856 857 858
    | Other(s,args) ->
      begin
        match parse_prover_name gconfig.config s args with
        | Some (prover_config, limit) ->
          clear_command_entry ();
859
          test_schedule_proof_attempt cont prover_config limit
860 861
        | None ->
          match s with
MARCHE Claude's avatar
MARCHE Claude committed
862 863 864
          | "auto" ->
             let s =
               match args with
MARCHE Claude's avatar
MARCHE Claude committed
865 866
               | "2"::_ -> "2"
               | _ -> "1"
MARCHE Claude's avatar
MARCHE Claude committed
867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882
             in
             clear_command_entry ();
             run_strategy_on_task s
          | "help" ->
             clear_command_entry ();
             let text = Pp.sprintf
                          "Please type a command among the following (automatic completion available)@\n\
                           @\n\
                           @ <transformation name> [arguments]@\n\
                           @ <prover name> [<time limit> [<mem limit>]]@\n\
                           @ <query> [arguments]@\n\
                           @ auto [auto level]@\n\
                           @\n\
                           Available queries are:@\n@[%a@]" help_on_queries ()
             in
             message_zone#buffer#set_text text
883 884
          | _ ->
             message_zone#buffer#set_text ("unknown command '"^s^"'")
885
      end
886 887
  with e when not (Debug.test_flag Debug.stack_trace) ->
       message_zone#buffer#set_text (Pp.sprintf "anomaly: %a" Exn_printer.exn_printer e)
MARCHE Claude's avatar
MARCHE Claude committed
888 889 890

let (_ : GtkSignal.id) =
  command_entry#connect#activate
891
    ~callback:(fun () -> add_command list_commands command_entry#text; interp command_entry#text)
892 893


894 895 896 897 898 899 900
let get_selected_row_references () =
  List.map
    (fun path -> goals_model#get_row_reference path)
    goals_view#selection#get_selected_rows

let on_selected_row r =
  try
901
    let session_element = get_index r#iter in
902 903
    current_selected_index := session_element;
    match session_element with
904 905
    | IproofNode id ->
       let task = get_task cont.controller_session id in
906
       let tables = get_tables cont.controller_session id in
907
       let s = Pp.string_of
908
                 (fun fmt -> Driver.print_task ~cntexample:false task_driver fmt tables)
909
                 task
Clément Fumex's avatar
Clément Fumex committed
910 911 912
       in task_view#source_buffer#set_text s;
       (* scroll to end of text *)
       task_view#scroll_to_mark `INSERT
913 914 915 916 917 918 919 920 921 922 923 924
    | _ -> task_view#source_buffer#set_text ""
  with
    | Not_found -> task_view#source_buffer#set_text ""

let (_ : GtkSignal.id) =
  goals_view#selection#connect#after#changed ~callback:
    (fun () ->
      match get_selected_row_references () with
        | [r] -> on_selected_row r
        | _ -> ())

(***********************)
925
(* start the interface *)
926
(***********************)
927 928

let () =
929
  build_tree_from_session cont;
930
  (* temporary *)
931
  init_comp cont;
Clément Fumex's avatar
Clément Fumex committed
932
  vpan222#set_position 500;
933
  goals_view#expand_all ();
934 935
  main_window#add_accel_group accel_group;
  main_window#set_icon (Some !Gconfig.why_icon);
936
  message_zone#buffer#set_text "Welcome to Why3 IDE\ntype 'help' for help";
937 938
  main_window#show ();
  GMain.main ()