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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
