[isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Forwarding this error report to the right mailing list ... --- Begin Message --- Referring to Isabelle_12-Sep-2013: When using overloading from Monad_Syntax, abbreviations are no longer displayed in output syntax: theory Scratch imports Main "~~/src/HOL/Library/Monad_Syntax" begin abbreviation "my_abbrev \ [True]" term "foo (Some my_abbrev) f" (* Yields: foo (Some my_abbrev) f *) term "bind (Some my_abbrev) f" (* Yields: Some [True] >>= f*) Note that the abbreviation is not displayed in the second term. Can I somehow get my abbreviations back? Note that this is a VERY ANNOYING behaviour, as it renders the output almost unreadable for larger terms! -- Peter --- End Message --- ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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 \ [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 \ [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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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 \ [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 \ [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
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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 \ [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 \ [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
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
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 # HG changeset patch # User Christian Sternagel # Date 1380546106 -32400 # Mon Sep 30 22:01:46 2013 +0900 # Node ID 1b2bc47df509d6d58dbf7fd8351f6e1f6e9eb736 # Parent c1097679e2955ad7460150e6c4aa8d573ce9b354 preserve types during rewriting diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML +++ b/src/Tools/adhoc_overloading.ML @@ -165,12 +165,15 @@ | _ => oconst) | insert_variants _ _ oconst = oconst; -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); +fun insert_overloaded ctxt = + let +fun proc t = + Term.map_types (K dummyT) t + |> get_overloaded ctxt + |> Option.map (Const o rpair (Term.type_of t)); + in +Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc] + end; fun check ctxt = map (fn t => Term.map_aterms (insert_variants ctxt t) t); ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Am 30.09.2013 um 15:07 schrieb 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). Done. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Thanks Jasmin! @Peter: Does this patch work with your developments as expected? cheers chris On 09/30/2013 10:18 PM, Jasmin Christian Blanchette wrote: Am 30.09.2013 um 15:07 schrieb 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). Done. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
On Di, 2013-10-01 at 14:12 +0900, Christian Sternagel wrote: > Thanks Jasmin! > > @Peter: Does this patch work with your developments as expected? > At first glance, everything looks fine! Thank you for fixing this. -- Peter p.s. I've commited the patch, it's e13b0c88c798 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
