Re: [isabelle] Scala codegen error: need NatO, natT, and NatC



On 12/24/2014 2:37 AM, Florian Haftmann wrote:
using »code_identifier«, you can explicitly control the naming of
identifiers in generated code.  The syntax is described in the Isar
reference manual and the theories in src/HOL contain various examples.
Florian,

Thanks. I'll use that someday, but all this led to several additional things. I hadn't considered the 'Eval' export_code option. The first section of codegen.pdf speaks of the four languages, so I missed that 'Eval' was an option. I saw 'Eval' the other day in the Isar reference manual, and now I've used it. It's more in line with what I've recently been focusing, which is a high-powered 'value'.

Reading your section 6 in codegen.pdf led me to your Parallel.thy. I experimented with 'Parallel.fork' and 'Parallel.join'. All that looks like it should be useful. I got a particular function, for a particular value, down from 4.5s to about 1s, by forking on the values of a list. Doing that with a 'fun' in a THY is good.

Thanks,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.