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

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
new file mode 100644
index 00000000..7df4bbb3
--- /dev/null
+++ b/Test/hofs/ResolveError.dfy
@@ -0,0 +1,51 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method ResolutionErrors() {
+    var x;
+    var g5 := x, y => (y, x);   // fail at resolution
+    var g6 := x, (y => (y, x)); // fail at resolution
+}
+
+// cannot assign functions
+
+class Apa {
+  function f() : int {
+    0
+  }
+}
+
+method Nope3() {
+  var apa := new Apa;
+  apa.f := () => 2;
+}
+
+method RequiresFail(f : int -> int)
+  // ok
+  requires f(0) == 0;
+  requires f.requires(0);
+  requires f.reads(0) == {};
+
+  // fail
+  requires f(0) == true;
+  requires f(1,2) == 0;
+  requires f(true) == 0;
+  requires f.requires(true);
+  requires f.requires(1) == 0;
+  requires f.requires(1,2);
+  requires f.reads(true) == {};
+  requires f.reads(1) == 0;
+  requires f.reads(1,2) == {};
+{
+}
+
+predicate method Bool()
+{
+  true
+}
+
+method Bla() {
+  assert Bool;
+}
+