[isabelle-dev] Code generation to OCaml and Scala

[Florian Haftmann]

Hi Frédéric,

thanks for going into this so thoroughly.

I will look after these errors as soon possible.

In ancient days, there was a dedicated theory which contained such
»challenges« for the code generator, but with more and more theories
with code generation this had been given up; maybe these synthetic
examples are critical enough to revive that.

Thanks a lot,
	Florian

Am 01.09.2015 um 17:37 schrieb 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

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/20150905/41af5b44/attachment.sig>