Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.

3 files changed, 14 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0e83f54a..41076a65 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -8693,7 +8693,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(codeContext != null);

         List<Expression> contextDecreases = codeContext.Decreases.Expressions;

         List<Expression> calleeDecreases = callee.Decreases.Expressions;

-        CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, etran.Old, builder, codeContext.InferredDecreases, null);

+        CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, tySubst, etran, etran.Old, builder, codeContext.InferredDecreases, null);

       }

 

       // Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.

@@ -8804,6 +8804,7 @@ namespace Microsoft.Dafny {
     void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Expression> calleeDecreases,

                               Bpl.Expr allowance,

                               Expression receiverReplacement, Dictionary<IVariable,Expression> substMap,

+                              Dictionary<TypeParameter, Type> typeMap,

                               ExpressionTranslator etranCurrent, ExpressionTranslator etranInitial, Bpl.StmtListBuilder builder, bool inferredDecreases, string hint) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(contextDecreases));

@@ -8835,7 +8836,7 @@ namespace Microsoft.Dafny {
         tok = new ForceCheckToken(tok);

       }

       for (int i = 0; i < N; i++) {

-        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

+        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap, typeMap);

         Expression e1 = contextDecreases[i];

         if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {

           N = i;

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

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

+

+function {:opaque} RefineSeqToSeq<T,U>(s:seq<T>, refine_func:T->U) : seq<U>

+    reads refine_func.reads;

+{

+    if |s| == 0 then []

+    else RefineSeqToSeq(s[1..], refine_func)

+}

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

+Dafny program verifier finished with 2 verified, 0 errors