Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

why3ide.ml 18 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 62 63
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers gconfig.config

let cont =
  Session_user_interface.cont_from_files spec usage_str gconfig.env files provers

64 65 66 67 68 69
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
70

71 72 73
(**********************)
(* Graphical elements *)
(**********************)
74 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 116 117 118 119

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

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)

120 121 122 123 124 125 126
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"

127 128 129 130 131 132 133 134
let (_ : GMenu.menu_item) =
  file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
    ~callback:(exit_function ~destroy:false)

(* 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
135
     2.2.2 a vertical paned containing
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
*)

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
154
let vpan222 = GPack.paned `VERTICAL ~packing:hp#add ()
155 156 157 158 159 160

(*  the scrolled window 2.2.1 contains a GTK tree

*)


MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164 165 166 167 168
(* view for the session tree *)
let scrolled_session_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
    ~packing:scrollview#add
    ()

169 170 171
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let index_column = cols#add Gobject.Data.int
MARCHE Claude's avatar
MARCHE Claude committed
172

173 174 175 176 177
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;
  view_name_column#add_attribute name_renderer "text" name_column
178

179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
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);
(*
  ignore (view#append_column view_status_column);
  ignore (view#append_column view_time_column);
*)
  Debug.dprintf debug " done@.";
  model,view
194

Clément Fumex's avatar
Clément Fumex committed
195
(* vpan222 contains:
196
   2.2.2.1 a view of the current task
Clément Fumex's avatar
Clément Fumex committed
197 198
   2.2.2.2 a vertiacal pan which contains
     2.2.2.2.1 the input field to type commands
199
     2.2.2.2.2 a scrolled window to hold the output of the commands
200 201 202 203 204 205
 *)

let scrolled_task_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
Clément Fumex's avatar
Clément Fumex committed
206
    ~packing:vpan222#add ()
207 208 209 210

let task_view =
  GSourceView2.source_view
    ~editable:false
Clément Fumex's avatar
Clément Fumex committed
211
    ~cursor_visible:false
212 213 214 215
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ()

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

218 219 220 221 222 223 224 225 226 227
let hbox22221 =
  GPack.hbox
    ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()

let command_entry = GEdit.entry ~packing:hbox22221#add ()

let monitor =
  GMisc.label
    ~text:"0/0/0"
    ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
228

MARCHE Claude's avatar
MARCHE Claude committed
229
let message_zone =
230 231 232 233
  let sv = GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
      ~shadow_type:`ETCHED_OUT ~packing:vbox2222#add ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
234
  GText.view ~editable:false ~cursor_visible:false
235 236
    ~packing:sv#add ()

