[isabelle-dev] adhoc overloading: ugly output

[Christian Sternagel]

Oops! You are right, of course. I was so delighted to see the nice 
output for my example that I completely forgot about checking whether 
previously "correct" results of adhoc overloading are still okay.

Thanks for testing and your report! I will have to investigate further ...

cheers

chris

On 01/28/2015 11:54 AM, Dmitriy Traytel wrote:
> 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
>