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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
