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

29 files changed, 206 insertions, 83 deletions

diff --git a/Test/hofs/Apply.dfy b/Test/hofs/Apply.dfy
index bdd102c2..28486398 100644
--- a/Test/hofs/Apply.dfy
+++ b/Test/hofs/Apply.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
index 91d7e384..2b892b35 100644
--- a/Test/hofs/Classes.dfy
+++ b/Test/hofs/Classes.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/Compilation.dfy b/Test/hofs/Compilation.dfy
new file mode 100644
index 00000000..c3132db2
--- /dev/null
+++ b/Test/hofs/Compilation.dfy
@@ -0,0 +1,48 @@
+
+class Ref<A> {
+  var val : A;
+}
+
+method Main() {
+  // simple
+  print "1 = ", (x => x)(1), "\n";
+  print "3 = ", (x => y => x + y)(1)(2), "\n";
+  print "3 = ", ((x,y) => y + x)(1,2), "\n";
+  print "0 = ", (() => 0)(), "\n";
+
+  // local variable
+  var y := 1;
+  var f := x => x + y;
+  print "3 = ", f(2), "\n";
+  print "4 = ", f(3), "\n";
+  y := 2;
+  print "3 = ", f(2), "\n";
+  print "4 = ", f(3), "\n";
+
+  // reference
+  var z := new Ref<int>;
+  z.val := 1;
+  f := x reads z requires z != null => x + z.val;
+  print "3 = ", f(2), "\n";
+  print "4 = ", f(3), "\n";
+  z.val := 2;
+  print "4 = ", f(2), "\n";
+  print "5 = ", f(3), "\n";
+
+  // loop
+  f := x => x;
+  y := 10;
+  while (y > 0)
+    invariant forall x :: f.requires(x);
+    invariant forall x :: f.reads(x) == {};
+  {
+    f := x => f(x+y);
+    y := y - 1;
+  }
+  print "55 = ", f(0), "\n";
+
+  // substitution test
+  print "0 = ", (x => var y:=x;y)(0), "\n";
+  print "1 = ", (y => (x => var y:=x;y))(0)(1), "\n";
+}
+
diff --git a/Test/hofs/Compilation.dfy.expect b/Test/hofs/Compilation.dfy.expect
new file mode 100644
index 00000000..0c6452d2
--- /dev/null
+++ b/Test/hofs/Compilation.dfy.expect
@@ -0,0 +1,3 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Compiled assembly into Compilation.exe

diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy
index c31b68da..be2672f5 100644
--- a/Test/hofs/Examples.dfy
+++ b/Test/hofs/Examples.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function Apply(f: A -> B, x: A): B
diff --git a/Test/hofs/Examples.dfy.expect b/Test/hofs/Examples.dfy.expect
index 76f19e0d..99fc5d0f 100644
--- a/Test/hofs/Examples.dfy.expect
+++ b/Test/hofs/Examples.dfy.expect
@@ -1,2 +1,3 @@
 

 Dafny program verifier finished with 7 verified, 0 errors

+Compiled assembly into Examples.dll

