[isabelle-dev] Code generation to OCaml and Scala
florian.haftmann at informatik.tu-muenchen.de
Sat Sep 5 18:20:35 CEST 2015
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,
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"
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev