Compile lambda functions and apply expressions, and change let expr compilation

1 files changed, 11 insertions, 3 deletions

diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy
index 4bb58078..c27fa82c 100644
--- a/Test/hofs/Simple.dfy
+++ b/Test/hofs/Simple.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function method MkId<A>() : A -> A {
@@ -81,10 +81,18 @@ function P(f: A -> B, x : A): B
   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);
+  reads P.reads(f,x);
+  requires f.requires(x);  // would be nice to be able to write P.requires(f,x)
 {
   P(f,x)
 }
 
+function QQ(f: U -> V, x : U): V
+  reads ((() => ((()=>f)()).reads)())((()=>x)());
+  requires ((() => ((()=>f)()).requires)())((()=>x)());
+{
+  ((() => P)())((()=>f)(),(()=>x)())
+}
+