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

45 files changed, 1684 insertions, 0 deletions

diff --git a/Test/hofs/Apply.dfy b/Test/hofs/Apply.dfy
new file mode 100644
index 00000000..bdd102c2
--- /dev/null
+++ b/Test/hofs/Apply.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method Apply(x : int) returns (i : int)
+  ensures i == x;
+{
+  i := (x => x)(x);
+}
+
+function method Const<A,B>(a : A) : B -> A {
+  b => a
+}
+
+method Test(m : map<int, int -> int -> int>)
+{
+  assume forall i :: i in m;
+  assume forall i, x :: m[i].requires(x);
+  assume forall i, x, y :: m[i](x).requires(y);
+  assume m[1](2)(3) > 5;
+  assert ((m[1])(2))(3) > 4;
+}
+
+method Main() {
+  assert forall x : int, y : int :: Const(x)(y) == (Const(x))(y);
+  assert (a => b => a) == (u : int) => (v : int) => u;
+  assert Const == (u : int) => (v : int) => u;
+}
+
diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect
new file mode 100644
index 00000000..fad1fe33
--- /dev/null
+++ b/Test/hofs/Apply.dfy.expect
@@ -0,0 +1,7 @@
+Apply.dfy(27,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Apply.dfy(26,35): anon15_Else

+    Apply.dfy(27,27): anon17_Else

+

+Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
new file mode 100644
index 00000000..91d7e384
--- /dev/null
+++ b/Test/hofs/Classes.dfy
@@ -0,0 +1,50 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+class C {
+  static function method Static() : bool
+  {
+    true
+  }
+}
+
+method K() {
+  var f := C.Static;
+  var o : object;
+  assert o !in f.reads();
+  assert f.requires();
+  assert f();
+}
+
+
+class T {
+  var h : int -> int;
+}
+
+function B(t : T) : int -> int
+  requires t != null;
+  reads t;
+{
+  t.h
+}
+
+function J(t : T) : int
+  requires t != null;
+  requires t.h.reads(0) == {};
+  reads t;
+  reads if t != null then t.h.reads(0) else {};
+{
+  if t.h.requires(0) then
+    B(t)(0)
+  else
+    B(t)(0)  // fail
+}
+
+method U(t : T)
+  requires t != null;
+  modifies t;
+{
+  t.h := x => x;
+  assert J(t) == 0; // ok
+}
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
new file mode 100644
index 00000000..84a0417e
--- /dev/null
+++ b/Test/hofs/Classes.dfy.expect
@@ -0,0 +1,10 @@
+Classes.dfy(41,5): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Then

+    (0,0): anon13_Else

+    (0,0): anon14_Else

+

+Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/hofs/Consequence.dfy b/Test/hofs/Consequence.dfy
new file mode 100644
index 00000000..35934470
--- /dev/null
+++ b/Test/hofs/Consequence.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Check() {
+  var f : nat -> nat;
+  assume f.requires(0);
+  var i : nat := f(0);
+}
+
diff --git a/Test/hofs/Consequence.dfy.expect b/Test/hofs/Consequence.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/hofs/Consequence.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

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))
+}
+
diff --git a/Test/hofs/Examples.dfy.expect b/Test/hofs/Examples.dfy.expect
new file mode 100644
index 00000000..76f19e0d
--- /dev/null
+++ b/Test/hofs/Examples.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/hofs/Field.dfy b/Test/hofs/Field.dfy
new file mode 100644
index 00000000..6d3412d7
--- /dev/null
+++ b/Test/hofs/Field.dfy
@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// calling fields should not make a resolution error:
+
+class Ref<A> {
+  var val: A;
+}
+
+method Nope() {
+  var f := new Ref<int -> bool>;
+  assert f.val(0);
+}
+
+class FnRef<A,B> {
+  var fn: A -> B;
+}
+
+method Nope2() {
+  var f := new FnRef<int,bool>;
+  assert f.fn(0);
+}
+
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect
new file mode 100644
index 00000000..927d8b06
--- /dev/null
+++ b/Test/hofs/Field.dfy.expect
@@ -0,0 +1,14 @@
+Field.dfy(12,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Field.dfy(12,12): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+Field.dfy(21,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Field.dfy(21,12): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 4 errors

diff --git a/Test/hofs/FnRef.dfy b/Test/hofs/FnRef.dfy
new file mode 100644
index 00000000..fb8136b7
--- /dev/null
+++ b/Test/hofs/FnRef.dfy
@@ -0,0 +1,70 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+class Ref<A> {
+  var val: A;
+}
+
+method Nope() {
+  var f : Ref<int -> bool>;
+  var g : int -> bool;
+
+  f := new Ref<int -> bool>;
+
+  f.val := x => true;
+
+  g := x reads f reads f.val.reads(x) => !f.val(x);
+}
+
+method M() {
+  var f : Ref<int -> bool>;
+  var g : int -> bool;
+
+  f := new Ref<int -> bool>;
+
+  f.val := x => true;
+
+  g := x reads f reads f.val.reads(x) requires f.val.requires(x) => !f.val(x);
+
+  f.val := g;
+
+  if (!g(0)) {
+    assert !g(0);
+  } else {
+    assert g(0);
+  }
+}
+
+
+method L() {
+  var f : Ref<() -> bool>;
+  f := new Ref<() -> bool>;
+  f.val := () reads f reads f.val.reads() requires !f.val.requires() => true;
+
+  if (f.val.requires()) {
+    assert !f.val.requires();
+  } else {
+    assert f.val.requires();
+  }
+}
+
+method LRead() {
+  var o : object;
+  var f : Ref<() -> bool>;
+  f := new Ref<() -> bool>;
+  f.val := () reads f
+              reads f.val.reads()
+              reads if o in f.val.reads() then {} else {o}
+              => true;
+
+  assume o != null;
+  assert o != f;
+
+  if (o in f.val.reads()) {
+    assert o !in f.val.reads();
+  } else {
+    assert o in f.val.reads();
+  }
+}
+
diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect
new file mode 100644
index 00000000..5185c21c
--- /dev/null
+++ b/Test/hofs/FnRef.dfy.expect
@@ -0,0 +1,27 @@
+FnRef.dfy(17,45): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    FnRef.dfy(15,12): anon5_Else

+    (0,0): anon6_Then

+FnRef.dfy(32,8): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    FnRef.dfy(26,12): anon9_Else

+    FnRef.dfy(28,8): anon10_Else

+FnRef.dfy(46,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    FnRef.dfy(43,13): anon7_Else

+    (0,0): anon9_Then

+FnRef.dfy(65,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    FnRef.dfy(56,13): anon8_Else

+    (0,0): anon10_Then

+FnRef.dfy(67,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    FnRef.dfy(56,13): anon8_Else

+    (0,0): anon10_Else

+

+Dafny program verifier finished with 4 verified, 5 errors

diff --git a/Test/hofs/Frame.dfy b/Test/hofs/Frame.dfy
new file mode 100644
index 00000000..891435ba
--- /dev/null
+++ b/Test/hofs/Frame.dfy
@@ -0,0 +1,128 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+class C { var u : int; }
+
+method M(f : int -> int)
+  requires f.requires(0);
+{
+  var init := f(0);
+  var o := new C;
+  assert init == f(0);
+}
+
+method M2()
+{
+  var c := new C;
+  c.u := 0;
+  var f := () reads c => c.u;
+  var init := f();
+  c.u := 1;
+  if * {
+    assert f() == init; // should fail
+  } else {
+    assert f() == 1;
+  }
+}
+
+method M3()
+{
+  var c := new C;
+  c.u := 0;
+  var f := () reads c => c.u;
+  assert f() == 0;
+  c.u := 1;
+  assert f() == 1;
+  assert f() == 0; // should fail
+  assert false;    // should fail
+}
+
+method Main() {
+   var x := 2;
+   var getX := () => x;
+   assert getX() == 2;
+   x := 3;
+   assert getX() == 2;  // the value is copied
+}
+
+method Refs() {
+  var a := new int[1];
+  a[0] := 2;
+  var get;
+  if * {
+
+    get := () reads a => a[0];       // OK
+    assert get() == 2;
+
+    a[0] := 3;
+    assert get() == 3;               // OK, the ref is copied, but not the entire array
+
+    a := new int[0];
+    assert get() == 3;               // OK, still 3
+    assert get() == 0 || get() == 2; // fail: is three!
+
+  } else if * {
+    get := () => a[0];               // fail: Not enough read
+  } else {
+    get := () reads {} => a[0];       // fail: Not enough read
+  }
+}
+
+method Fiddling(k : int -> int)
+{
+
+  var mkGet := (arr : array<int>) =>
+               () reads arr requires arr != null requires arr.Length > 0 => arr[0];
+
+  var a := new int[1];
+  var b := new int[1];
+
+  var get := mkGet(a);
+
+  a[0] := 0;
+  b[0] := 10;
+
+  assert get() == a[0];
+
+  b[0] := 20;
+
+  assert get() == a[0];
+}
+
+method HeapSucc0(k : int -> int)
+  requires k.requires(0);
+{
+  var init := k(0);
+  var a := new object;
+  assert k(0) == init;
+}
+
+method HeapSucc1(k : int -> int, c : C)
+  requires k.requires(0);
+  requires c !in k.reads(0);
+  modifies c;
+{
+  var init := k(0);
+  if ( c != null ) {
+    c.u := c.u + 1;
+    assert k(0) == init;
+  }
+}
+
+method HeapSucc2(k : int -> int, c : C)
+  requires k.requires(0);
+  modifies c;
+{
+  var init := k(0);
+  if ( c != null ) {
+    c.u := c.u + 1;
+    if ( c !in k.reads(0) ) {
+      assert k(0) == init;
+    } else {
+      assert k(0) == init; // Fail
+    }
+  }
+}
+
+
diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect
new file mode 100644
index 00000000..a4d10c47
--- /dev/null
+++ b/Test/hofs/Frame.dfy.expect
@@ -0,0 +1,38 @@
+Frame.dfy(23,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Frame.dfy(19,13): anon5_Else

+    (0,0): anon6_Then

+Frame.dfy(37,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Frame.dfy(33,13): anon3_Else

+Frame.dfy(63,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    Frame.dfy(55,13): anon14_Else

+    (0,0): anon15_Then

+    (0,0): anon5

+Frame.dfy(66,19): Error: insufficient reads clause to read array element

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Then

+    (0,0): anon17_Then

+Frame.dfy(68,28): Error: insufficient reads clause to read array element

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Else

+    (0,0): anon18_Then

+Frame.dfy(123,14): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Else

+Frame.dfy(123,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Else

+

+Dafny program verifier finished with 14 verified, 7 errors

diff --git a/Test/hofs/Lambda.dfy b/Test/hofs/Lambda.dfy
new file mode 100644
index 00000000..44adb4ce
--- /dev/null
+++ b/Test/hofs/Lambda.dfy
@@ -0,0 +1,60 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method M<A>() {
+    var f1 : A -> A := x   => x;
+    var f2 : A -> A := (x) => x;
+    var f3 : () -> () := () => ();
+    var tt : () := ();
+    var f4 : (A, A) -> (A, A) := (x, y) => (y, x);
+    var f5 := (x : int) => x;
+
+    var f6 := x requires x != 0 requires x != 1 => x;
+    var f7 := x requires 0 != x requires x != 1 => x;
+    assert f6(2) == f7(2);
+
+    var u := 0;
+    var f8 := () requires u == 0 => true;
+    assert f8();
+    u := 1;
+    assert f8(); // ok, u value is copied at creation of f8
+
+    var f9 := () requires u == 0 => true;
+    assert !f9.requires();
+
+}
+
+datatype List<A> = Cons(A,List<A>) | Nil
+
+method J(xs : List<int>) returns (z : int) {
+    match xs
+        case Cons(y,ys) => z := y;
+        case Nil        => z := 0;
+
+    if {
+        case true => z := z;
+        case true => z := 1;
+    }
+}
+
+function Adder() : (int, int) -> int
+  ensures forall x, y :: Adder().requires(x, y);
+  ensures forall x, y :: (Adder())(x, y) == x + y;
+{
+  (x, y) => x + y
+}
+
+function MkId<A>() : A -> A
+{
+  x => x
+}
+
+
+// storage and references to functions
+method T() {
+   var f := x => x + 1;
+   f := u => if u > 0 then f(u) else u;
+   assert f(1) == 2 && f(0) == 0;
+}
+
diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect
new file mode 100644
index 00000000..a32c27ff
--- /dev/null
+++ b/Test/hofs/Lambda.dfy.expect
@@ -0,0 +1,14 @@
+Lambda.dfy(24,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Lambda.dfy(6,24): anon31_Else

+    Lambda.dfy(7,26): anon32_Else

+    Lambda.dfy(8,27): anon33_Else

+    Lambda.dfy(10,39): anon34_Else

+    Lambda.dfy(11,23): anon35_Else

+    Lambda.dfy(13,15): anon36_Else

+    Lambda.dfy(14,15): anon39_Else

+    Lambda.dfy(18,16): anon42_Else

+    Lambda.dfy(23,16): anon44_Else

+

+Dafny program verifier finished with 7 verified, 1 error

diff --git a/Test/hofs/LambdaParsefail.dfy b/Test/hofs/LambdaParsefail.dfy
new file mode 100644
index 00000000..1d864d73
--- /dev/null
+++ b/Test/hofs/LambdaParsefail.dfy
@@ -0,0 +1,33 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Fails() {
+    var g1 := x.x => x;   // fail
+    var g2 := x() => x;   // fail
+    var g3 := ((x)) => x; // fail
+
+}
+
+method Fail() {
+    var g8 := x : int => x;   // not ok!
+}
+
+function f():() {
+  a.b(x); a.b(x)
+}
+
+method M() {
+  g := a.b(x);
+}
+
+method M() {
+  g := y => a(y);
+}
+
+method M() {
+  g := y => a.b(y);
+}
+
+function f():() {
+  (u => a.b(x); a(x))(); a(x)
+}
diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect
new file mode 100644
index 00000000..b1334b85
--- /dev/null
+++ b/Test/hofs/LambdaParsefail.dfy.expect
@@ -0,0 +1,5 @@
+LambdaParsefail.dfy(5,17): error: Invalid variable binding in lambda.

+LambdaParsefail.dfy(6,16): error: Expected variable binding.

+LambdaParsefail.dfy(7,16): error: Expected variable binding.

+LambdaParsefail.dfy(12,17): error: semi expected

+4 parse errors detected in LambdaParsefail.dfy

diff --git a/Test/hofs/LambdaParsefail2.dfy b/Test/hofs/LambdaParsefail2.dfy
new file mode 100644
index 00000000..148fc03c
--- /dev/null
+++ b/Test/hofs/LambdaParsefail2.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method Fail2() {
+    var g4 := (x, y : A) => (y, x : B); // RHS should fail!
+}
+
diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect
new file mode 100644
index 00000000..8bbf643c
--- /dev/null
+++ b/Test/hofs/LambdaParsefail2.dfy.expect
@@ -0,0 +1,2 @@
+LambdaParsefail2.dfy(6,33): error: Type specification not allowed here, comma separator was expected.

+1 parse errors detected in LambdaParsefail2.dfy

diff --git a/Test/hofs/Map.dfy b/Test/hofs/Map.dfy
new file mode 100644
index 00000000..a55be2be
--- /dev/null
+++ b/Test/hofs/Map.dfy
@@ -0,0 +1,117 @@
+
+datatype List<A> = Nil | Cons(hd: A,tl: List<A>);
+
+function method Map<A,B>(f : A -> B, xs : List<A>) : List<B>
+  requires forall x :: f.requires(x);
+  reads *;
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),Map(f,xs))
+}
+
+function method Id<A>(x : A) : A { x }
+
+method Test() {
+  assert Map(Id, Cons(1,Nil)) == Cons(1,Nil);
+  var inc := x => x + 1;
+  assert Map(inc, Cons(1,Nil)) == Cons(2,Nil);
+  assert Map(x => x + 1, Cons(1,Nil)) == Cons(2,Nil);
+  assert Map((x) requires x > 0 => x + 1, Nil) == Nil;
+}
+
+function CanCall<A,B>(f : A -> B, xs : List<A>) : bool
+  decreases xs;
+  reads *;
+{
+  match xs
+    case Nil => true
+    case Cons(x,xs) => f.requires(x) && CanCall(f, xs)
+}
+
+function method MegaMap<A,B>(f : A -> B, xs : List<A>) : List<B>
+  requires CanCall(f, xs);
+  reads *;
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),MegaMap(f,xs))
+}
+
+method Test2() {
+  assert MegaMap((x) requires x != 0 => 100 / x, Cons(2, Nil)).hd == 50;
+}
+
+function All<A>(p : A -> bool, xs : List<A>) : bool
+  requires forall x :: p.requires(x) /* && p.reads(x) == {} */;
+  reads *;
+  decreases xs;
+{
+  match xs
+    case Nil => true
+    case Cons(x,xs) => p(x) && All(p,xs)
+}
+
+/*
+function UnionMap(i : A -> set<B>, ys : List<A>): set<B>
+  requires forall x :: i.requires(x) && i.reads(x) == {};
+  decreases ys;
+{
+  match ys
+    case Nil => {}
+    case Cons(x,xs) => i(x) + UnionMap(i,xs)
+}
+*/
+
+function method NinjaMap<A,B>(f : A -> B, ys : List<A>) : List<B>
+  requires All(f.requires, ys);
+//  reads UnionMap(f.reads, ys);
+  reads *;
+  decreases ys;
+{
+  match ys
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),NinjaMap(f,xs))
+}
+
+function method Compose(f : B -> C, g : A -> B) : A -> C
+{
+  x requires g.requires(x) && f.requires(g(x))
+    reads    g.reads(x) + f.reads(g(x))
+    => f(g(x))
+}
+
+lemma {:induction 0} MapCompose(f : B -> C, g : A -> B, xs : List<A>)
+  requires All(g.requires, xs);
+  requires All(f.requires, NinjaMap(g,xs));
+  requires All(Compose(f,g).requires, xs);
+
+  decreases xs;
+  ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs);
+{
+  match xs
+    case Nil =>
+    case Cons(x,xs) =>
+      calc {
+            NinjaMap(f,NinjaMap(g,Cons(x,xs)));
+         == NinjaMap(f,Cons(g(x),NinjaMap(g,xs)));
+         == Cons(f(g(x)),NinjaMap(f,NinjaMap(g,xs)));
+         == { MapCompose(f,g,xs); }
+            Cons(f(g(x)),NinjaMap(Compose(f,g),xs));
+         == Cons(Compose(f,g)(x),NinjaMap(Compose(f,g),xs));
+         == NinjaMap(Compose(f,g),Cons(x,xs));
+      }
+}
+
+// auto-mode
+lemma MapCompose2(f : B -> C, g : A -> B, xs : List<A>)
+  requires All(g.requires, xs);
+  requires All(f.requires, NinjaMap(g,xs));
+  requires All(Compose(f,g).requires, xs);
+  decreases xs;
+  ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs);
+{
+}
+
diff --git a/Test/hofs/MutableField.dfy b/Test/hofs/MutableField.dfy
new file mode 100644
index 00000000..fa0a1f50
--- /dev/null
+++ b/Test/hofs/MutableField.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+class C {
+  function method f(x : int) : int { x }
+
+  var g : int -> int;
+
+  method M() modifies this;
+  {
+    f := g; // not ok
+  }
+}
+
diff --git a/Test/hofs/MutableField.dfy.expect b/Test/hofs/MutableField.dfy.expect
new file mode 100644
index 00000000..1ffdc239
--- /dev/null
+++ b/Test/hofs/MutableField.dfy.expect
@@ -0,0 +1,2 @@
+MutableField.dfy(12,4): Error: LHS of assignment must denote a mutable field

