Email Gateway (Aug 18 2022 at 15:06): Email Gateway (Aug 18 2022 at 15:06):From: Brian Huffman <brianh@cs.pdx.edu>
Hello all,
Peter Gammie recently brought this issue to my attention (with
"domain" instead of "datatype", but the behavior is the same for
both).
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).
Email Gateway (Aug 18 2022 at 15:06):From: Makarius <makarius@sketis.net>
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.)
Makarius
Email Gateway (Aug 18 2022 at 15:07):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Apr 15, 2010 at 1:20 PM, Makarius <makarius@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.
Email Gateway (Aug 18 2022 at 15:07):From: Makarius <makarius@sketis.net>
On Fri, 16 Apr 2010, Brian Huffman wrote:
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.
So far it is just another motivitation to start moving towards a localized
version. The datatype package is very complex, and Stefan Berghofer is
probably the only one who can update it without causing collateral damage.
Anyway, I think Stefan is already trying some small-scale improvements,
although such long standing oddities are hard to reform. For example,
old-style mixfix notation involves constant names with spaces and with
non-identifier characters, e.g. "op #". Due to earlier spring cleaning it
might actually work out this time.
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.
Full localization is certainly beyond the spring cleaning, it will take
more time. If you want to do some moves towards it for the domain
package, I can point to some spots that are probably easy to update.
Makarius
Last updated: Apr 18 2024 at 20:16 UTC