diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 19:20:09 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 19:20:09 -0700 |
| commit | 8c1bc1c2dd2d10303a40673c2bcf0168b16064d1 (patch) | |
| tree | db79830ded1f68c66929c25bc12d4fb6a283be2f | |
| parent | e350f5ede7c33b0c70df077930082b96859feb9d (diff) | |
Dafny: mark code for equality-support determination tentative
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 5592815f..269c8069 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -540,6 +540,7 @@ namespace Microsoft.Dafny { return false;
} else if (ResolvedClass is IndDatatypeDecl) {
var dt = (IndDatatypeDecl)ResolvedClass;
+#if SOON
Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);
if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {
return false;
@@ -552,6 +553,7 @@ namespace Microsoft.Dafny { }
i++;
}
+#endif
return true;
} else if (ResolvedParam != null) {
return ResolvedParam.MustSupportEquality;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 4b67a209..48916478 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1047,6 +1047,7 @@ namespace Microsoft.Dafny { Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+#if SOON
var scc = dependencies.GetSCC(startingPoint);
// First, the simple case: If any parameter of any inductive datatype in the SCC is of a codatatype type, then
// the whole SCC is incapable of providing the equality operation.
@@ -1134,6 +1135,7 @@ namespace Microsoft.Dafny { foreach (var dt in scc) {
dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;
}
+#endif
}
void ResolveAttributes(Attributes attrs, bool twoState) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 18b613b9..cd30fea6 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1329,14 +1329,10 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- EqualityTypes.dfy --------------------
EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters
EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters
-EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
-EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
-EqualityTypes.dfy(63,9): Error: ...(something goes here)
EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
-8 resolution/type errors detected in EqualityTypes.dfy
+4 resolution/type errors detected in EqualityTypes.dfy
-------------------- SplitExpr.dfy --------------------
|