trywhy3.ml 10.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 19 20 21
(* the view *)
module Console =
  struct
    let get_buffer () =
22 23
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
24 25 26
      Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |])

    let get_console () =
27
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
28 29 30 31 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 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 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 156 157 158

    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 *)
      let doc = Dom_html.document in
      match Js.Opt.to_option (doc ## getElementById (Js.string id)) with
        None -> log ("No element with id " ^ id)
      | Some li ->
         let span_icon = node_to_html ( li ## firstChild ) in
         let span_msg = node_to_html ( li ## lastChild ) in
         match res with
           Valid ->
           span_icon ## className <- (Js.string "fontawesome-ok-sign");
           (span_icon ## style) ## color <- (Js.string "green");

         | Unknown msg ->
            span_icon ## className <- (Js.string "fontawesome-question-sign");
            (span_icon ## style) ## color <- (Js.string "orange");
            span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
         | Invalid msg ->
            span_icon ## className <- (Js.string "fontawesome-remove-sign");
            (span_icon ## style) ## color <- (Js.string "red");
            span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))

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

    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


      | Tasks ((th_id, th_name),
               (task_id, task_name),
               (vc_id, vc_expl, vc_code)) ->

         let ul =
           try
             Dom_html.getElementById "theory-list"
           with
             Not_found ->
             let ul = Dom_html.createUl doc in
             ul ## id <- Js.string "theory-list";
             appendChild (get_console()) ul;
             ul
         in
         let th_ul =
           try
             node_to_html ((Dom_html.getElementById th_id) ## lastChild)
           with
             Not_found ->
             let li = Dom_html.createLi doc in
             li ## id <- Js.string th_id;
             appendChild ul li;
             appendChild li (doc ## createTextNode (Js.string th_name));
             let tul = Dom_html.createUl doc in
             appendChild li tul;
             tul
         in
         let task_ul =
           try
             node_to_html ((Dom_html.getElementById  task_id) ## lastChild)
           with
             Not_found ->
             let li = Dom_html.createLi doc in
             li ## id <- Js.string task_id;
             appendChild th_ul li;
             appendChild li (doc ## createTextNode (Js.string task_name));
             let tul = Dom_html.createUl doc in
             appendChild li tul;
             tul
         in
         let li = Dom_html.createLi doc in
         li ## id <- Js.string vc_id;
         appendChild task_ul li;
         let span = Dom_html.createSpan doc in
         span ## className <- Js.string "fontawesome-cogs pending";
         (span ## style) ## color <- (Js.string "blue");

         appendChild li (span);
         appendChild li (doc ## createTextNode (Js.string (" " ^ vc_expl ^ " ")));
         appendChild li (Dom_html.createSpan doc)

    let set_abort_icon () =
      let list = Dom_html.document ## getElementsByClassName (Js.string "pending") in
      List.iter (fun span ->
                 span ## className <- (Js.string "fontawesome-minus-sign");
                 (span ## style) ## color <- (Js.string "black"))
                (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
159
  in
160
  let button =
161
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
162 163
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
164

165 166 167 168 169

let task_queue  = Queue.create ()
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
170 171
let alt_ergo_steps = ref 100
let alt_ergo_workers = ref (Array.make num_workers Absent)
172 173 174 175 176 177 178

let rec init_alt_ergo_worker i =
  let worker = Worker.create "alt_ergo_worker.js" in
  worker ## onmessage <-
    (Dom.handler (fun ev ->
                  let (id, result) = unmarshal (ev ## data) in
                  Console.print_alt_ergo_output id result;
179
                  !alt_ergo_workers.(i) <- Free(worker);
180 181 182 183 184 185 186
                  process_task ();
                  Js._false));
  Free (worker)

and process_task () =
  let rec find_free_worker_slot i =
    if i < num_workers then
187
      match !alt_ergo_workers.(i) with
188 189 190 191 192 193 194 195
        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
196 197
    !alt_ergo_workers.(idx) <- Busy (w);
    w ## postMessage (marshal (OptionSteps !alt_ergo_steps));
198 199 200 201 202 203 204 205 206
    w ## postMessage (marshal task)
  | _ -> ()

let reset_workers () =
  Array.iteri
    (fun i w ->
     match w with
       Busy (w)  ->
                   w ## terminate ();
207 208
                   !alt_ergo_workers.(i) <- init_alt_ergo_worker i
     | Absent -> !alt_ergo_workers.(i) <- init_alt_ergo_worker i
209
     | Free _ -> ()
210
    ) !alt_ergo_workers
211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227

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
228
                      Tasks (_,_,(id,_,code)) -> push_task (Task (id,code))
229 230 231 232 233 234 235 236
                    | _ -> ()
                  in Js._false));
  worker

let why3_worker = ref (init_why3_worker ())

let why3_parse () =
  Console.clear ();
237
  Console.print_msg "Sending buffer to Alt-Ergo … ";
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
  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";
  !why3_worker ## postMessage (msg)

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
  !why3_worker ## postMessage (marshal (ExecuteBuffer code))


255
let () =
256 257 258 259 260 261
  add_button "prove" why3_parse ;
  add_button "run" why3_execute ;
  add_button "stop" (fun () ->
                     !why3_worker ## terminate ();
                     why3_worker := init_why3_worker ();
                     reset_workers ();
262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289
                     Console.set_abort_icon());
  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
      );
  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
      )
290

291

292
(* Predefined examples *)
293

294
let add_file_example (buttonname, file) =
295 296
  let handler = Dom.handler
    (fun _ev ->
297
      let text = Sys_js.file_content file in
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
      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" [| |]);
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
      Js._false)
  in
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
  in
  button ## onclick <- handler

let () =
313 314 315
  let files =
    [
      "drinkers", "/drinkers.why";
316
(*  add_file_example "simplearith" "/simplearith.why";*)
317 318 319 320 321 322
      "bin_mult", "/bin_mult.mlw";
      "fact", "/fact.mlw";
      "isqrt", "/isqrt.mlw"
    ]
  in
  List.iter add_file_example files;
323

MARCHE Claude's avatar
MARCHE Claude committed
324 325 326 327 328 329

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
End:
*)