Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and parallel statements.

5 files changed, 75 insertions, 6 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 61df448f..ac688143 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -509,6 +509,12 @@ namespace Dafny
       }

       return frall;

     }

+    public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {

+      foreach (var u in set) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

     // Enumerating other collections

     public delegate Dafny.Set<T> ComprehensionDelegate<T>();

     public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4544a01b..70b16578 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -235,7 +235,7 @@ namespace Microsoft.Dafny {
         //   }

         // }

         Indent(indent);

-        wr.Write("public class {0}", DtCtorName(ctor, dt.TypeArgs));

+        wr.Write("public class {0}", DtCtorDeclarationName(ctor, dt.TypeArgs));

         wr.WriteLine(" : Base_{0}{1} {{", dt.CompileName, typeParams);

         int ind = indent + IndentAmount;

 

@@ -249,7 +249,7 @@ namespace Microsoft.Dafny {
         }

 

         Indent(ind);

-        wr.Write("public {0}(", DtCtorName(ctor));

+        wr.Write("public {0}(", DtCtorDeclartionName(ctor));

         WriteFormals("", ctor.Formals);

         wr.WriteLine(") {");

         i = 0;

@@ -318,7 +318,7 @@ namespace Microsoft.Dafny {
     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

 

-      // public struct Dt<T> {

+      // public struct Dt<T> : IDatatype{

       //   Base_Dt<T> d;

       //   public Base_Dt<T> _D {

       //     get {

@@ -445,7 +445,25 @@ namespace Microsoft.Dafny {
         Indent(ind);

         wr.WriteLine("public bool is_{0} {{ get {{ return _D is {1}_{0}{2}; }} }}", ctor.CompileName, dt.CompileName, DtT_TypeArgs);

       }

-

+      if (dt.HasFinitePossibleValues) {

+        Indent(ind);

+        wr.WriteLine("public static System.Collections.Generic.IEnumerable<@{0}> AllSingletonConstructors {{", DtT);

+        Indent(ind + IndentAmount);

+        wr.WriteLine("get {");

+        foreach (var ctr in dt.Ctors) {

+          if (ctr.Formals.Count == 0) {

+            Indent(ind + IndentAmount + IndentAmount);

+            wr.WriteLine("yield return new @{0}(new {2}_{1}());", DtT, ctr.CompileName, dt.CompileName);

+          }

+        }

+        Indent(ind + IndentAmount + IndentAmount);

+        wr.WriteLine("yield break;");

+        Indent(ind + IndentAmount);

+        wr.WriteLine("}");

+        Indent(ind);

+        wr.WriteLine("}");

+      }

+  

       // destructors

       foreach (var ctor in dt.Ctors) {

         foreach (var arg in ctor.Formals) {

@@ -484,11 +502,20 @@ namespace Microsoft.Dafny {
       return formal.HasName ? formal.CompileName : "_a" + i;

     }

 

+    string DtName(DatatypeDecl decl) {

+      return decl.Module.IsDefaultModule ? decl.CompileName : decl.FullCompileName;

+    }

     string DtCtorName(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      return cce.NonNull(ctor.EnclosingDatatype).CompileName + "_" + ctor.CompileName;

+      return DtName(ctor.EnclosingDatatype) + "_" + ctor.CompileName;

+    }

+    string DtCtorDeclartionName(DatatypeCtor ctor) {

+      Contract.Requires(ctor != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+

+      return ctor.EnclosingDatatype.CompileName + "_" + ctor.CompileName;

     }

 

     string DtCtorName(DatatypeCtor ctor, List<TypeParameter> typeParams) {

@@ -501,6 +528,16 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

+    string DtCtorDeclarationName(DatatypeCtor ctor, List<TypeParameter> typeParams) {

+      Contract.Requires(ctor != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+

+      var s = DtCtorDeclartionName(ctor);

+      if (typeParams != null && typeParams.Count != 0) {

+        s += "<" + TypeParameters(typeParams) + ">";

+      }

+      return s;

+    }

 

     string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs) {

       Contract.Requires(ctor != null);

@@ -1138,6 +1175,9 @@ namespace Microsoft.Dafny {
             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").UniqueElements) { ");

+          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

+            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

@@ -1712,7 +1752,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

         var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs));

 

-        wr.Write("new {0}{1}(", dtv.DatatypeName, typeParams);

+        wr.Write("new {0}{1}(", DtName(dtv.Ctor.EnclosingDatatype), typeParams);

         if (!dtv.IsCoCall) {

           // For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:

           //   new Dt_Cons<T>( args )

@@ -2025,6 +2065,11 @@ namespace Microsoft.Dafny {
             wr.Write("Dafny.Helpers.QuantSeq(");

             TrExpr(b.Seq);

             wr.Write(", ");

+          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

+            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantDatatype(");

+

+            wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

@@ -2087,6 +2132,9 @@ namespace Microsoft.Dafny {
             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").Elements) { ");

+          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

+            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ae7e1a4c..4a211aee 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1038,6 +1038,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(1 <= ctors.Count);

       Ctors = ctors;

     }

+    public bool HasFinitePossibleValues {

+      get {

+        return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0));

+      }

+    }

   }

 

   public class IndDatatypeDecl : DatatypeDecl

@@ -3506,6 +3511,11 @@ namespace Microsoft.Dafny {
     public class BoolBoundedPool : BoundedPool

     {

     }

+    public class DatatypeBoundedPool : BoundedPool

+    {

+      public readonly DatatypeDecl Decl;

+      public DatatypeBoundedPool(DatatypeDecl d) { Decl = d; }

+    }

 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver

     // invariant Bounds == null || Bounds.Count == BoundVars.Count;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 74ddb08b..8c14cb0c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4946,6 +4946,8 @@ namespace Microsoft.Dafny
         if (bv.Type is BoolType) {

           // easy

           bounds.Add(new QuantifierExpr.BoolBoundedPool());

+        } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {

+          bounds.Add(new QuantifierExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

         } else {

           // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index d53fb6a5..ca1fcfb7 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.dfy
@@ -11,6 +11,7 @@ method M()
 

 function method Id(x: int): int { x }  // for triggering

 

+datatype D = A | B;

 // The following mainly test that set comprehensions can be compiled, but one would

 // have to run the resulting program to check that the compiler is doing the right thing.

 method Main()

@@ -18,6 +19,8 @@ method Main()
   var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;

   PrintSet(q);

   q := set b: bool | true :: if b then 3 else 7;

+  var d := set b:D | true;

+  var test := forall d:D :: d == A || d == B;

   PrintSet(q);

   var m := set k | k in q :: 2*k;

   PrintSet(m);