[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0

Andrei Paskevich andrei.paskevich at lri.fr
Thu Jul 26 09:33:38 CEST 2018


On 26 July 2018 at 09:09, Claire Dross <dross at adacore.com> wrote:
> Thanks Andrei for your answers.
>
> Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
>>
>> On 25 July 2018 at 17:31, Claire Dross <dross at 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?

No, there is no hard reason for that AFAIK. Can be added back. What is
your use case for multiline labels?

>>> 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.

>>>>> 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?

> 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.

Best,
Andrei


More information about the Why3-club mailing list