Commit 9a4b07f6 authored by Kim Nguyễn's avatar Kim Nguyễn

[trywhy3]

 * Preliminary work to implement 'Split & Prove' command.
 * Move some hard-coded style information to the .css file.
parent af7e117b
...@@ -49,7 +49,7 @@ let () = ...@@ -49,7 +49,7 @@ let () =
Options.set_steps_bound 100; Options.set_steps_bound 100;
Worker.set_onmessage (fun msg -> Worker.set_onmessage (fun msg ->
match unmarshal msg with match unmarshal msg with
Task (id, text) -> Goal (id, text) ->
let result = run_alt_ergo_on_task text in let result = run_alt_ergo_on_task text in
Worker.post_message (marshal (id,result)) Worker.post_message (marshal (id,result))
| OptionSteps i -> Options.set_steps_bound i) | OptionSteps i -> Options.set_steps_bound i)
...@@ -13,6 +13,12 @@ function highlightError (x1, y1, x2, y2) ...@@ -13,6 +13,12 @@ function highlightError (x1, y1, x2, y2)
marker = editor.session.addMarker(selectedRange, "error", "text"); marker = editor.session.addMarker(selectedRange, "error", "text");
} }
function highlightRegion (cls, x1, y1, x2, y2)
{
selectedRange = new Range (x1,y1,x2,y2);
marker = editor.session.addMarker(selectedRange, cls, "text");
}
function clearHighlight () function clearHighlight ()
{ {
......
...@@ -6,13 +6,32 @@ ...@@ -6,13 +6,32 @@
} }
/* tasks icons */
.task-pending {
color: blue;
}
.task-valid {
color:green;
}
.task-unknown {
color:orange;
}
.task-abort {
color:black;
}
/* ACE Editor */ /* ACE Editor */
.error { .error {
position:absolute; position:absolute;
background:rgba(200,100,100,0.5); background:rgba(200,100,100,0.5);
z-index:40; z-index:40;
} }
.hl-task {
position:absolute;
background:rgba(200,200,100,0.5);
z-index:40;
}
/* Interface */ /* Interface */
body { body {
padding:0; padding:0;
...@@ -211,7 +230,7 @@ body { ...@@ -211,7 +230,7 @@ body {
#console ul#theory-list { #console ul#theory-list {
list-style-type: none; list-style-type: none;
list-style-position: inside; list-style-position: inside;
padding: 0.5em; padding-left: 0.5em;
} }
#console ul#theory-list li { #console ul#theory-list li {
font-weight:bold; font-weight:bold;
...@@ -221,22 +240,20 @@ body { ...@@ -221,22 +240,20 @@ body {
font-weight:normal; font-weight:normal;
} }
#console ul ul { #console ul#theory-list ul {
list-style-type: square; list-style-type: none;
list-style-position: inside; list-style-position: inside;
padding: 0.5em;
} }
#console ul ul ul { #console ul#theory-list ul > li {
padding-left:1em;
}
#console ul#theory-list ul ul {
list-style-type: none; list-style-type: none;
list-style-position: inside; list-style-position: inside;
padding-left: 0.5em;
padding: 0.5em;
/*margin: 0.5em; */
} }
/* Confirmation dialog */ /* Confirmation dialog */
.btn { .btn {
width:100%; width:100%;
......
...@@ -18,6 +18,18 @@ let get_opt o = Js.Opt.get o (fun () -> assert false) ...@@ -18,6 +18,18 @@ let get_opt o = Js.Opt.get o (fun () -> assert false)
(* the view *) (* the view *)
module Console = module Console =
struct struct
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" [| |])
let get_buffer () = let get_buffer () =
let global = Js.Unsafe.global in let global = Js.Unsafe.global in
let editor = Js.Unsafe.get global (Js.string "editor") in let editor = Js.Unsafe.get global (Js.string "editor") in
...@@ -43,29 +55,47 @@ module Console = ...@@ -43,29 +55,47 @@ module Console =
let print_alt_ergo_output id res = let print_alt_ergo_output id res =
(* see alt_ergo_worker.ml and the Tasks case in print_why3_output *) (* see alt_ergo_worker.ml and the Tasks case in print_why3_output *)
let doc = Dom_html.document in let span_msg = Dom_html.getElementById (id ^ "_msg") in
match Js.Opt.to_option (doc ## getElementById (Js.string id)) with match res with
None -> log ("No element with id " ^ id) Valid -> ()
| Some li -> | Unknown msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
let span_icon = node_to_html ( li ## firstChild ) in | Invalid msg -> span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
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 = let appendChild o c =
ignore (o ## appendChild ( (c :> Dom.node Js.t))) ignore (o ## appendChild ( (c :> Dom.node Js.t)))
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
let print_why3_output o = let print_why3_output o =
let doc = Dom_html.document in let doc = Dom_html.document in
(* see why3_worker.ml *) (* see why3_worker.ml *)
...@@ -86,63 +116,26 @@ module Console = ...@@ -86,63 +116,26 @@ module Console =
li ## innerHTML <- (Js.string s); li ## innerHTML <- (Js.string s);
appendChild ul li;) sl appendChild ul li;) sl
| Theory (th_id, th_name) -> attach_to_parent th_id "theory-list" th_name []
| Tasks ((th_id, th_name), | Task (id, parent_id, expl, _code, loc) ->
(task_id, task_name), attach_to_parent id parent_id expl loc
(vc_id, vc_expl, vc_code)) -> | UpdateStatus(st, id) ->
try
let ul = let span_icon = Dom_html.getElementById (id ^ "_icon") in
try let cls =
Dom_html.getElementById "theory-list" match st with
with `New -> "fontawesome-cogs task-pending"
Not_found -> | `Valid -> "fontawesome-ok-sign task-valid"
let ul = Dom_html.createUl doc in | `Unknown -> "fontawesome-question-sign task-unknown"
ul ## id <- Js.string "theory-list"; in
appendChild (get_console()) ul; span_icon ## className <- Js.string cls
ul with
in Not_found -> ()
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 set_abort_icon () =
let list = Dom_html.document ## getElementsByClassName (Js.string "pending") in let list = Dom_html.document ## getElementsByClassName (Js.string "task-pending") in
List.iter (fun span -> List.iter (fun span ->
span ## className <- (Js.string "fontawesome-minus-sign"); span ## className <- (Js.string "fontawesome-minus-sign task-abort"))
(span ## style) ## color <- (Js.string "black"))
(Dom.list_of_nodeList list) (Dom.list_of_nodeList list)
end end
...@@ -169,13 +162,19 @@ type 'a status = Free of 'a | Busy of 'a | Absent ...@@ -169,13 +162,19 @@ type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4 let num_workers = 4
let alt_ergo_steps = ref 100 let alt_ergo_steps = ref 100
let alt_ergo_workers = ref (Array.make num_workers Absent) let alt_ergo_workers = ref (Array.make num_workers Absent)
let why3_worker = ref None
let get_why3_worker () =
match !why3_worker with
Some w -> w
| None -> log ("Why3 Worker not initialized !"); assert false
let rec init_alt_ergo_worker i = let rec init_alt_ergo_worker i =
let worker = Worker.create "alt_ergo_worker.js" in let worker = Worker.create "alt_ergo_worker.js" in
worker ## onmessage <- worker ## onmessage <-
(Dom.handler (fun ev -> (Dom.handler (fun ev ->
let (id, result) = unmarshal (ev ## data) in let (id, result) as res = unmarshal (ev ## data) in
Console.print_alt_ergo_output id result; Console.print_alt_ergo_output id result;
(get_why3_worker()) ## postMessage (marshal (status_of_result res));
!alt_ergo_workers.(i) <- Free(worker); !alt_ergo_workers.(i) <- Free(worker);
process_task (); process_task ();
Js._false)); Js._false));
...@@ -225,12 +224,12 @@ let init_why3_worker () = ...@@ -225,12 +224,12 @@ let init_why3_worker () =
Console.print_why3_output msg; Console.print_why3_output msg;
let () = let () =
match msg with match msg with
Tasks (_,_,(id,_,code)) -> push_task (Task (id,code)) Task (id,_,_,code,_) -> push_task (Goal (id,code))
| _ -> () | _ -> ()
in Js._false)); in Js._false));
worker worker
let why3_worker = ref (init_why3_worker ()) let () = why3_worker := Some (init_why3_worker ())
let why3_parse () = let why3_parse () =
Console.clear (); Console.clear ();
...@@ -241,7 +240,7 @@ let why3_parse () = ...@@ -241,7 +240,7 @@ let why3_parse () =
let code = Console.get_buffer () in let code = Console.get_buffer () in
let msg = marshal (ParseBuffer code) in let msg = marshal (ParseBuffer code) in
log_time "After marshalling in main thread"; log_time "After marshalling in main thread";
!why3_worker ## postMessage (msg) (get_why3_worker()) ## postMessage (msg)
let why3_execute () = let why3_execute () =
Console.clear (); Console.clear ();
...@@ -249,17 +248,18 @@ let why3_execute () = ...@@ -249,17 +248,18 @@ let why3_execute () =
log_time "Before marshalling in main thread"; log_time "Before marshalling in main thread";
reset_workers (); reset_workers ();
let code = Console.get_buffer () in let code = Console.get_buffer () in
!why3_worker ## postMessage (marshal (ExecuteBuffer code)) (get_why3_worker()) ## postMessage (marshal (ExecuteBuffer code))
let () = let () =
add_button "prove" why3_parse ; add_button "prove" why3_parse ;
add_button "run" why3_execute ; add_button "run" why3_execute ;
add_button "stop" (fun () -> add_button "stop" (fun () ->
!why3_worker ## terminate (); (get_why3_worker()) ## terminate ();
why3_worker := init_why3_worker (); why3_worker := Some (init_why3_worker ());
reset_workers (); reset_workers ();
Console.set_abort_icon()); Console.set_abort_icon());
let input_threads = get_opt Dom_html.(CoerceTo.input let input_threads = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-threads")) (getElementById "input-num-threads"))
in in
...@@ -274,6 +274,7 @@ let () = ...@@ -274,6 +274,7 @@ let () =
Console.set_abort_icon(); Console.set_abort_icon();
Js._false Js._false
); );
let input_steps = get_opt Dom_html.(CoerceTo.input let input_steps = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-steps")) (getElementById "input-num-steps"))
in in
...@@ -324,6 +325,6 @@ let () = ...@@ -324,6 +325,6 @@ let () =
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js" compile-command: "unset LANG; make -C ../.. trywhy3"
End: End:
*) *)
...@@ -52,6 +52,7 @@ let alt_ergo_driver : Driver.driver = ...@@ -52,6 +52,7 @@ let alt_ergo_driver : Driver.driver =
let () = log_time ("Initialising why3 worker: end ") let () = log_time ("Initialising why3 worker: end ")
let task_table = Hashtbl.create 17
let split_trans = Trans.lookup_transform_l "split_goal_wp" env let split_trans = Trans.lookup_transform_l "split_goal_wp" env
...@@ -65,7 +66,63 @@ let gen_id = ...@@ -65,7 +66,63 @@ let gen_id =
fun () -> incr c; "id" ^ (string_of_int !c) fun () -> incr c; "id" ^ (string_of_int !c)
let send msg = let send msg =
Worker.post_message (marshal msg) ignore (Worker.post_message (marshal msg))
let get_loc l =
match l with
Some (l) ->
let _, l, c1, c2 = Loc.get l in
Some (l, c1, l, c2)
| _ -> None
let send_task parent_id task =
let id = gen_id () in
let () = Hashtbl.add task_table id (`Task (task), parent_id, `New, []) in
let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
let expl = match expl with
| Some s -> s
| None -> vid.Ident.id_string
in
let msg = Task (id, parent_id, expl, task_to_string task, [ (* TODO *) ]) in
send msg;
send (UpdateStatus(`New, id));
id
let get_task = function `Task t -> t
| `Theory _ -> log ("called get_task on a theory !"); assert false
let why3_split id =
try
let task, parent_id,_,subtasks = Hashtbl.find task_table id in
match subtasks with
[] ->
let subtasks = Trans.apply split_trans (get_task task) in
send (UpdateStatus(`New, id));
let sub_ids = List.fold_left (fun acc t -> (send_task id t)::acc) [] subtasks in
Hashtbl.replace task_table id (task,parent_id, `New, sub_ids)
| _ -> ()
with
Not_found -> log ("No task with id " ^ id)
let set_status st id =
try
let task, parent_id, _, subs = Hashtbl.find task_table id in
Hashtbl.replace task_table id (task, parent_id, st, subs);
let _,_,_, depends = Hashtbl.find task_table parent_id in
send (UpdateStatus (st, id));
if
List.for_all (fun cid -> try
match Hashtbl.find task_table cid with
(_, _, `Valid, _) -> true
| _ -> false
with Not_found -> false) depends
then
send (UpdateStatus (`Valid, parent_id))
with
Not_found -> log ("No task with id " ^ id)
let why3_parse_theories theories = let why3_parse_theories theories =
let theories = let theories =
...@@ -80,30 +137,11 @@ let why3_parse_theories theories = ...@@ -80,30 +137,11 @@ let why3_parse_theories theories =
List.iter List.iter
(fun (_, (th_name, th)) -> (fun (_, (th_name, th)) ->
let th_id = gen_id () in let th_id = gen_id () in
let () = send (Theory(th_id, th_name)) in
send (UpdateStatus(`New, th_id));
let tasks = Task.split_theory th None None in let tasks = Task.split_theory th None None in
List.iter let task_ids = List.fold_left (fun acc t -> (send_task th_id t):: acc) [] tasks in
(fun task -> Hashtbl.add task_table th_id (`Theory(th), "theory-list", `New, task_ids)
let (id,expl,_) = Termcode.goal_expl_task ~root:true task in
let task_name = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let task_id = gen_id () in
List.iter
(fun vc ->
let vc_id = gen_id () in
let id, expl, _ = Termcode.goal_expl_task ~root:false vc in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let msg = Tasks ((th_id, th_name),
(task_id, task_name),
(vc_id, expl, task_to_string vc))
in
send msg)
(Trans.apply split_trans task)
) (List.rev tasks)
) theories ) theories
let execute_symbol m fmt ps = let execute_symbol m fmt ps =
...@@ -209,7 +247,7 @@ let why3_run f lang code = ...@@ -209,7 +247,7 @@ let why3_run f lang code =
let () = let () =
Worker.set_onmessage Worker.set_onmessage
(fun ev -> (fun ev ->
...@@ -217,10 +255,14 @@ let () = ...@@ -217,10 +255,14 @@ let () =
let ev = unmarshal ev in let ev = unmarshal ev in
log_time ("After unmarshal "); log_time ("After unmarshal ");
match ev with match ev with
| Transform (`Split, id) ->
why3_split id
| ParseBuffer code -> | ParseBuffer code ->
why3_run why3_parse_theories Env.base_language code Hashtbl.clear task_table;
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code -> | ExecuteBuffer code ->
why3_run why3_execute Mlw_module.mlw_language code why3_run why3_execute Mlw_module.mlw_language code
| SetStatus (st, id) -> set_status st id
) )
(* (*
Local Variables: Local Variables:
......
type id = string type id = string
type loc = int * int * int * int
type status = [`New | `Valid | `Unknown ]
type why3_command = ParseBuffer of string type why3_command = ParseBuffer of string
| ExecuteBuffer of string | ExecuteBuffer of string
| Transform of [ `Split ] * id
| SetStatus of status * id
type why3_output = Error of string (* msg *) type why3_output = Error of string (* msg *)
| ErrorLoc of ((int*int*int*int) * string) (* loc * msg *) | ErrorLoc of (loc * string) (* loc * msg *)
| Tasks of ((id * string) (* Theory (id, name) *) | Theory of id * string (* Theory (id, name) *)
* (id * string) (* Task (id, name *) | Task of (id * id * string * string * loc list) (* id, parent id, expl, code, location list *)
* (id * string * string)) (* VC (id, expl, code ) *) | Result of string list