Email Gateway (Aug 18 2022 at 13:01): Email Gateway (Aug 18 2022 at 13:01):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Sorry to be slow to the party, but the significance of the way the
definition/notation mechanism now works has only just started to sink
in. How do I find out more about it?
The mechanism seems to finally properly address the problem of
properly identifying and distinguishing constant and variables that
share names. This is really cool.
My question is as to how far this mechanism has penetrated the
pre-2008 world. It seems that datatype constructors are not included
in the new mechanism? Is there anyway include a const declared in the
old way, say because it is being defined by extension rather than
intension? Are type names included or planned for inclusion is a
similar scheme?
Brendan
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
On Fri, 20 Feb 2009, Dr. Brendan Patrick Mahony wrote:
Sorry to be slow to the party, but the significance of the way the
definition/notation mechanism now works has only just started to sink
in.
What you have discovered here is called "authentic syntax" in internal
jargon. It merely means that things work as expected, i.e. the syntax is
really attached to certain entities in a robust fashion.
Right now, the dividing line for unrobust legacy syntax and authentic
syntax is mostly the "local theory" interface. Thus newer commands like
'definition' and 'notation' already benefit on it, as well as 'inductive',
'function' etc. As we move on to make old packages fit for the local
theory concept, syntax will also improve, although this is only a small
thing compared to the full power of local theories. (Both of these
renovations coincide mostly by accident, though.)
Anyway, upgrading to authentic syntax is not completely trivial due to old
syntax translations, which usually expect syntactic const names in the
(fragile) unqualified form. Right now you can already use the
@{const_syntax foo} antiquotation in ML, or "CONST foo" in translation
rules, to make things fit for the future.
Is there anyway include a const declared in the old way, say because it
is being defined by extension rather than intension?
You can try it like this:
abbreviation "foo == old_foo" (mixfix)
which will produce an authentic const "foo", corresponding to some other
term, which happens to be based on non-authentic syntax (or no syntax at
all).
Are type names included or planned for inclusion is a similar scheme?
In the end, yes. It will probably happen in the next round, when we
provide typedecl/typedef interfaces for local theories (this is a bit
tricky, because local theories do not really support type constructors).
Makarius
Last updated: May 03 2024 at 12:27 UTC