1
Vote

attribute parsing does not allow type parameters

description

If f is a polymorphic function with one type argument, then (for example) f<int> is a legal expression in Dafny. Depending on the context, f may also be a legal expression, provided that the type argument can be inferred (but it is not legal if the type argument cannot be inferred, because expressions in Dafny are never polymorphic). Apparently, the parsing of attribute arguments does not allow f<int> to be parsed, which is a bug.

Repro: The example below parses, type checks, and verifies. However, the more natural way to write the fuel attribute on lemma Threes would be simply:
{:fuel fold, 2} 
which isn't accepted today.

Rustan
function triple(xs: List<int>): List<int>
{
  match xs
  case Nil => Nil
  case Cons(x, tail) => Cons(x, Cons(x, Cons(x, triple(tail))))
}

lemma {:fuel (fold<int,int>), 2} Threes(xs: List<int>)
  ensures fold((a,b) => a + b, 0, triple(xs)) % 3 == 0
{
}

function fold<A,B>(f: (A,B) -> B, z: B, xs: List<A>): B
  requires Total(f)
{
  match xs
  case Nil => z
  case Cons(a, tail) => f(a, fold(f, z, tail))
}

datatype List<A> = Nil | Cons(head: A, tail: List<A>)

predicate Total<A,B,C>(f: (A, B) -> C)
  reads f.reads
{
  forall a,b :: f.reads(a,b) == {} && f.requires(a,b)
}

comments