- the "-gen" option works only if the program verifies

3 files changed, 85 insertions, 71 deletions

diff --git a/Chalice/src/Chalice.cs b/Chalice/src/Chalice.cs
index 60e2afa9..cc7e98b6 100644
--- a/Chalice/src/Chalice.cs
+++ b/Chalice/src/Chalice.cs
@@ -9,96 +9,107 @@ using System.Threading;
 

 namespace Chalice

 {

-    public class ImmutableList<E>

+  public class ImmutableList<E>

+  {

+    private List<E> list;

+

+    public ImmutableList()

     {

-        private List<E> list;

-        

-        public ImmutableList() {

-            list = new List<E>();

-        }

+      list = new List<E>();

+    }

 

-        public ImmutableList(IEnumerable<E> elems)

-        {

-            list = new List<E>(elems);

-        }

+    public ImmutableList(IEnumerable<E> elems)

+    {

+      list = new List<E>(elems);

+    }

 

-        public ImmutableList<E> Append(ImmutableList<E> other)

-        {

-            var res = new ImmutableList<E>();

-            res.list.AddRange(list);

-            res.list.AddRange(other.list);

-            return res;

-        }

+    public ImmutableList<E> Append(ImmutableList<E> other)

+    {

+      var res = new ImmutableList<E>();

+      res.list.AddRange(list);

+      res.list.AddRange(other.list);

+      return res;

+    }

 

-        public E At(int index)

-        {

-            return list[index];

-        }

+    public E At(int index)

+    {

+      return list[index];

+    }

 

-        public ImmutableList<E> Take(int howMany)

-        {

-            var res = new ImmutableList<E>(this.list.Take(howMany));

-            return res;

-        }

+    public ImmutableList<E> Take(int howMany)

+    {

+      var res = new ImmutableList<E>(this.list.Take(howMany));

+      return res;

+    }

 

-        public ImmutableList<E> Drop(int howMany)

-        {

-            var res = new ImmutableList<E>(this.list.Skip(howMany));

-            return res;

-        }

+    public ImmutableList<E> Drop(int howMany)

+    {

+      var res = new ImmutableList<E>(this.list.Skip(howMany));

+      return res;

+    }

 

-        public int Length

-        {

-            get

-            {

-                return list.Count;

-            }

-        }

+    public int Length

+    {

+      get

+      {

+        return list.Count;

+      }

+    }

 

-        public static ImmutableList<int> Range(int min, int max)

-        {

-            ImmutableList<int> l = new ImmutableList<int>();

-            for (int i = min; i < max; i++)

-            {

-                l.list.Add(i);

-            }

-            return l;

-        }

+    public static ImmutableList<int> Range(int min, int max)

+    {

+      ImmutableList<int> l = new ImmutableList<int>();

+      for (int i = min; i < max; i++)

+      {

+        l.list.Add(i);

+      }

+      return l;

     }

-    

-  public class ChannelBuffer<E> {

-    private LinkedList<E> contents = new LinkedList<E>();

-    

-    public void Add(E e) {

-      lock(this) {

-        contents.AddFirst(e);

+  }

+

+  public class ChannelBuffer<E>

+  {

+    private Queue<E> contents = new Queue<E>();

+

+    public void Add(E e)

+    {

+      lock (this)

+      {

+        contents.Enqueue(e);

         Monitor.Pulse(this);

       }

     }

-    

-    public E Remove() {

-      lock(this) {

-        while(contents.Count == 0){

+

+    public E Remove()

+    {

+      lock (this)

+      {

+        while (contents.Count == 0)

+        {

           Monitor.Wait(this);

         }

-        E e = contents.Last.Value; 

-        contents.RemoveLast();

+        E e = contents.Dequeue();

         return e;

       }

     }

   }

 

-  public class ChalicePrint {

-    public void Int(int x) {

+  public class ChalicePrint

+  {

+    public void Int(int x)

+    {

       System.Console.WriteLine(x);

     }

-    public void Bool(bool x) {

+    public void Bool(bool x)

+    {

       System.Console.WriteLine(x);

     }

   }

 

-  public class ChaliceSystem {

-    public void Done() {

+  public class ChaliceSystem

+  {

+    public void Done()

+    {

       ChannelBuffer<int> buffer = new ChannelBuffer<int>();

       buffer.Remove();

     }

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 8b36e367..1bba1a99 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -37,7 +37,7 @@ object Chalice {
       else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)

       else if (a == "-defaults") defaults = 3

       else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }

-      else if (a == "-gen") { gen = true; doTranslate = false }

+      else if (a == "-gen") { gen = true; }

       else if (a == "-autoFold") autoFold = true

       else if (a == "-autoMagic") autoMagic = true

       else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe

@@ -67,11 +67,6 @@ object Chalice {
               Console.err.println("The program did not typecheck."); 

               msgs foreach { msg => Console.err.println(msg) }

             case Resolver.Success() =>

-              if(gen) {

-                val converter = new ChaliceToCSharp(); 

-                val cs = converter.convertProgram(prog);

-                writeFile("out.cs", cs);

-              }

               if (doTranslate) {

                 // checking if Boogie.exe exists

                 val boogieFile = new File(boogiePath);

@@ -94,10 +89,17 @@ object Chalice {
                 val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + "out.bpl"); 

                 val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));

                 var line = input.readLine();

+                var previous_line = null: String;

                 while(line!=null){

                   println(line);

+                  previous_line = line;

                   line = input.readLine();

                 }

+                if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

+                  val converter = new ChaliceToCSharp(); 

+                  println("Code generated in out.cs.");

+                  writeFile("out.cs", converter.convertProgram(prog));

+                }

               }

             }

         }

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 110f7a2a..56e0a358 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -183,6 +183,7 @@ class ChaliceToCSharp {
       case Append(s1, s2) => convertExpression(s1) + ".Append(" + convertExpression(s2) + ")" 

       case Take(s, i) => convertExpression(s) + ".Take(" + convertExpression(i) + ")"

       case Drop(s, i) => convertExpression(s) + ".Drop(" + convertExpression(i) + ")" 

+      case LockBelow(_, _) => "true"

       case bin: BinaryExpr => "(" + convertExpression(bin.E0) + " " + bin.OpName + " " + convertExpression(bin.E1) + ")"// todo: <==> and ==>

       case Unfolding(p, e) => convertExpression(e)

       case FunctionApplication(target, id, args) => convertExpression(target) + "." + id + "(" + repsep(args map convertExpression, ", ") + ")"