+1 resolution/type errors detected in MutableField.dfy

diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
new file mode 100644
index 00000000..17aa828a
--- /dev/null
+++ b/Test/hofs/Naked.dfy
@@ -0,0 +1,51 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Functions {
+  function f(x: nat): nat
+  {
+    if x == 0 then 0 else
+    if var b: bool :| true; b then
+      var h := f;
+      h(x-1)
+    else
+      (f)(x-1)
+  }
+
+  function f1(x: nat): nat { if x == 0 then 0 else f2(x - 1) }
+
+  function f2(x: nat): nat { if x == 0 then 0 else (f1)(x - 1) }
+}
+
+module Requires {
+  function t(x: nat): nat
+  requires !t.requires(x);
+  { x }
+
+  function g(x: nat): nat
+  requires !(g).requires(x);
+  { x }
+
+  function g2(x: int): int { h(x) }
+
+  function h(x: int): int
+    requires !g2.requires(x);
+  { x }
+}
+
+module Reads {
+  function t(x: nat): nat
+  reads t.reads(x);
+  { x }
+
+  function g(x: nat): nat
+  reads (g).reads(x);
+  { x }
+
+  function g2(x: int): int { h(x) }
+
+  function h(x: int): int
+    reads g2.reads(x);
+  { x }
+}
+
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
new file mode 100644
index 00000000..62c035b2
--- /dev/null
+++ b/Test/hofs/Naked.dfy.expect
@@ -0,0 +1,50 @@
+Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Else

