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.
I don't see his reply, were is it? On Why3 list?
- 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?
No, there is no hard reason for that AFAIK. Can be added back. What is
your use case for multiline labels?
They are for information to be printed back for manual proof I think.
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...
Why so? There is no dedicated sequence constructor anyway, sequences
are just "let-in" chains.
And even if you need a special case for that, it does not seem like a
complicated one.
Not so complicated. We have to check for the type of the expression when
printing a sequence, and I am forseeing troubles with cases where the
expression does not have a type. To be seen. What is sure, is that this
check does not bring us anything.
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.
I fail to see your logic here. The range types in WhyML were, in large
part, motivated by Spark use. As I've said earlier, it is easy to add
non-ghost range-to-int converter. What is the problem?
No problem, just yet another special case where we cannot use the same
function for the conversion when the conversion is done in the logic or
in the program domain. And yet again, for a check which does not bring
anything for us.
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...
That would be unfortunate indeed, and very far from our intention.
However, I do not understand why you think it is the case. The
questions you've raised so far do not seem to require complicated
changes in the code generator.
The code generator is very complicated in itself, and every special case
making it more so is a concern. But indeed, these are minor problems.
Maybe I am pessimistic, but I expect to encounter more of them, due to
this distinction between ghost and non-ghost code, and these features
for code extraction. They are yet another set of constraints that we
need to cope with for no gain, and I am concerned that it will make
things more complicated.
More serious problems I am expecting involve in particular equality.
Even if we don't provide logical equality at the level of SPARK, I am
pretty sure we use it at the level of Why3 and working around not having
it will be a pain, that's for sure...
--
Claire
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
