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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and