Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nested locales


view this post on Zulip Email Gateway (Aug 22 2022 at 16:54):

From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
Hello,

I am trying to achieve the following syntactic structure:

mainlocale Test =
fixes x::nat
begin
...
mylocale AA =
fixes y::nat
begin
...
end_mylocale
...
end_ mainlocale

mainlocale declaration should behave the same as a locale declaration

mylocale declaration should end mainlocale and then it should behave like
a locale declaration

end_mylocale should end mylocale and it should open the context of the
mainlocale Test.

end_ mainlocale should end the context of mainlocale Test.

I tried to add the following syntax for mylocale:

val End = (Toplevel.exit o Toplevel.end_local_theory o
Toplevel.close_target o
Toplevel.end_proof (K Proof.end_notepad));

fun begin_mylocale begin f = Toplevel.begin_local_theory begin f o End;

val _ =
Outer_Syntax.command @{command_keyword mylocale} "define named
specification context"
(Parse.binding --
Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), [])
-- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
begin_mylocale begin
(Expression.add_locale_cmd name Binding.empty expr elems #>
snd)));

where End is what seems to be done by the end keyword.

However, this does not work. End seems to do more than just closing the
previous mainlocale declaration.

Additionally, if possible, I would also like to have "end" keyword instead
of end_mylocale and
end_ mainlocale.

Best regards,

Viorel Preoteasa


Last updated: Mar 28 2024 at 16:17 UTC