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')
}
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.