[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

>> On 7 Jun 2015, at 07:38, Dmitriy Traytel <traytel at in.tum.de
>> <mailto:traytel at in.tum.de>> wrote:
>>
>> I'm not sure if this is something for the repository though, since it
>> has a factor of >2 impact on the build-time:
> 
> Thanks for investigating. But how do we explain this?
> 
> Possibly “fun” insists on converting on creating unconditional patterns
> only, while “recdef” allows conditional equations. But one could easily
> insert conditions manually in order to simplify the set of patterns.

As far as I know, this is due to layered architecture of the function
package.  »recdef« does everything in one bunch and can hence optimize
for sequential pattern matching.  Each layer of »function« must feed its
result to its successor in a standardized form, and since there is no
overall concept of sequential pattern matching, it has to be compiled
away once and for all from the very beginning. (roughly spoken)

An optimization would require a modified architecture.

	Florian

-- 

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/20150607/e685e305/attachment.sig>