Email Gateway (Nov 14 2021 at 00:39): Email Gateway (Nov 14 2021 at 00:39):From: Peter Lammich <lammich@in.tum.de>
Hello,
I'm getting an exception
exception Fail raised (line 673 of "variable.ML"): Bad context: clash
of fresh free for bound: :001 vs. xb
from "Sepref_Frame.prepare_fi_conv"
in afp/thys/Refine_Imperative_HOL/Sepref_Frame.thy
I assume that this is due to not sticking to some ominous 'context
discipline'. I tried an analogous fix to what has been done in
Refine_Util.f_tac_conv in
thys/Automatic_Refinement/Lib/Refine_Util.thy, i.e.,
Variable.declare_term just before Goal.prove_internal, and using the
resulting goal_context in the proof tactic, however, the exception
persists.
I'm lost! Can someone please explain what might go wrong here, and how
to debug and track down such errors, or point me to (ideally concise
and understandable) documentation about what 'context discipline'
exactly means.
Email Gateway (Nov 14 2021 at 12:08):From: Peter Lammich <lammich@in.tum.de>
Hi,
after a few hours of guessing and trying to figure out what happens, I
have tracked down the issue to the following dangerous pattern that
violates context discipline, but which, unfortunately, I used a lot.
I'm still trying to figure out a way how to systematically catch them
all, and how to fix it in some cases without potentially introducing
performance regressions.
Pattern:
fun some_conv ctxt = let
val inner_conv = Simplifier.rewrite (ctxt addsimps ...)
in
Conv.params_conv ~1 (K [...] inner_conv) ctxt
end
I probably thought it was a good idea, b/c it keeps the (maybe
expensive?) operations on the context, like adding a lot of simp-
lemmas, out of the conversion (in particular, if [...] applies the
conversion multiple times).
The obvious 'fix' would be to modify the simpset before invoking the
conversion, which, however, easily leads to modularity problems, as in:
fun complicated_inner_conv_reused_from_multiple_places ctxt = let
val ctxt = ctxt addsimps ...
[...]
in
Simplifier.rewrite ctxt
end
I cannot come up with a robust solution here, in particular if more
than one inner_conv is involved.
Last updated: Jul 15 2022 at 23:21 UTC