diff --git a/src/trywhy3/alt_ergo_worker.ml b/src/trywhy3/alt_ergo_worker.ml index c947edc03d38af8b1663160df1b746aeb3efc5bd..98b4da5dec33df2712475d14b554c75b6aff5436 100644 --- a/src/trywhy3/alt_ergo_worker.ml +++ b/src/trywhy3/alt_ergo_worker.ml @@ -48,6 +48,8 @@ let run_alt_ergo_on_task text = let () = Options.set_steps_bound 100; Worker.set_onmessage (fun msg -> - let (id, text) = unmarshal msg in - let result = run_alt_ergo_on_task text in - Worker.post_message (marshal (id,result))) + match unmarshal msg with + Task (id, text) -> + let result = run_alt_ergo_on_task text in + Worker.post_message (marshal (id,result)) + | OptionSteps i -> Options.set_steps_bound i) diff --git a/src/trywhy3/editor_helper.js b/src/trywhy3/editor_helper.js index e9145bdc2c587c86951c6a75b458d3c7f0e9b29e..ff1f23be77f6b2e370f9e40c18472fd91d49aa1b 100644 --- a/src/trywhy3/editor_helper.js +++ b/src/trywhy3/editor_helper.js @@ -147,24 +147,12 @@ function widescreenView() { var e = document.getElementById("editor"); var c = document.getElementById("console"); - e.style.width = "50%"; + e.style.width = "60%"; e.style.height = "100%"; c.style.width = "40%"; c.style.height = "100%"; editor.focus(); } -function prove() -{ - document.getElementById("console").innerHTML = "

Execution feature is not yet implemented

"; - console.focus(); - editor.focus(); -} - -function prove() -{ - document.getElementById("console").innerHTML = "

Call to Why3 is not yet implemented

"; - editor.focus(); -} editor.focus(); diff --git a/src/trywhy3/trywhy3.css b/src/trywhy3/trywhy3.css new file mode 100644 index 0000000000000000000000000000000000000000..cbdccdab2f6c317882a232ffc96d55cc14c559df --- /dev/null +++ b/src/trywhy3/trywhy3.css @@ -0,0 +1,253 @@ +@import url(fontawesome/fontawesome.css); + +/* fontawesome */ +[class*="fontawesome-"]:before { + font-family: 'FontAwesome', sans-serif; +} + + +/* ACE Editor */ +.error { + position:absolute; + background:rgba(200,100,100,0.5); + z-index:40; +} + +/* Interface */ +body { + padding:0; + margin:0; + font-family: sans-serif; +} + +#editor-panel { + height: 97vh; + box-sizing:border-box; + padding: 0; + margin: 0; +} + +#editor { + position:relative; + font-size: large; + box-sizing: border-box; + display:inline-block; + height:100%; + margin:0 0 0 0; + padding:0 0 0 0; + z-index:0; + vertical-align:top; + border-right: 1pt #ddd solid; + border-bottom: 1pt #ddd solid; + width:59%; +} + +#console { + box-sizing: border-box; + overflow: auto; + position:relative; + display:inline-block; + width:40%; + height:100%; + margin:0 0 0 0; + padding:0 0 0 0; + vertical-align:top; +} + +/* CSS MENU BAR */ + +.menu-bar { + margin:0; + z-index:10; + font-size:2vh; + height:3vh; + padding:0; +} + +.menu-bar:after { + content:""; + display:table; + clear:both; +} + +.menu-bar ul { + padding:0; + margin:0; + list-style: none; + position: relative; + background-image: linear-gradient(to bottom, #eee, #ccc); + height:3vh; + z-index:10; + box-sizing:border-box; + } + +/* Positioning the navigation items inline */ + +.menu-bar ul li { + margin: 0; + padding: 0; + display: inline-block; + float: left; + height: 100%; + box-sizing:border-box; +} + +/* Styling the links */ +.menu-bar > ul > li > span { + display:block; + padding:0pt 1em; + color:#444; + text-decoration:none; + border-radius: 5pt 5pt 0pt 0pt; + border-style:solid; + border-width:1pt; + border-color:transparent; + height:100%; + box-sizing:border-box; + margin:0; +} + +/* Background color change on Hover */ +.menu-bar > ul > li > span:hover { + background-image: linear-gradient(to bottom, #eee, #bbb); + border-color: #aaa; + box-sizing:border-box; + +} +.menu-bar > ul > li > ul { +/* display:none;*/ + height:0; + overflow:hidden; + box-sizing:border-box; + opacity: 0; + transition: opacity .3s ease-in-out; + -webkit-transition: opacity .3s ease-in-out; + -moz-transition: opacity .3s ease-in-out; + -o-transition: opacity .3s ease-in-out; + -ms-transition: opacity .3s ease-in-out; +} +.menu-bar > ul > li:hover > ul { + height:auto; + background-color:#ddd; + box-shadow:0pt 0pt 5pt #444; + opacity:1; +} +.menu-bar > ul > li > ul > li { + float:left; + display: inline-block; + clear:left; + width: 100%; + position: relative; + +} +.menu-bar > ul > li > ul > li { + display:block; + padding:1pt 2pt 1pt 2pt; + color:#444; + text-decoration:none; + border-radius: 1pt; + border-style:solid; + border-width:1pt; + border-color:transparent; + box-sizing:border-box; + height: 100%; +} +.menu-bar > ul > li > ul > li:before { + display:inline-block; + content:""; + width:0pt; + height: 100%; + vertical-align:middle; +} +.menu-bar > ul > li > ul > li:hover { + border-color:#cce; + background-image: linear-gradient(to bottom, #abe, #68b); +} + +/* Hidden file selector */ +#file-selector { + position:absolute; + left:0; + top:0; + width:0; + height:0; + z-index:-1; +} + +#editor-panel { + position:relative; + display:block; + box-sizing: border-box; + padding:0; + margin:0; + height:97vh; +} + + +#console ul#theory-list { + list-style-type: none; + list-style-position: inside; + padding: 0.5em; + /*margin: 0.5em; */ +} +#console ul#theory-list li { + font-weight:bold; +} +#console ul#theory-list li * { + font-weight:normal; +} + +#console ul ul { + list-style-type: square; + list-style-position: inside; + + padding: 0.5em; + /*margin: 0.5em;*/ +} + +#console ul ul ul { + list-style-type: none; + list-style-position: inside; + + padding: 0.5em; + /*margin: 0.5em; */ +} + + +/* Confirmation dialog */ +.btn { + width:100%; + z-index:1; + margin:0 0 4pt 0; + box-sizing:border-box; +} + +#confirm-dialog { + z-index:20; + display:none; + position:absolute; + margin: 0 auto; + padding: 2pt 0; + width:50%; + left:25%; + right:25%; + top:20%; + border-radius:5pt; + background: #eee; + text-align:center; +} + +#background-shadow { + display:none; + background-color: rgba(0,0,0,0.8); + position:absolute; + width:100%; + height:100%; + top: 0; + left:0; + z-index:15; +} + +#confirm-dialog .btn { + width:40%; +} diff --git a/src/trywhy3/trywhy3.html b/src/trywhy3/trywhy3.html new file mode 100644 index 0000000000000000000000000000000000000000..45275bcb2d6ac2a38e7c024926e45952989f9cfe --- /dev/null +++ b/src/trywhy3/trywhy3.html @@ -0,0 +1,116 @@ + + + + + + + Try Why3 + + + + + + + + + +
+
+ The content of the current buffer will be lost + +
+
+ + +
+
+
+ + +
+
+
+
+
+ + + + + + diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml index 59c573b03568c6657c509aea8a35b79702445903..b6a900e4d1774fda2edfff1e11cebe79c12ea4a1 100644 --- a/src/trywhy3/trywhy3.ml +++ b/src/trywhy3/trywhy3.ml @@ -167,8 +167,8 @@ let task_queue = Queue.create () let first_task = ref true type 'a status = Free of 'a | Busy of 'a | Absent let num_workers = 4 - -let alt_ergo_workers = Array.make num_workers Absent +let alt_ergo_steps = ref 100 +let alt_ergo_workers = ref (Array.make num_workers Absent) let rec init_alt_ergo_worker i = let worker = Worker.create "alt_ergo_worker.js" in @@ -176,7 +176,7 @@ let rec init_alt_ergo_worker i = (Dom.handler (fun ev -> let (id, result) = unmarshal (ev ## data) in Console.print_alt_ergo_output id result; - alt_ergo_workers.(i) <- Free(worker); + !alt_ergo_workers.(i) <- Free(worker); process_task (); Js._false)); Free (worker) @@ -184,7 +184,7 @@ let rec init_alt_ergo_worker i = and process_task () = let rec find_free_worker_slot i = if i < num_workers then - match alt_ergo_workers.(i) with + match !alt_ergo_workers.(i) with Free _ as w -> i, w | _ -> find_free_worker_slot (i+1) else -1, Absent @@ -193,7 +193,8 @@ and process_task () = match w with Free w when not (Queue.is_empty task_queue) -> let task = Queue.take task_queue in - alt_ergo_workers.(idx) <- Busy (w); + !alt_ergo_workers.(idx) <- Busy (w); + w ## postMessage (marshal (OptionSteps !alt_ergo_steps)); w ## postMessage (marshal task) | _ -> () @@ -203,10 +204,10 @@ let reset_workers () = match w with Busy (w) -> w ## terminate (); - alt_ergo_workers.(i) <- init_alt_ergo_worker i - | Absent -> alt_ergo_workers.(i) <- init_alt_ergo_worker i + !alt_ergo_workers.(i) <- init_alt_ergo_worker i + | Absent -> !alt_ergo_workers.(i) <- init_alt_ergo_worker i | Free _ -> () - ) alt_ergo_workers + ) !alt_ergo_workers let push_task task = Queue.add task task_queue; @@ -224,19 +225,16 @@ let init_why3_worker () = Console.print_why3_output msg; let () = match msg with - Tasks (_,_,(id,_,code)) -> push_task (id,code) + Tasks (_,_,(id,_,code)) -> push_task (Task (id,code)) | _ -> () in Js._false)); - (* seems necessary to warm-up the worker and start loading - the script premptively *) - worker ## postMessage(marshal Init); worker let why3_worker = ref (init_why3_worker ()) let why3_parse () = Console.clear (); - Console.print_msg "Sending buffer to Alt-ergo … "; + Console.print_msg "Sending buffer to Alt-Ergo … "; log_time "Before marshalling in main thread"; reset_workers (); first_task := true; @@ -261,7 +259,34 @@ let () = !why3_worker ## terminate (); why3_worker := init_why3_worker (); reset_workers (); - Console.set_abort_icon()) + 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 + ) (* Predefined examples *) diff --git a/src/trywhy3/why3_worker.ml b/src/trywhy3/why3_worker.ml index ed841c074d8abed2a8fce25e420a0ae436d1df87..7967cd4dfb02cffb7cb7aefdd0bd23fe262bd7fd 100644 --- a/src/trywhy3/why3_worker.ml +++ b/src/trywhy3/why3_worker.ml @@ -217,7 +217,6 @@ let () = let ev = unmarshal ev in log_time ("After unmarshal "); match ev with - Init -> () | ParseBuffer code -> why3_run why3_parse_theories Env.base_language code | ExecuteBuffer code -> diff --git a/src/trywhy3/worker_proto.ml b/src/trywhy3/worker_proto.ml index 6bf07484a33b86004d8f03d7005940d759b66808..6421d08f4e2728e94d1cb3401a89d77452f920d5 100644 --- a/src/trywhy3/worker_proto.ml +++ b/src/trywhy3/worker_proto.ml @@ -1,16 +1,19 @@ -type command = ParseBuffer of string +type id = string + +type why3_command = ParseBuffer of string | ExecuteBuffer of string - | Init -type output = Error of string (* msg *) +type why3_output = Error of string (* msg *) | ErrorLoc of ((int*int*int*int) * string) (* loc * msg *) - | Tasks of ((string * string) (* Theory (id, name) *) - * (string * string) (* Task (id, name *) - * (string * string * string)) (* VC (id, expl, code ) *) + | Tasks of ((id * string) (* Theory (id, name) *) + * (id * string) (* Task (id, name *) + * (id * string * string)) (* VC (id, expl, code ) *) | Result of string list -type prover_answer = Valid | Unknown of string | Invalid of string +type prover_command = OptionSteps of int | Task of id * string + +type prover_output = Valid | Unknown of string | Invalid of string let marshal a = Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))