why3ide.ml 25.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

75 76 77
(**********************)
(* Graphical elements *)
(**********************)
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

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
115 116
(* 1.1 "File" menu *)

117 118 119 120 121 122 123 124 125
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)

126 127 128 129 130 131 132
let (_ : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._S "_Save session"
    ~callback:(fun () -> Session_itp.save_session cont.Controller_itp.controller_session)

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

133 134 135 136
let (_ : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
    ~callback:(exit_function ~destroy:false)

MARCHE Claude's avatar
MARCHE Claude committed
137 138 139 140 141 142 143

(* 1.2 "View" menu

   the entries in that menu are defined later

*)

144 145 146 147
(* 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
148
     2.2.2 a vertical paned containing
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
*)

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
167
let vpan222 = GPack.paned `VERTICAL ~packing:hp#add ()
168 169 170 171 172 173

(*  the scrolled window 2.2.1 contains a GTK tree

*)


MARCHE Claude's avatar
MARCHE Claude committed
174 175 176 177 178 179 180 181
(* view for the session tree *)
let scrolled_session_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
    ~packing:scrollview#add
    ()

182 183 184
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let index_column = cols#add Gobject.Data.int
185
let status_column = cols#add Gobject.Data.gobject
MARCHE Claude's avatar
MARCHE Claude committed
186

187 188 189 190
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;
191 192 193 194 195 196
  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])()
197

198 199 200 201 202 203 204 205 206
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);
207
  ignore (view#append_column view_status_column);
208 209 210 211 212 213
(*
  ignore (view#append_column view_status_column);
  ignore (view#append_column view_time_column);
*)
  Debug.dprintf debug " done@.";
  model,view
214

Clément Fumex's avatar
Clément Fumex committed
215
(* vpan222 contains:
216
   2.2.2.1 a view of the current task
Clément Fumex's avatar
Clément Fumex committed
217 218
   2.2.2.2 a vertiacal pan which contains
     2.2.2.2.1 the input field to type commands
219
     2.2.2.2.2 a scrolled window to hold the output of the commands
220 221 222 223 224 225
 *)

let scrolled_task_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
Clément Fumex's avatar
Clément Fumex committed
226
    ~packing:vpan222#add ()
227 228 229 230

let task_view =
  GSourceView2.source_view
    ~editable:false
Clément Fumex's avatar
Clément Fumex committed
231
    ~cursor_visible:false
232 233 234 235
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ()

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

238 239 240 241 242 243
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
244 245 246
    ~text:"  0/0/0"
    ~width:80
    ~xalign:0.0
247
    ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
248

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

MARCHE Claude's avatar
MARCHE Claude committed
251
let message_zone =
252 253 254 255
  let sv = GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
      ~shadow_type:`ETCHED_OUT ~packing:vbox2222#add ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
256
  GText.view ~editable:false ~cursor_visible:false
257 258
    ~packing:sv#add ()

259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
(**** 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
274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
  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))


(*******************************)
(* 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 () =
  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;
  Gconfig.set_fonts ()
313

314 315 316 317 318 319 320 321 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
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

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)

348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
(****************************)
(* command entry completion *)
(****************************)

let completion_cols = new GTree.column_list
let completion_col = completion_cols#add Gobject.Data.string
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
  completion_model#set ~row ~column:completion_col s

363
let init_comp cont =
364 365 366 367 368 369 370
  (* 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 *)

371 372 373 374 375 376 377 378
  (* add provers *)
  Whyconf.Hprover.iter
      (fun p _ -> add_completion_entry (p.Whyconf.prover_name^","^p.Whyconf.prover_version))
      cont.Controller_itp.controller_provers;

  add_completion_entry "auto";
  add_completion_entry "auto 2";

379
  command_entry_completion#set_text_column completion_col;
380

381
  command_entry#set_completion command_entry_completion
382 383


MARCHE Claude's avatar
MARCHE Claude committed
384

Sylvain Dailler's avatar
Sylvain Dailler committed
385 386 387 388 389

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

390
let list_commands = create_historic()
Sylvain Dailler's avatar
Sylvain Dailler committed
391 392 393

let _ =
  command_entry#event#connect#key_press
394 395 396
    ~callback:(fun (ev: 'a Gdk.event) ->
      match GdkEvent.Key.keyval ev with
      | k when k = GdkKeysyms._Up -> (* Arrow up *)
397 398 399 400 401
          let s = print_next_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
402
      | k when k = GdkKeysyms._Down -> (* Arrow down *)
403 404 405 406 407
          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
408 409 410
      | _ -> false
      )

411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
(********************************************)
(* 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)

427 428 429 430 431 432
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

433 434 435 436 437 438
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)

439 440 441 442 443 444 445

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

type index =
  | Inone
446
  | IproofAttempt of proofAttemptID
447
  | IproofNode of proofNodeID
448
  | Itransformation  of transID
449 450 451 452
  | Ifile of file
  | Itheory of theory

let model_index : index Hint.t = Stdlib.Hint.create 17
453 454 455 456
(* To each proofnodeid we have the corresponding row_reference *)
let pn_id_to_gtree : GTree.row_reference Hpn.t = Hpn.create 17
let pan_id_to_gtree : GTree.row_reference Hpan.t = Hpan.create 17

457 458 459 460 461 462
let set_status_column_from_cont cont iter =
  let index = goals_model#get ~row:iter ~column:index_column in
  let index = Hint.find model_index index in
  let image = match index with
    | Inone -> assert false
    | IproofAttempt panid ->
463
      let pa = get_proof_attempt_node cont.controller_session panid in
464 465 466 467 468 469 470 471 472 473 474 475 476 477
      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
    | Ifile _ -> !image_file
    | Itheory th -> if th_proved cont th
      then !image_valid
      else !image_unknown
  in
  goals_model#set ~row:iter ~column:status_column image
478 479 480

let new_node =
  let cpt = ref (-1) in
481
  fun ?parent ?(collapse=false) name ind ->
482 483 484 485 486 487
  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;
488
  let new_ref = goals_model#get_row_reference (goals_model#get_path iter) in
489 490
  (* By default expand_path when creating a new node *)
  if not collapse then goals_view#expand_to_path (goals_model#get_path iter);
491 492 493 494 495 496 497 498 499
  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
    | _ -> ()
  end;
  new_ref
500

501
let build_subtree_proof_attempt_from_goal cont row_ref id =
502 503
  Whyconf.Hprover.iter
    (fun pa panid ->
504 505 506 507
       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)
508

509 510
let rec build_subtree_from_goal cont th_row_reference id =
  let ses = cont.controller_session in
511
  let name = get_proof_name ses id in
512
  let row_ref =
513 514
    new_node ~parent:th_row_reference name.Ident.id_string
             (IproofNode id)
MARCHE Claude's avatar
MARCHE Claude committed
515
  in
516
  set_status_column_from_cont cont row_ref#iter;
517 518
  List.iter
    (fun trans_id ->
519
      ignore (build_subtree_from_trans cont row_ref trans_id))
520
    (get_transformations ses id);
521
  build_subtree_proof_attempt_from_goal cont row_ref id
522

523 524
and build_subtree_from_trans cont goal_row_reference trans_id =
  let ses = cont.controller_session in
525 526 527
  let name = get_transf_name ses trans_id in
  let row_ref =
    new_node ~parent:goal_row_reference name (Itransformation trans_id) in
528
  set_status_column_from_cont cont row_ref#iter;
529 530
  List.iter
    (fun goal_id ->
531 532 533
      (build_subtree_from_goal cont row_ref goal_id))
    (get_sub_tasks ses trans_id);
  row_ref
534

535 536
let build_tree_from_session cont =
  let ses = cont.controller_session in
537 538 539 540
  let files = get_files ses in
  Stdlib.Hstr.iter
    (fun _ file ->
       let file_row_reference = new_node file.file_name (Ifile file) in
541
       set_status_column_from_cont cont file_row_reference#iter;
542 543 544 545 546 547
       List.iter (fun th ->
                  let th_row_reference =
                    new_node ~parent:file_row_reference
                             (theory_name th).Ident.id_string
                             (Itheory th)
                  in
548 549
                  set_status_column_from_cont cont th_row_reference#iter;
                  List.iter (build_subtree_from_goal cont th_row_reference)
550 551 552 553 554 555 556 557
                            (theory_goals th))
                 file.file_theories)
    files

(******************)
(*    actions     *)
(******************)

558 559
(* 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. *)
560 561
let current_selected_index = ref Inone

562 563 564 565 566 567
let rec update_status_column_from cont iter =
  set_status_column_from_cont cont iter;
  match goals_model#iter_parent iter with
  | Some p -> update_status_column_from cont p
  | None -> ()

568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
let match_transformation_exception (e: exn) =
  match e with
  | Args_wrapper.Arg_parse_error (s1, s2) ->
      message_zone#buffer#set_text ("Argument parsing error:" ^ s2 ^ "\n" ^ s1)
  | Args_wrapper.Arg_expected (s) ->
      message_zone#buffer#set_text ("Argument expected of type: " ^ s)
  | Args_wrapper.Arg_theory_not_found (s) ->
      message_zone#buffer#set_text ("Theory not found:" ^ s)
  | Args_wrapper.Arg_trans (s) ->
      message_zone#buffer#set_text ("Error in transformation function: " ^ s)
  | Args_wrapper.Arg_trans_term (s, Some s1, Some s2) ->
      message_zone#buffer#set_text ("Error in transformation " ^ s ^
                              " during unification of following two terms:\n" ^
                              s1 ^ "\n" ^ s2)
  | Controller_itp.Noprogress ->
      message_zone#buffer#set_text ("The transformation made no progress")
  | Args_wrapper.Arg_trans_type (s, Some s1, Some s2) ->
      message_zone#buffer#set_text ("Error in transformation function:" ^ s ^
                              ". These types should be equal:\n" ^ s1 ^ "\n" ^ s2)
  | Args_wrapper.Arg_hyp_not_found s ->
     message_zone#buffer#set_text ("Hypothesis not found during execution of " ^ s)
