subject:"Re\: \[isabelle\-dev\] adhoc overloading"

Re: [isabelle-dev] adhoc overloading: ugly output

2015-01-29 Thread Florian Haftmann

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

2015-01-28 Thread Dmitriy Traytel


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

2015-01-28 Thread 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
# 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

2015-01-28 Thread Florian Haftmann

  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

Re: [isabelle-dev] adhoc overloading: order inserting overloaded constant

2014-02-01 Thread Makarius


On Sat, 1 Feb 2014, Christian Sternagel wrote:

So my idea was to instead use top-down rewriting (i.e., first replace 
maximal subterms that fit a given pattern). This is what 
Pattern.rewrite_term_top does, right? So after replacing 
rewrite_term by rewrite_term_top, I get the expected results.


Now my question. Can anybody think of a reason why rewrite_term_top 
would not be generally preferable over rewrite_term inside of 
insert_overloaded?


This is an old story.  Printing usually works better top-down, e.g. see 
good old 'translations' with their yo-yo strategy.  When 'abbreviation' 
was introduced, there was Pattern.rewrite_term, but not 
Pattern.rewrite_term_top yet, so there was no other way.


I kept telling Stefan Berghofer about that omission until he made an 
laternative version in 2010: see 6e45e4c94751, 5d2fe4e09354 (with typical 
tell-nothing log entries).


So in analogy, the same will probably work for adhoc_overloading as well, 
without going through all the reasoning again.




If not, could one of the devs incorporate this tiny change please?


OK, I will try this out.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] adhoc overloading: order inserting overloaded constant

2014-02-01 Thread Makarius


On Sat, 1 Feb 2014, Makarius wrote:


 If not, could one of the devs incorporate this tiny change please?


OK, I will try this out.


See now:

changeset:   55237:1e341728bae9
user:wenzelm
date:Sat Feb 01 20:46:19 2014 +0100
files:   src/Tools/adhoc_overloading.ML
description:
prefer top-down rewriting for output (i.e. uncheck), in accordance to term 
abbreviations (see 5d2fe4e09354) and AST translations;



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

28 matches

Mail list logo