Re: [isabelle] Best practices for introducing domain specific notation

Hi Alex,

>> * In particular, I saw this pattern in the end of HOL/Library/Perm.thy,
>> which I found interesting.
>>     subsection ‹Syntax›
>>     bundle no_permutation_syntax
>>     begin
>>       no_notation swap    ("⟨_↔_⟩")
>>       no_notation cycle   ("⟨_⟩")
>>       no_notation "apply" (infixl "⟨$⟩" 999)
>>     end
>>     bundle permutation_syntax
>>     begin
>>       notation swap       ("⟨_↔_⟩")
>>       notation cycle      ("⟨_⟩")
>>       notation "apply"    (infixl "⟨$⟩" 999)
>>       no_notation "apply" ("(⟨$⟩)")
>>     end
>>     unbundle no_permutation_syntax
>> This effectively gives users an "on/off" switch, although it is not
>> particularly pretty when the respective (no_)notation declarations are
>> stacked onto each other. A similar thing is done in the end of
>> HOL/Decision_Procs/Approximation.thy and in several places in the AFP.

>> Given the observations above, I think in current Isabelle the best
>> practice for library developers would be:
>> * Provide a canonical entry point for users of your library.
>> * At the end of that entry point, remove any syntax that is specific to
>> your library.
>> * Declare a foo_syntax bundle that users can use to activate the syntax,
>> and possibly also a no_foo_syntax bundle.

thanks for digging into that.

This indeed resembles the state of the art (which is not applied
everywhere, though), with the following disadvantages:

* The switches have to be maintained by hand; at least they are in local
proximity, which is far superior than requiring ad-hoc no_notation
declarations which are fragile since priorities must match exactly etc.
 Extensible bundles would be helpful here.

* There is no way to store global syntax declarations in bundles, see e.
g. Library/Lattice_Syntax.thy.  This is the reason why e. g. lattice
syntax has not been organized using bundles yet.

>> I think locales were built mostly with the logical applications in mind.
>> I would consider their use for just syntax/extra-logical matters an
>> abuse, although that has been common...

Indeed.  The »subscriptive« nature of locales also provides no means for
switching on and off things, the conceptual main distinction between
locales and bundles.


Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.