[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

[Makarius]

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