File ‹dynamic_unfold.ML›
signature DYNAMIC_UNFOLD = sig
val enabled: bool Config.T
val simproc: morphism -> Proof.context -> cterm -> thm option
end
structure Dynamic_Unfold : DYNAMIC_UNFOLD = struct
val enabled = Attrib.setup_config_bool @{binding "dynamic_unfold"} (K false)
open Dict_Construction_Util
fun simproc _ ctxt ct =
if Config.get ctxt enabled then
let
val ctxt = Config.put enabled false ctxt
val thy = Proof_Context.theory_of ctxt
val unfold_thms =
all_consts (Thm.term_of ct)
|> filter (not o can dest_funT o snd)
|> map (snd o Code.equations_of_cert thy o Code.get_cert ctxt [] o fst)
|> cat_options
|> flat
|> map (fst o snd)
|> cat_options
in
if null unfold_thms then
NONE
else
SOME (changed_conv (Raw_Simplifier.rewrite ctxt false unfold_thms) ct)
end
else
NONE
end