237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
(**** 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;
  let r =
    if r=0 then "0" else
      (string_of_int r) ^ " " ^ (fan (!c / 4))
  in
  monitor#set_text ((string_of_int t) ^ "/" ^ (string_of_int s) ^ "/" ^ r)

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
(****************************)
(* 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

let init_comp () =
  (* 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 *)

  command_entry_completion#set_text_column completion_col;
282

283
  command_entry#set_completion command_entry_completion
284 285


MARCHE Claude's avatar
MARCHE Claude committed
286

Sylvain Dailler's avatar
Sylvain Dailler committed
287 288 289 290 291

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

292
let list_commands = create_historic()
Sylvain Dailler's avatar
Sylvain Dailler committed
293 294 295

let _ =
  command_entry#event#connect#key_press
296 297 298
    ~callback:(fun (ev: 'a Gdk.event) ->
      match GdkEvent.Key.keyval ev with
      | k when k = GdkKeysyms._Up -> (* Arrow up *)
299 300 301 302 303
          let s = print_next_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
304
      | k when k = GdkKeysyms._Down -> (* Arrow down *)
305 306 307 308 309
          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
310 311 312
      | _ -> false
      )

313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
(********************************************)
(* 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)

329 330 331 332 333 334
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

335 336 337 338 339 340
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)

341 342 343 344 345 346 347

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

type index =
  | Inone
348
  | IproofAttempt of proofAttemptID
349
  | IproofNode of proofNodeID
350
  | Itransformation  of transID
351 352 353 354
  | Ifile of file
  | Itheory of theory

let model_index : index Hint.t = Stdlib.Hint.create 17
355 356 357 358
(* 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

359 360 361

let new_node =
  let cpt = ref (-1) in
362
  fun ?parent ?(collapse=false) name ind ->
363 364 365 366 367 368
  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;
369
  let new_ref = goals_model#get_row_reference (goals_model#get_path iter) in
370 371
  (* By default expand_path when creating a new node *)
  if not collapse then goals_view#expand_to_path (goals_model#get_path iter);
372 373 374 375 376 377 378 379 380
  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
381

382
let build_subtree_proof_attempt_from_goal ses row_ref id =
383 384 385 386 387 388
  Whyconf.Hprover.iter
    (fun pa panid ->
     let name = Pp.string_of Whyconf.print_prover pa in
      ignore(new_node ~parent:row_ref name
                 (IproofAttempt panid)))
    (get_proof_attempt_ids ses id)
389 390

let rec build_subtree_from_goal ses th_row_reference id =
391
  let name = get_proof_name ses id in
392
  let row_ref =
393 394
    new_node ~parent:th_row_reference name.Ident.id_string
             (IproofNode id)
MARCHE Claude's avatar
MARCHE Claude committed
395
  in
396 397 398 399 400 401 402 403 404 405 406 407 408 409
  List.iter
    (fun trans_id ->
      build_subtree_from_trans ses row_ref trans_id)
    (get_transformations ses id);
  build_subtree_proof_attempt_from_goal ses row_ref id

and build_subtree_from_trans ses goal_row_reference trans_id =
  let name = get_transf_name ses trans_id in
  let row_ref =
    new_node ~parent:goal_row_reference name (Itransformation trans_id) in
  List.iter
    (fun goal_id ->
      (build_subtree_from_goal ses row_ref goal_id))
    (get_sub_tasks ses trans_id)
410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430

let build_tree_from_session ses =
  let files = get_files ses in
  Stdlib.Hstr.iter
    (fun _ file ->
       let file_row_reference = new_node file.file_name (Ifile file) in
       List.iter (fun th ->
                  let th_row_reference =
                    new_node ~parent:file_row_reference
                             (theory_name th).Ident.id_string
                             (Itheory th)
                  in
                  List.iter (build_subtree_from_goal ses th_row_reference)
                            (theory_goals th))
                 file.file_theories)
    files

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

431 432
(* 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. *)
433 434
let current_selected_index = ref Inone

435
(* Callback of a transformation *)
MARCHE Claude's avatar
MARCHE Claude committed
436
let callback_update_tree_transform ses status =
437 438
  match status with
  | TSdone trans_id ->
MARCHE Claude's avatar
MARCHE Claude committed
439 440 441 442
     let id = get_trans_parent ses trans_id in
     let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
     build_subtree_from_trans ses row_ref trans_id;
     (match Session_itp.get_sub_tasks ses trans_id with
443
      | first_goal :: _ ->
MARCHE Claude's avatar
MARCHE Claude committed
444 445
         (* Put the selection on the first goal *)
         goals_view#selection#select_iter (Hpn.find pn_id_to_gtree first_goal)#iter
446
      | [] -> ())
447 448
  | _ -> ()

449
let apply_transform ses t args =
450 451
  match !current_selected_index with
  | IproofNode id ->
MARCHE Claude's avatar
MARCHE Claude committed
452 453 454
     let callback = callback_update_tree_transform ses in
    C.schedule_transformation cont id t args ~callback
  | _ -> printf "Error: Give the name of the transformation@."
455 456 457


(* Callback of a proof_attempt *)
MARCHE Claude's avatar
MARCHE Claude committed
458 459 460 461
let callback_update_tree_proof ses panid pa_status =
  let pa = get_proof_attempt ses panid in
  let prover = pa.prover in
  let name = Pp.string_of Whyconf.print_prover prover in
462
  match pa_status with
MARCHE Claude's avatar
MARCHE Claude committed
463 464
  | Scheduled ->
     begin
465 466
       try
         let r = Hpan.find pan_id_to_gtree panid in
MARCHE Claude's avatar
MARCHE Claude committed
467 468 469 470 471 472 473 474 475 476 477 478 479
         goals_model#set ~row:r#iter ~column:name_column (name ^ " scheduled")
       with Not_found ->
         let parent_id = get_proof_attempt_parent ses panid in
         let parent = Hpn.find pn_id_to_gtree parent_id in
         ignore(new_node ~parent (name ^ " scheduled") (IproofAttempt panid))
     end
  | Done pr ->
     let r = Hpan.find pan_id_to_gtree panid in
     let res = Pp.string_of Call_provers.print_prover_result pr in
     goals_model#set ~row:r#iter ~column:name_column (name ^ " " ^ res)
  | Running ->
     let r = Hpan.find pan_id_to_gtree panid in
     goals_model#set ~row:r#iter ~column:name_column (name ^ " running")
480
  | _ ->  () (* TODO ? *)
481

482
let test_schedule_proof_attempt ses (p: Whyconf.config_prover) limit =
483 484
  match !current_selected_index with
  | IproofNode id ->
485
    let prover = p.Whyconf.prover in
MARCHE Claude's avatar
MARCHE Claude committed
486 487
    let callback = callback_update_tree_proof ses in
    C.schedule_proof_attempt cont id prover ~limit ~callback
488
  | _ -> message_zone#buffer#set_text ("Must be on a proof node to use a prover.")
489

MARCHE Claude's avatar
MARCHE Claude committed
490 491 492 493 494 495 496 497 498 499 500 501 502 503 504

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
505 506 507 508 509 510 511
          let callback_pa =
            callback_update_tree_proof cont.controller_session
          in
          let callback_tr st =
            callback_update_tree_transform cont.controller_session st
          in
          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
MARCHE Claude's avatar
MARCHE Claude committed
512 513
    | _ -> printf "Strategy '%s' not found@." s
     end
514 515
  | _ -> (
)
MARCHE Claude's avatar
MARCHE Claude committed
516

517
let clear_command_entry () = command_entry#set_text ""
MARCHE Claude's avatar
MARCHE Claude committed
518

Sylvain Dailler's avatar
Sylvain Dailler committed
519 520 521 522
let current_id id =
  match id with
  | IproofNode id -> id
  | _ -> assert (false) (* TODO *)
MARCHE Claude's avatar
MARCHE Claude committed
523 524

let interp cmd =
Sylvain Dailler's avatar
Sylvain Dailler committed
525 526
  let id = current_id !current_selected_index in
  match interp cont.controller_env id cont.controller_session cmd with
527 528 529 530 531
    | Transform(s,_t,args) ->
       clear_command_entry ();
       apply_transform cont.controller_session s args
    | Query s ->
       message_zone#buffer#set_text s
532 533 534 535 536 537 538 539
    | Other(s,args) ->
      begin
        match parse_prover_name gconfig.config s args with
        | Some (prover_config, limit) ->
          clear_command_entry ();
          test_schedule_proof_attempt cont.controller_session prover_config limit
        | None ->
          match s with
MARCHE Claude's avatar
MARCHE Claude committed
540 541 542 543 544 545 546 547 548
       | "auto" ->
           let s =
             match args with
               | "2"::_ -> "2"
               | _ -> "1"
           in
           clear_command_entry ();
           run_strategy_on_task s
       | _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
549
      end
MARCHE Claude's avatar
MARCHE Claude committed
550 551 552 553 554 555
(*
       match s with
       | "c" -> clear_command_entry ();
                test_schedule_proof_attempt cont.controller_session
       | _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
 *)
MARCHE Claude's avatar
MARCHE Claude committed
556 557 558

let (_ : GtkSignal.id) =
  command_entry#connect#activate
559
    ~callback:(fun () -> add_command list_commands command_entry#text; interp command_entry#text)
560 561


562 563 564 565 566 567 568 569
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
570 571
    let session_element = Hint.find model_index index in
    let () = match session_element with
572
             | IproofNode id -> Hpn.add pn_id_to_gtree id r (* TODO maybe not the good place to fill
573 574 575 576
                                                                    this table *)
             | _ -> () in
    current_selected_index := session_element;
    match session_element with
577 578 579 580 581
    | 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
582 583 584
       in task_view#source_buffer#set_text s;
       (* scroll to end of text *)
       task_view#scroll_to_mark `INSERT
585 586 587 588 589 590 591 592 593 594 595 596
    | _ -> 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
        | _ -> ())

(***********************)
597
(* start the interface *)
598
(***********************)
599 600

let () =
601 602
  build_tree_from_session cont.controller_session;
  (* temporary *)
603
  init_comp ();
Clément Fumex's avatar
Clément Fumex committed
604
  vpan222#set_position 500;
605
  goals_view#expand_all ();
606 607 608 609
  main_window#add_accel_group accel_group;
  main_window#set_icon (Some !Gconfig.why_icon);
  main_window#show ();
  GMain.main ()