+    (0,0): anon9_Then

+Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Else

+    (0,0): anon9_Else

+Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Else

+Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Naked.dfy(29,30): Error: possible violation of function precondition

+Naked.dfy(32,14): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+Naked.dfy(38,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+Naked.dfy(42,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 1 verified, 12 errors

diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy
new file mode 100644
index 00000000..73b08fe2
--- /dev/null
+++ b/Test/hofs/OneShot.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class Ref<A> {
+  var val : A;
+}
+
+method OneShot() {
+  var g : () -> bool;
+  var i : Ref<int>;
+  i := new Ref;
+
+  g := () -> true;
+
+  assert g();
+
+  i.val := i.val + 1; // heap changes
+
+  if * {
+    assert g();         // should fail
+  } else {
+    assert !g();        // should fail
+  }
+}
+
diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect
new file mode 100644
index 00000000..78a9864b
--- /dev/null
+++ b/Test/hofs/OneShot.dfy.expect
@@ -0,0 +1,20 @@
+OneShot.dfy(20,12): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    OneShot.dfy(13,9): anon5_Else

+    (0,0): anon6_Then

+OneShot.dfy(22,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    OneShot.dfy(13,9): anon5_Else

+    (0,0): anon6_Else

+OneShot.dfy(22,13): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    OneShot.dfy(13,9): anon5_Else

+    (0,0): anon6_Else

+

+Dafny program verifier finished with 1 verified, 3 errors

diff --git a/Test/hofs/Quant.dfy b/Test/hofs/Quant.dfy
new file mode 100644
index 00000000..70d15902
--- /dev/null
+++ b/Test/hofs/Quant.dfy
@@ -0,0 +1,132 @@
+
+module QuantReads {
+
+  function All<A>(p : A -> bool) : bool
+    reads set x : A, y : object | y in p.reads(x) :: y;
+    requires forall x : A :: p.requires(x);
+  {
+    forall x : A :: p(x)
+  }
+
+  lemma AllQuant<A>(p : A -> bool)
+    requires All.requires(p);
+    requires All(p);
+    ensures forall x : A :: p(x);
+  {
+  }
+
+}
+
+module Forall {
+
+  function All<A>(p : A -> bool) : bool
+  {
+    forall x :: p.requires(x) && p(x)
+  }
+
+  function CallMe(f : int -> int) : int
+    requires All(f.requires);
+  {
+    f(1) + f(2)
+  }
+
+}
+
+module Quant {
+
+  function All<A>(p : A -> bool) : bool
+    requires forall x : A :: p.requires(x);
+  {
+    forall x : A :: p(x)
+  }
+
+  lemma AllBool(p : bool -> bool)
+    requires forall x : bool :: p.requires(x);
+    requires All(p);
+    ensures p(true) && p(false);
+  {
+  }
+
+  method Boo()
+    requires All(x => x);
+    ensures false;
+  {
+    AllBool(x => x);
+  }
+
+  lemma AllQuant<A>(p : A -> bool)
+    requires All.requires(p);
+    requires All(p);
+    ensures forall x : A :: p(x);
+  {
+  }
+
+  method Boo2()
+    requires All(x => x);
+    ensures false;
+  {
+    assert (x => x)(false);
+  }
+
+
+  method Koo(s : set<int>, t : set<int>)
+    requires All(x => (x in s ==> x in t) && (x in t ==> x in s));
+    ensures All(x => x in s <==> x in t);
+  {
+  }
+
+}
+
+module ReadAll {
+
+  datatype List<A> = Nil | Cons(A,List<A>);
+
+  function All(p : A -> bool, xs : List) : bool
+    reads (set x, y | y in p.reads(x) :: y);
+    requires forall x :: p.reads(x) == {} && p.requires(x);
+    decreases xs;
+  {
+    match xs
+      case Nil => true
+      case Cons(x,xs) => p(x) && All(p,xs)
+  }
+
+  function Div(xs : List<int>) : List<int>
+    requires All(x => x > 0, xs);
+  {
+    match xs
+      case Nil => Nil
+      case Cons(x,xs) => Cons(100 / x,Div(xs))
+  }
+
+}
+
+module Requires {
+
+  method SmallTest(f : int -> int)
+    requires f.requires(0);
+  {
+    print f(0);
+  }
+
+  datatype List<A> = Nil | Cons(hd: A,tl: List<A>);
+
+  function All<A>(p : A -> bool, xs : List<A>) : bool
+    requires forall x :: p.requires(x);
+    decreases xs;
+  {
+    match xs
+      case Nil => true
+      case Cons(x,xs) => p(x) && All(p,xs)
+  }
+
+  function method Map<A,B>(f : A -> B, ys : List<A>) : List<B>
+    requires All(f.requires, ys);
+    decreases ys;
+  {
+    match ys
+      case Nil => Nil
+      case Cons(x,xs) => Cons(f(x),Map(f,xs))
+  }
+
+}
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)
+}
+
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
new file mode 100644
index 00000000..50f74728
--- /dev/null
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -0,0 +1,18 @@
+ReadsReads.dfy(30,5): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+ReadsReads.dfy(35,3): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+ReadsReads.dfy(46,10): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+ReadsReads.dfy(57,5): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 6 verified, 4 errors

diff --git a/Test/hofs/Renaming.dfy b/Test/hofs/Renaming.dfy
new file mode 100644
index 00000000..7a3f69a5
--- /dev/null
+++ b/Test/hofs/Renaming.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function OnId(f : (bool -> bool) -> int) : int
+  reads f.reads(x => x);
+  requires f.requires(y => y);
+{
+  f(z => z)
+}
+
+method Equal() {
+  var id1 : bool -> bool := x => x;
+  var id2                := y => y;
+  assert forall x :: id1(x) == id2(x);
+  assert id1 == id2;
+}
+
+method K<A,B>(P : (A -> A) -> bool)
+{
+  assume P.requires(x => x);
+  assume P(y => y);
+  assert P(z => z);
+  assert (x => y => x) == ((a : A) => (b : B) => a);
+}
+
diff --git a/Test/hofs/Renaming.dfy.expect b/Test/hofs/Renaming.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/hofs/Renaming.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 5 verified, 0 errors

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;
+}
+
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
new file mode 100644
index 00000000..acc01b73
--- /dev/null
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -0,0 +1,14 @@
+ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

+ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

+ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field

+ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)

+ResolveError.dfy(32,12): Error: cannot apply arguments with types int,int to expression with type int -> int

+ResolveError.dfy(33,12): Error: cannot apply arguments with types bool to expression with type int -> int

+ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)

+ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)

+ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)

+ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool)

+ResolveError.dfy(38,22): Error: arguments must have the same type (got set<object> and int)

+ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1)

+ResolveError.dfy(49,9): Error: condition is expected to be of type bool, but is () -> bool

+13 resolution/type errors detected in ResolveError.dfy

diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy
new file mode 100644
index 00000000..4bb58078
--- /dev/null
+++ b/Test/hofs/Simple.dfy
@@ -0,0 +1,90 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function method MkId<A>() : A -> A {
+  x => x
+}
+
+function method IntId() : int -> int {
+  y => y
+}
+
+function method DivZero() : int -> int
+{
+  z => 5 / z  // div by zero
+}
+
+function method DivZeroWithReq() : int -> int
+{
+  (z) requires z != 0 => 5 / z
+}
+
+function method DivZero2() : (int, int) -> int {
+  (x, y) requires y != 0 => x / y
+}
+
+function method DivZero3() : int -> int {
+  z => z / 0   // div by zero
+}
+
+function method Shadow() : int -> real -> real {
+  x => x => x
+}
+
+method Reqs() {
+  var fn := (u) requires u => u;
+  print fn(true);
+  print fn(false);  // precond violation
+}
+
+method Main() {
+  var id := IntId();
+  print id(5);
+  var polyid : int -> int := MkId();
+  print polyid(5);
+  assert id(2) == polyid(2);
+  assert id(3) != 4 && 5 != polyid(6);
+  var divvy := DivZero2();
+  print divvy(2,5);
+  print divvy(2,0); // precond violation
+}
+
+function method succ(x : int) : int
+  requires x > 0;
+{
+  x + 1
+}
+
+method Main2() {
+  var suc := succ;
+  assert suc(3) == succ(3);
+  assert suc(-1) == 0; // precond violation
+}
+
+function method Id<A>(x : A) : A {
+  x
+}
+
+
+method Main3() {
+  var id := Id;
+  assert id(3) == 3;
+  assert forall x :: (Id(id))(x) == (y => y)(x);
+  assert forall x :: (Id(id))(x) == (y => y)(2); // should fail
+}
+
+
+function P(f: A -> B, x : A): B
+  reads (f.reads)(x);
+  requires (f.requires)(x);
+{
+  f(x)
+}
+
+function Q(f: U -> V, x : U): V
+  reads (f.reads)(x);  // would be nice to be able to write P.reads(f,x)
+  requires (f.requires)(x);
+{
+  P(f,x)
+}
+
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
new file mode 100644
index 00000000..76871e06
--- /dev/null
+++ b/Test/hofs/Simple.dfy.expect
@@ -0,0 +1,32 @@
+Simple.dfy(14,10): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+Simple.dfy(27,10): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+Simple.dfy(37,9): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    Simple.dfy(35,15): anon5_Else

