Commit c1eae8fa authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: theories embedded in the JS file

parent 527ed884
......@@ -268,6 +268,10 @@ pvsbin/
/modules/mach/array/
/modules/mach/int/
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
/src/trywhy3/theories.ml
# jessie3
/src/jessie/config.log
......
......@@ -1427,14 +1427,17 @@ install_local:: bin/why3doc
#########
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
-syntax camlp4o -I src/trywhy3
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
src/trywhy3/trywhy3.byte: lib/why3/why3.cma src/trywhy3/theories.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/theories.ml: src/trywhy3/gentheories.ml
ocaml src/trywhy3/gen_theories.ml
src/trywhy3/%.cmo: src/trywhy3/%.ml
$(JSOCAMLC) $(BFLAGS) -c $<
......
#load "unix.cma"
#directory "../util"
#load "sysutil.cmo"
open Format
let gen_dir fmt d suffix =
let dir = "../.." ^ d in
let t = Sys.readdir dir in
for i = 0 to Array.length t - 1 do
let file = t.(i) in
let f = Filename.concat dir file in
if Filename.check_suffix f suffix then
let c = String.escaped (Sysutil.file_contents f) in
fprintf fmt "\"%s/%s\",@\n\"%s@\n\";@\n" d file c
done
let () =
let ch = open_out "src/trywhy3/theories.ml" in
let fmt = formatter_of_out_channel ch in
fprintf fmt "(* generated by gen_theories.ml *)@\n@\n";
fprintf fmt "let theories = [@\n";
gen_dir fmt "/theories" ".why";
gen_dir fmt "/modules" ".mlw";
gen_dir fmt "/modules/mach" ".mlw";
fprintf fmt "]@\n";
close_out ch
......@@ -2,8 +2,8 @@
let examples =
["Drinkers paradox",
"theory T
[ "Drinkers paradox","
theory T
(** Type of all persons *)
type person
......@@ -16,9 +16,26 @@ let examples =
goal drinkers_paradox: exists x:person. drinks x -> forall y:person. drinks y
end
"
";
"Simple Arithmetic","
theory T
use import int.Int
goal g: exists x:int. x*(x+1) = 42
end
";
]
(** registering the std lib *)
let () =
List.iter
(fun (name,content) ->
Sys_js.register_file ~name ~content;
) Theories.theories
(** Rendering in the browser *)
module D = Dom_html
......@@ -44,16 +61,48 @@ let () =
open Why3
let run textbox preview _ =
(* TODO: loading from standard library.
piste: utiliser Sys_js.register_autoload et
XmlHttpRequest.get
*)
let env = Env.create_env ["/theories" (*; "/modules"*)]
(*
let bad_suffix path name =
match path with
| "/theories" -> not (Filename.check_suffix name ".why")
| "/modules" -> not (Filename.check_suffix name ".mlw")
| _ -> true
let load_file_from_the_web (path,name) =
if bad_suffix path name then None else
let t = XmlHttpRequest.get
("http://why3.lri.fr/try" ^ path ^ "/" ^ name)
in
let c = ref "" in
Lwt.on_success t
(fun frame ->
let content = frame. XmlHttpRequest.content in
(* useless ?
Sys_js.register_file ~name:(path ^ "/" ^ name) ~content; *)
c := content);
Some !c
let () = Sys_js.register_autoload ~path:"/theories" load_file_from_the_web
*)
let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
let text = Js.to_string (textbox##value) in
let ch = open_out temp_file_name in
output_string ch text;
close_out ch;
let env = Env.create_env [] in
let answer =
try
let _x = Env.read_file Env.base_language env temp_file_name in
"parsing and typing OK"
let x = Env.read_file Env.base_language env temp_file_name in
Pp.sprintf "parsing and typing OK, %d theories"
(Stdlib.Mstr.cardinal x)
with
| Loc.Located(loc,Parser.Error) ->
let (_,l,b,e) = Loc.get loc in
......@@ -87,7 +136,7 @@ let onload (_event : #Dom_html.event Js.t) : bool Js.t =
Dom.appendChild body b;
b##onclick <-
D.handler
(fun _ ->
(fun (_ : D.mouseEvent Js.t) ->
textbox##textContent <- Js.some (Js.string text);
Js._false))
examples;
......
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