On 26 October, 2015 10:38 CET, Tobias Nipkow <nip...@in.tum.de> wrote: > My desire to generate code from locale interpretations w/o having to make a > number of trivial function definitions was what started this whole business a > number of years back. Florian's very useful implementation of that really > needs > to make it into Main.
It could simply be integrated with the current interpretation and sublocale commands, where the definitions could be supplied in a separate clause, as suggested by Florian, perhaps using "defines" as keyword. Would this suit your needs? (Independently I intend to change the keyword for the rewrite morphisms clause of these commands from "where" to "rewrites", to better distinguish it from named instantiations in locale expressions.) > My understanding of "sublocale" is that it is an interpretation within a > locale > and I have used that explanation in papers because I find it very succinct. > Thus > I would welcome if the same keyword is used. This view is of course valid, but it isn't the whole story. With "sublocale" these interpretations are orchestrated in a manner such that the locale hierarchy is effectively changed. Now I can see that there might be domains where this more abstract view is not relevant, but when working with a hierarchy of locales representing algebraic structures it is certainly appropriate. It should also be kept in mind that "sublocale" is established in the locale documentation including my JAR paper [1]. If the desire for a different keyword is so strong, perhaps an alias might be a solution. Clemens [1] Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 52(2):123–153, 2014. > On 25/10/2015 11:16, Clemens Ballarin wrote: > > Hi Florian, > > > > this proposal goes too far, of perhaps, not far enough. Let me explain. > > > > There is of course nothing wrong with providing new commands and > > enhancements for frequent use cases. However, I don't see a good reason > > why users should be forced to write 'permanent_interpretation' where they > > could write 'interpretation' or 'sublocale'. > > > > I don't object to a careful evolution of the user interface to locales, but > > I don't think you're heading in the right direction. Your > > 'permanent_interpretation' lets users make some definitions followed by, > > depending on the context, an interpretation or a sublocale declaration. > > This is certainly useful, but it is not general enough for making it the > > preferred command. For example, it doesn't permit function declarations. > > It also blurs the distinction between 'interpretation' and 'sublocale' by > > calling the latter 'permanent_interpretation' when in a locale context, but > > not at the level of theories, but instead calling the former > > 'permanent_interpretation' at the level of theories. > > > > It should be kept in mind that in the current design the 'interpretation' > > commands are effective for the lifetime of their context: in theories they > > are therefore permanent, in context blocks they persist for that block and > > within a proof 'interpret' provides services for that proof. This is > > pretty straightforward. On the other hand, 'locale' and 'sublocale' are > > theory-level commands that relate a locale to a locale expression (which in > > both cases becomes a sublocale of the locale). Their only difference is > > that 'locale' declares a new locale while 'sublocale' refers to an existing > > one. We have allowed the use of 'sublocale' in locale contexts as a > > notational convenience, but I don't consider it a good idea to further blur > > the distinction between 'interpretation' and 'sublocale'. Calling > > 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in > > others is certainly bad. The current design is, of course, not cast in > > stone, but for changing it, there has to be a > consistent vision first, so we know where we are heading. > > > > Certainly, your work has partly been inspired by the feeling that the > > current locale commands only provide the bare basics for manipulating > > locales. For example, basing an interpretation or sublocale declaration on > > definitions is certainly something that could be done in a fancier manner. > > The situation is perhaps a bit similar to that of 'axclass' several years > > ago, where your work on type classes has improved the user experience > > dramatically. If you would like to bring locales forward, you might > > consider developing ideas along those lines. The required definitions and > > proofs for an interpretation could for example be collected in a dedicated > > context in a step-by-step manner similar to that of class instantiation. > > Your work also seems to be inspired by the desire to gradually rename > > 'sublocale' to 'interpretation', which I find surprising, because, compared > > to classes, 'sublocale' is the direct analogue of 'subclass' and > > 'interpretation' is the direct analogue of 'instantiation > '. > > > > Clemens > > > > > > On 13 October, 2015 15:13 CEST, Florian Haftmann > > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > > >> Recently in private discussion there was the question what the supposed > >> future of permanent_interpretation is supposed to be. > >> > >> It looks as follows: > >> Step 1) > >> * Put »permanent_interpretation« into Pure directly. > >> Step 2) > >> * Careful revisiting of the documentation to emphasize the presence of > >> permanent_interpretation. > >> * »permanent_interpretation« as leading construct in the distribution > >> and the AFP as far as appropriate > >> Step 3) > >> * Discontinue theory-global »interpretation«, which then is just a > >> degenerated form of »permanent_interpretation«. > >> * Discontinue locale-level »sublocale«, which then is just a > >> degenerated form of »permanent_interpretation«. > >> > >> There will definitely be one release to breath between step 2 and step 3. > >> Cheers, > >> Florian > >> > >> -- > >> > >> PGP available: > >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > >> > > > > > > > > > > > > > > > > > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
