Dear Florian and Peter,
first, sorry for my long silence, I was on holidays.
On 09/20/2013 12:30 AM, Florian Haftmann wrote:
Hi Peter, hi Christian
Referring to Isabelle_12-Sep-2013:
When using overloading from Monad_Syntax, abbreviations are no longer
displayed in output syntax:
is this »no longer« referring to the state of Isabelle2013? Or did it
also go wrong then?
This works as expected with Isabelle2013. Most likely, my recent
localization of adhoc overloading caused the new behavior (which I agree
is not nice). I was not aware of this myself, thanks for bringing it to
my attention.
theory Scratch
imports
Main
"~~/src/HOL/Library/Monad_Syntax"
abbreviation "my_abbrev \<equiv> [True]"
term "foo (Some my_abbrev) f" (* Yields: foo (Some my_abbrev) f *)
term "bind (Some my_abbrev) f" (* Yields: Some [True] >>= f*)
A first analysis:
theory Monad_Syn
imports
Main
"~~/src/Tools/Adhoc_Overloading"
begin
consts
bind :: "['a, 'b ⇒ 'c] ⇒ 'd"
adhoc_overloading
bind Set.bind Predicate.bind Option.bind List.bind
abbreviation "my_abbrev \<equiv> [True]"
term "foo (Some my_abbrev) f" (* Yields: foo (Some my_abbrev) f *)
term "bind (Some my_abbrev) f" (* Yields: bind (Some [True]) f *)
The monad syntax is not to blame, the problem is already in adhoc
overloading.
Using
declare [[show_variants]]
term "foo (Some my_abbrev) f" (* Yields: foo (Some my_abbrev) f *)
term "bind (Some my_abbrev) f" (* Yields: Option.bind (Some
my_abbrev) f *)
Going to the corresponding lines in adhoc_overloading.ML:
fun uncheck ctxt =
if Config.get ctxt show_variants then I
else map (insert_overloaded ctxt);
I roughly guess something in insert_overloaded modifies the term in a
way that the abbreviation does not apply any longer (again, only a rough
guess).
Thanks for the nice analysis.
@Christian: maybe you have a suggestion what is going on here?
At the moment not. I will investigate this issue and come back to the
mailing list as soon as I find out more.
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