+Simple.dfy(49,9): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+Simple.dfy(61,10): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+Simple.dfy(61,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Simple.dfy(73,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Simple.dfy(72,38): anon5_Else

+    Simple.dfy(73,38): anon6_Else

+

+Dafny program verifier finished with 13 verified, 7 errors

diff --git a/Test/hofs/TreeMap.dfy b/Test/hofs/TreeMap.dfy
new file mode 100644
index 00000000..95b07590
--- /dev/null
+++ b/Test/hofs/TreeMap.dfy
@@ -0,0 +1,215 @@
+
+datatype List<A> = Nil | Cons(head: A,tail: List<A>);
+
+datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>);
+
+function Set(xs : List) : set
+  ensures forall x :: x in Set(xs) ==> x < xs;
+{
+  match xs
+    case Nil => {}
+    case Cons(x,xs) => {x} + Set(xs)
+}
+
+function TSet(t0 : Tree) : set
+  ensures forall t :: t in TSet(t0) ==> t < t0;
+{
+  match t0 case Branch(x,ts) => {x} + set t, y | t in Set(ts) && y in TSet(t) :: y
+}
+
+// reads {}
+
+function ReadNothingMap(f : A -> B, xs: List<A>): List<B>
+  requires forall x :: x in Set(xs) ==> f.requires(x);
+  requires forall x :: f.reads(x) == {};
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),ReadNothingMap(f,xs))
+}
+
+function TReadNothingMap(f: A -> B, t0: Tree<A>): Tree<B>
+  requires forall x {:heapQuantifier} :: f.requires(x);
+  requires forall x {:heapQuantifier} :: f.reads(x) == {};
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x), ReadNothingMap(t requires t in Set(ts) => TReadNothingMap(f,t), ts))
+}
+
+function TReadNothingMap2(f: A -> B, t0: Tree<A>): Tree<B>
+  requires forall x :: f.requires(x);
+  requires forall x :: f.reads(x) == {};
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x), ReadNothingMap(t requires t in Set(ts) -> TReadNothingMap2(f,t), ts))
+}
+
+function TReadNothingMap3(f: A -> B, t0: Tree<A>): Tree<B>
+  requires forall x :: f.requires(x);
+  requires forall x :: f.reads(x) == {};
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x), ReadNothingMap(
+    t requires t in Set(ts)
+      requires (forall x :: x in TSet(t) ==> f.requires(x))
+    => TReadNothingMap(f,t), ts))
+}
+
+method TestReadNothingStar() {
+  assert TReadNothingMap(x => x + 1, Branch(1,Nil)).Branch?;
+
+  assert TReadNothingMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil);
+
+  assert TReadNothingMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
+      == Branch(2,Cons(Branch(1,Nil),Nil));
+
+  assert TReadNothingMap2(x -> x + 1, Branch(1,Nil)).Branch?;
+
+  assert TReadNothingMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
+
+  assert TReadNothingMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
+      == Branch(2,Cons(Branch(1,Nil),Nil));
+}
+
+/// reads *
+
+function ReadStarMap(f : A -> B, xs: List<A>): List<B>
+  requires forall x :: x in Set(xs) ==> f.requires(x);
+  reads *;
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),ReadStarMap(f,xs))
+}
+
+function TReadStarMap(f: A -> B, t0: Tree<A>): Tree<B>
+  requires forall x {:heapQuantifier} :: f.requires(x);
+  reads *;
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) => TReadStarMap(f,t), ts))
+}
+
+function TReadStarMap2(f: A -> B, t0: Tree<A>): Tree<B>
+  requires forall x :: f.requires(x);
+  reads *;
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts))
+}
+
+lemma LitTReadStarMap2(f : A -> B, x : A, ts: List<Tree<A>>)
+  requires forall u :: f.requires(u);
+  ensures TReadStarMap2(f, Branch(x,ts)) ==
+    Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts));
+{
+  assert TReadStarMap2(f, Branch(x,ts)).val == f(x);
+  if (ts.Nil?) {
+    assert TReadStarMap2(f, Branch(x,ts)).trees ==
+      ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts);
+  } else {
+    assert TReadStarMap2(f, Branch(x,ts)).trees ==
+      ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts);
+  }
+}
+
+method TestReadStar() {
+  assert TReadStarMap(x => x + 1, Branch(1,Nil)).Branch?;
+
+  assert TReadStarMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil);
+
+  assert ReadStarMap(t reads * requires t in Set(Cons(Branch(0,Nil),Nil)) -> TReadStarMap(x => x + 1,t)
+                    , Cons(Branch(0,Nil),Nil))
+      == Cons(Branch(1,Nil),Nil);
+
+  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).Branch?;
+
+  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).val == 2;
+
+  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).trees == Cons(Branch(1,Nil),Nil);
+
+  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
+      == Branch(2,Cons(Branch(1,Nil),Nil));
+
+  assert TReadStarMap2(x -> x + 1, Branch(1,Nil)).Branch?;
+
+  assert TReadStarMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
+
+  assert TReadStarMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
+      == Branch(2,Cons(Branch(1,Nil),Nil));
+}
+
+/// reads exact
+
+function Map(f : A -> B, xs: List<A>): List<B>
+  requires forall x :: x in Set(xs) ==> f.requires(x);
+  reads set x, y | x in Set(xs) && y in f.reads(x) :: y;
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),Map(f,xs))
+}
+
+function TMap(f : A -> B, t0: Tree<A>): Tree<B>
+  requires forall t :: t in TSet(t0) ==> f.requires(t);
+  reads set x, y | x in TSet(t0) && y in f.reads(x) :: y;
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(
+    f(x),
+    Map( t requires t in Set(ts)
+           reads set x, y | x in TSet(t) && y in f.reads(x) :: y
+           -> TMap(f,t)
+       , ts)
+  )
+}
+
+lemma LitTMap(f : A -> B,x : A, ts: List<Tree<A>>)
+  requires f.requires(x);
+  requires forall t, u :: t in Set(ts) && u in TSet(t) ==> f.requires(u);
+  ensures TMap(f, Branch(x,ts)) ==
+    Branch(f(x),
+      Map( t requires t in Set(ts)
+             reads set x, y | x in TSet(t) && y in f.reads(x) :: y
+             -> TMap(f,t),ts));
+{
+  assert TMap(f, Branch(x,ts)).val == f(x);
+  assert TMap(f, Branch(x,ts)).trees ==
+      Map(t requires t in Set(ts)
+            reads set x, y | x in TSet(t) && y in f.reads(x) :: y
+            -> TMap(f,t),ts);
+}
+
+method Test() {
+  assert TMap(x -> x + 1, Branch(1,Nil)).Branch?;
+
+  assert TMap(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
+
+  calc {
+       TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)));
+    == { LitTMap(x -> x + 1,1, Cons(Branch(0,Nil),Nil)); }
+       Branch((x -> x + 1)(1),Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
+    ==
+       Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
+    ==
+       Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
+    ==
+       Branch(2,Cons(TMap(x -> x + 1,Branch(0,Nil)),Nil));
+    ==
+       Branch(2,Cons(Branch((x -> x + 1)(0),Nil),Nil));
+    ==
+       Branch(2,Cons(Branch(1,Nil),Nil));
+  }
+
+  assert TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
+      == Branch(2,Cons(Branch(1,Nil),Nil));
+}
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
new file mode 100644
index 00000000..3ba4ffd6
--- /dev/null
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -0,0 +1,49 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype List<A> = Nil | Cons(head: A,tail: List<A>);
+
+datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>);
+
+function ListData(xs : List) : set
+  ensures forall x :: x in ListData(xs) ==> x < xs;
+{
+  match xs
+    case Nil => {}
+    case Cons(x,xs) => {x} + ListData(xs)
+}
+
+function TreeData(t0 : Tree) : set
+  ensures forall t :: t in TreeData(t0) ==> t < t0;
+{
+  var Branch(x,ts) := t0;
+  {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
+}
+
+function Pre(f : A -> B, s : set<A>) : bool
+  reads (set x, y | x in s && y in f.reads(x) :: y);
+{
+  forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
+}
+
+function method Map(xs : List<A>, f : A -> B): List<B>
+  reads (set x, y | x in ListData(xs) && y in f.reads(x) :: y);
+  requires Pre(f, ListData(xs));
+  decreases xs;
+{
+  match xs
+    case Nil => Nil
+    case Cons(x,xs) => Cons(f(x),Map(xs,f))
+}
+
+function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
+  reads (set x, y | x in TreeData(t0) && y in f.reads(x) :: y);
+  requires Pre(f, TreeData(t0));
+  decreases t0;
+{
+  var Branch(x,ts) := t0;
+  Branch(f(x),Map(ts, t  requires t in ListData(ts)
+                         requires Pre(f, TreeData(t))
+                      => TMap(t,f)))
+}
+
diff --git a/Test/hofs/TreeMapSimple.dfy.expect b/Test/hofs/TreeMapSimple.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/hofs/TreeMapSimple.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 5 verified, 0 errors

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))
+}
+
diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect
new file mode 100644
index 00000000..5ba4b47b
--- /dev/null
+++ b/Test/hofs/Twice.dfy.expect
@@ -0,0 +1,11 @@
+Twice.dfy(27,22): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Twice.dfy(23,12): anon3_Else

