Implement Synthesis/Verification Tabs

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("")

web/app/examples/Example.scala

 package examples
 
-case class Example(title: String, code: String)
+case class Example(title: String, kind: String, code: String)

web/app/examples/SynthesisExamples.scala

+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)
+}

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._

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)
       }

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)

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();
+        }
+    });
+}

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;
+}