>> On 7 Jun 2015, at 07:38, Dmitriy Traytel <tray...@in.tum.de >> <mailto:tray...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
