diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 7 |
2 files changed, 22 insertions, 9 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) {
|