diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 7 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 22 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 9 |
4 files changed, 42 insertions, 20 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index ac56db1e..46c0808d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4930,6 +4930,9 @@ namespace Microsoft.Dafny return subst;
}
+ /// <summary>
+ /// If the substitution has no effect, the return value is pointer-equal to 'type'
+ /// </summary>
public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/, Type/*!*/>/*!*/ subst) {
Contract.Requires(type != null);
Contract.Requires(cce.NonNullDictionaryAndValues(subst));
@@ -4938,11 +4941,17 @@ namespace Microsoft.Dafny if (type is BasicType) {
return type;
} else if (type is MapType) {
- MapType t = (MapType)type;
- return new MapType(SubstType(t.Domain, subst), SubstType(t.Range, subst));
+ var t = (MapType)type;
+ var dom = SubstType(t.Domain, subst);
+ var ran = SubstType(t.Range, subst);
+ if (dom == t.Domain && ran == t.Range) {
+ return type;
+ } else {
+ return new MapType(dom, ran);
+ }
} else if (type is CollectionType) {
- CollectionType t = (CollectionType)type;
- Type arg = SubstType(t.Arg, subst);
+ var t = (CollectionType)type;
+ var arg = SubstType(t.Arg, subst);
if (arg == t.Arg) {
return type;
} else if (type is SetType) {
@@ -4955,7 +4964,7 @@ namespace Microsoft.Dafny Contract.Assert(false); throw new cce.UnreachableException(); // unexpected collection type
}
} else if (type is UserDefinedType) {
- UserDefinedType t = (UserDefinedType)type;
+ var t = (UserDefinedType)type;
if (t.ResolvedParam != null) {
Contract.Assert(t.TypeArgs.Count == 0);
Type s;
@@ -4995,10 +5004,9 @@ namespace Microsoft.Dafny TypeProxy t = (TypeProxy)type;
if (t.T == null) {
return type;
- } else {
- // bypass the proxy
- return SubstType(t.T, subst);
}
+ var s = SubstType(t.T, subst);
+ return s == t.T ? type : s;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index fa202ef5..55ae7330 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -10111,6 +10111,10 @@ namespace Microsoft.Dafny { Contract.Assert(false); // unexpected ComprehensionExpr
}
}
+ // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)
+ foreach (var bv in e.BoundVars) {
+ substMap.Remove(bv);
+ }
} else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
@@ -10156,7 +10160,8 @@ namespace Microsoft.Dafny { /// <summary>
/// Return a list of bound variables, of the same length as vars but with possible substitutions.
- /// For any change necessary, update 'substMap' to reflect the new substitution.
+ /// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for
+ /// undoing these changes once the updated 'substMap' has been used.
/// If no changes are necessary, the list returned is exactly 'vars' and 'substMap' is unchanged.
/// </summary>
private List<BoundVar> CreateBoundVarSubstitutions(List<BoundVar> vars) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index aa573505..51243ca6 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1131,7 +1131,7 @@ Execution trace: (0,0): anon0
(0,0): anon5_Then
-Dafny program verifier finished with 39 verified, 6 errors
+Dafny program verifier finished with 40 verified, 6 errors
-------------------- Coinductive.dfy --------------------
Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
@@ -1672,36 +1672,36 @@ Execution trace: Dafny program verifier finished with 38 verified, 11 errors
-------------------- Superposition.dfy --------------------
-
+ Verifying CheckWellformed$$_0_M0.C.M ...
[0 proof obligations] verified
-
+ Verifying Impl$$_0_M0.C.M ...
[4 proof obligations] verified
-
+ Verifying CheckWellformed$$_0_M0.C.P ...
[4 proof obligations] verified
-
+ Verifying CheckWellformed$$_0_M0.C.Q ...
[3 proof obligations] error
Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
-
+ Verifying CheckWellformed$$_0_M0.C.R ...
[3 proof obligations] error
Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
-
+ Verifying CheckWellformed$$_1_M1.C.M ...
[0 proof obligations] verified
-
+ Verifying Impl$$_1_M1.C.M ...
[1 proof obligation] verified
-
+ Verifying CheckWellformed$$_1_M1.C.P ...
[1 proof obligation] error
Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
@@ -1710,10 +1710,10 @@ Execution trace: (0,0): anon7_Else
(0,0): anon9_Then
(0,0): anon6
-
+ Verifying CheckWellformed$$_1_M1.C.Q ...
[0 proof obligations] verified
-
+ Verifying CheckWellformed$$_1_M1.C.R ...
[0 proof obligations] verified
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 5598844d..b00d5c21 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -272,3 +272,12 @@ function foo(f: Fwd): int {
if f.FwdNil? then 0 else f.k
}
+
+// -- regression test --
+
+predicate F(xs: List, vs: map<int,int>)
+{
+ match xs
+ case Nil => true
+ case Cons(_, tail) => forall vsi :: F(tail, vsi)
+}
|