trywhy3.ml 12.3 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 19 20
(* the view *)
module Console =
  struct
Kim Nguyễn's avatar
Kim Nguyễn committed
21 22 23 24 25 26 27 28 29 30 31 32
    let highlightRegion s l1 c1 l2 c2 =
      ignore (Js.Unsafe.meth_call Js.Unsafe.global
                                  "highlightRegion"
                                  Js.Unsafe.( [| inject (Js.string s);
                                                inject l1;
                                                inject c1;
                                                inject l2;
                                                inject c2 |] ) )

    let clearHighlight ()=
      ignore (Js.Unsafe.meth_call Js.Unsafe.global
                                  "clearHighlight" [| |])
33
    let get_buffer () =
34 35
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
36 37 38
      Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |])

    let get_console () =
39
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57

    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
58 59
      let span_msg = Dom_html.getElementById (id ^ "_msg") in
      match res with
60
        Valid -> span_msg ## innerHTML <- Js.string ""
Kim Nguyễn's avatar
Kim Nguyễn committed
61 62
      | Unknown msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
      | Invalid msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
63 64 65 66

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

67 68 69 70 71 72 73 74 75 76 77 78
    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
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
    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;
99
	li ## innerHTML <- mk_li_content id expl
Kim Nguyễn's avatar
Kim Nguyễn committed
100 101


102 103 104 105 106 107
    let task_selection = Hashtbl.create 17
    let task_deselect () =
      Hashtbl.iter (fun _ span -> span ## classList ## remove (Js.string "task-selected"))
                   task_selection;
      Hashtbl.clear task_selection

108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
    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) ->
         ignore (Js.Unsafe.meth_call Js.Unsafe.global
                                     "highlightError"
                                     (Array.map Js.Unsafe.inject [| l1; b; l2; e |]));
         print_error s
      | 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

128 129 130
      | Theory (th_id, th_name) ->
	 attach_to_parent th_id "theory-list" th_name []

Kim Nguyễn's avatar
Kim Nguyễn committed
131
      | Task (id, parent_id, expl, _code, loc) ->
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
	 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
		span ## onclick <-
		  Dom.handler
		    (fun ev ->
		     let ctrl = Js.to_bool (ev ## ctrlKey) in
		     if Hashtbl.mem task_selection id then
                       if ctrl then
			 begin
			   Hashtbl.remove task_selection id;
			   (span ## classList) ## remove (Js.string "task-selected");
			 end
                       else
			 task_deselect ()
		     else begin
			 if not ctrl then task_deselect ();
			 Hashtbl.add task_selection id span;
			 (span ## classList) ## add (Js.string "task-selected")
                       end;
		     Js._false)
	 end


Kim Nguyễn's avatar
Kim Nguyễn committed
159 160 161 162 163 164 165 166 167 168 169 170
      | 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 -> ()
171 172

    let set_abort_icon () =
Kim Nguyễn's avatar
Kim Nguyễn committed
173
      let list = Dom_html.document ## getElementsByClassName (Js.string "task-pending") in
174
      List.iter (fun span ->
Kim Nguyễn's avatar
Kim Nguyễn committed
175
                 span ## className <- (Js.string "fontawesome-minus-sign task-abort"))
176 177 178 179 180 181 182 183 184 185 186 187 188
                (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
189
  in
190
  let button =
191
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
192 193
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
194

195 196 197 198 199

let task_queue  = Queue.create ()
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
200 201
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
202 203 204 205 206
let why3_worker = ref None
let get_why3_worker () =
  match !why3_worker with
    Some w -> w
  | None -> log ("Why3 Worker not initialized !"); assert false
207 208 209 210 211

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
212
                  let (id, result) as res = unmarshal (ev ## data) in
213
                  Console.print_alt_ergo_output id result;
Kim Nguyễn's avatar
Kim Nguyễn committed
214
                  (get_why3_worker()) ## postMessage (marshal (status_of_result res));
215
                  !alt_ergo_workers.(i) <- Free(worker);
216 217 218 219 220 221 222
                  process_task ();
                  Js._false));
  Free (worker)

and process_task () =
  let rec find_free_worker_slot i =
    if i < num_workers then
223
      match !alt_ergo_workers.(i) with
224 225 226 227 228 229 230 231
        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
232 233
    !alt_ergo_workers.(idx) <- Busy (w);
    w ## postMessage (marshal (OptionSteps !alt_ergo_steps));
234 235 236 237 238 239 240 241 242
    w ## postMessage (marshal task)
  | _ -> ()

let reset_workers () =
  Array.iteri
    (fun i w ->
     match w with
       Busy (w)  ->
                   w ## terminate ();
243 244
                   !alt_ergo_workers.(i) <- init_alt_ergo_worker i
     | Absent -> !alt_ergo_workers.(i) <- init_alt_ergo_worker i
245
     | Free _ -> ()
246
    ) !alt_ergo_workers
247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263

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
264 265 266
                      Task (id,_,_,code,_) ->
		      log ("Got task " ^ id);
		      push_task (Goal (id,code))
267 268 269 270
                    | _ -> ()
                  in Js._false));
  worker

Kim Nguyễn's avatar
Kim Nguyễn committed
271
let () = why3_worker := Some (init_why3_worker ())
272 273 274

let why3_parse () =
  Console.clear ();
275
  Console.print_msg "Sending buffer to Alt-Ergo … ";
276 277 278 279 280 281
  log_time "Before marshalling in main thread";
  reset_workers ();
  first_task := true;
  let code = Console.get_buffer () in
  let msg = marshal (ParseBuffer code) in
  log_time "After marshalling in main thread";
Kim Nguyễn's avatar
Kim Nguyễn committed
282
  (get_why3_worker()) ## postMessage (msg)
283 284 285 286 287 288 289

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

292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
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;
      Console.task_deselect ()
    end

313

314
let () =
315
  add_button "prove_all" why3_parse ;
316 317
  add_button "run" why3_execute ;
  add_button "stop" (fun () ->
Kim Nguyễn's avatar
Kim Nguyễn committed
318 319
                     (get_why3_worker()) ## terminate ();
                     why3_worker := Some (init_why3_worker ());
320
                     reset_workers ();
321
                     Console.set_abort_icon());
322 323 324
  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
325

326 327 328 329 330 331 332 333 334 335 336 337 338 339
  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
340

341 342 343 344 345 346 347 348 349 350 351 352 353
  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
      )
354

355

356
(* Predefined examples *)
357

358
let add_file_example (buttonname, file) =
359 360
  let handler = Dom.handler
    (fun _ev ->
361
      let text = Sys_js.file_content file in
362 363 364 365 366 367
      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" [| |]);
368
      Console.clear ();
369
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
370

371 372 373 374 375 376 377 378
      Js._false)
  in
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
  in
  button ## onclick <- handler

let () =
379 380 381
  let files =
    [
      "drinkers", "/drinkers.why";
382
(*  add_file_example "simplearith" "/simplearith.why";*)
383 384 385 386 387 388
      "bin_mult", "/bin_mult.mlw";
      "fact", "/fact.mlw";
      "isqrt", "/isqrt.mlw"
    ]
  in
  List.iter add_file_example files;
389

MARCHE Claude's avatar
MARCHE Claude committed
390 391 392

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