On 26 July 2018 at 09:09, Claire Dross <dr...@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 <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?
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 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
