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

[Christian Sternagel]

It seems that the required changes are minimal. See the attached patch. 
To be on the safe side: could somebody push this to the test server (in 
my local tests I just loaded all theories from the Isabelle repo and the 
AFP that contained the keyword "adhoc_overloading" in Isabelle/jEdit 
instead of building all heap images).

cheers

chris

On 09/30/2013 08:50 PM, Christian Sternagel wrote:
> On 09/30/2013 07:33 PM, Makarius wrote:
>> On Tue, 24 Sep 2013, Christian Sternagel wrote:
>>
>>> 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?
>>
>> I've looked only briefly so far.  Abbreviations are only contracted for
>> type-correct terms, but above that information is not fully preserved.
>>
>> Pattern.rewrite_term needs to re-used the type of the replaced subterm
>> (within the proc), not the overall type of the term called "variant"
>> above.
>
> Thanks! That's a valuable hint. I will look into it and hope to make
> adhoc overloading and abbreviations produce the expected results again,
> before the release.
>
> cheers
>
> chris
>
>>
>>
>>      Makarius
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: adhoc_overloading_and_abbreviations.patch
Type: text/x-patch
Size: 1091 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130930/de886ffa/attachment-0002.bin>