[isabelle-dev] Code generation to OCaml and Scala

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 10 11:58:28 CEST 2015

Hi Fréderic,

see now


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

For SML, I kept everything as it is since
a) the code is separate from OCaml anyway
b) the "let … end" is always safe regardless of surrounding whitespace.

Or did I miss something here?

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

Abstractions in Scala are now always in parenthesis, but only once for
abstraction chains.

Thanks a lot again,


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150910/6e21f36a/attachment.sig>

More information about the isabelle-dev mailing list