1 files changed, 70 insertions, 0 deletions
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();
+  }
+}
+