Add higher-order-functions and some other goodies

  * The reads clause now needs to be self framing.

  * The requires clause now needs to be framed by the reads clause.

  * There are one-shot lambdas, with a single arrow, but they will probably be
    removed.

  * There is a {:heapQuantifier} attribute to quantifiers, but they will
    probably be removed.

  * Add smart handling of type variables

  * Add < and > for datatype & type parameter

1 files changed, 52 insertions, 2 deletions

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
index 30258092..61004ddd 100644
--- a/Source/Dafny/Util.cs
+++ b/Source/Dafny/Util.cs
@@ -3,11 +3,17 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Text;

 

+using Microsoft.Boogie;

+

+

 namespace Microsoft.Dafny {

   class Util

   {

-    public delegate string ToString<T>(T t);

-    public static string Comma<T>(string comma, IEnumerable<T> l, ToString<T> f) {

+    public static string Comma<T>(IEnumerable<T> l, Func<T, string> f) {

+      return Comma(",", l, f);

+    }

+

+    public static string Comma<T>(string comma, IEnumerable<T> l, Func<T,string> f) {

       string res = "";

       string c = "";

       foreach(var t in l) {

@@ -16,5 +22,49 @@ namespace Microsoft.Dafny {
       }

       return res;

     }

+

+    public static List<B> Map<A,B>(IEnumerable<A> xs, Func<A,B> f)

+    {

+      List<B> ys = new List<B>();

+      foreach (A x in xs) {

+        ys.Add(f(x));

+      }

+      return ys;

+    }

+

+    public static List<A> Nil<A>() {

+      return new List<A>();

+    }

+

+    public static List<A> Singleton<A>(A x) {

+      return new List<A> { x };

+    }

+

+    public static List<A> Cons<A>(A x, List<A> xs) {

+      return Concat(Singleton(x), xs);

+    }

+

+    public static List<A> Snoc<A>(List<A> xs, A x) {

+      return Concat(xs, Singleton(x));

+    }

+

+    public static List<A> Concat<A>(List<A> xs, List<A> ys) {

+      List<A> cpy = new List<A>(xs);

+      cpy.AddRange(ys);

+      return cpy;

+    }

+

+    public static Dictionary<A,B> Dict<A,B>(IEnumerable<A> xs, IEnumerable<B> ys) {

+      return Dict<A,B>(xs.Zip(ys)); 

+    }

+

+    public static Dictionary<A,B> Dict<A,B>(IEnumerable<Tuple<A,B>> xys) {

+      Dictionary<A,B> res = new Dictionary<A,B>();

+      foreach (var p in xys) {

+        res[p.Item1] = p.Item2; 

+      }

+      return res;

+    }

+

   }

 }