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
(* 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 60 61 62
      let span_msg = Dom_html.getElementById (id ^ "_msg") in
      match res with
        Valid -> ()
      | 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)))

Kim Nguyễn's avatar
Kim Nguyễn committed
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
    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;
        let span_icon = Dom_html.createSpan doc in
        appendChild li span_icon;
        span_icon ## id <- Js.string (id ^ "_icon");
        appendChild li (doc ## createTextNode (Js.string (" " ^ expl ^ " ")));
        let span_msg = Dom_html.createSpan doc in
        span_msg ## id <- Js.string (id ^ "_msg");
        appendChild li span_msg;
        let tul = Dom_html.createUl doc in
        tul ## id <- Js.string (id ^ "_ul");
        appendChild li tul


99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
    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

Kim Nguyễn's avatar
Kim Nguyễn committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
      | Theory (th_id, th_name) -> attach_to_parent th_id "theory-list" th_name []
      | Task (id, parent_id, expl, _code, loc) ->
         attach_to_parent id parent_id expl loc
      | 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 -> ()
134 135

    let set_abort_icon () =
Kim Nguyễn's avatar
Kim Nguyễn committed
136
      let list = Dom_html.document ## getElementsByClassName (Js.string "task-pending") in
137
      List.iter (fun span ->
Kim Nguyễn's avatar
Kim Nguyễn committed
138
                 span ## className <- (Js.string "fontawesome-minus-sign task-abort"))
139 140 141 142 143 144 145 146 147 148 149 150 151
                (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
152
  in
153
  let button =
154
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
155 156
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
157

158 159 160 161 162

let task_queue  = Queue.create ()
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
163 164
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
165 166 167 168 169
let why3_worker = ref None
let get_why3_worker () =
  match !why3_worker with
    Some w -> w
  | None -> log ("Why3 Worker not initialized !"); assert false
170 171 172 173 174

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
175
                  let (id, result) as res = unmarshal (ev ## data) in
176
                  Console.print_alt_ergo_output id result;
Kim Nguyễn's avatar
Kim Nguyễn committed
177
                  (get_why3_worker()) ## postMessage (marshal (status_of_result res));
178
                  !alt_ergo_workers.(i) <- Free(worker);
179 180 181 182 183 184 185
                  process_task ();
                  Js._false));
  Free (worker)

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

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

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
Kim Nguyễn's avatar
Kim Nguyễn committed
227
                      Task (id,_,_,code,_) -> push_task (Goal (id,code))
228 229 230 231
                    | _ -> ()
                  in Js._false));
  worker

Kim Nguyễn's avatar
Kim Nguyễn committed
232
let () = why3_worker := Some (init_why3_worker ())
233 234 235

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

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
251
   (get_why3_worker()) ## postMessage (marshal (ExecuteBuffer code))
252 253


254
let () =
255 256 257
  add_button "prove" why3_parse ;
  add_button "run" why3_execute ;
  add_button "stop" (fun () ->
Kim Nguyễn's avatar
Kim Nguyễn committed
258 259
                     (get_why3_worker()) ## terminate ();
                     why3_worker := Some (init_why3_worker ());
260
                     reset_workers ();
261
                     Console.set_abort_icon());
Kim Nguyễn's avatar
Kim Nguyễn committed
262

263 264 265 266 267 268 269 270 271 272 273 274 275 276
  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
277

278 279 280 281 282 283 284 285 286 287 288 289 290
  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
      )
291

292

293
(* Predefined examples *)
294

295
let add_file_example (buttonname, file) =
296 297
  let handler = Dom.handler
    (fun _ev ->
298
      let text = Sys_js.file_content file in
299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
      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 () =
314 315 316
  let files =
    [
      "drinkers", "/drinkers.why";
317
(*  add_file_example "simplearith" "/simplearith.why";*)
318 319 320 321 322 323
      "bin_mult", "/bin_mult.mlw";
      "fact", "/fact.mlw";
      "isqrt", "/isqrt.mlw"
    ]
  in
  List.iter add_file_example files;
324

MARCHE Claude's avatar
MARCHE Claude committed
325 326 327

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