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

diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy
new file mode 100644
index 00000000..2178db9f
--- /dev/null
+++ b/Test/hofs/Twice.dfy
@@ -0,0 +1,38 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function method Twice(f : A -> A): A -> A
+{
+  x requires f.requires(x) && f.requires(f(x))
+    reads f.reads(x) reads if f.requires(x) then f.reads(f(x)) else {}
+  => f(f(x))
+}
+
+method Simple() {
+  assert Twice(x => x + 1)(0) == 2;
+  assert Twice(Twice(x => x + 1))(0) == 4;
+
+  // why does these fail? need requires/reads for literals?
+  // assert Twice(Twice)(x => x + 1)(0) == 4;
+  // assert Twice(Twice)(Twice)(x => x + 1)(0) == 16;
+}
+
+method WithReads() {
+  var a : array<int> := new int[1];
+  a[0] := 1;
+  var f := x reads a => x + a[0];
+  assert Twice(f)(0) == 2;
+  a[0] := 2;
+  assert Twice(f)(0) == 4;
+  assert Twice(f)(0) == 2; // should fail
+  assert false;            // should fail
+}
+
+
+function method Twice_bad(f : A -> A): A -> A
+{
+  x requires f.requires(x) && f.requires(f(x))
+    reads f.reads(x) + f.reads(f(x))
+  => f(f(x))
+}
+