(this continues the previous mail) >>>> 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.
According to my feelings, the whole locale machinery is an excellent and powerful part of the systems. The addition of mixin definitions as special case of mixin rewrites do not touch the foundations (locale.ML / expression.ML) at all – there is no restriction to achieve the same result without them. This implementation simplicity is the main reason I dared to undertake this adventure. > This is certainly useful, but it is not general enough for making it the > preferred command. For example, it doesn't permit function declarations. I don't think this generality is needed. The idea behind mixin definitions could be fomulated as »reinterpret this term as a new definition«; the properties are already there afterwards, there is no need for definitional extensions or construct them. > 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. This could be thought of, but is another story. > 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 > '. You are right with the type class / locale analogy. But type classes only permit the algebraic view, they are too restricted for the »local everything« approach. As mentioned in my previous mail, I am happy to leave both views stand in the long run, if we find a way to sort out the (now still hypothetic) corner cases of epheremal interpretation on the theory level and permanent interpretation in a nested context. -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
