[isabelle-dev] Code generation to OCaml and Scala
florian.haftmann at informatik.tu-muenchen.de
Thu Sep 10 11:58:28 CEST 2015
>> 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
Thanks a lot again,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev