trywhy3.ml 14.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12
(* simple helpers *)
13
open Worker_proto
14

15
let get_opt o = Js.Opt.get o (fun () -> assert false)
16 17


18
(* the view *)
19
module Editor =
20
  struct
21 22 23 24 25 26 27 28 29 30
    type range
    type marker
    let editor =
      let open Js.Unsafe in
      get global (Js.string "editor")

    let get_buffer_js () : Js.js_string Js.t =
      let open Js.Unsafe in
      meth_call editor "getValue" [| |]

31
    let get_buffer () =
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
      Js.to_string (get_buffer_js ())

    let mk_range l1 c1 l2 c2 =
      let open Js.Unsafe in
      let range : (int -> int -> int -> int -> range Js.t) Js.constr =
        get global (Js.string "Range")
      in
      jsnew range (l1, c1, l2, c2)

    let set_selection_range r =
      let open Js.Unsafe in
      let selection = meth_call editor "getSelection" [| |] in
      ignore (meth_call selection "setSelectionRange" [| inject r |])

    let add_marker cls r : marker =
      let open Js.Unsafe in
      let session = meth_call editor "getSession" [| |] in
      meth_call session "addMarker"
                                 [| inject r;
                                    inject (Js.string cls);
                                    inject (Js.string "text") |]

    let remove_marker m =
      let open Js.Unsafe in
      let session = meth_call editor "getSession" [| |] in
      ignore (meth_call session "removeMarker" [| inject  m|])

    let get_char buffer i = int_of_float (buffer ## charCodeAt(i))
    let why3_loc_to_range buffer loc =
      let goto_line lstop =
        let rec loop lcur i =
          if lcur == lstop then i
          else
            let c = get_char buffer i in
            loop (if c == 0 then lcur+1 else lcur) (i+1)
        in
        loop 1 0
      in
      let rec convert_range l c i n =
        if n == 0 then (l, c) else
          if (get_char buffer i) == 10
          then convert_range (l+1) 0 (i+1) (n-1)
          else convert_range l (c+1) (i+1) (n-1)
      in
      let l1, b, e = loc in
      let c1 = b in
      let i = goto_line l1 in
      let l2, c2 = convert_range l1 b (i+b) (e-b) in
      mk_range (l1-1) c1 (l2-1) c2

    let set_on_event e f =
      let open Js.Unsafe in
      ignore (meth_call editor "on" [| inject (Js.string e);
                                       inject f|])
  end

module Console =
  struct
90 91

    let get_console () =
92
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110

    let clear () =
      (get_console ()) ## innerHTML <- (Js.string "")

    let print cls msg =
        (get_console ()) ## innerHTML <-
          (Js.string ("<p class='" ^ cls ^ "'>" ^
                        msg ^ "</p>"))

    let print_error = print "error"

    let print_msg = print "msg"

    let node_to_html n =
      Dom_html.element (get_opt (Dom.CoerceTo.element (get_opt n)))

    let print_alt_ergo_output id res =
      (* see alt_ergo_worker.ml and the Tasks case in print_why3_output *)
Kim Nguyễn's avatar
Kim Nguyễn committed
111 112
      let span_msg = Dom_html.getElementById (id ^ "_msg") in
      match res with
113
        Valid -> span_msg ## innerHTML <- Js.string ""
Kim Nguyễn's avatar
Kim Nguyễn committed
114 115
      | Unknown msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
      | Invalid msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
116 117 118 119

    let appendChild o c =
      ignore (o ## appendChild ( (c :> Dom.node Js.t)))

120 121 122 123 124 125 126 127 128 129 130 131
    let mk_li_content id expl =
      Js.string (Format.sprintf
		   "<span id='%s_container'><span id='%s_icon'></span> %s <span id='%s_msg'></span></span><ul id='%s_ul'></ul>"
		   id id expl id id)

    let clean_task id =
      try
	let ul = Dom_html.getElementById (id ^ "_ul") in
	ul ## innerHTML <- Js.string ""
      with
	Not_found -> ()

Kim Nguyễn's avatar
Kim Nguyễn committed
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
    let attach_to_parent id parent_id expl _loc =
      let doc = Dom_html.document in
      let ul =
        try
          Dom_html.getElementById parent_id
        with
          Not_found ->
          let ul = Dom_html.createUl doc in
          ul ## id <- Js.string parent_id;
          appendChild (get_console()) ul;
          ul
      in
      try
        ignore (Dom_html.getElementById id);
        log ("li element " ^ id ^ " already exists !")
      with
        Not_found ->
        let li = Dom_html.createLi doc in
        li ## id <- Js.string id;
        appendChild ul li;
152
	li ## innerHTML <- mk_li_content id expl
Kim Nguyễn's avatar
Kim Nguyễn committed
153 154


155
    let task_selection = Hashtbl.create 17
156 157 158 159 160
    let is_selected id = Hashtbl.mem task_selection id
    let select_task id span loc =
      (span ## classList) ## add (Js.string "task-selected");
      let markers = List.map (Editor.add_marker "hl-task") loc in
      Hashtbl.add task_selection id (span, loc, markers)
161

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
    let deselect_task id =
      try
        let span, loc, markers = Hashtbl.find task_selection id in
        (span ## classList) ## remove (Js.string "task-selected");
        List.iter Editor.remove_marker markers;
        Hashtbl.remove task_selection id
      with
        Not_found -> ()

    let clear_task_selection () =
      let l = Hashtbl.fold (fun id _ acc -> id :: acc) task_selection [] in
      List.iter deselect_task l

    let error_marker = ref None
    let () =
      Editor.set_on_event
        "change"
        (Js.wrap_callback (fun () -> clear_task_selection ();
                                  match !error_marker with
                                    None -> ()
                                  | Some (m, _) -> Editor.remove_marker m))

    let () =
      Editor.set_on_event
        "focus"
        (Js.wrap_callback (fun () ->
                           clear_task_selection ();
                           match !error_marker with
                             None -> ()
                           | Some (_, r) -> Editor.set_selection_range r))
192 193 194 195 196 197 198
    let print_why3_output o =
      let doc = Dom_html.document in
      (* see why3_worker.ml *)
      match o with
        Error s -> print_error s

      | ErrorLoc ((l1, b, l2, e), s) ->
199 200
         let r = Editor.mk_range l1 b l2 e in
         error_marker := Some (Editor.add_marker "error" r, r);
201
         print_error s
202

203 204 205 206 207 208 209 210 211
      | Result sl ->
         clear ();
         let ul = Dom_html.createUl doc in
         appendChild (get_console()) ul;
         List.iter (fun (s : string) ->
                    let li = Dom_html.createLi doc in
                    li ## innerHTML <- (Js.string s);
                    appendChild ul li;) sl

212 213 214
      | Theory (th_id, th_name) ->
	 attach_to_parent th_id "theory-list" th_name []

Kim Nguyễn's avatar
Kim Nguyễn committed
215
      | Task (id, parent_id, expl, _code, loc) ->
216 217 218 219 220 221
	 begin
	   try
	     ignore (Dom_html.getElementById id)
	   with Not_found ->
		attach_to_parent id (parent_id ^ "_ul") expl loc;
		let span = Dom_html.getElementById (id ^ "_container") in
222 223
                let buffer = Editor.get_buffer_js () in
                let loc = List.map (Editor.why3_loc_to_range buffer) loc in
224 225 226 227
		span ## onclick <-
		  Dom.handler
		    (fun ev ->
		     let ctrl = Js.to_bool (ev ## ctrlKey) in
228 229 230
		     if is_selected id then
                       if ctrl then deselect_task id else
			 clear_task_selection ()
231
		     else begin
232 233
			 if not ctrl then clear_task_selection ();
                         select_task id span loc
234 235 236 237 238
                       end;
		     Js._false)
	 end


Kim Nguyễn's avatar
Kim Nguyễn committed
239 240 241 242 243 244 245 246 247 248 249 250
      | UpdateStatus(st, id) ->
         try
           let span_icon = Dom_html.getElementById (id ^ "_icon") in
           let cls =
             match st with
               `New -> "fontawesome-cogs task-pending"
             | `Valid -> "fontawesome-ok-sign task-valid"
             | `Unknown -> "fontawesome-question-sign task-unknown"
           in
           span_icon ## className <- Js.string cls
         with
           Not_found -> ()
251 252

    let set_abort_icon () =
Kim Nguyễn's avatar
Kim Nguyễn committed
253
      let list = Dom_html.document ## getElementsByClassName (Js.string "task-pending") in
254
      List.iter (fun span ->
Kim Nguyễn's avatar
Kim Nguyễn committed
255
                 span ## className <- (Js.string "fontawesome-minus-sign task-abort"))
256 257 258 259 260 261 262 263 264 265 266 267 268
                (Dom.list_of_nodeList list)

  end

let add_button buttonname f =
  let handler =
    Dom.handler
      (fun _ev ->
       f ();
       let global = Js.Unsafe.global in
       let editor = Js.Unsafe.get global (Js.string "editor") in
       ignore (Js.Unsafe.meth_call editor "focus" [| |]);
       Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
269
  in
270
  let button =
271
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
272 273
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
274

275 276 277 278 279

let task_queue  = Queue.create ()
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
280 281
let alt_ergo_steps = ref 100
let alt_ergo_workers = ref (Array.make num_workers Absent)
Kim Nguyễn's avatar
Kim Nguyễn committed
282 283 284 285 286
let why3_worker = ref None
let get_why3_worker () =
  match !why3_worker with
    Some w -> w
  | None -> log ("Why3 Worker not initialized !"); assert false
287 288 289 290 291

let rec init_alt_ergo_worker i =
  let worker = Worker.create "alt_ergo_worker.js" in
  worker ## onmessage <-
    (Dom.handler (fun ev ->
Kim Nguyễn's avatar
Kim Nguyễn committed
292
                  let (id, result) as res = unmarshal (ev ## data) in
293
                  Console.print_alt_ergo_output id result;
Kim Nguyễn's avatar
Kim Nguyễn committed
294
                  (get_why3_worker()) ## postMessage (marshal (status_of_result res));
295
                  !alt_ergo_workers.(i) <- Free(worker);
296 297 298 299 300 301 302
                  process_task ();
                  Js._false));
  Free (worker)

and process_task () =
  let rec find_free_worker_slot i =
    if i < num_workers then
303
      match !alt_ergo_workers.(i) with
304 305 306 307 308 309 310 311
        Free _ as w -> i, w
      | _ -> find_free_worker_slot (i+1)
    else -1, Absent
  in
  let idx, w = find_free_worker_slot 0 in
  match w with
    Free w when not (Queue.is_empty task_queue) ->
    let task = Queue.take task_queue in
312 313
    !alt_ergo_workers.(idx) <- Busy (w);
    w ## postMessage (marshal (OptionSteps !alt_ergo_steps));
314 315 316 317 318 319 320 321 322
    w ## postMessage (marshal task)
  | _ -> ()

let reset_workers () =
  Array.iteri
    (fun i w ->
     match w with
       Busy (w)  ->
                   w ## terminate ();
323 324
                   !alt_ergo_workers.(i) <- init_alt_ergo_worker i
     | Absent -> !alt_ergo_workers.(i) <- init_alt_ergo_worker i
325
     | Free _ -> ()
326
    ) !alt_ergo_workers
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343

let push_task task =
  Queue.add  task task_queue;
  process_task ()

let init_why3_worker () =
  let worker = Worker.create "why3_worker.js" in
  worker ## onmessage <-
    (Dom.handler (fun ev ->
                  let msg = unmarshal (ev ## data) in
                  if !first_task then begin
                      first_task := false;
                      Console.clear ()
                    end;
                  Console.print_why3_output msg;
                  let () =
                    match msg with
344 345 346
                      Task (id,_,_,code,_) ->
		      log ("Got task " ^ id);
		      push_task (Goal (id,code))
347 348 349 350
                    | _ -> ()
                  in Js._false));
  worker

Kim Nguyễn's avatar
Kim Nguyễn committed
351
let () = why3_worker := Some (init_why3_worker ())
352 353 354

let why3_parse () =
  Console.clear ();
355
  Console.print_msg "Sending buffer to Alt-Ergo … ";
356 357 358
  log_time "Before marshalling in main thread";
  reset_workers ();
  first_task := true;
359
  let code = Editor.get_buffer () in
360 361
  let msg = marshal (ParseBuffer code) in
  log_time "After marshalling in main thread";
Kim Nguyễn's avatar
Kim Nguyễn committed
362
  (get_why3_worker()) ## postMessage (msg)
363 364 365 366 367 368

let why3_execute () =
  Console.clear ();
  Console.print_msg "Compiling buffer … ";
  log_time "Before marshalling in main thread";
  reset_workers ();
369
  let code = Editor.get_buffer () in
Kim Nguyễn's avatar
Kim Nguyễn committed
370
   (get_why3_worker()) ## postMessage (marshal (ExecuteBuffer code))
371

372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
let array_for_all a f =
  let rec loop i n =
    if i < n then (f a.(i)) && loop (i+1) n
    else true
  in
  loop 0 (Array.length a)

let alt_ergo_not_running () =
  array_for_all !alt_ergo_workers (function Busy _ -> false | _ -> true)

let why3_transform tr f () =
  if alt_ergo_not_running () then
    begin
      Hashtbl.iter
        (fun id _ ->
	 f id;
	 (get_why3_worker()) ## postMessage (marshal (Transform(tr, id))))
	Console.task_selection;
390
      Console.clear_task_selection ()
391 392
    end

393

394
let () =
395
  add_button "prove_all" why3_parse ;
396 397
  add_button "run" why3_execute ;
  add_button "stop" (fun () ->
Kim Nguyễn's avatar
Kim Nguyễn committed
398 399
                     (get_why3_worker()) ## terminate ();
                     why3_worker := Some (init_why3_worker ());
400
                     reset_workers ();
401
                     Console.set_abort_icon());
402 403 404
  add_button "prove" (why3_transform `Prove (fun _ -> ()));
  add_button "split_prove" (why3_transform `Split (fun _ -> ()));
  add_button "clean" (why3_transform `Clean Console.clean_task);
Kim Nguyễn's avatar
Kim Nguyễn committed
405

406 407 408 409 410 411 412 413 414 415 416 417 418 419
  let input_threads = get_opt Dom_html.(CoerceTo.input
					  (getElementById "input-num-threads"))
  in
  input_threads ## oninput <-
    Dom.handler
      (fun ev ->
       let len = int_of_string (Js.to_string (input_threads ## value)) in
       Array.iter (function Busy (w) | Free (w) -> w ## terminate () | _ -> ())
		  !alt_ergo_workers;
       log (string_of_int len);
       alt_ergo_workers := Array.make len Absent;
       Console.set_abort_icon();
       Js._false
      );
Kim Nguyễn's avatar
Kim Nguyễn committed
420

421 422 423 424 425 426 427 428 429 430 431 432 433
  let input_steps = get_opt Dom_html.(CoerceTo.input
					  (getElementById "input-num-steps"))
  in
  input_steps ## oninput <-
    Dom.handler
      (fun ev ->
       let steps = int_of_string (Js.to_string (input_steps ## value)) in
       log(string_of_int steps);
       alt_ergo_steps := steps;
       reset_workers ();
       Console.set_abort_icon();
       Js._false
      )
434

435

436
(* Predefined examples *)
437

438
let add_file_example (buttonname, file) =
439 440
  let handler = Dom.handler
    (fun _ev ->
441
      let text = Sys_js.file_content file in
442 443 444 445 446 447
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
      Js.Unsafe.set global (Js.string "loadedBuffer") (Js.string text);
      let loaded = Filename.basename file in
      Js.Unsafe.set global (Js.string "loadedFilename") (Js.string loaded);
      ignore (Js.Unsafe.meth_call global "replaceWithLoaded" [| |]);
448
      Console.clear ();
449
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
450

451 452 453 454 455 456 457 458
      Js._false)
  in
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
  in
  button ## onclick <- handler

let () =
459 460 461
  let files =
    [
      "drinkers", "/drinkers.why";
462
(*  add_file_example "simplearith" "/simplearith.why";*)
463 464 465 466 467 468
      "bin_mult", "/bin_mult.mlw";
      "fact", "/fact.mlw";
      "isqrt", "/isqrt.mlw"
    ]
  in
  List.iter add_file_example files;
469

MARCHE Claude's avatar
MARCHE Claude committed
470 471 472

(*
Local Variables:
Kim Nguyễn's avatar
Kim Nguyễn committed
473
compile-command: "unset LANG; make -C ../.. trywhy3"
MARCHE Claude's avatar
MARCHE Claude committed
474 475
End:
*)