diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 3 | ||||
| -rw-r--r-- | Test/dafny4/Bug71.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny4/Bug71.dfy.expect | 2 |
4 files changed, 18 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 75e30b40..0b94f7fb 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -5225,12 +5225,14 @@ namespace Microsoft.Dafny { return e;
}
- public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {
+ public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e, Dictionary<TypeParameter, Type> typeMap=null) {
Contract.Requires(oldVars != null && newVars != null);
Contract.Requires(oldVars.Count == newVars.Count);
Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
- Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+ if (typeMap == null) {
+ typeMap = new Dictionary<TypeParameter, Type>();
+ }
for (int i = 0; i < oldVars.Count; i++) {
var id = new IdentifierExpr(newVars[i].tok, newVars[i].Name);
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 091ee24a..72649b5f 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -672,7 +672,8 @@ namespace Microsoft.Dafny // Substitute the forall's variables for those of the fn
var formals = fn.Formals.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x);
- reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs);
+ var typeMap = Util.Dict<TypeParameter, Type>(fn.TypeArgs, Util.Map(origForall.TypeArgs, x => new UserDefinedType(x)));
+ reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs, typeMap);
var newImpl = Expression.CreateImplies(reqs, origImpl.E1);
//var newForall = Expression.CreateQuantifier(origForall, true, newImpl);
diff --git a/Test/dafny4/Bug71.dfy b/Test/dafny4/Bug71.dfy new file mode 100644 index 00000000..1c3fcf61 --- /dev/null +++ b/Test/dafny4/Bug71.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function{:opaque} MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>
+//function MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>
+ reads f.reads;
+ requires forall x :: f.requires(x);
+{
+ set x | x in xs :: f(x)
+}
\ No newline at end of file diff --git a/Test/dafny4/Bug71.dfy.expect b/Test/dafny4/Bug71.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Bug71.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
|