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, 60 insertions, 0 deletions

diff --git a/Test/hofs/Lambda.dfy b/Test/hofs/Lambda.dfy
new file mode 100644
index 00000000..44adb4ce
--- /dev/null
+++ b/Test/hofs/Lambda.dfy
@@ -0,0 +1,60 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method M<A>() {
+    var f1 : A -> A := x   => x;
+    var f2 : A -> A := (x) => x;
+    var f3 : () -> () := () => ();
+    var tt : () := ();
+    var f4 : (A, A) -> (A, A) := (x, y) => (y, x);
+    var f5 := (x : int) => x;
+
+    var f6 := x requires x != 0 requires x != 1 => x;
+    var f7 := x requires 0 != x requires x != 1 => x;
+    assert f6(2) == f7(2);
+
+    var u := 0;
+    var f8 := () requires u == 0 => true;
+    assert f8();
+    u := 1;
+    assert f8(); // ok, u value is copied at creation of f8
+
+    var f9 := () requires u == 0 => true;
+    assert !f9.requires();
+
+}
+
+datatype List<A> = Cons(A,List<A>) | Nil
+
+method J(xs : List<int>) returns (z : int) {
+    match xs
+        case Cons(y,ys) => z := y;
+        case Nil        => z := 0;
+
+    if {
+        case true => z := z;
+        case true => z := 1;
+    }
+}
+
+function Adder() : (int, int) -> int
+  ensures forall x, y :: Adder().requires(x, y);
+  ensures forall x, y :: (Adder())(x, y) == x + y;
+{
+  (x, y) => x + y
+}
+
+function MkId<A>() : A -> A
+{
+  x => x
+}
+
+
+// storage and references to functions
+method T() {
+   var f := x => x + 1;
+   f := u => if u > 0 then f(u) else u;
+   assert f(1) == 2 && f(0) == 0;
+}
+