From 149540a251282e2b0ed0a4be940d1d91d2908627 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 17 Jul 2012 18:27:03 -0700 Subject: Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and parallel statements. --- Binaries/DafnyRuntime.cs | 6 +++++ Source/Dafny/Compiler.cs | 60 +++++++++++++++++++++++++++++++++++++----- Source/Dafny/DafnyAst.cs | 10 +++++++ Source/Dafny/Resolver.cs | 2 ++ Test/dafny0/Comprehensions.dfy | 3 +++ 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(IEnumerable set, bool frall, System.Predicate pred) { + foreach (var u in set) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } // Enumerating other collections public delegate Dafny.Set ComprehensionDelegate(); public delegate Dafny.Map MapComprehensionDelegate(); 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 { + // public struct Dt : IDatatype{ // Base_Dt d; // public Base_Dt _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() != 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() != null); + + return ctor.EnclosingDatatype.CompileName + "_" + ctor.CompileName; } string DtCtorName(DatatypeCtor ctor, List typeParams) { @@ -501,6 +528,16 @@ namespace Microsoft.Dafny { } return s; } + string DtCtorDeclarationName(DatatypeCtor ctor, List typeParams) { + Contract.Requires(ctor != null); + Contract.Ensures(Contract.Result() != null); + + var s = DtCtorDeclartionName(ctor); + if (typeParams != null && typeParams.Count != 0) { + s += "<" + TypeParameters(typeParams) + ">"; + } + return s; + } string DtCtorName(DatatypeCtor ctor, List 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( 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 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); -- cgit v1.2.3