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

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
d3373d05 · MARCHE Claude · 8c6d96ee · d3373d05 · d3373d05 · d3373d05
Commit d3373d05 authored Aug 29, 2015 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 103 additions and 0 deletions

Makefile.in Makefile.in +22 -0

src/trywhy3/index.html src/trywhy3/index.html +24 -0

src/trywhy3/trywhy3.ml src/trywhy3/trywhy3.ml +57 -0

No files found.
--- 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
 ########

--- a/src/trywhy3/index.html
+++ b/src/trywhy3/index.html
+<!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>
--- a/src/trywhy3/trywhy3.ml
+++ b/src/trywhy3/trywhy3.ml
+
+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