Fix issue #71. When substitute the forall's variables for those of the

fn in fixupRevealLemma substitute the types as well.

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