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/Examples.dfy b/Test/hofs/Examples.dfy
new file mode 100644
index 00000000..c31b68da
--- /dev/null
+++ b/Test/hofs/Examples.dfy
@@ -0,0 +1,59 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function Apply(f: A -> B, x: A): B
+  reads f.reads(x);
+  requires f.requires(x);
+{
+  f(x)
+}
+
+function Apply'(f: A -> B) : A -> B
+{
+  x reads f.reads(x)
+    requires f.requires(x)
+    => f(x)
+}
+
+
+function Compose(f: B -> C, g:A -> B): A -> C
+{
+  x reads g.reads(x)
+    reads if g.requires(x) then f.reads(g(x)) else {}
+    requires g.requires(x)
+    requires f.requires(g(x))
+    => f(g(x))
+}
+
+function W(f : (A,A) -> A): A -> A
+{
+  x requires f.requires(x,x)
+    reads f.reads(x,x)
+    => f(x,x)
+}
+
+function Curry(f : (A,B) -> C) : A -> B -> C
+{
+  x => y requires f.requires(x,y)
+         reads f.reads(x,y)
+         => f(x,y)
+}
+
+function Uncurry(f : A -> B -> C) : (A,B) -> C
+{
+  (x,y) requires f.requires(x)
+        requires f(x).requires(y)
+        reads f.reads(x)
+        reads if f.requires(x) then f(x).reads(y) else {}
+        => f(x)(y)
+}
+
+function S(f : (A,B) -> C, g : A -> B): A -> C
+{
+  x requires g.requires(x)
+    requires f.requires(x,g(x))
+    reads g.reads(x)
+    reads if g.requires(x) then f.reads(x,g(x)) else {}
+    => f(x,g(x))
+}
+