Fix issue #55 and #64. When performing type argument substitution for function

F's corresponding F_FULL, make sure the function is indeed the FullVesion
before the substitution. Also keep the TypeArgsSubst for the enclosingClass in
the typeMap.

3 files changed, 26 insertions, 6 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 12b5adfc..4cda8fd8 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -627,20 +627,24 @@ namespace Microsoft.Dafny
       var origForall = lem.Ens[0].E as ForallExpr;

       if (origForall != null) {

         Contract.Assert(origForall.TypeArgs.Count == fn.TypeArgs.Count);

-        fixupTypeArguments(lem.Ens[0].E, origForall.TypeArgs);

+        fixupTypeArguments(lem.Ens[0].E, fn, origForall.TypeArgs);

       }

     }

 

-    protected void fixupTypeArguments(Expression expr, List<TypeParameter> qparams) {

+    // Type argument substitution for the fn_FULL function using the orginal 

+    // fn function.

+    protected void fixupTypeArguments(Expression expr, Function fn, List<TypeParameter> qparams) {

       FunctionCallExpr e;

-      if ((e = expr as FunctionCallExpr) != null) {

-        e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

+      if (((e = expr as FunctionCallExpr) != null) && (e.Function == fullVersion[fn])) {

+        var newTypeArgsSubst = new Dictionary<TypeParameter, Type>();

+        fn.EnclosingClass.TypeArgs.ForEach(tp => newTypeArgsSubst.Add(tp, e.TypeArgumentSubstitutions[tp]));

         for (int i = 0; i < e.Function.TypeArgs.Count; i++) {

-          e.TypeArgumentSubstitutions[e.Function.TypeArgs[i]] = new UserDefinedType(qparams[i]);

+          newTypeArgsSubst.Add(e.Function.TypeArgs[i], new UserDefinedType(qparams[i]));

         }

+        e.TypeArgumentSubstitutions = newTypeArgsSubst;

       }

       foreach (var ee in expr.SubExpressions) {

-        fixupTypeArguments(ee, qparams);

+        fixupTypeArguments(ee, fn, qparams);

       }

     }

 

diff --git a/Test/dafny4/Bug55.dfy b/Test/dafny4/Bug55.dfy
new file mode 100644
index 00000000..bcbef2e8
--- /dev/null
+++ b/Test/dafny4/Bug55.dfy
@@ -0,0 +1,14 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate {:opaque} G(f:int->bool)

+  reads f.reads;

+  requires f.requires(0);

+{

+  true

+}

+

+predicate A<T>(s:set<T>)

+

+predicate{:opaque} B(s:set<int>)

+    requires A(s);

diff --git a/Test/dafny4/Bug55.dfy.expect b/Test/dafny4/Bug55.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/dafny4/Bug55.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 5 verified, 0 errors