Email Gateway (Aug 19 2022 at 11:55): Email Gateway (Aug 19 2022 at 11:55):From: Walther Neuper <wneuper@ist.tugraz.at>
In a file like ...
/-----------------------------------------------------------------------------------------------------------------
theory Foo imports Bar begin
ML {*
@{theory Bar};
(*OK *)
(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory
entry for "Bar"'*)
*}
end
-----------------------------------------------------------------------------------------------------------------/
... "Thy_Info.get_theory" causes the theory loader to say "undefined
theory entry", although "@{theory Bar}" works as expected.
However, if a session Bar is built from Bar.thy, then the theory loader
is informed and 'Thy_Info.get_theory "Bar"' finds the theory.
So my question is:
Is there a way to tell the theory loader about newly imported
theories ?
(without the detour via session)
Thanks for any help,
Walther
PS: Such a way would simplify certain situations in Isac development.
Email Gateway (Aug 19 2022 at 11:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Walther,
without being an expert I would guess that you may only retrieve
finished theories in that manner.
Cf. in Isabelle 2013
theory Foo
imports Main
begin
ML {* @{theory Foo} *} -- failure
ML {* @{theory Main} *} -- ok
As a first recommendation I would say to split up such theories in two,
roughly.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
On Thu, 5 Sep 2013, Walther Neuper wrote:
In a file like ...
/-----------------------------------------------------------------------------------------------------------------
theory Foo imports Bar begin
ML {*
@{theory Bar}; (*OK *)
(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for
"Bar"'*)
*}
end
-----------------------------------------------------------------------------------------------------------------/... "Thy_Info.get_theory" causes the theory loader to say "undefined theory
entry", although "@{theory Bar}" works as expected.However, if a session Bar is built from Bar.thy, then the theory loader is
informed and 'Thy_Info.get_theory "Bar"' finds the theory.
This observation is correct. The @{theory} antiquotation follows the
logical context, and thus can only refer to the import graph of the
current theory context. The global theory loader operation
Thy_Info.get_theory can step outside the context, but only for theories
that have been loaded into the parent session already (and can no longer
change).
In Isabelle2013 there is still a mix of old and new concepts how sessions
and the overall proof document state of PIDE are managed. This will take
further rounds of refinement, but the trend is more and more away from
global stateful things like Thy_Info.get_theory.
Is there a way to tell the theory loader about newly imported theories ?
(without the detour via session)
Probably not.
Such a way would simplify certain situations in Isac development.
As usual, one needs to step back and rethink the actual motivation behind
this former use of Thy_Info.get_theory.
Makarius
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
In the middle of theory body Foo, you can refer to the current background
context via @{theory}. Of course the final @{theory Foo} might be
something else, but it is guaranteed to be a super-theory.
Makarius
Email Gateway (Aug 19 2022 at 11:58):From: Walther Neuper <wneuper@ist.tugraz.at>
Thank you for that hint, it will have impact on our plans !
Walther
Last updated: Apr 25 2024 at 01:08 UTC