589
  | _ -> message_zone#buffer#set_text (Pp.sprintf "Uncatched error: %a" Exn_printer.exn_printer e)
590

591
(* Callback of a transformation *)
592
let callback_update_tree_transform cont status =
593 594
  match status with
  | TSdone trans_id ->
595 596 597 598 599 600 601 602 603 604
    let ses = cont.controller_session in
    let id = get_trans_parent ses trans_id in
    let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
    let r = build_subtree_from_trans cont row_ref trans_id in
    update_status_column_from cont r#iter;
    (match Session_itp.get_sub_tasks ses trans_id with
     | first_goal :: _ ->
       (* Put the selection on the first goal *)
       goals_view#selection#select_iter (Hpn.find pn_id_to_gtree first_goal)#iter
     | [] -> ())
605
  | TSfailed e -> match_transformation_exception e
606 607
  | _ -> ()

608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
let move_current_row_selection_up () =
  let current_view = List.hd (goals_view#selection#get_selected_rows) in
  let current_row = goals_model#get_row_reference current_view in
  begin match goals_model#iter_parent current_row#iter with
    | Some parent_iter -> goals_view#selection#select_iter parent_iter
    | None -> ()
  end

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

let rec apply_transform cont t args =
629 630
  match !current_selected_index with
  | IproofNode id ->
631
     let callback = callback_update_tree_transform cont in
632
     C.schedule_transformation cont id t args ~callback
633
  | IproofAttempt _ ->
634 635
    move_current_row_selection_up ();
    apply_transform cont t args
636
  | Itransformation _ | Ifile _ | Itheory _ | Inone ->
637 638 639 640
    begin try move_current_row_selection_down () with
      Not_found -> printf "no goals to apply transform"
    end;
    apply_transform cont t args
641 642

(* Callback of a proof_attempt *)
643 644
let callback_update_tree_proof cont panid pa_status =
  let ses = cont.controller_session in
645
  let pa = get_proof_attempt_node ses panid in
MARCHE Claude's avatar
MARCHE Claude committed
646 647
  let prover = pa.prover in
  let name = Pp.string_of Whyconf.print_prover prover in
648 649
  let obsolete = pa.proof_obsolete in
  let r = match pa_status with
MARCHE Claude's avatar
MARCHE Claude committed
650 651
  | Scheduled ->
     begin
652
       try
653
         Hpan.find pan_id_to_gtree panid
MARCHE Claude's avatar
MARCHE Claude committed
654 655 656
       with Not_found ->
         let parent_id = get_proof_attempt_parent ses panid in
         let parent = Hpn.find pn_id_to_gtree parent_id in
657
         new_node ~parent name (IproofAttempt panid)
MARCHE Claude's avatar
MARCHE Claude committed
658
     end
659 660 661 662 663 664 665 666 667 668 669 670
  | Done _ ->
    let r = Hpan.find pan_id_to_gtree panid in
    begin match goals_model#iter_parent r#iter with
    | Some iter -> update_status_column_from cont iter
    | None -> ()
    end;
    r
  | _  -> Hpan.find pan_id_to_gtree panid (* TODO ? *)
  in
  goals_model#set ~row:r#iter ~column:status_column
    (image_of_pa_status ~obsolete pa_status)

671
let rec test_schedule_proof_attempt cont (p: Whyconf.config_prover) limit =
672 673
  match !current_selected_index with
  | IproofNode id ->
674
    let prover = p.Whyconf.prover in
675
    let callback = callback_update_tree_proof cont in
MARCHE Claude's avatar
MARCHE Claude committed
676
    C.schedule_proof_attempt cont id prover ~limit ~callback
677 678 679 680 681 682 683 684
  | IproofAttempt _ | Itransformation _ ->
    move_current_row_selection_up ();
    test_schedule_proof_attempt cont p limit
  | Ifile _ | Itheory _ | Inone ->
    begin try move_current_row_selection_down () with
      Not_found -> printf "no goals to run prover on"
    end;
    test_schedule_proof_attempt cont p limit
MARCHE Claude's avatar
MARCHE Claude committed
685 686 687 688 689 690 691 692 693 694 695 696 697 698 699

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
700
          let callback_pa =
701
            callback_update_tree_proof cont
MARCHE Claude's avatar
MARCHE Claude committed
702 703
          in
          let callback_tr st =
704
            callback_update_tree_transform cont st
MARCHE Claude's avatar
MARCHE Claude committed
705 706
          in
          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
MARCHE Claude's avatar
MARCHE Claude committed
707 708
    | _ -> printf "Strategy '%s' not found@." s
     end
709 710
  | _ -> (
)
MARCHE Claude's avatar
MARCHE Claude committed
711

712
let clear_command_entry () = command_entry#set_text ""
MARCHE Claude's avatar
MARCHE Claude committed
713 714

let interp cmd =
MARCHE Claude's avatar
MARCHE Claude committed
715 716 717 718 719
  let id =
    match !current_selected_index with
    | IproofNode id -> Some id
    | _ -> None
  in
720 721
  try
  match interp cont id cmd with
722 723
    | Transform(s,_t,args) ->
       clear_command_entry ();
724
       apply_transform cont s args
725
    | Query s ->
MARCHE Claude's avatar
MARCHE Claude committed
726
       clear_command_entry ();
727
       message_zone#buffer#set_text s
728 729 730 731 732
    | Other(s,args) ->
      begin
        match parse_prover_name gconfig.config s args with
        | Some (prover_config, limit) ->
          clear_command_entry ();
733
          test_schedule_proof_attempt cont prover_config limit
734 735
        | None ->
          match s with
MARCHE Claude's avatar
MARCHE Claude committed
736 737 738
          | "auto" ->
             let s =
               match args with
MARCHE Claude's avatar
MARCHE Claude committed
739 740
               | "2"::_ -> "2"
               | _ -> "1"
MARCHE Claude's avatar
MARCHE Claude committed
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756
             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
757 758
          | _ ->
             message_zone#buffer#set_text ("unknown command '"^s^"'")
759
      end
760 761
  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
762 763 764

let (_ : GtkSignal.id) =
  command_entry#connect#activate
765
    ~callback:(fun () -> add_command list_commands command_entry#text; interp command_entry#text)
766 767


768 769 770 771 772 773 774 775
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 =
  let index = goals_model#get ~row:r#iter ~column:index_column in
  try
776 777 778
    let session_element = Hint.find model_index index in
    current_selected_index := session_element;
    match session_element with
779 780 781 782 783
    | IproofNode id ->
       let task = get_task cont.controller_session id in
       let s = Pp.string_of
                 (Driver.print_task ~cntexample:false task_driver)
                 task
Clément Fumex's avatar
Clément Fumex committed
784 785 786
       in task_view#source_buffer#set_text s;
       (* scroll to end of text *)
       task_view#scroll_to_mark `INSERT
787 788 789 790 791 792 793 794 795 796 797 798
    | _ -> 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
        | _ -> ())

(***********************)
799
(* start the interface *)
800
(***********************)
801 802

let () =
803
  build_tree_from_session cont;
804
  (* temporary *)
805
  init_comp cont;
Clément Fumex's avatar
Clément Fumex committed
806
  vpan222#set_position 500;
807
  goals_view#expand_all ();
808 809
  main_window#add_accel_group accel_group;
  main_window#set_icon (Some !Gconfig.why_icon);
810
  message_zone#buffer#set_text "Welcome to Why3 IDE\ntype 'help' for help";
811 812
  main_window#show ();
  GMain.main ()