Dafny: Support class type parameters in refinements. Added another regression test -- a sequence refined by a singly linked list.

2 files changed, 11 insertions, 4 deletions

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 3c206066..96ae33c6 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -173,7 +173,6 @@ namespace Microsoft.Dafny {
         }

         decl.Refined = (ClassDecl!) a;

         // TODO: copy over remaining members of a

-        // TODO: extend with type parameters for refinements               

       }        

     }  

       

@@ -469,6 +468,13 @@ namespace Microsoft.Dafny {
     }

         

     void ResolveTypeParameters(List<TypeParameter!>! tparams, bool emitErrors, TypeParameter.ParentType! parent) {

+      // push type arguments of the refined class

+      if (parent is ClassRefinementDecl) {

+        ClassDecl refined = ((ClassRefinementDecl)parent).Refined;

+        assert refined != null;

+        ResolveTypeParameters(refined.TypeArgs, false, refined);

+      }

+    

       // push non-duplicated type parameter names

       foreach (TypeParameter tp in tparams) {

         if (emitErrors) {

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index f6fc5142..ff88c67f 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1797,12 +1797,13 @@ namespace Microsoft.Dafny {
       //  assume I($Heap, $Heap)              

       builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));     

       

-      // assign input formals of m

+      // assign input formals of m (except "this")

       for (int i = 0; i < m.Ins.Count; i++) {        

         Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName,  TrType(m.Ins[i].Type)));

         localVariables.Add(arg);

-        assert inParams[i+1] != null;

-        builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, inParams[i+1])));

+        Bpl.Variable var = inParams[i+1];

+        assert var != null;

+        builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, var)));

       }

             

       //  call inlined m;