Email Gateway (Aug 22 2022 at 11:05): Email Gateway (Aug 22 2022 at 11:05):From: Lars Hupel <hupel@in.tum.de>
Dear BNF implementers,
I'm currently working on some Isabelle/ML code which produces a bunch of
datatype specifications, ultimately calling
'BNF_FP_Def_Sugar.co_datatypes' for all of them. This generally works
fine, but there appears to be some corner case. I've attached a minimal
failing example. Loading this with Isabelle2015 gives the following error
message related to the declaration of the second data type:
Undeclared hyps:
size_String0 ≡ size_String0
The error(s) above occurred for the goal statement⌂:
map_pre_Rational0 id = id
(and some more along the same lines)
If I put a call to 'Local_Theory.restore' in between, the error
disappears. (Not that I have any idea why.)
Cheers
Lars
Reproducer.thy
Email Gateway (Aug 22 2022 at 11:07):From: Lars Hupel <hupel@in.tum.de>
Hello again,
I have found another one of those corner cases. This time, it looks like I
might be using the ML interface wrong. Once again, I've attached a theory
reproducing the error.
It appears that there is some difference between dealing with a finished
theory and a non-finished theory. Makarius, maybe you could shed some
light on this. Is it generally not supported to modify finished theories
in Isabelle/ML?
Cheers
Lars
Reproducer.thy
Email Gateway (Aug 22 2022 at 11:08):From: Lars Hupel <hupel@in.tum.de>
After some more investigation, I think I can answer that myself: Yes,
there is a difference. If I, instead of using a finished theory directly,
first call 'Theory.begin_theory', everything works as expected.
The underlying problem in the source file I attached wasn't that the
datatype wasn't being created, but rather that it was created without
qualification. (It was just called 'String0'.) I've seen similar things
with 'Local_Theory.define', that after some switching between local and
global theories the naming discipline stopped making sense, i.e. morphisms
producing unqualified constant names. I still don't know whether this is
expected or not, but after looking at the implementation manual I think it
probably is (Sec 1.1.1):
The begin operation starts a new theory by importing several parent
theories
and entering a special mode of nameless incremental updates, until the
final
end operation is performed.
I couldn't find anything about the 'end' operation though.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:24):From: Makarius <makarius@sketis.net>
Local_Theory.restore essentially introduces a command-transaction
boundary, so the two invocations in ML behave like two Isar commands
within a theory file. I can't explain the deeper reason of the problem
seen here -- there might be something wrong with the context-discipline of
the BNF implementation, which is rather complex.
Dmitriy Traytel has recently updated that for the coming release, see
http://isabelle.in.tum.de/repos/isabelle/rev/7b915ca69af1
The motivation for that change was to allow the name space management of
Isabelle2015 via "context begin private/qualified ... end" work for
(co)datatype definitions as well, although a few more changes in the
repository were required to get it into proper shape (e.g. 2618e7e3b5ea).
As it happens, these changes also make the problems exposed in the example
disappear. This might be an accident, though, and the true reasons for the
breakdown still lingering in the dark.
For now I recommend to keep the Local_Theory.restore workaround and try
again when the first release candidates for Isabelle2016 emerge,
presumably at the start of the year 2016.
Makarius
Email Gateway (Aug 22 2022 at 11:24):From: Makarius <makarius@sketis.net>
On Wed, 12 Aug 2015, Lars Hupel wrote:
It appears that there is some difference between dealing with a finished
theory and a non-finished theory. Makarius, maybe you could shed some
light on this. Is it generally not supported to modify finished theories
in Isabelle/ML?After some more investigation, I think I can answer that myself: Yes,
there is a difference. If I, instead of using a finished theory directly,
first call 'Theory.begin_theory', everything works as expected.
Theory updates always need to happen within a theory body, as defined by
Theory.begin_theory ... Theory.end_theory. Under normal circumstances,
the system does that for you, so there are not many words in the
implementation manual what happens outside. That behaviour is essentially
undefined (or arbitrary).
The underlying problem in the source file I attached wasn't that the
datatype wasn't being created, but rather that it was created without
qualification. (It was just called 'String0'.)
That is an accidental effect of continuing updates after end_theory (of
the existing theory Main), which is treated like a formal "extend"
operation. Thus the naming policy is reset to a global default, without
any theory prefix yet.
There could be more explicit checks and error messages. I used to have
that on my TODO list until approx. 15 years ago, and then removed it for
lack of practical relevance -- at least at that time in the past.
Makarius
Email Gateway (Aug 22 2022 at 11:24):From: Lars Hupel <hupel@in.tum.de>
Theory updates always need to happen within a theory body, as defined by
Theory.begin_theory ... Theory.end_theory. Under normal circumstances,
the system does that for you, so there are not many words in the
implementation manual what happens outside. That behaviour is essentially
undefined (or arbitrary).
Okay, that makes sense.
There could be more explicit checks and error messages. I used to have
that on my TODO list until approx. 15 years ago, and then removed it for
lack of practical relevance -- at least at that time in the past.
I would find more of these checks very helpful, since in my work I'm often
exercising parts of the system in perhaps unintended ways.
Cheers
Lars
Last updated: Apr 19 2024 at 20:15 UTC