+Twice.dfy(35,32): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+

+Dafny program verifier finished with 4 verified, 2 errors

diff --git a/Test/hofs/Types.dfy b/Test/hofs/Types.dfy
new file mode 100644
index 00000000..9f62763a
--- /dev/null
+++ b/Test/hofs/Types.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method FnEqGhost<A>() {
+  ghost var f : A -> A -> A;
+  ghost var g : A -> (A -> A);
+  ghost var h : (A -> A) -> A;
+  ghost var b1 := f == g; // type checking should be ok
+  ghost var b2 := f == h; // type checking should fail
+
+  ghost var z;
+  ghost var b3 := f == z; // unify in progress
+  ghost var b4 := g == z; // should now be ok
+  ghost var b5 := h == z; // should now fail
+
+  ghost var zz;
+  ghost var b6 := h == zz; // unify in progress
+  ghost var b7 := g == zz; // should fail
+}
+
diff --git a/Test/hofs/Types.dfy.expect b/Test/hofs/Types.dfy.expect
new file mode 100644
index 00000000..11d74db0
--- /dev/null
+++ b/Test/hofs/Types.dfy.expect
@@ -0,0 +1,4 @@
+Types.dfy(9,20): Error: arguments must have the same type (got A -> A -> A and (A -> A) -> A)

