Re: [isabelle-dev] adhoc overloading: ugly output
Hi Christian, Thanks for pointing this out. While yours is a valid observation, it seems that observing abbrev_mode is not enough to obtain nicer output, i.e., when using 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 (not o can Term.type_of) ts then ts else map (insert_overloaded ctxt) ts; instead of the above, the output of term xs ≤⇩♯ ys stays the same as in my initial post, namely Foo.le_sharp ♯ xs ys i.e. the problem is still open, although the formal gap between abbreviations and ad-hoc overloading got closer. I have this issue on my agenda, though not prioritized. The abbreviation machinery is a delicate issue, and so is the (un)check machinery: it is not compositional, and additions are supposed to work smoothly with all pre-existing plugins here. In similar situations in the past I always did some phyiscal experiments to get some clues what to examine next. The idea is to plug in an (un)checker which does nothing than diagnostic output. Feeding this with terms can give valid inspirations. A tedious issue, of course. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading: ugly output
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
Re: [isabelle-dev] adhoc overloading: ugly output
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
# 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.MLSun Jan 25 22:11:06 2015 +0100
+++ b/src/Tools/adhoc_overloading.MLTue 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 =
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading: ugly output
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; Nb. is_none o try f -- not o can f This got swapped in this patch and is maybe the reason for failing to solve the problem. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] adhoc overloading: ugly output
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
