diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 41 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 19 | ||||
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 2 |
4 files changed, 51 insertions, 14 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 20b61809..d4d7abe8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1216,6 +1216,10 @@ namespace Microsoft.Dafny foreach (var member in ((ClassDecl)d).Members) {
if (member is Method) {
var m = (Method)member;
+ m.Req.Iter(mfe => CheckTypeInference(mfe.E));
+ m.Ens.Iter(mfe => CheckTypeInference(mfe.E));
+ m.Mod.Expressions.Iter(fe => CheckTypeInference(fe.E));
+ m.Decreases.Expressions.Iter(CheckTypeInference);
if (m.Body != null) {
CheckTypeInference(m.Body);
bool tail = true;
@@ -1243,6 +1247,10 @@ namespace Microsoft.Dafny }
} else if (member is Function) {
var f = (Function)member;
+ f.Req.Iter(CheckTypeInference);
+ f.Ens.Iter(CheckTypeInference);
+ f.Reads.Iter(fe => CheckTypeInference(fe.E));
+ f.Decreases.Expressions.Iter(CheckTypeInference);
if (f.Body != null) {
CheckTypeInference(f.Body);
bool tail = true;
@@ -1982,17 +1990,27 @@ namespace Microsoft.Dafny }
}
- bool CheckTypeInference(Expression e) {
- if (e == null) return false;
- foreach (Expression se in e.SubExpressions) {
- if (CheckTypeInference(se))
- return true;
+ void CheckTypeIsDetermined(IToken tok, Type t, string what) {
+ Contract.Requires(tok != null);
+ Contract.Requires(t != null);
+ Contract.Requires(what != null);
+ t = t.Normalize();
+ if (t is TypeProxy && !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy)) {
+ Error(tok, "the type of this {0} is underspecified, but it cannot be an arbitrary type.", what);
}
- if (e.Type is TypeProxy && !(e.Type is InferredTypeProxy || e.Type is ParamTypeProxy || e.Type is ObjectTypeProxy)) {
- Error(e.tok, "the type of this expression is underspecified, but it cannot be an arbitrary type.");
- return true;
+ }
+ void CheckTypeInference(Expression e) {
+ if (e == null) return;
+ e.SubExpressions.Iter(CheckTypeInference);
+ var ce = e as ComprehensionExpr;
+ if (ce != null) {
+ foreach (var bv in ce.BoundVars) {
+ if (bv.Type.Normalize() is TypeProxy) {
+ Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly", bv.Name);
+ }
+ }
}
- return false;
+ CheckTypeIsDetermined(e.tok, e.Type, "expression");
}
void CheckTypeInference(Statement stmt) {
Contract.Requires(stmt != null);
@@ -2012,9 +2030,7 @@ namespace Microsoft.Dafny } else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
s.SubStatements.Iter(CheckTypeInference);
- if (s.Type is TypeProxy && !(s.Type is InferredTypeProxy || s.Type is ParamTypeProxy || s.Type is ObjectTypeProxy)) {
- Error(s.Tok, "the type of this expression is underspecified, but it cannot be an arbitrary type.");
- }
+ CheckTypeIsDetermined(s.Tok, s.Type, "local variable");
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
CheckTypeInference(s.Receiver);
@@ -2051,6 +2067,7 @@ namespace Microsoft.Dafny var s = (ParallelStmt)stmt;
CheckTypeInference(s.Range);
CheckTypeInference(s.Body);
+ s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
s.SubExpressions.Iter(e => CheckTypeInference(e));
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index cd5529fe..ddabad3d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -508,6 +508,7 @@ ResolutionErrors.dfy(466,7): Error: RHS (of type List<A>) not assignable to LHS ResolutionErrors.dfy(471,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(485,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(497,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
+ResolutionErrors.dfy(532,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly
ResolutionErrors.dfy(396,2): Error: More than one default constructor
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
@@ -577,7 +578,7 @@ ResolutionErrors.dfy(510,7): Error: let-such-that expressions are allowed only i ResolutionErrors.dfy(510,20): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(512,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(513,18): Error: unresolved identifier: w
-73 resolution/type errors detected in ResolutionErrors.dfy
+74 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 69b8ea38..6c86e7a8 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -513,3 +513,22 @@ method LetSuchThat(ghost z: int, n: nat) x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope
ghost var xg := var w :| w == 2*w; w;
}
+
+// ------------ quantified variables whose types are not inferred ----------
+
+module NonInferredType {
+ predicate P<T>(x: T)
+
+ method NonInferredType0(x: int)
+ {
+ var t;
+ assume forall z :: P(z) && z == t;
+ assume t == x; // this statement determined the type of z
+ }
+
+ method NonInferredType1(x: int)
+ {
+ var t;
+ assume forall z :: P(z) && z == t; // error: the type of z is not determined
+ }
+}
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 19e0645f..777be464 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -121,7 +121,7 @@ ghost method Lemma_Revacc(xs: List, ys: List) assert concat(revacc(xrest, Cons(x, Nil)), ys)
== revacc(xrest, concat(Cons(x, Nil), ys));
- assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+ assert forall g: _T0, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
assert revacc(xrest, concat(Cons(x, Nil), ys))
== // the assert lemma just above
|