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

Gerwin Klein gerwin.klein at nicta.com.au
Tue Jul 5 13:27:35 CEST 2011


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




More information about the isabelle-dev mailing list