Skip to content

GitLab

why3
why3
Commit eeecc325 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Try Why3: new version with a more elaborate text editor 

needs 'ace' to run, which can be retrieved using

git clone https://github.com/ajaxorg/ace-builds.git
parent 09db98a3
Show whitespace changes
Inline Side-by-side
Showing with 574 additions and 208 deletions
src/trywhy3/editor_helper.js 0 → 100644
View file @ eeecc325
/* Global objects */
var editor = ace.edit("editor");
editor.setTheme("ace/theme/chrome");
editor.getSession().setMode("ace/mode/ocaml");
var Range = ace.require("ace/range").Range;
var selectedRange = null;
var marker = null;
editor.$blockScrolling = Infinity;
function highlightError (x1, y1, x2, y2)
{
selectedRange = new Range (x1,y1,x2,y2);
marker = editor.session.addMarker(selectedRange, "error", "text");
}
function clearHighlight ()
{
if (marker) {
editor.session.removeMarker(marker);
marker = null;
};
}
editor.on("change", clearHighlight);
function moveToError ()
{
if (selectedRange) {
editor.selection.setSelectionRange(selectedRange);
editor.moveCursorToPosition(selectedRange.start);
selectedRange = null;
}
}
editor.on("focus", moveToError);
function clearConsole ()
{
document.getElementById("console").innerHTML = "";
editor.focus();
}
function openFile ()
{
document.getElementById("file-selector").click();
editor.focus();
}
var loadedBuffer = "";
var loadedFilename = "";
var currentFilename = "";
var fileSelector = document.getElementById("file-selector");
function realReplaceBuffer()
{
editor.setValue(loadedBuffer,-1);
currentFilename = loadedFilename;
//document.getElementById("filename_panel").innerHTML = loadedFilename;
loadedFilename = "";
loadedBuffer = "";
}
function confirmReplace ()
{
realReplaceBuffer();
document.getElementById("background-shadow").style.display = "none";
document.getElementById("confirm-dialog").style.display = "none";
editor.focus();
}
function cancelReplace ()
{
loadedBuffer = "";
loadedFilename = "";
document.getElementById("background-shadow").style.display = "none";
document.getElementById("confirm-dialog").style.display = "none";
editor.focus();
}
function replaceWithLoaded()
{
if (/\S/.test(editor.getValue())) {
document.getElementById("background-shadow").style.display = "block";
document.getElementById("confirm-dialog").style.display = "block";
}
else {
realReplaceBuffer();
}
editor.focus();
}
function clearBuffer ()
{
loadedBuffer = "";
loadedFilename = "";
replaceWithLoaded();
}
function realOpenFile (ev)
{
var f = ev.target.files[0];
if (f) {
var r = new FileReader();
r.onload = function(e) {
loadedBuffer = e.target.result;
loadedFilename = f.name;
replaceWithLoaded();
};
r.readAsText(f);
};
this.value = null;
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");
document.body.appendChild(a);
a.style.height = "0";
a.style.width = "0";
a.style.position = "absolute";
a.style.top = "0";
a.style.left = "0";
a.style.zIndex = "-10";
return function () {
a.href = "data:application/octet-stream;base64," + btoa(editor.getValue()+"\n");
a.download = /\S/.test(currentFilename) ? currentFilename : "Test.cd";
a.click();
editor.focus();
};
}) ();
function standardView()
{
var e = document.getElementById("editor");
var c = document.getElementById("console");
e.style.width = "100%";
e.style.height = "60vh";
c.style.width = "100%";
c.style.height = "37vh";
editor.focus();
}
function widescreenView()
{
var e = document.getElementById("editor");
var c = document.getElementById("console");
e.style.width = "50%";
e.style.height = "100%";
c.style.width = "40%";
c.style.height = "100%";
editor.focus();
}
function prove()
{
document.getElementById("console").innerHTML = "<p>Execution feature is not yet implemented</p>";
console.focus();
editor.focus();
}
function prove()
{
document.getElementById("console").innerHTML = "<p>Call to Why3 is not yet implemented</p>";
editor.focus();
}
editor.focus();
src/trywhy3/index.html
View file @ eeecc325
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html style="font-family:Verdana,Arial,Sans-Serif">
<html xmlns="http://www.w3.org/1999/xhtml"
style="font-family:Verdana,Arial,Sans-Serif">
<head>
<title>Try Why3</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" type="text/css" href="style.css" />
<!-- color customisation -->
<style>
.stdout { color : #bbccff; }
.stderr { color : #ffcccc ; }
.error {
position:absolute;
background:rgba(200,100,100,0.5);
z-index:40;
}
</style>
</head>
<body style="background-color:#ddd">
<h1 style="background-color:#356aa0;color:#fff">Try Why3</h1>
<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">
<!--invisible elements for the open file dialog -->
<input type="file" id="file-selector" />
<div id="background-shadow">
<div id="confirm-dialog" >
The content of the current buffer will be lost.<br/>
<div style="width:70%; display:inline-block;">
<button class="btn"
onclick="confirmReplace();">Confirm</button>
<button class="btn"
onclick="cancelReplace();">Cancel</button>
</div>
</div>
<td width="50%" style="vertical-align:top">
<div id="output">
<script type="text/javascript" src="trywhy3.js"></script>
</div>
</table>
<hr>
<!-- the main page -->
<h1 style="background-color:#356aa0;color:#fff">Try Why3</h1>
<p>Type some program in the text area below, then select
'Prove all' in the Why3 menu to generate proof obligations.</p>
<p>Related links
<ul>
<li>The <a href="http://why3.lri.fr/">Why3 home page</a>
......@@ -28,5 +40,63 @@
compiler used to produce this page
</ul>
</p>
<div class="menu-bar">
<ul>
<li><a href="#">File</a>
<ul>
<li><a href="#" onclick="openFile();">Open file…</a></li>
<li><a href="#" onclick="saveFile();">Save file as…</a></li>
</ul>
</li>
<li><a href="#">Edit</a>
<ul>
<li><a href="#" onclick="editor.undo();">Undo</a></li>
<li><a href="#" onclick="editor.redo();">Redo</a></li>
<li><a href="#" onclick="clearBuffer();">Clear buffer</a></li>
</ul>
</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>
</ul>
</li>
<li><a href="#">Why3</a>
<ul>
<li><a href="#" id="run">Run main function</a></li>
<li><a href="#" id="prove">Prove all</a></li>
</ul>
</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();"
/>Split Vertically</a>
</li>
<li></li>
</ul>
</li>
<li style="float:right;"><a href="#">Help</a></li>
</ul>
</div>
<div id="editor-panel">
<div id="editor" title="Editor" tabindex="-1" ></div>
<div title="Console" id="console">
</div>
</div>
<script defer="true" src="ace-builds/src-noconflict/ace.js" type="text/javascript" charset="utf-8"></script>
<script defer="true" type="text/javascript" src="editor_helper.js" ></script>
<script defer="true" type="text/javascript" src="try.js" ></script>
</body>
</html>
src/trywhy3/style.css 0 → 100644
View file @ eeecc325
body {
padding:0;
margin:0;
font-family: sans-serif;
}
/* CSS MENU BAR */
.menu-bar {
margin:0;
z-index:10;
font-size:2vh;
padding:0;
}
.menu-bar:after {
content:"";
display:table;
clear:both;
}
.menu-bar ul {
padding:0;
margin:0;
list-style: none;
position: relative;
background-image: linear-gradient(to bottom, #eee, #ccc);
height:3vh;
z-index:10;
box-sizing:border-box;
}
/* Positioning the navigation items inline */
.menu-bar ul li {
margin: 0;
padding:0;
display:inline-block;
float: left;
height:100%;
box-sizing:border-box;
}
/* Styling the links */
.menu-bar > ul > li > a {
display:block;
padding:0pt 1em;
color:#444;
text-decoration:none;
border-radius: 5pt 5pt 0pt 0pt;
border-style:solid;
border-width:1pt;
border-color:transparent;
height:100%;
box-sizing:border-box;
margin:0;
}
/* Background color change on Hover */
.menu-bar > ul > li > a:hover {
background-image: linear-gradient(to bottom, #eee, #bbb);
border-color: #aaa;
box-sizing:border-box;
}
.menu-bar > ul > li > ul {
/* display:none;*/
height:0;
overflow:hidden;
box-sizing:border-box;
}
.menu-bar > ul > li:hover > ul {
height:auto;
background-color:#ddd;
box-shadow:0pt 0pt 5pt #444;
}
.menu-bar > ul > li > ul > li {
float:none;
display:list-item;
position: relative;
}
.menu-bar > ul > li > ul > li > a {
display:block;
padding:1pt 2pt 1pt 2pt;
color:#444;
text-decoration:none;
border-radius: 1pt;
border-style:solid;
border-width:1pt;
border-color:transparent;
box-sizing:border-box;
}
.menu-bar > ul > li > ul > li > a:hover {
border-color:#cce;
background-image: linear-gradient(to bottom, #abe, #68b);
}
/* Hidden file selector */
#file-selector {
position:absolute;
left:0;
top:0;
width:0;
height:0;
z-index:-1;
}
#editor-panel {
position:relative;
display:block;
box-sizing: border-box;
padding:0;
margin:0;
height:97vh;
}
#console {
position:relative;
display:inline-block;
box-sizing: border-box;
font-size: large;
font-family: monospace;
white-space: pre-wrap;
width:40%;
height:100%;
/* background: #444; */
margin:0 0 0 0;
padding:0 0 0 0;
vertical-align:top;
}
#editor {
position:relative;
font-size: large;
box-sizing: border-box;
display:inline-block;
width:50%;
height:100%;
margin:0 0 0 0;
padding:0 0 0 0;
z-index:0;
vertical-align:top;
}
/* Confirmation dialog */
.btn {
width:100%;
z-index:1;
margin:0 0 4pt 0;
box-sizing:border-box;
}
#confirm-dialog {
z-index:20;
display:none;
position:absolute;
margin: 0 auto;
padding: 2pt 0;
width:50%;
left:25%;
right:25%;
top:20%;
border-radius:5pt;
background: #eee;
text-align:center;
}
#background-shadow {
display:none;
background-color: rgba(0,0,0,0.8);
position:absolute;
width:100%;
height:100%;
top: 0;
left:0;
z-index:15;
}
#confirm-dialog .btn {
width:40%;
}
src/trywhy3/trywhy3.ml
View file @ eeecc325
let examples =
[ "Drinkers paradox","
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
";
"Simple Arithmetic","
theory T
use import int.Int
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
";
]
(** 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
module Html = struct
......@@ -96,6 +27,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)
let temp_file_name = "/input.mlw"
let why3_conf_file = "/why3.conf"
......@@ -140,25 +78,38 @@ let run_alt_ergo_on_task t =
Driver.print_task alt_ergo_driver str_formatter t;
let text = flush_str_formatter () in
(* TODO ! *)
(* from Alt-Ergo:
let a = Why_parser.file Why_lexer.token lb in
let ltd, typ_env = Why_typing.file false Why_typing.empty_env a in
let declss = Why_typing.split_goals ltd in
SAT.start ();
let declss = List.map (List.map fst) declss in
let report = FE.print_status in
let pruning =
List.map
(fun d ->
if select () > 0 then Pruning.split_and_prune (select ()) d
else [List.map (fun f -> f,true) d])
in
List.iter
(List.iter
(fun dcl ->
let cnf = Cnf.make dcl in
ignore (Queue.fold (FE.process_decl report)
(SAT.empty (), true, Explanation.empty) cnf)
)) (pruning declss)
*)
text
let split_trans = 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 prove text =
let ch = open_out temp_file_name in
output_string ch text;
close_out ch;
let answer =
try
(* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
let theories = Env.read_file Env.base_language env temp_file_n