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

[Florian Haftmann]

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?

> 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).

@Christian: maybe you have a suggestion what is going on here?

@Peter: »uncheck« would be the entrance point for further investigation.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130919/c5360b2c/attachment.sig>