Allow "match" expressions anywhere

3 files changed, 121 insertions, 41 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c8386aa..7b52292f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2959,8 +2959,7 @@ namespace Microsoft.Dafny
       }

       if (f.Body != null) {

         var prevErrorCount = ErrorCount;

-        List<IVariable> matchVarContext = new List<IVariable>(f.Formals);

-        ResolveExpression(f.Body, false, f, matchVarContext);

+        ResolveExpression(f.Body, false, f);

         if (!f.IsGhost && prevErrorCount == ErrorCount) {

           CheckIsNonGhost(f.Body);

         }

@@ -5455,16 +5454,6 @@ namespace Microsoft.Dafny
     void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) {

       Contract.Requires(expr != null);

       Contract.Requires(codeContext != null);

-      ResolveExpression(expr, twoState, codeContext, null);

-    }

-

-    /// <summary>

-    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;

-    /// if null, no "match" expression will be allowed.

-    /// </summary>

-    void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext, List<IVariable> matchVarContext) {

-      Contract.Requires(expr != null);

-      Contract.Requires(codeContext != null);

       Contract.Ensures(expr.Type != null);

       if (expr.Type != null) {

         // expression has already been resovled

@@ -5478,7 +5467,7 @@ namespace Microsoft.Dafny
 

       if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

-        ResolveExpression(e.E, twoState, codeContext, matchVarContext);  // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression

+        ResolveExpression(e.E, twoState, codeContext);

         e.ResolvedExpression = e.E;

         e.Type = e.E.Type;

 

@@ -5688,7 +5677,7 @@ namespace Microsoft.Dafny
         if (!twoState) {

           Error(expr, "old expressions are not allowed in this context");

         }

-        ResolveExpression(e.E, twoState, codeContext, null);

+        ResolveExpression(e.E, twoState, codeContext);

         expr.Type = e.E.Type;

 

       } else if (expr is MultiSetFormingExpr) {

@@ -6118,13 +6107,7 @@ namespace Microsoft.Dafny
         }

 

       } else if (expr is MatchExpr) {

-        MatchExpr me = (MatchExpr)expr;

-        if (matchVarContext == null) {

-          Error(me, "'match' expressions are not supported in this context");

-          matchVarContext = new List<IVariable>();

-        } else {

-          Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

-        }

+        var me = (MatchExpr)expr;

         ResolveExpression(me.Source, twoState, codeContext);

         Contract.Assert(me.Source.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

@@ -6135,7 +6118,6 @@ namespace Microsoft.Dafny
           dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);

         }

         Dictionary<string, DatatypeCtor> ctors;

-        IVariable goodMatchVariable = null;

         if (dtd == null) {

           Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);

           ctors = null;

@@ -6144,15 +6126,6 @@ namespace Microsoft.Dafny
           ctors = datatypeCtors[dtd];

           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

 

-          IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;

-          if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {

-            Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");

-          } else if (!matchVarContext.Contains(ie.Var)) {

-            Error(me.Source.tok, "match source expression '{0}' has already been used as a match source expression in this context", ie.Var.Name);

-          } else {

-            goodMatchVariable = ie.Var;

-          }

-

           // build the type-parameter substitution map for this use of the datatype

           for (int i = 0; i < dtd.TypeArgs.Count; i++) {

             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);

@@ -6197,12 +6170,7 @@ namespace Microsoft.Dafny
             }

             i++;

           }

-          List<IVariable> innerMatchVarContext = new List<IVariable>(matchVarContext);

-          if (goodMatchVariable != null) {

-            innerMatchVarContext.Remove(goodMatchVariable);  // this variable is no longer available for matching

-          }

-          innerMatchVarContext.AddRange(mc.Arguments);

-          ResolveExpression(mc.Body, twoState, codeContext, innerMatchVarContext);

+          ResolveExpression(mc.Body, twoState, codeContext);

           Contract.Assert(mc.Body.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(expr.Type, mc.Body.Type)) {

             Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);

@@ -6258,7 +6226,7 @@ namespace Microsoft.Dafny
       int j = 0;

       foreach (Expression arg in dtv.Arguments) {

         Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

-        ResolveExpression(arg, twoState, codeContext, null);

+        ResolveExpression(arg, twoState, codeContext);

         Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

         if (formal != null) {

           Type st = SubstType(formal.Type, subst);

@@ -6752,7 +6720,7 @@ namespace Microsoft.Dafny
         var resolved = ResolvePredicateOrField(e.Tokens[p], r, e.Tokens[p].val);

         if (resolved != null) {

           r = resolved;

-          ResolveExpression(r, twoState, codeContext, null);

+          ResolveExpression(r, twoState, codeContext);

         }

       }

 

@@ -6781,7 +6749,7 @@ namespace Microsoft.Dafny
           r = null;

         } else {

           r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.OpenParen, e.Arguments);

-          ResolveExpression(r, twoState, codeContext, null);

+          ResolveExpression(r, twoState, codeContext);

         }

       } else if (e.Arguments != null) {

         Contract.Assert(p == e.Tokens.Count);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1c5ecf49..5ef39185 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1205,6 +1205,45 @@ Execution trace:
 Dafny program verifier finished with 50 verified, 8 errors

 

 -------------------- Datatypes.dfy --------------------

+Datatypes.dfy(294,10): Error BP5003: A postcondition might not hold on this return path.

+Datatypes.dfy(292,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon14_Else

+    (0,0): anon15_Then

+    (0,0): anon6

+Datatypes.dfy(295,12): Error: missing case in case statement: Appendix

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon14_Else

+    (0,0): anon15_Else

+    (0,0): anon16_Then

+Datatypes.dfy(346,5): Error: missing case in case statement: Cons

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Then

+Datatypes.dfy(346,5): Error: missing case in case statement: Nil

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Datatypes.dfy(353,8): Error: missing case in case statement: Cons

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Then

+Datatypes.dfy(353,8): Error: missing case in case statement: Nil

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Else

+    (0,0): anon12_Then

 Datatypes.dfy(79,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -1236,7 +1275,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Then

 

-Dafny program verifier finished with 40 verified, 6 errors

+Dafny program verifier finished with 44 verified, 12 errors

 

 -------------------- StatementExpressions.dfy --------------------

 StatementExpressions.dfy(52,11): Error: cannot prove termination; try supplying a decreases clause

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index b00d5c21..11646695 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -281,3 +281,76 @@ predicate F(xs: List, vs: map<int,int>)
   case Nil => true

   case Cons(_, tail) => forall vsi :: F(tail, vsi)

 }

+

+// -- match expressions in arbitrary positions --

+

+module MatchExpressionsInArbitraryPositions {

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

+  datatype AList<T> = ANil | ACons(head: T, tail: AList) | Appendix(b: bool)

+

+  method M(xs: AList<int>) returns (y: int)

+    ensures 0 <= y;

+  {

+    if * {

+      y := match xs  // error: missing case Appendix

+           case ANil => 0

+           case ACons(x, _) => x;  // error: might be negative

+    } else {

+      y := 0;

+      ghost var b := forall tl ::

+                       match ACons(8, tl)

+                       case ACons(w, _) => w <= 16;

+      assert b;

+    }

+  }

+

+  function F(xs: List<int>, ys: List<int>): int

+  {

+    match xs

+    case Cons(x, _) =>

+      (match ys

+       case Nil => x

+       case Cons(y, _) => x + y)

+    case Nil =>

+      (match ys

+       case Nil => 0

+       case Cons(y, _) => y)

+  }

+

+  function G(xs: List<int>, ys: List<int>, k: int): int

+  {

+    match xs

+    case Cons(x, _) =>

+      (if k == 0 then 3 else

+        match ys

+        case Nil => x

+        case Cons(y, _) => x + y)

+    case Nil =>

+      (if k == 0 then 3 else

+        match ys

+        case Nil => 3

+        case Cons(y, _) => 3 + y)

+  }

+

+  function H(xs: List<int>, ys: List<int>, k: int): int

+  {

+    if 0 <= k then

+      (if k < 10 then 0 else 3) + (if k < 100 then 2 else 5)

+    else

+      if k < -17 then 10 else

+        (if k < -110 then 0 else 3) + (if k < -200 then 2 else 5)

+  }

+

+  function J(xs: List<int>): int

+  {

+    match xs  // error: missing cases

+  }

+

+  function K(xs: List<int>): int

+  {

+    match xs

+    case Cons(_, ys) =>

+      (match ys)  // error: missing cases

+    case Nil => 0

+  }

+}