Attributes in variant clause
I am using attribute to keep a track of the different properties to prove. It works well for almost all properties, except for variants.
use int.Int
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x }
x <- x - 1
done
For instance, consider this program. I put an attribute [@variant:x]
on the variant, and the goal generated for the variant looks like:
goal f'vc [@expl:VC for f] :
[@vc:annotation] [@expl:loop variant decrease]
[@loop:/home/cluzel/tis/tis-analyzer/tis-analyzer/jessie3/a.f.mlw:5:2:69]
0 <= ([@variant:x] x1) /\ ([@variant:x] x) < ([@variant:x] x1)
The attribute [@variant:x]
is still located with the term x
while I would expect the variant attribute to be moved at toplevel to find it more easily automatically. I.E. I would like to have a goal that looks like:
goal f'vc [@expl:VC for f] :
[@vc:annotation] [@expl:loop variant decrease]
[@loop:/home/cluzel/tis/tis-analyzer/tis-analyzer/jessie3/a.f.mlw:5:2:69]
[@variant:x]
0 <= ([@variant:x] x1) /\ ([@variant:x] x) < ([@variant:x] x1)
Is there a reason that would prevent you to do this transformation? If not do you think that it can be implemented easily?