Email Gateway (Aug 19 2022 at 16:56): Email Gateway (Aug 19 2022 at 16:56):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear list,
For debugging purposes, I'd like to disable the simprocs from the record package.
Otherwise, the simplifier trace with [[simp_debug]] is obfuscated by the trace of these
simprocs. I tried [[simproc del: "record" record_eq record_upd]], but I only get the error
message that none of the simprocs exist. Next, I tried
local_setup {*
fn ctxt => ctxt delsimprocs [Record.simproc, Record.eq_simproc, Record.upd_simproc]
*}
Then, print_simpset no longer lists these simprocs. Nevertheless, they still show up in
the trace. Here's an example:
lemma "foo" using [[simp_debug]] apply(simp)
So, how can I get rid of these simprocs?
By the way, does the new tracing facility for the simplifier provide control over
simprocs, too?
Best,
Andreas
Email Gateway (Aug 19 2022 at 16:56):From: Makarius <makarius@sketis.net>
On Thu, 15 Jan 2015, Andreas Lochbihler wrote:
I tried
local_setup {*
fn ctxt => ctxt delsimprocs [Record.simproc, Record.eq_simproc,
Record.upd_simproc]
*}Then, print_simpset no longer lists these simprocs.
The 'local_setup' command operates on a local_theory, but above you merely
downgrade it to a Proof.context, i.e. only the so-called "auxiliary
context" is affected, and the update is not really persistent.
In contrast, the 'declaration' command is the usual way to update a
local_theory via ML declarations. This is how it works for the above
application:
declaration ‹
K (Simplifier.map_ss
(fn ctxt => ctxt delsimprocs [Record.simproc, Record.eq_simproc, Record.upd_simproc]))
›
Since the canonical way to maintain the Simplifier context via ML has
changed several times over the years, I had to do myself a standard
hypersearch to find current applications in the sources, e.g. addsimprocs,
addloop.
In a global theory situation it is also possible to use this form:
setup ‹map_theory_simpset
(fn ctxt => ctxt delsimprocs [Record.simproc, Record.eq_simproc, Record.upd_simproc])›
By the way, does the new tracing facility for the simplifier provide
control over simprocs, too?
Not yet.
Makarius
Email Gateway (Aug 19 2022 at 16:57):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
Thanks a lot, this works fine. Just out of curiosity: Why does the Isar declaration
[[simproc del: record_eq]] not work?
Cheers,
Andreas
Email Gateway (Aug 19 2022 at 16:57):From: Makarius <makarius@sketis.net>
The record package is not localized, which means it uses quite old
operations like Simplifier.simproc_global (or Simplifier.mk_simproc and
the bottom of it).
In order to show up in the simproc name space within the context, tools
need to use Simplifier.def_simproc or the corresponding Isar command
'simproc_setup'.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC