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

[Tobias Nipkow]

I agree with Gerwin. Records are datatypes. Hence one should be able to 
pattern match against them as in FP languages. The record package can 
arrange for this very easily via rep_datatype. On performance: I 
recently came across an example of a short ML function with very 
complicated pattern matching (no records) that took polyML one minute to 
compile. Even the best systems have performance limits. Our standard 
solution is the one Gerwin suggested.

Tobias

>
> On 01/07/2011, at 2:16 PM, Makarius wrote:
>
>> 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 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 agree that feature variants by options are problematic, they tend to explode in number.
>
> To add some data to the discussion, I've measure runtime of the rep_datatype one-liner that Alex proposed. Things look good in the beginning, but the datatype package does not scale well (have not measured memory usage):
>
> 100 fields:
>    12s record definition
>    2.35s rep_datatype
>
> 200:
>    57.6
>    23.14
>
> 300:
>    138.537
>    95.827
>
> 400:
>    347.242
>    342.078
>
> 500:
>    643.64
>    3421.79
>
> For more than 500 fields this doesn't look feasible any more. Not sure if this hit some memory bound on my machine, I was in a meeting when the test was running, but even the trajectory up to 400 does not promise anything good beyond 400.
>
> There is of course the slightly evil option of checking for size and just not do the rep_datatype for very large records (with warning emitted). It's not even without precedent, lots of other packages have limits where they give up on things, and the matching syntax at least only makes sense for smaller records anyway.
>
> Making the syntax available for matching would fit naturally into the Isabelle/HOL as programming language paradigm that people have been propagating for a while..
>
> Cheers,
> Gerwin
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev