[isabelle-dev] Code generation to OCaml and Scala
frederic.tuong at lri.fr
Tue Sep 1 17:37:44 CEST 2015
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
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
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"
More information about the isabelle-dev