Commit 53b2d976 authored by Kim Nguyễn's avatar Kim Nguyễn

[trywhy3] : Implement splitting of tasks, cleaning of splited tasks and prove individual tasks.

parent 9a4b07f6
......@@ -60,7 +60,8 @@ function realReplaceBuffer()
currentFilename = loadedFilename;
//document.getElementById("filename_panel").innerHTML = loadedFilename;
loadedFilename = "";
loadedBuffer = "";
loadedBuffer = "";
document.getElementById("console").innerHTML = "";
}
function confirmReplace ()
......
......@@ -19,7 +19,9 @@
.task-abort {
color:black;
}
.task-selected {
background:rgba(250,220,90,0.7);
}
/* ACE Editor */
.error {
......@@ -228,32 +230,48 @@ body {
#console ul#theory-list {
position:relative;
list-style-type: none;
list-style-position: inside;
padding-left: 0.5em;
}
#console ul#theory-list li {
font-weight:bold;
position:relative;
}
#console ul#theory-list li * {
#console ul#theory-list li {
font-weight:normal;
padding-top:0.5em;
padding-bottom:0.5em;
}
#console ul#theory-list ul {
list-style-type: none;
list-style-position: inside;
padding-left: 2em;
}
#console ul#theory-list ul > li {
padding-left:1em;
}
#console ul#theory-list ul ul {
list-style-type: none;
list-style-position: inside;
padding-left: 0.5em;
padding-left: 2em;
}
#console ul#theory-list ul li:before {
display:inline-block;
position:absolute;
content: "";
height:50%;
top:0;
left:-1.5em;
width:1.25em;
border-bottom: 2pt solid #ddd;
border-left: 2pt solid #ddd;
}
/* Confirmation dialog */
.btn {
width:100%;
......
......@@ -69,7 +69,10 @@ yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html -->
<li><span>Why3</span>
<ul>
<li id="run">Execute Buffer</li>
<li id="prove">Prove with Alt-Ergo</li>
<li id="prove_all">Prove All with Alt-Ergo</li>
<li id="prove">Prove Goal</li>
<li id="split_prove">Split Goal and Prove</li>
<li id="clean">Clean Goal</li>
<li id="stop">Stop Alt-ergo</li>
</ul>
</li>
......
......@@ -64,6 +64,18 @@ module Console =
let appendChild o c =
ignore (o ## appendChild ( (c :> Dom.node Js.t)))
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 -> ()
let attach_to_parent id parent_id expl _loc =
let doc = Dom_html.document in
let ul =
......@@ -84,18 +96,15 @@ module Console =
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
li ## innerHTML <- mk_li_content id expl
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
let print_why3_output o =
let doc = Dom_html.document in
(* see why3_worker.ml *)
......@@ -116,9 +125,37 @@ module Console =
li ## innerHTML <- (Js.string s);
appendChild ul li;) sl
| Theory (th_id, th_name) -> attach_to_parent th_id "theory-list" th_name []
| 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
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
| UpdateStatus(st, id) ->
try
let span_icon = Dom_html.getElementById (id ^ "_icon") in
......@@ -224,7 +261,9 @@ let init_why3_worker () =
Console.print_why3_output msg;
let () =
match msg with
Task (id,_,_,code,_) -> push_task (Goal (id,code))
Task (id,_,_,code,_) ->
log ("Got task " ^ id);
push_task (Goal (id,code))
| _ -> ()
in Js._false));
worker
......@@ -250,15 +289,39 @@ let why3_execute () =
let code = Console.get_buffer () in
(get_why3_worker()) ## postMessage (marshal (ExecuteBuffer code))
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
let () =
add_button "prove" why3_parse ;
add_button "prove_all" why3_parse ;
add_button "run" why3_execute ;
add_button "stop" (fun () ->
(get_why3_worker()) ## terminate ();
why3_worker := Some (init_why3_worker ());
reset_workers ();
Console.set_abort_icon());
add_button "prove" (why3_transform `Prove (fun _ -> ()));
add_button "split_prove" (why3_transform `Split (fun _ -> ()));
add_button "clean" (why3_transform `Clean Console.clean_task);
let input_threads = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-threads"))
......@@ -302,7 +365,9 @@ let add_file_example (buttonname, file) =
let loaded = Filename.basename file in
Js.Unsafe.set global (Js.string "loadedFilename") (Js.string loaded);
ignore (Js.Unsafe.meth_call global "replaceWithLoaded" [| |]);
Console.clear ();
ignore (Js.Unsafe.meth_call editor "focus" [| |]);
Js._false)
in
let button =
......
......@@ -51,8 +51,15 @@ let alt_ergo_driver : Driver.driver =
let () = log_time ("Initialising why3 worker: end ")
(* *** *)
type task_info = { task : [ `Theory of Theory.theory | `Task of Task.task ];
parent_id : id;
mutable status : status;
mutable subtasks : id list;
loc : loc list;
expl : string; }
let task_table = Hashtbl.create 17
let task_table : (id, task_info) Hashtbl.t = Hashtbl.create 17
let split_trans = Trans.lookup_transform_l "split_goal_wp" env
......@@ -68,7 +75,6 @@ let gen_id =
let send msg =
ignore (Worker.post_message (marshal msg))
let get_loc l =
match l with
Some (l) ->
......@@ -77,52 +83,96 @@ let get_loc l =
| _ -> None
let send_task parent_id task =
let register_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));
let task_info = { task = `Task(task);
parent_id = parent_id;
status = `New;
subtasks = [];
loc = [ (* todo *) ];
expl = expl }
in
Hashtbl.add task_table id task_info;
id
let get_task = function `Task t -> t
| `Theory _ -> log ("called get_task on a theory !"); assert false
let rec set_status id st =
try
let info = Hashtbl.find task_table id in
if info.status <> st then begin
info.status <- st;
send (UpdateStatus (st, id));
let par_info = Hashtbl.find task_table info.parent_id in
let has_new, has_unknown =
List.fold_left
(fun (an, au) id ->
let info = Hashtbl.find task_table id in
(an || info.status = `New), (au || info.status = `Unknown))
(false, false) par_info.subtasks
in
let par_status = if has_new then `New else if
has_unknown then `Unknown
else `Valid
in
if par_info.status <> par_status then
set_status info.parent_id par_status
end
with
Not_found -> ()
let rec why3_prove id =
let t = Hashtbl.find task_table id in
match t.subtasks with
[] -> t.status <- `Unknown;
let task = get_task t.task in
let msg = Task (id, t.parent_id, t.expl, task_to_string task, t.loc) in
send msg;
set_status id `New
| l -> List.iter why3_prove l
let why3_split id =
try
let task, parent_id,_,subtasks = Hashtbl.find task_table id in
match subtasks with
let t = Hashtbl.find task_table id in
match t.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)
let subtasks = Trans.apply split_trans (get_task t.task) in
t.subtasks <- List.fold_left (fun acc t ->
let tid = register_task id t in
why3_prove tid;
tid :: acc) [] subtasks
| _ -> ()
with
Not_found -> log ("No task with id " ^ id)
let set_status st id =
let rec clean_task 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))
let info = Hashtbl.find task_table id in
List.iter clean_task info.subtasks;
Hashtbl.remove task_table id
with
Not_found -> log ("No task with id " ^ id)
Not_found -> ()
let why3_clean id =
try
let t = Hashtbl.find task_table id in
List.iter clean_task t.subtasks;
t.subtasks <- [];
set_status id `Unknown;
with
Not_found -> ()
let why3_parse_theories theories =
let theories =
......@@ -140,8 +190,16 @@ let why3_parse_theories theories =
let () = send (Theory(th_id, th_name)) in
send (UpdateStatus(`New, th_id));
let tasks = Task.split_theory th None None in
let task_ids = List.fold_left (fun acc t -> (send_task th_id t):: acc) [] tasks in
Hashtbl.add task_table th_id (`Theory(th), "theory-list", `New, task_ids)
let task_ids = List.fold_left (fun acc t ->
let tid = register_task th_id t in
why3_prove tid;
tid:: acc) [] tasks in
Hashtbl.add task_table th_id { task = `Theory(th);
parent_id = "theory-list";
status = `New;
subtasks = task_ids;
loc = [ (* todo *) ];
expl = th_name }
) theories
let execute_symbol m fmt ps =
......@@ -255,14 +313,15 @@ let () =
let ev = unmarshal ev in
log_time ("After unmarshal ");
match ev with
| Transform (`Split, id) ->
why3_split id
| Transform (`Split, id) -> why3_split id
| Transform (`Prove, id) -> why3_prove id
| Transform (`Clean, id) -> why3_clean id
| ParseBuffer code ->
Hashtbl.clear task_table;
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code ->
why3_run why3_execute Mlw_module.mlw_language code
| SetStatus (st, id) -> set_status st id
| SetStatus (st, id) -> set_status id st
)
(*
Local Variables:
......
......@@ -3,7 +3,7 @@ type loc = int * int * int * int
type status = [`New | `Valid | `Unknown ]
type why3_command = ParseBuffer of string
| ExecuteBuffer of string
| Transform of [ `Split ] * id
| Transform of [ `Prove | `Split | `Clean ] * id
| SetStatus of status * id
type why3_output = Error of string (* msg *)
......@@ -11,7 +11,7 @@ type why3_output = Error of string (* msg *)
| Theory of id * string (* Theory (id, name) *)
| Task of (id * id * string * string * loc list) (* id, parent id, expl, code, location list *)
| Result of string list
| UpdateStatus of status * id
| UpdateStatus of status * id
type prover_command = OptionSteps of int | Goal of id * string
type prover_output = Valid | Unknown of string | Invalid of string
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment