[isabelle-dev] Code generation to OCaml and Scala

[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