Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Towards localized syntax: bundle mixins fo...


view this post on Zulip Email Gateway (Nov 01 2020 at 16:52):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,

my recent re-working of parts of the local theory infrastructure has
inspired me to close a long-standing gap in our module system: the
ability to organize syntax declarations into bundles and use them in
confined nested blocks

context
includes bundles
begin

end

so far did not extend to class and locale specifications, which by their
very nature are always given at the outermost specification layer.

Taking the existing »includes« syntax as a base, the result looks as
follows:

locale / class foo = import +
includes bundles
fixes …
assumes …
begin

end

The declarations from the given bundle(s) are active for the locale /
class specification itself and the optional following context block.

For consistency, also the syntax for re-opening of named contexts is
extended:

context foo
includes bundles
begin

end

This is effectively equal to

context foo
begin

context
includes bundles
begin

end

end

See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples.

This refers to rev. 589645894305.

NEWS entries and documentation updates have still to be written, but I
want to discuss possible alternative syntactic notations in a separate
thread.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Nov 01 2020 at 17:09):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,

currently the syntax for bundle mixins for locale / class specifications
looks as follows:

locale / class foo = import +
includes bundles
fixes …
assumes …
begin

end

While this use of »includes« rests firmly on established traditions, it
is a little bit unsatisfactory since it also applies to the »import«
expression, but is notated after it.

I had thought about something like

context
includes bundles
begin

locale foo = import +
fixes …
assumes …
begin

end

end

instead but this would require an artificial construction identifying
nested contexts as »morally being global« internally.

A more inspiring solution could be to abandon the existing »includes«
syntax entirely and replace it by a specific toplevel construct, e.g.

including bundles lemma foo: ‹…› if ‹…› for …

including bundles context group
begin

end

including bundles locale bar = …

This looks charming but the progressive participle is reserved for
proofs. For the same reason »with« won't do.

Cheers,
Florian
signature.asc


Last updated: Mar 04 2024 at 12:30 UTC