diff --git a/Test/hofs/Field.dfy b/Test/hofs/Field.dfy
index 6d3412d7..7d3f571d 100644
--- a/Test/hofs/Field.dfy
+++ b/Test/hofs/Field.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // calling fields should not make a resolution error:
diff --git a/Test/hofs/FnRef.dfy b/Test/hofs/FnRef.dfy
index fb8136b7..5f084bd4 100644
--- a/Test/hofs/FnRef.dfy
+++ b/Test/hofs/FnRef.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect
index 5185c21c..016ee494 100644
--- a/Test/hofs/FnRef.dfy.expect
+++ b/Test/hofs/FnRef.dfy.expect
@@ -18,10 +18,5 @@ 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

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/hofs/Frame.dfy b/Test/hofs/Frame.dfy
index 891435ba..6c4c12ad 100644
--- a/Test/hofs/Frame.dfy
+++ b/Test/hofs/Frame.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/Lambda.dfy b/Test/hofs/Lambda.dfy
index 44adb4ce..eae83095 100644
--- a/Test/hofs/Lambda.dfy
+++ b/Test/hofs/Lambda.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/LambdaParsefail.dfy b/Test/hofs/LambdaParsefail.dfy
index 1d864d73..a9da4c5e 100644
--- a/Test/hofs/LambdaParsefail.dfy
+++ b/Test/hofs/LambdaParsefail.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Fails() {
diff --git a/Test/hofs/LambdaParsefail2.dfy b/Test/hofs/LambdaParsefail2.dfy
index 148fc03c..ead3b9ec 100644
--- a/Test/hofs/LambdaParsefail2.dfy
+++ b/Test/hofs/LambdaParsefail2.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/MutableField.dfy b/Test/hofs/MutableField.dfy
index fa0a1f50..1783fe5c 100644
--- a/Test/hofs/MutableField.dfy
+++ b/Test/hofs/MutableField.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
index 17aa828a..fa99377f 100644
--- a/Test/hofs/Naked.dfy
+++ b/Test/hofs/Naked.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module Functions {
diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy
index 73b08fe2..286be898 100644
--- a/Test/hofs/OneShot.dfy
+++ b/Test/hofs/OneShot.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Ref<A> {
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index bc80713d..47f7f575 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -1,59 +1,103 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function MyReadsOk(f : A -> B, a : A) : set<object>
-  reads f.reads(a);
-{
-  f.reads(a)
-}
+module ReadsRequiresReads {
+  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 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 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 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 MyReadsBad(f : A -> B, a : A) : set<object>
+  {
+    f.reads(a)
+  }
 
-function MyReadsBad2(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 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 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 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)
+  function MyRequiresBad(f : A -> B, a : A) : bool
+  {
+    f.requires(a)
+  }
 }
 
+module WhatWeKnowAboutReads {
+  function ReadsNothing():(){()}
+
+  lemma IndeedNothing() {
+    assert ReadsNothing.reads() == {};
+  }
+
+  method NothingHere() {
+    assert (() => ()).reads() == {};
+  }
+
+  class S {
+    var s : S;
+  }
+
+  function ReadsSomething(s : S):()
+    reads s;
+  {()}
+
+  method MaybeSomething() {
+    var s  := new S;
+    var s' := new S;
+           if * { assert s in ReadsSomething.reads(s) || ReadsSomething.reads(s) == {};
+    } else if * { assert s in ReadsSomething.reads(s);
+    } else if * { assert ReadsSomething.reads(s) == {};
+    } else if * { assert s' !in ReadsSomething.reads(s);
+    } else if * { assert s' in ReadsSomething.reads(s);
+    }
+  }
+
+  method SomethingHere() {
+    var s  := new S;
+    var s' := new S;
+    var f := (u) reads u => ();
+           if * { assert s in f.reads(s) || f.reads(s) == {};
+    } else if * { assert s in f.reads(s);
+    } else if * { assert f.reads(s) == {};
+    } else if * { assert s' !in f.reads(s);
+    } else if * { assert s' in f.reads(s);
+    }
+  }
+}
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index 50f74728..e83e017c 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -1,18 +1,39 @@
-ReadsReads.dfy(30,5): Error: insufficient reads clause to invoke function

+ReadsReads.dfy(31,7): 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

+ReadsReads.dfy(36,5): 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

+ReadsReads.dfy(47,12): 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

+ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

+ReadsReads.dfy(66,33): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+ReadsReads.dfy(86,50): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Then

+ReadsReads.dfy(88,29): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon18_Then

+ReadsReads.dfy(98,37): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ReadsReads.dfy(95,16): anon15_Else

+    (0,0): anon19_Then

+ReadsReads.dfy(100,29): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ReadsReads.dfy(95,16): anon15_Else

+    (0,0): anon21_Then

 

-Dafny program verifier finished with 6 verified, 4 errors

+Dafny program verifier finished with 13 verified, 9 errors

diff --git a/Test/hofs/Renaming.dfy b/Test/hofs/Renaming.dfy
index 7a3f69a5..8a2dc03a 100644
--- a/Test/hofs/Renaming.dfy
+++ b/Test/hofs/Renaming.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function OnId(f : (bool -> bool) -> int) : int
@@ -16,9 +16,9 @@ method Equal() {
 }
 
 method K<A,B>(P : (A -> A) -> bool)
+  requires P.requires(x => x);
+  requires P(y => y);
 {
-  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
index 790f6509..54fc4d53 100644
--- a/Test/hofs/Renaming.dfy.expect
+++ b/Test/hofs/Renaming.dfy.expect
@@ -1,2 +1,3 @@
 

 Dafny program verifier finished with 5 verified, 0 errors

+Compiled assembly into Renaming.dll

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 7df4bbb3..fa5ffb0c 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
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)())
+}
+
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 76871e06..55fe50e0 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -29,4 +29,4 @@ Execution trace:
     Simple.dfy(72,38): anon5_Else

     Simple.dfy(73,38): anon6_Else

 

-Dafny program verifier finished with 13 verified, 7 errors

+Dafny program verifier finished with 14 verified, 7 errors

diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index 3ba4ffd6..e717b096 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype List<A> = Nil | Cons(head: A,tail: List<A>);
@@ -27,7 +27,7 @@ function Pre(f : A -> B, s : set<A>) : bool
 }
 
 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);
+  reads Pre.reads(f, ListData(xs));
   requires Pre(f, ListData(xs));
   decreases xs;
 {
@@ -37,7 +37,7 @@ function method Map(xs : List<A>, f : A -> B): List<B>
 }
 
 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);
+  reads Pre.reads(f, TreeData(t0));
   requires Pre(f, TreeData(t0));
   decreases t0;
 {
diff --git a/Test/hofs/TreeMapSimple.dfy.expect b/Test/hofs/TreeMapSimple.dfy.expect
index 790f6509..f523ef5d 100644
--- a/Test/hofs/TreeMapSimple.dfy.expect
+++ b/Test/hofs/TreeMapSimple.dfy.expect
@@ -1,2 +1,3 @@
 

 Dafny program verifier finished with 5 verified, 0 errors

+Compiled assembly into TreeMapSimple.dll

diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy
index 2178db9f..add7e83c 100644
--- a/Test/hofs/Twice.dfy
+++ b/Test/hofs/Twice.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function method Twice(f : A -> A): A -> A
diff --git a/Test/hofs/Types.dfy b/Test/hofs/Types.dfy
index 9f62763a..e3813bcb 100644
--- a/Test/hofs/Types.dfy
+++ b/Test/hofs/Types.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method FnEqGhost<A>() {
diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy
index dd95cc76..f79562e9 100644
--- a/Test/hofs/WhileLoop.dfy
+++ b/Test/hofs/WhileLoop.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Ref<A> {
diff --git a/Test/hofs/WhileLoop.dfy.expect b/Test/hofs/WhileLoop.dfy.expect
index 4ef2de53..7984cc3b 100644
--- a/Test/hofs/WhileLoop.dfy.expect
+++ b/Test/hofs/WhileLoop.dfy.expect
@@ -1,2 +1,3 @@
 

 Dafny program verifier finished with 6 verified, 0 errors

+Compiled assembly into WhileLoop.dll