Automatic Test Gen: Type Parameter Translation

[tbean79]

Dafny version: 3.6.0.40511

When running /generateTestMode:Block on this Dafny method

module Test {
  method IsEvenLength<K, V>(m: map<K, V>) returns (isEven: bool)
  {
    if (|m| % 2 == 0) {
      return true;
    } else {
      return false;
    }
  }
}

the tests generated take on this form

method test0() returns (r0:bool)  {
r0 := Test.IsEvenLength(null, null, map[null := null, null := null, null := null]);
}

The first two parameters are meant to be type parameters, but instead get lumped in with the other parameters. This occurs because the instrumented boogie implementation signature of IsEvenLength looks like this:

implementation Impl$$Test.__default.IsEvenLength(Test._default.IsEvenLength$K: Ty, Test._default.IsEvenLength$V: Ty, m#0: Map Box Box) returns (isEven#0: bool, $_reverifyPost: bool)

Would there be any simple means of preserving the List<TypeParameter> TypeArgs; of the Dafny Method so that TestMethod.cs is aware of how many there are when it builds the call to the test method? I see this as difficult because the ProgramModifier is a visitor of the BoogieAST, not the Dafny AST.