On Thu, 30 Jun 2011, Alexander Krauss wrote:
(cc'ing isabelle-dev)
On 06/30/2011 11:11 AM, Gerwin Klein wrote:
Hi Tom,
sounds like an easy addition to the record package (see below).
Can you think of anything speaking against generating this declaration?
Cheers,
Gerwin
I am not sure if it would generate bloat for very large records... But
on the other hand, it is just one constructor. Makarius or Stefan might
be able to comment. At least, I would be surprised if nobody had thought
about this idea before.
Indeed, after so many years it has become very difficult to come up with
ideas that have not been tried before.
The second version of the record package by Naraschewski/Wenzel from 1998
was based on datatype internally, because this was a bit more convenient
than typedef, which did not have any supporting infrastructure at that
time. Thus the record package was very slow, due to an order of magnitude
extra overhead for datatype, with all its derived priciples.
Back then we had one type for each record field, now it is only one type
for each record extensions. On the other hand, the datatype package has
become more bloated, with all its "interpretation" plugins. There will be
also some new overhead both for record and datatype when they are
localized at last. (I am occasionally worried about the impact on large
applications as the one of Gerwin.)
If there are no reasons against it, it would certainly be nice, as it
would also allow record patterns in case expressions, not just "fun"
definitions.
Even in the ancient versions, where we had full datatypes in the
background, we did not provide any support for record patterns on purpose.
First off all, simplicity and minimality has always been the recipe for
survival in the long term. (In 1998 the record package was tiny compared
to today, but even that was already a bit complex.) In exchange for the
lack of tuple patterns, there was convenient notation for selectors and
updates, with related proof tool support. I have no precise overview of
the current state of the art wrt. these record simprocs, and if record
patterns would demand yet more of that.
Even now I always associate datatype and record with "feature bloat" par
excellence. It is also the practical reason, why the localization will
take again a bit longer, but it has to happen someday.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
