From eeecc325c74fe558a28cbb1c09992c2b4a8f9459 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Sun, 6 Sep 2015 21:22:32 +0200 Subject: [PATCH] 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 --- src/trywhy3/editor_helper.js | 202 ++++++++++++++++++++++++ src/trywhy3/index.html | 104 +++++++++++-- src/trywhy3/style.css | 182 ++++++++++++++++++++++ src/trywhy3/trywhy3.ml | 294 ++++++++++++----------------------- 4 files changed, 574 insertions(+), 208 deletions(-) create mode 100644 src/trywhy3/editor_helper.js create mode 100644 src/trywhy3/style.css diff --git a/src/trywhy3/editor_helper.js b/src/trywhy3/editor_helper.js new file mode 100644 index 000000000..27ce2bb06 --- /dev/null +++ b/src/trywhy3/editor_helper.js @@ -0,0 +1,202 @@ +/* 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 = "

Execution feature is not yet implemented

"; + console.focus(); + editor.focus(); +} + +function prove() +{ + document.getElementById("console").innerHTML = "

Call to Why3 is not yet implemented

"; + editor.focus(); +} + +editor.focus(); diff --git a/src/trywhy3/index.html b/src/trywhy3/index.html index 9e551cfc0..da2aec558 100644 --- a/src/trywhy3/index.html +++ b/src/trywhy3/index.html @@ -1,26 +1,38 @@ - - + Try Why3 + + + -

Try Why3

-

Type some program in the text area below, then click on - button 'Go' on the left to run Why3 on it.

-

Click on the other buttons to select one of the proposed examples.

- - -
-
-
- 		-
- + + +
+
+ The content of the current buffer will be lost.
+
+ + +
+
-
-
+ +

Try Why3

+

Type some program in the text area below, then select + 'Prove all' in the Why3 menu to generate proof obligations.

Related links

+
+ +
+
+
+
+
+
+ + + + diff --git a/src/trywhy3/style.css b/src/trywhy3/style.css new file mode 100644 index 000000000..dba45f93e --- /dev/null +++ b/src/trywhy3/style.css @@ -0,0 +1,182 @@ +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%; +} diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml index 5da9d3281..c5e284072 100644 --- a/src/trywhy3/trywhy3.ml +++ b/src/trywhy3/trywhy3.ml @@ -1,74 +1,5 @@ - -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,141 +78,115 @@ 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_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.map - (fun t -> - let (id,expl,_) = Termcode.goal_expl_task ~root:true t in - let expl = match expl with - | Some s -> s - | None -> id.Ident.id_string - in - let tl = Trans.apply split_trans t in - let tasks = - List.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 - let result = run_alt_ergo_on_task task in - let result = - if String.length result > 80 then - "..." ^ String.sub result (String.length result - 80) 80 - else result - in - [Html.of_string (expl ^" : " ^ result)]) - tl - in - [Html.of_string expl; Html.ul tasks]) - tasks - in - [ Html.of_string ("Theory " ^ thname); Html.ul tasks] - :: acc) - theories [] - in - Html.ul theories -(* - Stdlib.Mstr.iter - (fun _thname th -> + try + (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *) + let theories = Env.read_file Env.base_language env temp_file_name in + let theories = + Stdlib.Mstr.fold + (fun thname th acc -> let tasks = Task.split_theory th None None in - List.iter - (fun task -> - let (id,expl,_) = Termcode.goal_expl_task ~root:true task in + let tasks = List.map + (fun t -> + let (id,expl,_) = Termcode.goal_expl_task ~root:true t in let expl = match expl with | Some s -> s | None -> id.Ident.id_string in - push_answer - (Pp.sprintf "Goal: %s@\n" expl)) - tasks) -*) - 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 - Html.par - [Html.of_string - (Pp.sprintf - "error line %d, columns %d-%d: %a" l b e - Exn_printer.exn_printer e')] - | e -> - Html.par - [Html.of_string - (Pp.sprintf - "unexpected exception: %a (%s)" Exn_printer.exn_printer e - (Printexc.to_string e))] + let tl = Trans.apply split_trans t in + let tasks = + List.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 + let result = run_alt_ergo_on_task task in + let result = + if String.length result > 80 then + "..." ^ String.sub result (String.length result - 80) 80 + else result + in + [Html.of_string (expl ^" : " ^ result)]) + tl + in + [Html.of_string expl; Html.ul tasks]) + tasks + in + [ Html.of_string ("Theory " ^ thname); Html.ul tasks] + :: acc) + theories [] + in + Html.ul 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 + Html.par + [Html.of_string + (Pp.sprintf + "error line %d, columns %d-%d: %a" l b e + Exn_printer.exn_printer e')] + | e -> + Html.par + [Html.of_string + (Pp.sprintf + "unexpected exception: %a (%s)" Exn_printer.exn_printer e + (Printexc.to_string e))] +let () = + let handler = Dom.handler + (fun _ev -> + log "why3 prove is running"; + let global = Js.Unsafe.global in + let editor = Js.Unsafe.get global (Js.string "editor") in + let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in + let answer = prove code in + (* remove the previous answer if any *) + let console = + get_opt (Dom_html.document ## getElementById (Js.string "console")) + in + Js.Opt.iter (console##lastChild) (Dom.removeChild console); + (* put the new answer *) + Dom.appendChild console answer; + Js._false) 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 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 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) Html.d in - b##textContent <- Js.some (Js.string name); - Dom.appendChild output b; - b##onclick <- - D.handler - (fun (_ : D.mouseEvent Js.t) -> - textbox##value <- Js.string text; - Js._false)) - examples; - Dom.appendChild output (D.createBr Html.d); - (* third, the go button *) - let go = D.createButton ~name:(Js.string "go") Html.d in - go##textContent <- Js.some (Js.string "Go"); - Dom.appendChild output go; - Dom.appendChild output (D.createBr Html.d); - (* then, the answer zone *) - 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 output preview; - Js._false - -let _ = D.window##onload <- D.handler onload + let button = + get_opt (Dom_html.document ## getElementById (Js.string "prove")) + in + button ## onclick <- handler (* -- GitLab