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
