[isabelle-dev] adhoc overloading: ugly output

[Dmitriy Traytel]

Hi Chris,

I've pushed it to the testboard (and will push it to the repository in 
case of success):

http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac

Cheers,
Dmitriy

On 28.01.2015 09:55, Christian Sternagel wrote:
> It is amazing how easy some things get when a wizard is looking over 
> your shoulder (thanks Florian!). It turns out that adhoc overloading 
> (which is in essence very similar to abbreviations) did not observe 
> some conventions that are followed by the "abbreviation" command.
>
> By peeking into the sources - even without understanding much of it ;) 
> - it can be seen that the flag "abbrev_mode" is checked for 
> abbreviations. By doing the same inside "adhoc_overloading" the ugly 
> output I presented earlier, turned into beautiful symbols.
>
> Could one of the developers be so kind to apply the attached (mq) 
> patch (after testing it of course) ;) ?
>
> cheers
>
> chris
>
> On 01/16/2015 02:40 PM, Christian Sternagel wrote:
>> Here is a related thread
>>
>>
>> https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html 
>>
>>
>>
>> which was originated by myself ;) (how embarassing).
>>
>> cheers
>>
>> chris
>>
>> On 01/16/2015 02:35 PM, Christian Sternagel wrote:
>>> Dear all,
>>>
>>> in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
>>> using adhoc overloading together with abbreviations is not optimal
>>> (maybe this was already discovered before but I forgot about it). Now,
>>> it turns out that the same issue (at least superficially it's the same,
>>> but maybe caused by different reasons) arises also for definitions in
>>> local theory contexts (or are those the same as mere abbreviations?).
>>>
>>> Let me illustrate what I'm talking about by the following example:
>>>
>>> theory Foo
>>> imports
>>>    Main
>>>    "~~/src/Tools/Adhoc_Overloading"
>>> begin
>>>
>>> consts SHARP :: "'a ⇒ 'b" ("♯")
>>>
>>> context
>>>    fixes shp :: "'a ⇒ 'a"
>>> begin
>>>
>>> adhoc_overloading
>>>    SHARP shp
>>>
>>> definition le_sharp (infix "≤⇩♯" 50)
>>> where
>>>    "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"
>>>
>>> term "xs ≤⇩♯ ys"
>>> text ‹
>>>    Result in @{term "Foo.le_sharp ♯ xs ys"} instead of
>>>    more desirable @{term "xs ≤⇩♯ ys"}. (The same happens
>>>    when we turn the above definition into an abbreviation.)
>>> ›
>>>
>>> end
>>>
>>> text ‹
>>>    In the "global" theory this also happens, but only for
>>>    abbreviations, not for definitions.
>>> ›
>>>
>>> definition "shp = id"
>>>
>>> adhoc_overloading SHARP shp
>>>
>>> definition le_sharp' (infix "≤⇩♯" 50)
>>> where
>>>    "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"
>>>
>>> term "xs ≤⇩♯ ys"
>>>
>>> end
>>>
>>> Unfortunately, at the moment I do not have time to look into adhoc
>>> overloading myself, but let this thread be a reminder. If anybody else
>>> can provide explanations/comments/solutions, please go ahead!
>>>
>>> cheers
>>>
>>> chris
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150128/79d26630/attachment-0002.html>