Beefed up axioms about cardinality and the empty (multi)set, which fixes Issue 17 on dafny.codeplex.com.

Added information that allows multiset members to be unboxed as needed (mimicking what was already done for sets).

1 files changed, 20 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9628f14b..242d6589 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6504,10 +6504,18 @@ namespace Microsoft.Dafny {
       type = type.Normalize();

       if (type is SetType) {

         var t = (SetType)type;

-        // $IsGoodSet(x, V), where V is a value whose type is the same as the element type of the set.

+        // $IsGoodSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.

         var ex = ExemplaryBoxValue(t.Arg);

         if (ex != null) {

-          var p = FunctionCall(tok, "$IsGoodSet", Bpl.Type.Bool, x, ex);

+          var p = FunctionCall(tok, BuiltinFunction.IsGoodSet_Extended, null, x, ex);

+          r = r == null ? p : BplAnd(r, p);

+        }

+      } else  if (type is MultiSetType) {

+        var t = (MultiSetType)type;

+        // $IsGoodMultiSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.

+        var ex = ExemplaryBoxValue(t.Arg);

+        if (ex != null) {

+          var p = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet_Extended, null, x, ex);

           r = r == null ? p : BplAnd(r, p);

         }

       } else if (type.IsDatatype) {

@@ -8559,6 +8567,7 @@ namespace Microsoft.Dafny {
       SetEqual,

       SetSubset,

       SetDisjoint,

+      IsGoodSet_Extended,

 

       MultiSetCard,

       MultiSetEmpty,

@@ -8572,6 +8581,7 @@ namespace Microsoft.Dafny {
       MultiSetFromSet,

       MultiSetFromSeq,      

       IsGoodMultiSet,

+      IsGoodMultiSet_Extended,

 

       SeqLength,

       SeqEmpty,

@@ -8671,6 +8681,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);

+        case BuiltinFunction.IsGoodSet_Extended:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsGoodSet_Extended", Bpl.Type.Bool, args);

 

         case BuiltinFunction.MultiSetCard:

           Contract.Assert(args.Length == 1);

@@ -8722,6 +8736,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);

+        case BuiltinFunction.IsGoodMultiSet_Extended:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsGoodMultiSet_Extended", Bpl.Type.Bool, args);

 

         case BuiltinFunction.SeqLength:

           Contract.Assert(args.Length == 1);