diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 23 | ||||
| -rw-r--r-- | Test/dafny4/Bug129.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny4/Bug129.dfy.expect | 2 |
3 files changed, 32 insertions, 5 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bddf62e2..e47220d7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4171,23 +4171,36 @@ namespace Microsoft.Dafny Contract.Ensures(!Contract.Result<bool>() || dt.DefaultCtor != null);
// Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
+ DatatypeCtor defaultCtor = null;
+ List<TypeParameter> lastTypeParametersUsed = null;
foreach (DatatypeCtor ctor in dt.Ctors) {
- var typeParametersUsed = new List<TypeParameter>();
+ List<TypeParameter> typeParametersUsed = new List<TypeParameter>();
foreach (Formal p in ctor.Formals) {
if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) {
// the argument type (has a component which) is not yet known to be constructable
goto NEXT_OUTER_ITERATION;
}
}
- // this constructor satisfies the requirements, so the datatype is allowed
- dt.DefaultCtor = ctor;
+ // this constructor satisfies the requirements, check to see if it is a better fit than the
+ // one found so far. By "better" it means fewer type arguments. Between the ones with
+ // the same number of the type arguments, pick the one shows first.
+ if (defaultCtor == null || typeParametersUsed.Count < lastTypeParametersUsed.Count) {
+ defaultCtor = ctor;
+ lastTypeParametersUsed = typeParametersUsed;
+ }
+
+ NEXT_OUTER_ITERATION: { }
+ }
+
+ if (defaultCtor != null) {
+ dt.DefaultCtor = defaultCtor;
dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count];
for (int i = 0; i < dt.TypeArgs.Count; i++) {
- dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
+ dt.TypeParametersUsedInConstructionByDefaultCtor[i] = lastTypeParametersUsed.Contains(dt.TypeArgs[i]);
}
return true;
- NEXT_OUTER_ITERATION: { }
}
+
// no constructor satisfied the requirements, so this is an illegal datatype declaration
return false;
}
diff --git a/Test/dafny4/Bug129.dfy b/Test/dafny4/Bug129.dfy new file mode 100644 index 00000000..f6cf0fe8 --- /dev/null +++ b/Test/dafny4/Bug129.dfy @@ -0,0 +1,12 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Maybe<T> = Some(v:T) | None
+datatype B = B(b:Maybe<B>)
+
+datatype List<T> = Nil | Cons(T, List<T>)
+datatype Tree<T> = Nodes(children: List<Tree<T>>)
+
+
+
+
diff --git a/Test/dafny4/Bug129.dfy.expect b/Test/dafny4/Bug129.dfy.expect new file mode 100644 index 00000000..a1c1f7b9 --- /dev/null +++ b/Test/dafny4/Bug129.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 0 verified, 0 errors
|