On 10/22/2012 08:22 AM, Lukas Bulwahn wrote:
I had a further look at the issue with the "Simplifier: renamed bound variable" to repair the set_comprehension_pointfree simproc and to turn the warning into an error for the future.On 10/19/2012 04:35 PM, Makarius wrote:On the weekend, I had a look at this issue in the set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and already noticed what could make things difficult turning this into an error.On Fri, 19 Oct 2012, Lukas Bulwahn wrote:Operations like Simplifier.context, Simplifier.inherit_context should help here. Once that is repaired, I will see if the warning can now be made an error that is more explicit about the reasons.I am certainly in favour of this. First, tool developers mainly react on errors with test runs, but do not see the warnings. Secondly, users do not know who to report those warnings and do not know if they are caused by their scripts or the tools.Historically, the weak warning was a necessity due to too many simprocs still not working with the context.Let's hope that it can be easily switched to an explicit error after so many years now.Two examples:- the hypsubst_tac internally uses the simplifier, but the interface does not allow to pass the current simpset to this tactic. - An implementer has to avoid certain functions, such asRaw_Simplifier.rewrite, that assume to be used only in a non-nested context.
However, I was very surprised that the warning occurs even if I pass around the context following typical Isabelle programming idioms.
To state my expectation more formally: For every simpset ss and ss', I would expectSimplifier.context (Simplifier.the_context ss) ss' == Simplifier.inherit_context ss ss'
Attached, there is an simple example that shows a warning for "Simplifier.context (Simplifier.the_context ss)", but it does not for Simplifier.inherit_context ss.
Looking at the code of the simplifier, I did understand my misunderstanding:It is NOT ONLY "working with the context" correctly, but also "passing around the simpset" correctly---a programming paradigm that I (and probably many others) are not aware of.
Lukas
Scratch.thy
Description: application/isabelle-theory
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
