VSCode fix incorrectly inserts computed decreases

[yannickmoy]

On the code below, Dafny extension for VSCode proposes a fix to insert the decreases es,unit on method OptimizeAndFilter, but it inserts it between List and instead of after List.

datatype List<T> = Nil | Cons(head: T, tail: List<T>)
datatype Op = Add | Mul
datatype Expr = Const(nat)
              | Var(string)
              | Node(op: Op, args: List<Expr>)

function method Unit(op: Op): nat {
    match op case Add => 0 case Mul => 1
}

function method Optimize(e : Expr): Expr decreases  e
 {
    if e.Node? then
        var args := OptimizeAndFilter(e.args, Unit(e.op));
        Shorten(e.op, args)
    else
        e
}

function method Shorten(op: Op, args: List<Expr>): Expr {
    match args
    case Nil => Const(Unit(op))
    case Cons(e, Nil) => e
    case Cons(_, Cons(_, _)) => Node(op, args)
}

function method OptimizeAndFilter(es: List<Expr>,
                                  unit: nat): List<Expr>
{
    match es
    case Nil => Nil
    case Cons(e, tail) =>
        var e', tail' := Optimize(e), OptimizeAndFilter(tail, unit);
        if e' == Const(unit) then tail' else Cons(e', tail')
}

[fabianhauser]

Thanks for reporting this issue @yannickmoy. We are currently working on a major release of the plugin (better integrated to the main dafny project), which should make a clean implementation of this much easier 🙂