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



On Thu, Apr 15, 2010 at 1:20 PM, Makarius <makarius at sketis.net> wrote:
> 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.

So your recommendation is to wait until the datatype package has been
converted to use local theories, rather than adding any new
(temporary) error checks. OK.

> 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.)

So will the conversion of the datatype package be part of this "spring
cleaning"? Has anyone committed to doing the conversion? Of course,
I'll take responsibility for converting the domain package, but I need
to have the datatype package done first, so I can see how it's done.

- Brian





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