Hi Clemens, thanks for undertaking this.
I will have a look at this and give feedback. Cheers, Florian Am 27.10.2015 um 18:59 schrieb Clemens Ballarin: > Related to the below discussion on isabelle-users, I have now refined the > patch I had circulated then. Here is the NEWS entry: > > * More gentle suppression of syntax along locale morphisms while > printing terms. Previously 'abbreviation' and 'notation' declarations > > would be suppressed for morphisms (except term identity). Now merely > 'notation' is suppressed. This can be of great help when working with > > complex locale hierarchies, because proof states are displayed much > more succinctly. It also means that only notation needs to be > redeclared if desired, as illustrated by this example: > > locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65) > begin > definition derived (infixl "\<odot>" 65) where ... > end > > locale morphism = > left!: struct composition + right!: struct composition' > for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" > 65) > begin > notation right.derived ("\<odot>''") > end > > The full patch is attached. Interestingly, it is fully compatible also with > the AFP. Since I'm not particularly familiar with generic_target.ML I'm > posting it here for feedback. My intention is to push this in the near > future. > > Clemens > > > On 28 July, 2015 12:12 CEST, Andreas Lochbihler > <andreas.lochbih...@inf.ethz.ch> wrote: > >> Hi Julian, >> >> First of all, I would be very happy if you could solve this problem of >> missing >> contractions. Clemens has never showed me an example where folding of >> abbreviations would >> lead to non-termination. And I do not know precisely how abbreviations and >> locales are >> implemented, so it is hard for me to decide whether something would lead to >> a problem. >> Nevertheless, here is another example: >> >> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a" >> definition (in l) foo where "foo ≡ f (%x. x)" >> interpretation l "id" where "l.foo id == id (%x. x)" sorry >> >> If the interpretation installs abbreviations which respect the rewrite >> morphism, then the >> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it >> does not, then >> "id (%x. x)" is always printed as "foo". This might not be optimal, as the >> right-hand >> sides can be arbitrary general terms that should remain the way they are. >> >> Andreas >> >> On 28/07/15 11:33, Julian Brunner wrote: >>> Hi Andreas, >>> >>> Good call on the overlapping abbreviations, I did not consider this case. >>> However, the >>> conflict already arises with the current implementation. Consider the >>> following: >>> >>> locale foo = >>> fixes f :: "'a => 'a => bool" >>> fixes g :: "'a => 'a => 'a => bool" >>> begin >>> >>> definition test where "test = f" >>> sublocale f!: foo f "% x y z. g y z x" by this >>> >>> end >>> >>> This generates the following abbreviations (they end up in the Consts >>> record in this order): >>> >>> f.test == foo.test f >>> f.f.test == foo.test f >>> test == foo.test f >>> >>> Since 'test' only depends on the parameter f, which is interpreted under >>> the identity >>> morphism (eta contraction seems to matter here, so this does not happen >>> with your original >>> example), all of these abbreviations are set up to be contracted before >>> printing. In fact, >>> 'test' is printed as 'f.test' (presumably due to the order of the >>> abbreviations in the >>> Consts record). >>> >>> Given that these contraction conflicts are already a problem as it is, I do >>> not think that >>> it would make things significantly worse to allow contraction of >>> abbreviations introduced >>> via other morphisms (barring other problems like the one you discussed with >>> Clemens Ballarin). >>> >>> On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler >>> <andreas.lochbih...@inf.ethz.ch >>> <mailto:andreas.lochbih...@inf.ethz.ch>> wrote: >>> >>> Hi Julian, >>> >>> I also regularly suffer from these pretty-printing nightmares, but I >>> vaguely remember a >>> discussion with Clemens Ballarin on the subject. IIRC the problem is >>> that it is not clear >>> whether collapsing the abbreviations terminates in all cases. Clemens >>> has never showed me >>> an example where it actually happens, though. >>> >>> Yet, I can still think of difficult situations as as the following: >>> >>> locale foo = >>> fixes f :: "'a => 'a => bool" >>> and g :: "'a => 'a => 'a => bool" >>> >>> definition (in foo) test where "test = f" >>> >>> sublocale foo ⊆ f: foo "%x y. f y x" "%x y z. g y z x" . >>> >>> This sublocale declaration makes the locale subgraph cyclic, However, >>> the round-up >>> algorithm realises that if you go six times through the circle, the >>> composed parameter >>> instantiations are alpha-beta-eta-equivalent to f and g again, so it >>> stops. That means >>> that the sublocale command adds five copies of foo to itself. Now >>> consider the situation >>> for the abbreviations. We have >>> >>> local.test == foo.test f >>> >>> from the original definition. From the sublocale command, we would also >>> get >>> >>> local.f.test == foo.test (%x y. f y x) >>> local.f.f.test == foo.test f >>> local.f.f.f.test == foo.test (%x y. f y x) >>> local.f.f.f.f.test == foo.test f >>> local.f.f.f.f.f.test == foo.test (%x y. f y x) >>> >>> Obviously, they overlap. So which one should be used by the >>> pretty-printer? >>> >>> Andreas >>> >>> >>> On 27/07/15 21:12, Julian Brunner wrote: >>> > Dear all, >>> > >>> > Isabelle will not contract the abbreviations introduced for locale >>> > definitions when the locale is interpreted through a morphism other >>> than >>> > the identity. This behavior is described in the following threads: >>> > >>> > >>> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-September/msg00040.html >>> > >>> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-January/msg00029.html >>> > >>> > The workaround that is proposed in these threads is to introduce >>> additional >>> > abbreviations after having interpreted the locale. In my >>> formalization, >>> > this would result in so much boilerplate as to make the whole >>> appproach >>> > using locales unusable. Now I'm wondering why this behavior was >>> introduced >>> > in the first place. Since there is no problem with expanding these >>> > abbreviations, why would there be one with contracting them? >>> > >>> > It seems like the reason for the abbreviations not being contracted >>> is that >>> > they use the "internal" print mode. Unfortunately, I was unable to >>> find the >>> > place where the print mode is set on these abbreviations in order to >>> do >>> > more experiments on this. So, before spending more time on this, I >>> wanted >>> > to ask what the original reasons for this behavor were and if it >>> might be >>> > possible to enable contraction of these abbreviations. >>> > >>> >> > > > > > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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