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

[Makarius]

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