[isabelle-dev] adhoc overloading: ugly output

[Dmitriy Traytel]

Hi,

after looking a little bit closer at the proposed patch, I doubt that it 
has the desired effect: it basically disables the uncheck phase almost 
always (e.g. for term and lemma). Consider:

consts T :: 'a
adhoc_overloading T True
declare[[show_variants = false]]
term T

The term command will show True (=the expected output with show_variants 
= true), whereas T is expected with show_variants = false.

Cheers,
Dmitriy

On 28.01.2015 10:40, Dmitriy Traytel wrote:
> 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
>
>
>
> _______________________________________________
> 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/6b93af2c/attachment-0002.html>