Commit ba2f367a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Try restoring trywhy3.

parent 75cc40ed
PKG js_of_ocaml js_of_ocaml.syntax ocplib-simplex
REC
......@@ -25,7 +25,7 @@ let get_global ident =
let int_of_js_string s = int_of_string (Js.to_string s)
let blob_url_of_string s =
let s = JSU.inject (Js.string (Sys_js.file_content s)) in
let s = JSU.inject (Js.string (Sys_js.read_file ~name:s)) in
let _Blob = get_global "Blob" in
let blob =
jsnew _Blob (Js.array [| s |])
......@@ -682,21 +682,23 @@ module ToolBar =
let open_ = getElement AsHtml.input "why3-open"
let () =
open_ ## onchange <-
Dom.handler
(fun _e ->
open_ ## onchange <- Dom.handler (fun _e ->
ExampleList.unselect ();
match Js.Optdef.to_option (open_ ## files) with
None -> Js._false
| Some (f) -> match Js.Opt.to_option (f ## item (0)) with
None -> Js._false
| None -> Js._false
| Some (f) ->
match Js.Opt.to_option (f ## item (0)) with
| None -> Js._false
| Some f ->
ignore (
Lwt.bind (File.readAsText f)
(fun str ->
let reader = jsnew File.fileReader () in
reader##onloadend <- Dom.handler (fun _ ->
match Js.Opt.to_option (File.CoerceTo.string (reader##result)) with
| None -> Js._true
| Some content ->
Editor.name := File.filename f;
Editor.set_value str;
Lwt.return_unit));
Editor.set_value content;
Js._true);
reader##readAsText ((f :> File.blob Js.t));
Js._true
)
let open_ () = if Editor.confirm_unsaved () then open_ ## click ()
......@@ -1063,7 +1065,7 @@ let () =
));
ToolBar.add_action Dialogs.button_close Dialogs.close;
KeyBinding.add_global Keycode.esc Dialogs.close;
(*KeyBinding.add_global Keycode.esc Dialogs.close;*)
Dialogs.(set_onchange radio_wide (fun _ -> Panel.set_wide true));
Dialogs.(set_onchange radio_column (fun _ -> Panel.set_wide false))
......
......@@ -318,57 +318,17 @@ let why3_parse_theories theories =
List.iter (fun i -> why3_prove i) subs
) theories
let execute_symbol m fmt ps =
match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
| None ->
fprintf fmt "function '%s' has no definition"
ps.Mlw_expr.ps_name.Ident.id_string
| Some d ->
let lam = d.Mlw_expr.fun_lambda in
match lam.Mlw_expr.l_args with
| [pvs] when
Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
begin
let spec = lam.Mlw_expr.l_spec in
let eff = spec.Mlw_ty.c_effect in
let writes = eff.Mlw_ty.eff_writes in
let body = lam.Mlw_expr.l_expr in
try
let res, _final_env =
Mlw_interp.eval_global_expr env m.Mlw_module.mod_known
m.Mlw_module.mod_theory.Theory.th_known writes body
in
match res with
| Mlw_interp.Normal v -> Mlw_interp.print_value fmt v
| Mlw_interp.Excep(x,v) ->
fprintf fmt "exception %s(%a)"
x.Mlw_ty.xs_name.Ident.id_string Mlw_interp.print_value v
| Mlw_interp.Irred e ->
fprintf fmt "cannot execute expression@ @[%a@]"
Mlw_pretty.print_expr e
| Mlw_interp.Fun _ ->
fprintf fmt "result is a function"
with e ->
fprintf fmt
"failure during execution of function: %a (%s)"
Exn_printer.exn_printer e
(Printexc.to_string e)
end
| _ ->
fprintf fmt "Only functions with one unit argument can be executed"
let why3_execute (modules,_theories) =
let why3_execute modules =
let result =
let mods =
Wstdlib.Mstr.fold
(fun _k m acc ->
let th = m.Mlw_module.mod_theory in
let th = m.Pmodule.mod_theory in
let modname = th.Theory.th_name.Ident.id_string in
try
let ps =
Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
let rs = Pmodule.ns_find_rs m.Pmodule.mod_export ["main"]
in
let result = Pp.sprintf "%a" (execute_symbol m) ps in
let result = Pp.sprintf "%a" (Pinterp.eval_global_symbol env m) rs in
let loc =
Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
in
......@@ -390,7 +350,7 @@ let why3_execute (modules,_theories) =
W.send result
let () = Sys_js.register_file ~name:temp_file_name ~content:""
let () = Sys_js.create_file ~name:temp_file_name ~content:""
let why3_run f lang code =
try
......@@ -430,7 +390,7 @@ let () =
| ExecuteBuffer code ->
Task.clear_warnings ();
Task.clear_table ();
why3_run why3_execute Mlw_module.mlw_language code
why3_run why3_execute Pmodule.mlw_language code
| SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
in
W.send Idle
......
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