[isabelle-dev] Data slots for runtime compiler invocation

[Florian Haftmann]

>> Recently I changed the interface for invoking the compiler at runtime
>> on generated code to use proof data slots rather than unsychronized
>> references.  The consequence is that there are a lot of non-joinable
>> proof data slots laying around in the same module, cf.
>> http://isabelle.in.tum.de/reports/Isabelle/rev/f6ab14e61604
> 
> Which are the non-joinable ones in particular? Did I overlook anything
> important?

The ones in predicate_compile_core.ML.  They are not used as data
storage but as storage for results of runtime evaluation, which for
technical reasons requires separate slots.  Of course you could
generalize this mechanisms to permit application of combinators or such
before storing, but I would argue that runtime evaluation is fragile
enough that you do not want to make it more complicated than needed anyway.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110111/d77b8531/attachment.sig>