[isabelle-dev] adhoc overloading: ugly output

[Christian Sternagel]

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
-------------- next part --------------
# HG changeset patch
# Parent 4427f04fca57ea90f7fd8dbc271ac29a9268ec75
adhoc overloading must follow the same conventions as abbreviations

diff -r 4427f04fca57 -r fbefd978e72d src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Sun Jan 25 22:11:06 2015 +0100
+++ b/src/Tools/adhoc_overloading.ML	Tue Jan 27 13:59:16 2015 +0100
@@ -179,7 +179,9 @@
   map (fn t => Term.map_aterms (insert_variants ctxt t) t);
 
 fun uncheck ctxt ts =
-  if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
+  if Proof_Context.abbrev_mode ctxt orelse
+    Config.get ctxt show_variants orelse
+    exists (can Term.type_of) ts then ts
   else map (insert_overloaded ctxt) ts;
 
 fun reject_unresolved ctxt =