diff options
Diffstat (limited to 'Dafny')
-rw-r--r-- | Dafny/Compiler.cs | 60 | ||||
-rw-r--r-- | Dafny/DafnyAst.cs | 10 | ||||
-rw-r--r-- | Dafny/Resolver.cs | 2 |
3 files changed, 66 insertions, 6 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 4544a01b..70b16578 100644 --- a/Dafny/Compiler.cs +++ b/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/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index ae7e1a4c..4a211aee 100644 --- a/Dafny/DafnyAst.cs +++ b/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/Dafny/Resolver.cs b/Dafny/Resolver.cs index 74ddb08b..8c14cb0c 100644 --- a/Dafny/Resolver.cs +++ b/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;
|