Thanks Andrei for your answers.
Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
On 25 July 2018 at 17:31, Claire Dross <dr...@adacore.com> wrote:
I have been trying to adapt the spark tool to use the new Why3 release. I
cannot say how it is going yet, I still have a long way to go, but I already
have some questions:
- the "no inlining" and "lskept" metas seem to have disappear, did they
changed names or are they completely removed?
No, the polymorphism encoding didn't change at all, so everything
should still be there, see François' reply.
- labels "..." are not accepted anymore. By looking at the parser, I have
replaced them with [@...], is this correct?
Yes.
OK, multiline labels are no longer supported then. On purpose?
(BTW, I am really missing the Language Reference section of the LRM, any chance
there is a draft I can use somewhere?)
I'm working on that, albeit slowly. Apart from the Appendix François
mentioned, you can see the text under construction in
doc/syntaxref.tex
I will look at it, thanks.
I also found 2 cases of constructs which were accepted before but are not
anymore:
- We can no longer ignore a non unit value:
let main () = 15; ()
This is on purpose, OCaml does that same. "let _ = 15 in ()" should work.
Yes it does, but it will require special casing in the code generator...
Cannot cast an integer literal to type unit
- Conversion to int of range types is ghost:
type tt = < range 1 5 >
let function to_rep (x : tt) : int = (tt'int x)
Function to_rep must be explicitly marked ghost
This is also on purpose: the tt'int operation is used for
specification purposes, if you make it non-ghost, you would need to
link the extracted code with an arbitrary-precision arithmetic
library.
Then I think we are back to not using range types and defining our own
projections. I will see if we can avoid that.
Unfortunately, it seems that the modifications, if they make whyml
better for code extraction, and probably a better language to program
with directly, seem to make it more complicated to use as an
intermediate language...
Thanks again for your answers,
--
Claire
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
