Skip to content

GitLab

Commit 510a24ec authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Try Why3: split goals

parent a3e4a012
Hide whitespace changes
Inline Side-by-side
Showing with 139 additions and 46 deletions
Makefile.in
View file @ 510a24ec
......@@ -1427,7 +1427,7 @@ install_local:: bin/why3doc
#########
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3
-syntax camlp4o -I src/trywhy3
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml +weak.js +nat.js $^
......
src/trywhy3/index.html
View file @ 510a24ec
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html>
<html style="font-family:Verdana,Arial,Sans-Serif">
<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">
<p>Type some program in the text area below, then click on
button 'Go' on the left to run Why3 on it.</p>
<p>Click on the other buttons to select one of the proposed examples.</p>
<table>
<tr>
<td width="50%" style="vertical-align:top">
<div id="input">
</div>
<td width="50%" style="vertical-align:top">
<div id="output">
<script type="text/javascript" src="trywhy3.js"></script>
</div>
</table>
<hr>
<p>Related links
<ul>
......
src/trywhy3/trywhy3.ml
View file @ 510a24ec
......@@ -24,6 +24,34 @@ theory T
goal g: exists x:int. x*(x+1) = 42
end
";
"Integral square root","
module M
use import int.Int
use import ref.Ref
function sqr (x:int) : int = x * x
let isqrt (x:int) : int
requires { x >= 0 }
ensures { result >= 0 }
ensures { result <= x < sqr (result + 1) }
= let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { !count >= 0 }
invariant { x >= sqr !count }
invariant { !sum = sqr (!count+1) }
variant { x - !count }
count := !count + 1;
sum := !sum + 2 * !count + 1
done;
!count
let main () ensures { result = 4 } = isqrt 17
end
";
]
......@@ -36,22 +64,35 @@ let () =
Sys_js.register_file ~name ~content;
) Theories.theories
(** Rendering in the browser *)
module D = Dom_html
module Html = struct
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 of_string s = node (d##createTextNode (Js.string s))
let html_of_string (s:string) =
d##createElement (Js.string "p") <|
[node (d##createTextNode (Js.string s))]
let par nl =
let x = d##createElement (Js.string "p") in
List.iter (Dom.appendChild x) nl;
node x
let rec removeChildren p =
Js.Opt.iter (p##lastChild) (fun c -> Dom.removeChild p c; removeChildren p)
let ul nl =
let x = d##createElement (Js.string "ul") in
List.iter
(fun n ->
let y = d##createElement (Js.string "li") in
List.iter (Dom.appendChild y) n;
Dom.appendChild x (node y))
nl;
node x
end
let temp_file_name = "/input.mlw"
......@@ -92,19 +133,49 @@ let load_file_from_the_web (path,name) =
let () = Sys_js.register_autoload ~path:"/theories" load_file_from_the_web
*)
let split_trans = Why3.Trans.lookup_transform_l "split_goal_wp" env
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 answer = ref [] in
let push_answer s = answer := s :: !answer in
begin
let answer =
try
let x = Env.read_file Env.base_language env temp_file_name in
push_answer
(Pp.sprintf "parsing and typing OK, %d theories"
(Stdlib.Mstr.cardinal x));
let theories = Env.read_file Env.base_language env temp_file_name in
(*
Html.par
[Html.of_string
(Pp.sprintf "parsing and typing OK, %d theories"
(Stdlib.Mstr.cardinal theories))]
*)
let theories =
Stdlib.Mstr.fold
(fun thname th acc ->
let tasks = Task.split_theory th None None in
let tasks = List.fold_left
(fun acc t ->
let tl = Trans.apply split_trans t in
List.rev_append tl acc)
[] tasks
in
let tasks =
List.rev_map
(fun task ->
let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
[Html.of_string ("Goal: " ^ expl)])
tasks
in
[ Html.of_string ("Theory " ^ thname); Html.ul tasks]
:: acc)
theories []
in
Html.par [Html.ul theories]
(*
Stdlib.Mstr.iter
(fun _thname th ->
let tasks = Task.split_theory th None None in
......@@ -118,61 +189,75 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
push_answer
(Pp.sprintf "Goal: %s@\n" expl))
tasks)
x
*)
with
| Loc.Located(loc,Parser.Error) ->
let (_,l,b,e) = Loc.get loc in
push_answer
(Pp.sprintf "syntax error line %d, columns %d-%d" l b e)
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
push_answer
(Pp.sprintf
"error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e')
Html.par
[Html.of_string
(Pp.sprintf
"error line %d, columns %d-%d: %a" l b e
Exn_printer.exn_printer e')]
| e ->
push_answer
(Pp.sprintf
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e))
end;
removeChildren preview;
List.iter
(fun s -> Dom.appendChild preview (html_of_string s)) (List.rev !answer);
Html.par
[Html.of_string
(Pp.sprintf
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e))]
in
(* remove the previous answer if any *)
Js.Opt.iter (preview##lastChild) (Dom.removeChild preview);
(* put the new answer *)
Dom.appendChild preview answer;
Js._false
let onload (_event : #Dom_html.event Js.t) : bool Js.t =
let body =
Js.Opt.get (d##getElementById(Js.string "trywhy3"))
let input =
Js.Opt.get (Html.d##getElementById(Js.string "input"))
(fun () -> assert false) in
let output =
Js.Opt.get (Html.d##getElementById(Js.string "output"))
(fun () -> assert false) in
(* first, the textbox *)
let textbox = D.createTextarea d in
textbox##rows <- 20; textbox##cols <- 100;
Dom.appendChild body textbox;
Dom.appendChild body (D.createBr d);
let textbox = D.createTextarea Html.d in
textbox##rows <- 32; textbox##cols <- 64;
Dom.appendChild input textbox;
(* second, the example buttons *)
List.iter
(fun (name,text) ->
let b = D.createButton ~name:(Js.string name) d in
let b = D.createButton ~name:(Js.string name) Html.d in
b##textContent <- Js.some (Js.string name);
Dom.appendChild body b;
Dom.appendChild output b;
b##onclick <-
D.handler
(fun (_ : D.mouseEvent Js.t) ->
textbox##textContent <- Js.some (Js.string text);
Js._false))
examples;
Dom.appendChild body (D.createBr d);
Dom.appendChild output (D.createBr Html.d);
(* third, the go button *)
let go = D.createButton ~name:(Js.string "go") d in
let go = D.createButton ~name:(Js.string "go") Html.d in
go##textContent <- Js.some (Js.string "Go");
Dom.appendChild body go;
Dom.appendChild body (D.createBr d);
Dom.appendChild output go;
Dom.appendChild output (D.createBr Html.d);
(* then, the answer zone *)
let preview = D.createDiv d in
let preview = D.createDiv Html.d in
go##onclick <- D.handler (run textbox preview);
preview##style##border <- Js.string "1px black";
preview##style##padding <- Js.string "5px";
Dom.appendChild body preview;
Dom.appendChild output preview;
Js._false
let _ = D.window##onload <- D.handler onload
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
End:
*)
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