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

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
new file mode 100644
index 00000000..bc80713d
--- /dev/null
+++ b/Test/hofs/ReadsReads.dfy
@@ -0,0 +1,59 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function MyReadsOk(f : A -> B, a : A) : set<object>
+  reads f.reads(a);
+{
+  f.reads(a)
+}
+
+function MyReadsOk2(f : A -> B, a : A) : set<object>
+  reads f.reads(a);
+{
+  (f.reads)(a)
+}
+
+function MyReadsOk3(f : A -> B, a : A) : set<object>
+  reads (f.reads)(a);
+{
+  f.reads(a)
+}
+
+function MyReadsOk4(f : A -> B, a : A) : set<object>
+  reads (f.reads)(a);
+{
+  (f.reads)(a)
+}
+
+function MyReadsBad(f : A -> B, a : A) : set<object>
+{
+  f.reads(a)
+}
+
+function MyReadsBad2(f : A -> B, a : A) : set<object>
+{
+  (f.reads)(a)
+}
+
+function MyReadsOk'(f : A -> B, a : A, o : object) : bool
+  reads f.reads(a);
+{
+  o in f.reads(a)
+}
+
+function MyReadsBad'(f : A -> B, a : A, o : object) : bool
+{
+  o in f.reads(a)
+}
+
+function MyRequiresOk(f : A -> B, a : A) : bool
+  reads f.reads(a);
+{
+  f.requires(a)
+}
+
+function MyRequiresBad(f : A -> B, a : A) : bool
+{
+  f.requires(a)
+}
+