On Fri, 1 Jul 2011, Thomas Sewell wrote:
The 'ext' constant, which constructs the (| a = 1, b = 2 |) style
syntax, looks like it's been there a while. Assuming this syntax is used
in the future, it will probably be backed by a constant. Naming it as a
constructor would seem reasonable, but I have no idea what the
ramifications would be. I don't know anything at all about the internals
of the datatype package.
The only concern I can see is a potential performance problem with the
datatype package - there are some very large records in use. At least
one, anyway. I did consider at one point adding a flag which would turn
off some features of the package for users concerned about performance.
This would make it easier to add new features in if needed.
This was introduced by Norber Schirmer in 2004, see especially
http://isabelle.in.tum.de/repos/isabelle/rev/2f885b7e5ba7
He also did a lot of optimizations for the proofs, exploiting the special
situation that these are just "gloried tuples" and not arbitrary
datatypes. He even had some odd flags to select between two proof
versions, one slightly faster with some other disadvantages unkown to me.
You have later noticed yourself (or was it Rafal?) that a lot of that was
often unused and broken at some point.
This merely illustrates that if there is anything worse than a lot of
features it is feature variants. E.g. we used to have certain "options"
in datatype, and it made Florian Haftmann's code generation on top of it
incredibly difficult. So we spent some efforts to remove such variants
from datatype again, to get back to some sanity.
I am also inviting people to study the history of the record package after
the performance refinements of Norbert and you guys from NICTA. Even
though it was all very solid work, there very many fine points to be
cleared. The time spent for maintanence is usually more than for the
original implementation.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
