MLCFG frontend : feature wishes
-
allow a mlcfg
file to contain no module at all, like in regular WhyML -
The new keywords cfg/var/goto/switch
should be colored in emacs and Why3 ide -
The use of the var
section at the beginning of the body seems superfluous, it could suffice to allow introduction oflet in
at the beginning -
the first could have a label too -
it should not be mandatory to name invariants -
allow the rec
keyword on MLCFG functions so as to define recursive ones -
allow a variant of the switch statement were the patterns are integer constants, such as
switch (e)
| 1 -> ...
| 2 | 3 -> ...
| 4..7 -> ...
end
-
allow scopes to be opened in mlcfg modules. See following code:
module B
scope A
let cfg test () : () = { () }
end
end