summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
committerGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
commit0d003990dd503ceb9cc56e7fb590981e752b5cfa (patch)
treedf346ae8ea4724f406a1b030ecf4b7df6a538c8d /Source/Dafny
parent2be514ca20e1478b6df02ef2b4c2725c319ac934 (diff)
Fix issue 129. When looking for a constructor for which Dafny knows how to
instantiate all it arguments, don't stop as soon as one instantiable constructor is found. Instead, figure out all instantiable constructors and then pick the best among these. A simple and reasonable "best" is an instantiable constructor that requires a minimal number of already constructed type arguments, and to break ties among these, pick the first one listed.
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Resolver.cs23
1 files changed, 18 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;
}