From c617e3d0e5b40a7029d74e16ca352ab280e8c2df Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 12 Dec 2012 16:10:12 +0100
Subject: [PATCH] Implement Synthesis/Verification Tabs
---
web/app/controllers/Application.scala | 2 +-
web/app/examples/Example.scala | 2 +-
web/app/examples/SynthesisExamples.scala | 87 +++++++++++++++++++++
web/app/examples/VerificationExamples.scala | 4 +-
web/app/models/LeonConsole.scala | 17 ++++
web/app/views/index.scala.html | 48 ++++++++----
web/public/javascripts/leon.js | 31 +++++++-
web/public/stylesheets/leon.css | 31 ++++++++
8 files changed, 200 insertions(+), 22 deletions(-)
create mode 100644 web/app/examples/SynthesisExamples.scala
diff --git a/web/app/controllers/Application.scala b/web/app/controllers/Application.scala
index 1d2269a49..94a48eba4 100644
--- a/web/app/controllers/Application.scala
+++ b/web/app/controllers/Application.scala
@@ -12,7 +12,7 @@ import models.LeonConsole
object Application extends Controller {
- val examples = VerificationExamples.allExamples
+ val examples = VerificationExamples.allExamples ++ SynthesisExamples.allExamples
def index = Action { implicit request =>
val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
diff --git a/web/app/examples/Example.scala b/web/app/examples/Example.scala
index 8cd2b871a..dcf38d999 100644
--- a/web/app/examples/Example.scala
+++ b/web/app/examples/Example.scala
@@ -1,3 +1,3 @@
package examples
-case class Example(title: String, code: String)
+case class Example(title: String, kind: String, code: String)
diff --git a/web/app/examples/SynthesisExamples.scala b/web/app/examples/SynthesisExamples.scala
new file mode 100644
index 000000000..6ee3b804d
--- /dev/null
+++ b/web/app/examples/SynthesisExamples.scala
@@ -0,0 +1,87 @@
+package examples
+
+object SynthesisExamples {
+ var allExamples = List[Example]()
+
+ def newExample(title: String, code: String) {
+ allExamples = allExamples ::: Example(title, "synthesis", code) :: Nil
+ }
+
+ newExample("ADT Induction", """
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object SortedList {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ // proved with unrolling=0
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ //def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
+
+ def content(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ //def artifialSubcase(v : Int) = choose {
+ // (out : List) =>
+ // content(out) == (content(Nil()) -- Set(v))
+ //}
+
+ def deleteSynth(in: List, v: Int) = choose {
+ (out: List) =>
+ // This spec is too weak. Maybe use later as bad example?
+ //!(content(out) contains v) && size(out)+1 >= size(in)
+ (content(out) == (content(in) -- Set(v)))
+ }
+
+ def concatSynth(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+}""".trim)
+
+ newExample("Binary Tree", """
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def content(t : Tree): Set[Int] = t match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def delete(in : Tree, v : Int) = choose { (out : Tree) =>
+ content(out) == (content(in) -- Set(v))
+ }
+}
+ """.trim)
+
+ newExample("Seconds to Time", """
+import leon.Utils._
+
+object Sec2Time {
+
+ def s2t(total: Int) : (Int, Int, Int) = choose((h: Int, m: Int, s: Int) => 3600*h + 60*m + s == total && h >= 0 && m >= 0 && m < 60 && s >= 0 && s < 60)
+
+}
+ """.trim)
+}
diff --git a/web/app/examples/VerificationExamples.scala b/web/app/examples/VerificationExamples.scala
index 60a053b84..f0243f699 100644
--- a/web/app/examples/VerificationExamples.scala
+++ b/web/app/examples/VerificationExamples.scala
@@ -4,10 +4,10 @@ object VerificationExamples {
var allExamples = List[Example]()
def newExample(title: String, code: String) {
- allExamples = allExamples ::: Example(title, code) :: Nil
+ allExamples = allExamples ::: Example(title, "verification", code) :: Nil
}
- val default = Example("Default", """
+ val default = Example("Default", "verification", """
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala
index 04da86e2a..f4e910b88 100644
--- a/web/app/models/LeonConsole.scala
+++ b/web/app/models/LeonConsole.scala
@@ -18,6 +18,7 @@ import play.api.Play.current
import leon.{LeonContext, Settings, Reporter}
import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
+import leon.synthesis.SynthesisPhase
import leon.verification.AnalysisPhase
object LeonConsole {
@@ -115,6 +116,22 @@ class ConsoleSession extends Actor {
event("started")
isStarted = true
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = true,
+ xlang = false,
+ verify = false
+ ),
+ files = Nil,
+ reporter = new WSReporter(channel)
+ )
+
+ val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen SynthesisPhase
+
+ pipeline.run(ctx)((code, "--parallel" :: "--timeout=10" :: Nil))
+
+ event("stopped")
+
case _ =>
error("Invalid request mode: "+mode)
}
diff --git a/web/app/views/index.scala.html b/web/app/views/index.scala.html
index 1f132f0a5..e1e8188c6 100644
--- a/web/app/views/index.scala.html
+++ b/web/app/views/index.scala.html
@@ -14,34 +14,50 @@
<div id="codecolumn">
<div id="codebox">@default.code</div>
<input type="submit" id="askbutton" value="Ask Leon !">
- <textarea id="consolebox"></textarea>
+ <div><textarea id="consolebox"></textarea></div>
</div>
<div id="selectcolumn">
- <h3>Load an Example:</h3>
- <div>We provide you with a list of code-examples, select one from the list below to load it:</div>
- <select id="example-loader" name="codeexample" onchange="loadExample('@prefix');">
- <option value="">-- Load Example --</option>
- @exs.zipWithIndex.map{ case (ex, i) =>
- <option value="@i">@ex.title</option>
- }
- </select>
+ <input type="hidden" id="leon-mode" value="">
+ <div id="tabs">
+ <a href="#verification">Verification</a>
+ <a href="#synthesis">Synthesis</a>
+ </div>
+ <div id="tabcontent">
+ <div id="tab-synthesis" class="tab synthesis">
+ <h3>Load an Example:</h3>
+ <div>We provide you with a list of code-examples, select one from the list below to load it:</div>
+ <select id="example-loader-synthesis" name="codeexample" onchange="loadExample('synthesis', '@prefix');">
+ <option value="">-- Load Example --</option>
+ @exs.zipWithIndex.collect{ case (ex, i) if ex.kind == "synthesis" =>
+ <option value="@i">@ex.title</option>
+ }
+ </select>
+ </div>
+ <div id="tab-verification" class="tab verification">
+ <h3>Load an Example:</h3>
+ <div>We provide you with a list of code-examples, select one from the list below to load it:</div>
+ <select id="example-loader-verification" name="codeexample" onchange="loadExample('verification', '@prefix');">
+ <option value="">-- Load Example --</option>
+ @exs.zipWithIndex.collect{ case (ex, i) if ex.kind == "verification" =>
+ <option value="@i">@ex.title</option>
+ }
+ </select>
+ </div>
+ </div>
+
</div>
</form>
<script>
$(document).ready(function() {
var WS = window['MozWebSocket'] ? MozWebSocket : WebSocket
var leonSocket = new WS("@leon.web.controllers.routes.Application.openConsole().webSocketURL()")
-
- var sendMessage = function() {
- }
-
+
var receiveEvent = function(event) {
var data = JSON.parse(event.data)
if (data.kind == "error") {
alert(data.message);
} else if (data.kind == "log") {
var txt = $("#consolebox")
-
txt.val(txt.val()+"\n"+data.message);
txt.scrollTop(txt[0].scrollHeight - txt.height())
} else if (data.kind == "event") {
@@ -52,14 +68,14 @@
}
}
}
-
+
leonSocket.onmessage = receiveEvent
var leonStatus = "stopped"
$("#leoninput").submit(function () {
var msg = JSON.stringify(
- {action: "start", mode: "verification", code: editor.getValue()}
+ {action: "start", mode: $("#leon-mode").val(), code: editor.getValue()}
)
leonSocket.send(msg)
diff --git a/web/public/javascripts/leon.js b/web/public/javascripts/leon.js
index 301629a40..6d2a774b9 100644
--- a/web/public/javascripts/leon.js
+++ b/web/public/javascripts/leon.js
@@ -4,8 +4,8 @@ function appendError(title, msg) {
alert(title+": "+msg)
}
-function loadExample(prefix) {
- var value = $("#example-loader").val()
+function loadExample(kind, prefix) {
+ var value = $("#example-loader-"+kind).val()
if (value) {
$.ajax({
@@ -32,5 +32,32 @@ $(document).ready(function() {
editor.getSession().setMode("ace/mode/scala");
editor.getSession().setUseWrapMode(true);
+
+ $("#tabs a").click(function() {
+ activateTab($(this).attr("href"));
+ });
+
+ var hash = window.location.hash
+
+ if (hash == "") {
+ activateTab("#verification");
+ } else {
+ activateTab(hash);
+ }
});
+
+function activateTab(tab) {
+
+ $("#tabs a").each(function() {
+ var wh = $(this).attr("href").substr(1);
+ if ($(this).attr("href") == tab) {
+ $(this).addClass("active");
+ $("#tab-"+wh).show();
+ $("#leon-mode").val(wh);
+ } else {
+ $(this).removeClass("active");
+ $("#tab-"+wh).hide();
+ }
+ });
+}
diff --git a/web/public/stylesheets/leon.css b/web/public/stylesheets/leon.css
index ba3362693..c2c8f7f19 100644
--- a/web/public/stylesheets/leon.css
+++ b/web/public/stylesheets/leon.css
@@ -173,3 +173,34 @@ textarea#consolebox {
font-family: "Lucida Console", monospace;
font-size: 11px;
}
+
+#tabcontent div.tab {
+ display: none;
+}
+
+#tabcontent div.tab.active {
+ display: block;
+}
+
+#tabcontent {
+ clear: both;
+ padding: 20px 10px 10px 10px;
+ border-left: 1px solid black;
+}
+
+#tabs a {
+ float: left;
+ padding: 10px;
+ border-right: 1px solid black;
+ border-bottom: 1px solid black;
+}
+
+#tabs a:first-child {
+ border-left: 1px solid black;
+}
+
+#tabs a.active {
+ background: white;
+ border-bottom: none;
+ border-top: 1px solid black;
+}
--
GitLab