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.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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