[isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]

[Christian Sternagel]

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