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

[Christian Sternagel]

Some more details:

until 0d0c20a0a34f we have the expected behavior. With

changeset:   52622:e0ff1625e96d
user:        wenzelm
date:        Fri Jul 12 16:19:05 2013 +0200
summary:     localized and modernized adhoc-overloading (patch by 
Christian Sternagel);

term "bind (Some my_abbrev) f"

is not accepted at all (red, but no error message; but I think this is 
an orthogonal issue of implicit assumptions on my side that where not 
correct and which was resolved in the meanwhile). Nevertheless, this is 
the changeset I suspect to introduce the new behavior, since here the 
implementation of "insert_internal_same" (which is now called 
"insert_overloaded") is drastically changed.

Before this changeset variants are always Consts and thus replacing 
variants with their overloaded constant is easily done by 
pattern-matching on variants.

After this changeset, variants may be arbitrary terms (due to 
localization). Now replacing a variant by the corresponding overloaded 
constant is done by rewriting (as Florian already pointed out, this 
happens in "insert_overloaded") as follows

   fun insert_overloaded ctxt variant =
     (case try Term.type_of variant of
       NONE => variant
     | SOME T =>
       Pattern.rewrite_term (Proof_Context.theory_of ctxt) []
         [Option.map (Const o rpair T) o
         get_overloaded ctxt o Term.map_types (K dummyT)] variant);

Apparently this interferes with abbreviations. Am I doing anything 
strange here?

cheers

chris

On 09/24/2013 01:06 PM, Christian Sternagel wrote:
> 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
>
>
>
>