[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode
makarius at sketis.net
Fri Jul 1 14:16:35 CEST 2011
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
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
More information about the isabelle-dev