From d3373d05c3cb7e9a857e738b460948db025a85ce Mon Sep 17 00:00:00 2001 From: Claude Marche <Claude.Marche@inria.fr> Date: Sat, 29 Aug 2015 08:04:21 +0200 Subject: [PATCH] TryWhy3: first skeleton compile it with make src/trywhy3/trywhy3.js run it by loading src/trywhy3/index.html in your favorite browser first issue to solve : loading of standard library --- Makefile.in | 22 ++++++++++++++++ src/trywhy3/index.html | 24 ++++++++++++++++++ src/trywhy3/trywhy3.ml | 57 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 103 insertions(+) create mode 100644 src/trywhy3/index.html create mode 100644 src/trywhy3/trywhy3.ml diff --git a/Makefile.in b/Makefile.in index e0848d9530..6e4e498bb3 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1422,6 +1422,28 @@ install_no_local:: install_local:: bin/why3doc +######### +# trywhy3 +######### + +JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \ + -syntax camlp4o + +src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte + js_of_ocaml +weak.js +nat.js $^ + +src/trywhy3/trywhy3.byte: lib/why3/why3.cma src/trywhy3/trywhy3.cmo + $(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^ + +src/trywhy3/%.cmo: src/trywhy3/%.ml + $(JSOCAMLC) $(BFLAGS) -c $< + +src/trywhy3/%.cmi: src/trywhy3/%.mli + $(JSOCAMLC) $(BFLAGS) -c $< + +clean:: + rm -f src/trywhy3/trywhy3.byte + ######## # bench ######## diff --git a/src/trywhy3/index.html b/src/trywhy3/index.html new file mode 100644 index 0000000000..c88a52577e --- /dev/null +++ b/src/trywhy3/index.html @@ -0,0 +1,24 @@ +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" + "http://www.w3.org/TR/html4/strict.dtd"> +<html> + <head> + <title>Try Why3</title> + <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> + </head> + <body style="background-color:#ddd"> + <h1 style="background-color:#356aa0;color:#fff">Try Why3</h1> + <p>Type some program in the window below, then click on + button 'Go' to run Why3 on it.</p> + <div id="trywhy3"> + <script type="text/javascript" src="trywhy3.js"></script> + </div> + <hr> + <p>Related links + <ul> + <li>The <a href="http://why3.lri.fr/">Why3 home page</a> + <li>The <a href="http://ocsigen.org/js_of_ocaml/">Js_of_ocaml</a> + compiler used to produce this page + </ul> + </p> + </body> +</html> diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml new file mode 100644 index 0000000000..8eeb946597 --- /dev/null +++ b/src/trywhy3/trywhy3.ml @@ -0,0 +1,57 @@ + +module D = Dom_html + +let d = D.document + +let node x = (x : #Dom.node Js.t :> Dom.node Js.t) + +let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e + +let html_of_string (s:string) = + d##createElement (Js.string "p") <| + [node (d##createTextNode (Js.string s))] + +let replace_child p n = + Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c); + Dom.appendChild p n + +let temp_file_name = "/input.mlw" + +open Why3 + +let run textbox preview _ = + let text = Js.to_string (textbox##value) in + Sys_js.register_file ~name:temp_file_name ~content:text; + let env = Env.create_env [] in + let answer = + try + let _x = Env.read_file Env.base_language env temp_file_name in + "parsing OK" + with e -> + Pp.sprintf + "exception raised in parsing: %a" Exn_printer.exn_printer e + in + replace_child preview (html_of_string answer); + Js._false + +let onload (_event : #Dom_html.event Js.t) : bool Js.t = + let body = + Js.Opt.get (d##getElementById(Js.string "trywhy3")) + (fun () -> assert false) in + let textbox = D.createTextarea d in + textbox##rows <- 20; textbox##cols <- 100; + let go = D.createButton ~name:(Js.string "go") d in + go##textContent <- Js.some (Js.string "Go"); + let preview = D.createDiv d in + preview##style##border <- Js.string "1px black"; + preview##style##padding <- Js.string "5px"; + Dom.appendChild body textbox; + Dom.appendChild body (D.createBr d); + Dom.appendChild body go; + Dom.appendChild body (D.createBr d); + Dom.appendChild body preview; + replace_child preview (html_of_string "(Answer)"); + go##onclick <- D.handler (run textbox preview); + Js._false + +let _ = D.window##onload <- D.handler onload -- GitLab