+Types.dfy(14,20): Error: arguments must have the same type (got (A -> A) -> A and A -> A -> A)

+Types.dfy(18,20): Error: arguments must have the same type (got A -> A -> A and (A -> A) -> A)

+3 resolution/type errors detected in Types.dfy

diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy
new file mode 100644
index 00000000..dd95cc76
--- /dev/null
+++ b/Test/hofs/WhileLoop.dfy
@@ -0,0 +1,50 @@
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class Ref<A> {
+  var val: A;
+}
+
+method Nice(n: int) {
+  var f : int -> int := x => x;
+  var i := new Ref<int>;
+  i.val := 0;
+  while (i.val < n)
+    invariant forall u :: f.requires(u);
+    invariant forall u :: f.reads(u) == {};
+    invariant forall u :: f(u) == u + i.val;
+  {
+    i.val := i.val + 1;
+    f := x => f(x) + 1;
+  }
+}
+
+
+method OneShot(n: int) {
+  var f : int -> int := x => x;
+  var i := 0;
+  while (i < n)
+    invariant forall u :: f.requires(u);
+    invariant forall u :: f(u) == u + i;
+  {
+    i := i + 1;
+    f := x reads f.reads(x) -> f(x) + 1;
+  }
+}
+
+method HeapQuant(n: int) {
+  var f : int -> int := x => x;
+  var i := new Ref<int>;
+  ghost var r := 0;
+  i.val := 0;
+  while (i.val < n)
+    invariant forall u {:heapQuantifier} :: f.requires(u);
+    invariant forall u {:heapQuantifier} :: f.reads(u) == {};
+    invariant r == i.val;
+    invariant forall u {:heapQuantifier} :: f(u) == u + r;
+  {
+    i.val, r := i.val + 1, r + 1;
+    f := x => f(x) + 1;
+  }
+}
+
diff --git a/Test/hofs/WhileLoop.dfy.expect b/Test/hofs/WhileLoop.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/hofs/WhileLoop.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors