Merge

4 files changed, 61 insertions, 7 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 8d1485f7..460c8a07 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3350,6 +3350,13 @@ namespace Microsoft.Dafny
           if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) {

             return false;

           }

+        } else if (t is MultiSetType) {

+          if (!UnifyTypes(iProxy.Arg, Type.Int)) {

+            return false;

+          }

+          if (!UnifyTypes(iProxy.Domain, ((MultiSetType)t).Arg)) {

+            return false;

+          }

         } else {

           return false;

         }

@@ -5114,6 +5121,17 @@ namespace Microsoft.Dafny
             Error(e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);

           }

           expr.Type = e.Seq.Type;

+        } else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) {

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

+          if (!UnifyTypes(e.Index.Type, elementType)) {

+            Error(e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);

+          }

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

+          if (!UnifyTypes(e.Value.Type, Type.Int)) {

+            Error(e.Value, "multiset update requires integer value (got {0})", e.Value.Type);

+          }

+          expr.Type = e.Seq.Type;

+

         } else {

           Error(expr, "update requires a sequence or map (got {0})", e.Seq.Type);

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a988db16..68bd9795 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2968,6 +2968,8 @@ namespace Microsoft.Dafny {
           Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);

           inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type));

           builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv));

+        } else if (e.Seq.Type is MultiSetType) {

+          // cool

           

         } else {

           if (e.E0 != null) {

@@ -3019,12 +3021,16 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Seq, options, locals, builder, etran);

         Bpl.Expr seq = etran.TrExpr(e.Seq);

         Bpl.Expr index = etran.TrExpr(e.Index);

+        Bpl.Expr value = etran.TrExpr(e.Value);

         CheckWellformed(e.Index, options, locals, builder, etran);

         if (e.Seq.Type is SeqType) {

           builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv));

+        } else if (e.Seq.Type is MapType) {          

+          // updates to maps are always valid if the values are well formed

+        } else if (e.Seq.Type is MultiSetType) {

+          builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), value), "new number of occurrences might be negative", options.AssertKv));

         } else {

-          Contract.Assert(e.Seq.Type is MapType);

-          // updates add to maps, so are always valid if the values are well formed.

+          Contract.Assert(false);

         }

         CheckWellformed(e.Value, options, locals, builder, etran);

       } else if (expr is FunctionCallExpr) {

@@ -7519,6 +7525,9 @@ namespace Microsoft.Dafny {
           } else if (e.Seq.Type is MapType) {

             domainType = ((MapType)e.Seq.Type).Domain;

             elmtType = ((MapType)e.Seq.Type).Range;

+          } else if (e.Seq.Type is MultiSetType) {

+            domainType = ((MultiSetType)e.Seq.Type).Arg;

+            elmtType = Type.Int;

           } else { Contract.Assert(false); }

           Bpl.Type elType = translator.TrType(elmtType);

           Bpl.Type dType = translator.TrType(domainType);

@@ -7535,8 +7544,10 @@ namespace Microsoft.Dafny {
             } else if (e.Seq.Type is MapType) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);

               x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));

+            } else if (e.Seq.Type is MultiSetType) {

+              x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType));

             } else { Contract.Assert(false); x = null; }

-            if (!ModeledAsBoxType(elmtType)) {

+            if (!ModeledAsBoxType(elmtType) && !(e.Seq.Type is MultiSetType)) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);

             }

             return x;

@@ -7562,13 +7573,20 @@ namespace Microsoft.Dafny {
             Bpl.Expr index = TrExpr(e.Index);

             Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);

             return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);

-          } else {

-            Contract.Assert(e.Seq.Type is MapType);

+          } else if (e.Seq.Type is MapType) {

             MapType mt = (MapType)e.Seq.Type;

             Bpl.Type maptype = predef.MapType(expr.tok, predef.BoxType, predef.BoxType);

             Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain);

             Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range);

             return translator.FunctionCall(expr.tok, "Map#Build", maptype, seq, index, val);

+          } else if (e.Seq.Type is MultiSetType) {

+            Type elmtType = cce.NonNull((MultiSetType)e.Seq.Type).Arg;

+            Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType);

+            Bpl.Expr val = TrExpr(e.Value);

+            return Bpl.Expr.StoreTok(expr.tok, seq, index, val);

+          } else {

+            Contract.Assert(false);

+            throw new cce.UnreachableException();

           }

         } else if (expr is MultiSelectExpr) {

           MultiSelectExpr e = (MultiSelectExpr)expr;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2e1bd93c..72c142ac 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1689,8 +1689,13 @@ MultiSets.dfy(163,3): Error BP5003: A postcondition might not hold on this retur
 MultiSets.dfy(162,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+MultiSets.dfy(176,11): Error: new number of occurrences might be negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

 

-Dafny program verifier finished with 38 verified, 2 errors

+Dafny program verifier finished with 39 verified, 3 errors

 

 -------------------- PredExpr.dfy --------------------

 PredExpr.dfy(4,12): Error: condition in assert expression might not hold

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index 22b93442..a3a28222 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -161,5 +161,18 @@ class BoxTests<G> {
     requires forall x :: x in a ==> x in b;

     ensures a <= b;  // error: this property does not hold for multisets

   {

-  }

+  }  

 }

+

+// ---------- indexing and updates ----------

+method test12(a: nat, b: nat, c: int)

+{

+  var m0, m1, m2: multiset<bool>;

+  m0 := multiset{false, true, true};

+  m1 := multiset{true}[false := a];

+  m2 := multiset{}[false := b];

+  assert (m0 + m1 + m2)[true] == 3;

+  assert (m1 * m2)[false] == if a <= b then a else b;

+  m2 := m2[true := c]; // error: c might be negative

+}

+