Commit 2e512dba authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: attempt to implement the execute feature

parent d277a2a6
......@@ -1430,7 +1430,7 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=why3.conf:/ \
js_of_ocaml --extern-fs -I src/trywhy3 -I . --file=why3.conf:/ \
--file=alt_ergo.drv:/ \
--file=drinkers.why:/ \
--file=simplearith.why:/ \
......
(*
module for generating HTML elements
*)
module Html = struct
let d = Dom_html.document
......@@ -30,7 +36,6 @@ let get_opt o =
let log s =
Firebug.console ## log (Js.string s)
let temp_file_name = "/input.mlw"
let why3_conf_file = "/why3.conf"
......@@ -100,50 +105,90 @@ let run_alt_ergo_on_task t =
let split_trans = Trans.lookup_transform_l "split_goal_wp" env
let prove global text =
let why3_prove theories =
let theories =
Stdlib.Mstr.fold
(fun thname th acc ->
let tasks = Task.split_theory th None None in
let tasks = List.map
(fun t ->
let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let tl = Trans.apply split_trans t in
let tasks =
List.map
(fun task ->
let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let result = run_alt_ergo_on_task task in
let result =
if String.length result > 80 then
"..." ^ String.sub result (String.length result - 80) 80
else result
in
[Html.of_string (expl ^" : " ^ result)])
tl
in
[Html.of_string expl; Html.ul tasks])
tasks
in
[ Html.of_string ("Theory " ^ thname); Html.ul tasks]
:: acc)
theories []
in
Html.ul theories
let why3_execute (modules,_theories) =
let mods =
Stdlib.Mstr.fold
(fun _k m acc ->
let th = m.Mlw_module.mod_theory in
let name = th.Theory.th_name.Ident.id_string in
[Html.of_string ("Module " ^ name)] :: acc)
modules []
in
Html.ul mods
(* from ../tools/why3execute.ml
let do_exec (mid,name) =
let m = try Mstr.find mid mm with Not_found ->
eprintf "Module '%s' not found.@." mid;
exit 1 in
let ps =
try Mlw_module.ns_find_ps m.Mlw_module.mod_export [name]
with Not_found ->
eprintf "Function '%s' not found in module '%s'.@." name mid;
exit 1 in
match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
| None ->
eprintf "Function '%s.%s' has no definition.@." mid name;
exit 1
| Some d ->
try
printf "@[<hov 2>Execution of %s.%s ():@\n" mid name;
Mlw_interp.eval_global_symbol env m d;
with e when Debug.test_noflag Debug.stack_trace ->
printf "@\n@]@.";
raise e in
Queue.iter do_exec opt_exec
*)
let run_why3 f lang global text =
let ch = open_out temp_file_name in
output_string ch text;
close_out ch;
try
(* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
let theories = Env.read_file Env.base_language env temp_file_name in
let theories =
Stdlib.Mstr.fold
(fun thname th acc ->
let tasks = Task.split_theory th None None in
let tasks = List.map
(fun t ->
let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let tl = Trans.apply split_trans t in
let tasks =
List.map
(fun task ->
let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let result = run_alt_ergo_on_task task in
let result =
if String.length result > 80 then
"..." ^ String.sub result (String.length result - 80) 80
else result
in
[Html.of_string (expl ^" : " ^ result)])
tl
in
[Html.of_string expl; Html.ul tasks])
tasks
in
[ Html.of_string ("Theory " ^ thname); Html.ul tasks]
:: acc)
theories []
in
Html.ul theories
let theories = Env.read_file lang env temp_file_name in
f theories
with
(*
| Loc.Located(loc,Parser.Error) ->
......@@ -167,14 +212,15 @@ let prove global text =
(Pp.sprintf
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e))]
let () =
let add_why3_cmd buttonname f lang =
let handler = Dom.handler
(fun _ev ->
log "why3 prove is running";
let global = Js.Unsafe.global in
let editor = Js.Unsafe.get global (Js.string "editor") in
let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
let answer = prove global code in
let answer = run_why3 f lang global code in
(* remove the previous answer if any *)
let console =
get_opt (Dom_html.document ## getElementById (Js.string "console"))
......@@ -186,10 +232,14 @@ let () =
Js._false)
in
let button =
get_opt (Dom_html.document ## getElementById (Js.string "prove"))
get_opt (Dom_html.document ## getElementById (Js.string buttonname))
in
button ## onclick <- handler
let () =
add_why3_cmd "prove" why3_prove Env.base_language;
add_why3_cmd "run" why3_execute Mlw_module.mlw_language
let add_file_example buttonname file =
let handler = Dom.handler
(fun _ev ->
......
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