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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
