Allow left-hand sides of a let expression to be patterns (like in the case of a match expression).

Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator.
Fixed compilation of match expressions, to allow them anywhere.

2 files changed, 110 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 472932c5..7da30e96 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2289,8 +2289,32 @@ LetExpr.dfy(104,21): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon11_Then

+LetExpr.dfy(248,19): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+LetExpr.dfy(253,24): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+LetExpr.dfy(282,14): Error: RHS is not certain to look like the pattern 'Agnes'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+LetExpr.dfy(299,42): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+LetExpr.dfy(301,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

 

-Dafny program verifier finished with 28 verified, 2 errors

+Dafny program verifier finished with 38 verified, 8 errors

 

 Dafny program verifier finished with 0 verified, 0 errors

 

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index 3947737b..77bb4fad 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -216,3 +216,88 @@ class TrickySubstitution {
     s := old(var y :| y == w; y);

   }

 }

+

+datatype List<T> = Nil | Cons(head: T, tail: List)

+

+method Q(list: List<int>, anotherList: List<int>)

+  requires list != Nil;

+{

+  var x :=

+    var Cons(h, t) := list;

+    Cons(h, t);

+  var y := match anotherList

+    case Nil => (match anotherList case Nil => 5)

+    case Cons(h, t) => h;

+  assert list == x;

+  assert anotherList.Cons? ==> y == anotherList.head;

+  assert anotherList.Nil? ==> y == 5;

+}

+

+// ------------- pattern LHSs ---------------

+

+datatype Tuple<T,U> = Pair(0: T, 1: U)

+

+function method Together(x: int, y: bool): Tuple<int, bool>

+{

+  Pair(x, y)

+}

+

+method LikeTogether() returns (z: int)

+{

+  if * {

+    z := var Pair(xx: nat, yy) := Together(-10, true); xx + 3;  // error: int-to-nat failure

+    assert 0 <= z;  // follows from the bogus type of xx

+  } else if * {

+    var t: nat := -30;  // error: int-to-nat failure in assignment statement

+  } else {

+    z := var t: nat := -30; t;  // error: int-to-nat failure in let expression

+  }

+}

+

+method Mountain() returns (z: int, t: nat)

+{

+  z := var Pair(xx: nat, yy) := Together(10, true); xx + 3;

+  assert 0 <= z;

+}

+

+function method Rainbow<X>(tup: Tuple<X, int>): int

+  ensures 0 <= Rainbow(tup);

+{

+  var Pair(left, right) := tup; right*right

+}

+

+datatype Friend = Agnes(int) | Agatha(int) | Jermaine(int) | Jack(int)

+

+function Fr(x: int): Friend

+{

+  if x < 10 then Jermaine(x) else Agnes(x)

+}

+

+method Friendly(n: nat) returns (ghost c: int)

+  ensures c == n;

+{

+  if n < 3 {

+    c := var Jermaine(y) := Fr(n); y;

+  } else {

+    c := var Agnes(y) := Fr(n); y;  // error: Fr might return something other than an Agnes

+  }

+}

+

+function method F_good(d: Tuple<

+                             Tuple<bool, int>,

+                             Tuple< Tuple<int,int>, Tuple<bool,bool> >>): int

+  requires 0 <= d.1.0.1 < 100;

+{

+  var p, Pair(Pair(b0, x), Pair(Pair(y0, y1: nat), Pair(b1, b2))), q: int := d.0, d, d.1.0.1;

+  assert q < 200;

+  p.1 + if b0 then x + y0 else x + y1

+}

+function method F_bad(d: Tuple<

+                            Tuple<bool, int>,

+                            Tuple< Tuple<int,int>, Tuple<bool,bool> >>): int

+{

+  var p, Pair(Pair(b0, x), Pair(Pair(y0, y1: nat), Pair(b1, b2))), q: int  // error: int-to-nat failure

+   := d.0, d, d.1.0.1;

+  assert q < 200;  // error: assertion failure

+  p.1 + if b0 then x + y0 else x + y1

+}