diff options
| -rw-r--r-- | Dafny/DafnyAst.cs | 24 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 98 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 11 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 89 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 1 |
6 files changed, 214 insertions, 11 deletions
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index a9e34dca..5592815f 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -540,14 +540,17 @@ namespace Microsoft.Dafny { return false;
} else if (ResolvedClass is IndDatatypeDecl) {
var dt = (IndDatatypeDecl)ResolvedClass;
- // TODO
- // For now, say 'no' if some constructor takes a parameter that is a codatatype. This is BOGUS.
- foreach (var ctor in dt.Ctors) {
- foreach (var arg in ctor.Formals) {
- if (arg.Type.IsCoDatatype) {
- return false;
- }
+ Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);
+ if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {
+ return false;
+ }
+ Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count);
+ var i = 0;
+ foreach (var tp in dt.TypeArgs) {
+ if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) {
+ return false;
}
+ i++;
}
return true;
} else if (ResolvedParam != null) {
@@ -769,6 +772,8 @@ namespace Microsoft.Dafny { get { return EqualitySupport != EqualitySupportValue.Unspecified; }
}
+ public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl
+
public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)
: base(tok, name, null) {
Contract.Requires(tok != null);
@@ -935,7 +940,10 @@ namespace Microsoft.Dafny { public class IndDatatypeDecl : DatatypeDecl
{
public DatatypeCtor DefaultCtor; // set during resolution
- public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as
+ public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as the number of type arguments
+
+ public enum ES { NotYetComputed, Never, ConsultTypeArguments }
+ public ES EqualitySupport = ES.NotYetComputed;
public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,
[Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 29aa3bd7..4b67a209 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -399,15 +399,16 @@ namespace Microsoft.Dafny { allTypeParameters.PopMarker();
}
- // Perform the stratosphere check on inductive datatypes
+ // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
// do the following check once per SCC, so call it on each SCC representative
SccStratosphereCheck(dtd, datatypeDependencies);
+ DetermineEqualitySupport(dtd, datatypeDependencies);
}
}
- // Perform the guardedness check on co-datatypes
if (ErrorCount == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved
+ // Perform the guardedness check on co-datatypes
foreach (var decl in declarations) {
var cl = decl as ClassDecl;
if (cl != null) {
@@ -1042,6 +1043,99 @@ namespace Microsoft.Dafny { return true;
}
+ void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
+ Contract.Requires(startingPoint != null);
+ Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+
+ 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.
+ foreach (var dt in scc) {
+ Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var anotherIndDt = arg.Type.AsIndDatatype;
+ if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {
+ // arg.Type is known never to support equality
+ // So, go around the entire SCC and record what we learnt
+ foreach (var ddtt in scc) {
+ ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;
+ }
+ return; // we are done
+ }
+ }
+ }
+ }
+
+ // Now for the more involved case: we need to determine which type parameters determine equality support for each datatype in the SCC
+ // We start by seeing where each datatype's type parameters are used in a place known to determine equality support.
+ bool thingsChanged = false;
+ foreach (var dt in scc) {
+ if (dt.TypeArgs.Count == 0) {
+ // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
+ continue;
+ }
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var typeArg = arg.Type.AsTypeParameter;
+ if (typeArg != null) {
+ typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ } else {
+ var otherDt = arg.Type.AsIndDatatype;
+ if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC
+ var otherUdt = (UserDefinedType)arg.Type.Normalize();
+ var i = 0;
+ foreach (var otherTp in otherDt.TypeArgs) {
+ if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+ var tp = otherUdt.TypeArgs[i].AsTypeParameter;
+ if (tp != null) {
+ tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ // Then we propagate this information up through the SCC
+ while (thingsChanged) {
+ thingsChanged = false;
+ foreach (var dt in scc) {
+ if (dt.TypeArgs.Count == 0) {
+ // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
+ continue;
+ }
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var otherDt = arg.Type.AsIndDatatype;
+ if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC
+ var otherUdt = (UserDefinedType)arg.Type.Normalize();
+ var i = 0;
+ foreach (var otherTp in otherDt.TypeArgs) {
+ if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+ var tp = otherUdt.TypeArgs[i].AsTypeParameter;
+ if (tp != null) {
+ tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ }
+ }
+ i++;
+ }
+ }
+ }
+ }
+ }
+ }
+ // Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones
+ // where equality support should be checked by looking at the type arguments.
+ foreach (var dt in scc) {
+ dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;
+ }
+ }
+
void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter much for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c8cca5d3..18b613b9 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1327,6 +1327,17 @@ Dafny program verifier finished with 12 verified, 3 errors 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
+
-------------------- SplitExpr.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy new file mode 100644 index 00000000..bbcb988f --- /dev/null +++ b/Test/dafny0/EqualityTypes.dfy @@ -0,0 +1,89 @@ +module A {
+ datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);
+ datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);
+
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T>(x: Inferred<T>)
+ }
+}
+
+module B refines A {
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T(==)>(x: Inferred<T>)
+ }
+}
+
+// ----------------------------
+
+module C {
+ type X(==);
+ type Y(==);
+}
+
+module D refines C {
+ class X { }
+ datatype Y = Red | Green | Blue;
+}
+
+module E refines C {
+ codatatype X = Next(int, X); // error: X requires equality and codatatypes don't got it
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green(X) | Blue;
+}
+
+module F refines C {
+ datatype X<T> = Nil | Cons(T, X<T>); // error: not allowed to add a type parameter to type X
+ class Y<T> { } // error: not allowed to add a type parameter to type Y
+}
+
+module G refines C {
+ datatype X = Nil | Next(Z, X); // error: X does not support equality
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green | Blue;
+}
+
+// ----------------------------
+
+module H {
+ datatype Dt<T> = Nil | Cons(T, Dt);
+
+ datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);
+ datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);
+ datatype BulkyListAuxAux<T> = GoBack(BulkyList);
+
+ codatatype Stream<T> = Next(head: T, tail: Stream<T>);
+
+ method M<T(==)>(x: T)
+ { }
+ function F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ { if x == y then 5 else 7 } // this equality is allowed
+ function G<T>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
+ function G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // fine
+
+ method Caller0(b: BulkyList, y: int) {
+ match (b) {
+ case Nothing =>
+ case Wrapper(t, bla) =>
+ var u;
+ if (y < 100) { u := t; }
+ // The following call is allowed, because it will be inferred that
+ // 'u' is of a type that supports equality
+ M(u);
+ }
+ }
+ method Caller1(d: Dt) {
+ match (d) {
+ case Nil =>
+ case Cons(t, rest) =>
+ M(t); // error: t may be of a type that does not support equality
+ }
+ }
+ method Caller2(co: Stream) {
+ var d := Cons(co, Nil);
+ Caller1(d); // case in point for the error in Caller1
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index ac7c8aed..d352cf44 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy
- TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
+ TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 051d60f4..af789102 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -42,6 +42,7 @@ % the following isn't actually Dafny, but it gives the option to produce nicer latex
{<<}{$\langle$}1
{>>}{$\rangle$}1
+ {(==)}{${}^{(=)}$}2
{...}{$\ldots$}1
{\\alpha}{$\alpha$}1
{\\beta}{$\beta$}1
|