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

fn in fixupRevealLemma substitute the types as well.

2 files changed, 6 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);