problem with bundles for notation

[maxhaslbeck]

Peter comments:

problem with bundles is, they cannot be extended (or has this changed already?) So you cannot use your own basic syntax in your theory, unless you use very fine-grained bundle structure. I usually use locales instead, which can be interpreted on demand. (Drawback: the syntax cannot be "undone" in an unstructured way, as with a no-syntax bundle. Only the structured way, e.g., context begin interpret ... end) works.

[kappelmann]

I think I do not understand the problem setting well enough to work on this. What's the use case for extending bundles? To make it easier to get all notation from a given theory? Does this happen a lot? Is it a big burden in practice if one has to explicitly state each notation individually?

A benefit I see from using contexts is that one cannot forget to disable unbundled notations again, right?

What's your thought on this @maxhaslbeck ?

[wimmers]

For bundles that involve fact declarations, it may indeed be useful to extend them. For notation, I would guess that the use does typically not arise? At least I do not know of such examples? My assumption would be that all of your definitions with notation can go into a basic theory and then you can declare your bundle at the end of that theory.

There are not many disadvantages to the contexts I suppose, besides introducing a bit more syntactic clutter.

[kappelmann]

This seems to work for me and maybe is a good solution?

bundle nat_zero_syntax begin notation nat_zero ("0") end
bundle no_nat_zero_syntax begin no_notation nat_zero ("0") end

bundle nat_one_syntax begin notation nat_one ("1") end
bundle no_nat_one_syntax begin no_notation nat_one ("1") end

bundle nat_syntax
begin
  unbundle nat_zero_syntax
  unbundle nat_one_syntax
end

bundle no_nat_syntax
begin
  unbundle no_nat_zero_syntax
  unbundle no_nat_one_syntax
end

unbundle nat_syntax

One could also readily write some ML to make this more automatic and concise.

[maxhaslbeck]

I think the minimum thing to demand in the community guidelines is that one should use bundles for syntax, and also provide no_syntax bundles. That's already included.

I would not restrict further how people should do that and how fine-grained they should define their bundles.

Getting "extendable bundles" with locales and using them in an structured way (context begin interpret end) as Peter suggests fits better into the cook book.

I'd acknowledge the issue but would leave it as is.

[kappelmann]

I agree. It might be nice to add a more sophisticated approach in the cookbook and just refer it here in the future.