Re: [isabelle] should this use of the datatype package produce an error?

On Thu, 15 Apr 2010, Brian Huffman wrote:

The following datatype definition is accepted without any warning messages:

datatype tree = "tree list"

Can anyone guess what this type definition actually means?

That's right, it defines a datatype with a single nullary constructor,
which is called "tree list". Never mind that the constructor's name
contains a space, and is therefore impossible to parse.

Clearly, no one would ever write such a datatype definition on purpose.

A feature request: If the name of a constant contains a space or other illegal character, the datatype package should issue an error (or at the very least, a warning message).

This known problem shows up once a year or so. By using the proper local theory layer for the package, it will just dissappear, because there are sanity checks built in. Numerous other problems will be solved by localizing old-style packages.

Just today Alex has pointed out another yearly accident: sort constraints within type definitions (this time for record). The basic packages can (typedecl, typedef, record) now handle that. The more complex ones (datatype family, domain) still have their own partial ways of coping with sorts.

Maybe now is a good time for some spring cleaning, before we get too close to the next Isabelle release. (It is already > 4 months after Isabelle2009-1.)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.