[isabelle-dev] Code generation to OCaml and Scala

[Florian Haftmann]

Hi Fréderic,

see now

http://isabelle.in.tum.de/repos/isabelle/rev/774752af4a1f
http://isabelle.in.tum.de/repos/isabelle/rev/8e736ce4c6f4

>> 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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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