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

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
new file mode 100644
index 00000000..645494cb
--- /dev/null
+++ b/Test/dafny0/Reads.dfy
@@ -0,0 +1,57 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Checking that the reads clause also is checked over requires
+
+class C { var u : int; }
+
+function nope1(c : C):()
+     requires c != null && c.u > 0;
+{()}
+
+function ok1(c : C):()
+     requires c != null && c.u > 0;
+     reads c;
+{()}
+
+function nope2(c : C):()
+     requires c != null && c.u > 0;
+     reads if c != null then {} else {c};
+{()}
+
+function ok2(c : C):()
+     requires c != null && c.u > 0;
+     reads if c != null then {c} else {};
+{()}
+
+function nope3(xs : seq<C>):()
+     requires |xs| > 0 && xs[0] != null && xs[0].u > 0;
+{()}
+
+function ok3(xs : seq<C>):()
+     requires |xs| > 0 && xs[0] != null && xs[0].u > 0;
+     reads xs;
+{()}
+
+function nope4(c : C, xs : set<C>):()
+     requires c != null && c !in xs ==> c.u > 0;
+     reads xs;
+{()}
+
+function ok4(c : C, xs : set<C>):()
+     requires c != null && c in xs ==> c.u > 0;
+     reads xs;
+{()}
+
+// reads over itself
+
+class R { var r : R; }
+
+function nope5(r : R):()
+  reads if r != null then {r.r} else {};
+{()}
+
+function ok5(r : R):()
+  reads if r != null then {r, r.r} else {};
+{()}
+