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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
