diff --git a/Makefile.in b/Makefile.in index 57c313a08f9e0a590398a51dd64a97aeebec8d95..75615d99518cd0b1397387f5212ebbf81d3753f5 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1430,8 +1430,8 @@ 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 src/trywhy3 -I . --file=why3.conf:/ \ - --file=alt_ergo.drv:/ \ + js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \ + --file=try_alt_ergo.drv:/ \ --file=drinkers.why:/ \ --file=simplearith.why:/ \ --file=isqrt.mlw:/ \ diff --git a/src/trywhy3/alt_ergo.drv b/src/trywhy3/try_alt_ergo.drv similarity index 94% rename from src/trywhy3/alt_ergo.drv rename to src/trywhy3/try_alt_ergo.drv index 501cc54758357c9274cc239a06b88a66eeb76b2f..6e49dde407a0e6d99b61d6efe9bb636c417d7eae 100644 --- a/src/trywhy3/alt_ergo.drv +++ b/src/trywhy3/try_alt_ergo.drv @@ -1,10 +1,13 @@ -(* Driver for Alt-Ergo version >= 0.95 *) +(* Driver for Alt-Ergo, specific variant for Try Why3 *) +(* FIXME: it would be better to share the common parts with the regular + Alt-Ergo driver *) -prelude "(* this is the prelude for Alt-Ergo, any versions *)" +prelude "(* this is the prelude for Alt-Ergo, version for Try Why3 *)" printer "alt-ergo" filename "%f-%t-%g.why" +(* Try Why3 doesn't need these valid "Valid" invalid "Invalid" unknown "I don't know" "" @@ -13,17 +16,11 @@ steplimitexceeded "Steps limit reached" outofmemory "Fatal error: out of memory" outofmemory "Fatal error: exception Stack_overflow" fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1" -(* -time "Valid (%s)" -time "Valid (%s)" -steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2 -steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2 -time "why3cpulimit time : %s s" *) -(* À discuter *) -transformation "inline_trivial" +(* FIXME: remaining of this file should be shared with regular Alt-Ergo driver *) +transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_recursion" transformation "eliminate_inductive" @@ -31,7 +28,6 @@ transformation "eliminate_algebraic" transformation "eliminate_epsilon" transformation "eliminate_if" transformation "eliminate_let" - transformation "split_premise_right" transformation "simplify_formula" (*transformation "simplify_trivial_quantification_in_goal"*) diff --git a/src/trywhy3/why3.conf b/src/trywhy3/trywhy3.conf similarity index 93% rename from src/trywhy3/why3.conf rename to src/trywhy3/trywhy3.conf index 66966f22ac8d6ea1ca0db706874f27689e11884f..80b07cf1193125c80e0d52b8e23e605a40ae2cae 100644 --- a/src/trywhy3/why3.conf +++ b/src/trywhy3/trywhy3.conf @@ -10,7 +10,7 @@ timelimit = 5 [prover] command = "%l/why3-cpulimit %T %m -s alt-ergo-0.99.1 -timelimit %t %f" command_steps = "%l/why3-cpulimit %U %m -s alt-ergo-0.99.1 -steps-bound %S %f" -driver = "/alt_ergo.drv" +driver = "/try_alt_ergo.drv" editor = "altgr-ergo" in_place = false interactive = false diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml index f1ed036de686b812d55d9d6752896af5091d09bb..839d612e6be24433dd57338a0babbdaa9fa8d279 100644 --- a/src/trywhy3/trywhy3.ml +++ b/src/trywhy3/trywhy3.ml @@ -1,4 +1,17 @@ +(* + + small helpers + + *) + +let get_opt o = + Js.Opt.get o (fun () -> assert false) + +let log s = + Firebug.console ## log (Js.string s) + + (* module for generating HTML elements @@ -30,17 +43,13 @@ let ul nl = end -let get_opt o = - Js.Opt.get o (fun () -> assert false) +(* -let log s = - Firebug.console ## log (Js.string s) + Interface to Why3 and Alt-Ergo -let temp_file_name = "/input.mlw" -let why3_conf_file = "/why3.conf" +*) -let () = - Sys_js.register_file ~name:temp_file_name ~content:"" +let why3_conf_file = "/trywhy3.conf" open Why3 open Format @@ -63,7 +72,6 @@ let alt_ergo : Whyconf.config_prover = (* builds the environment from the [loadpath] *) let env : Env.env = Env.create_env (Whyconf.loadpath main) - let alt_ergo_driver : Driver.driver = try Printexc.record_backtrace true; @@ -74,7 +82,6 @@ let alt_ergo_driver : Driver.driver = Exn_printer.exn_printer e s; exit 1 - let run_alt_ergo_on_task t = (* printing the task in a string *) Driver.print_task alt_ergo_driver str_formatter t; @@ -181,6 +188,18 @@ let why3_execute (modules,_theories) = *) + +(* + + Connecting why3 calls to the interface + + *) + +let temp_file_name = "/input.mlw" + +let () = + Sys_js.register_file ~name:temp_file_name ~content:"" + let run_why3 f lang global text = let ch = open_out temp_file_name in output_string ch text; @@ -190,13 +209,6 @@ let run_why3 f lang global text = let theories = Env.read_file lang env temp_file_name in f theories with -(* - | Loc.Located(loc,Parser.Error) -> - let (_,l,b,e) = Loc.get loc in - Html.par - [Html.of_string - (Pp.sprintf "syntax error line %d, columns %d-%d" l b e)] -*) | Loc.Located(loc,e') -> let (_,l,b,e) = Loc.get loc in ignore (Js.Unsafe.meth_call global "highlightError" @@ -240,6 +252,13 @@ let () = add_why3_cmd "prove" why3_prove Env.base_language; add_why3_cmd "run" why3_execute Mlw_module.mlw_language + +(* + + Predefined examples + +*) + let add_file_example buttonname file = let handler = Dom.handler (fun _ev ->