Hi Frédéric, thanks for going into this so thoroughly.
I will look after these errors as soon possible.
In ancient days, there was a dedicated theory which contained such
»challenges« for the code generator, but with more and more theories
with code generation this had been given up; maybe these synthetic
examples are critical enough to revive that.
Thanks a lot,
Florian
Am 01.09.2015 um 17:37 schrieb Frédéric Tuong:
> Dear all,
>
> The following is a list with 2 elements:
> definition "l = [let x = True in x, False]"
> However after doing "export_code l in OCaml", we obtain a list with only
> 1 element, because at the end no parentheses are inserted around the
> corresponding "let".
> In particular by default in OCaml [let x = true in x ; false] is
> understood as [let x = true in (x ; false)]
> and then a warning can be raised whenever x does not have type unit.
>
> By comparing the generating code for SML and OCaml in
> src/Tools/Code/code_ml.ML, I would be tempted to replace
> "brackify_block" by "brackets" everytime in the corresponding
> "print_case" clause, and skip this optimization like in the SML part
> where "let"..."in"..."end" are inserted everytime, what about you?
>
>
> In the same spirit, the following code does not compile after exporting
> to Scala:
> datatype n = N nat
> definition "b = (let _ = N in False)"
> This is because N is a function, and no parentheses are generated around
> functions (at least in this example).
>
> Whereas this behavior can be very useful for detecting ghost functions
> in a large project (the detection may also not be complete), it does not
> mean that errors only occur with ghost code.
> For example, the following code is well-typed in Isabelle but not in Scala:
> definition "f l = (%x. x | True) # (%x. x | False) # l"
>
> Cheers,
> Frédéric
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
