Commit cd5c5c02 authored by MARCHE Claude's avatar MARCHE Claude

Try why3: add examples from external fs

parent 9aa91c18
......@@ -1432,6 +1432,9 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=why3.conf:/ \
--file=alt_ergo.drv:/ \
--file=drinkers.why:/ \
--file=simplearith.why:/ \
--file=isqrt.mlw:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
......
theory T
(** Type of all persons *)
type person
(** Predicate saying that some person drinks *)
predicate drinks person
(** Paradox: there exists a person x such that if x drinks,
then everybody drinks *)
goal drinkers_paradox:
exists x:person. drinks x ->
forall y:person. drinks y
end
......@@ -36,14 +36,6 @@ function moveToError ()
editor.on("focus", moveToError);
function clearConsole ()
{
document.getElementById("console").innerHTML = "";
editor.focus();
}
function openFile ()
{
document.getElementById("file-selector").click();
......@@ -119,32 +111,8 @@ function realOpenFile (ev)
editor.focus();
}
function drinkers(ev)
{
loadedBuffer = "theory T\n\
\n\
(** Type of all persons *)\n\
type person\n\
\n\
(** Predicate saying that some person drinks *)\n\
predicate drinks person\n\
\n\
(** Paradox: there exists a person x such that\n\
if x drinks, then everybody drinks *)\n\
goal drinkers_paradox: \n\
exists x:person. drinks x ->\n\
forall y:person. drinks y\n\
\n\
end\n\
";
loadedFilename = "drinkers.why";
replaceWithLoaded();
editor.focus();
}
fileSelector.addEventListener("change", realOpenFile, false);
var saveFile = (function ()
{
var a = document.createElement ("a");
......
......@@ -57,9 +57,9 @@
</li>
<li><a href="#">Examples</a>
<ul>
<li><a href="#" onclick="drinkers();">Drinker's paradox</a></li>
<li><a href="#" onclick="simplearith();">Simple Arithmetic</a></li>
<li><a href="#" onclick="isqrt();">Integral square root</a></li>
<li><a href="#"><div id="drinkers">Drinker's paradox</div></a></li>
<li><a href="#"><div id="simplearith">Simple Arithmetic</div></a></li>
<li><a href="#"><div id="isqrt">Integral square root</div></a></li>
</ul>
</li>
<li><a href="#">Why3</a>
......@@ -70,20 +70,19 @@
</li>
<li><a href="#">Preferences</a>
<ul>
<li><a href="#"
onclick="document.getElementById('radio-std').click();"
>
<input id="radio-std" type="radio" name="view" value="std"
checked="checked" onchange="standardView();"
/>Split Horizontally</a></li>
<li><a href="#"
onclick="document.getElementById('radio-wide').click();"
>
<input id="radio-wide" type="radio" name="view"
value="wide" onchange="widescreenView();"
<input id="radio-wide" type="radio" name="view"
value="wide" checked="checked" onchange="widescreenView();"
/>Split Vertically</a>
</li>
<li></li>
<li><a href="#"
onclick="document.getElementById('radio-std').click();"
>
<input id="radio-std" type="radio" name="view" value="std"
onchange="standardView();"
/>Split Horizontally</a></li>
</ul>
</li>
<li style="float:right;"><a href="#">Help</a></li>
......
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
theory T
use import int.Int
goal g: exists x:int. x*(x+1) = 42
end
module D = Dom_html
module Html = struct
let d = D.document
let d = Dom_html.document
let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
......@@ -193,6 +190,29 @@ let () =
in
button ## onclick <- handler
let add_file_example buttonname file =
let handler = Dom.handler
(fun _ev ->
let text = Sysutil.file_contents file in
let global = Js.Unsafe.global in
let editor = Js.Unsafe.get global (Js.string "editor") in
Js.Unsafe.set global (Js.string "loadedBuffer") (Js.string text);
let loaded = Filename.basename file in
Js.Unsafe.set global (Js.string "loadedFilename") (Js.string loaded);
ignore (Js.Unsafe.meth_call global "replaceWithLoaded" [| |]);
ignore (Js.Unsafe.meth_call editor "focus" [| |]);
Js._false)
in
let button =
get_opt (Dom_html.document ## getElementById (Js.string buttonname))
in
button ## onclick <- handler
let () =
add_file_example "drinkers" "/drinkers.why";
add_file_example "simplearith" "/simplearith.why";
add_file_example "isqrt" "/isqrt.mlw"
(*
Local Variables:
......
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