Theory Code_Utils

theory Code_Utils
imports ML_Utils
begin

ML‹
  fun setup_conditional_functrans binding functrans =
    let
      val enabled = Attrib.setup_config_bool binding (K false)
      val code_functrans = Code_Preproc.simple_functrans (fn ctxt =>
        if Config.get ctxt enabled then
          functrans ctxt
        else
          K NONE)
      val _ = Theory.setup (Code_Preproc.add_functrans (Binding.name_of binding, code_functrans))
    in
      enabled
    end
›

ML_file "pattern_compatibility.ML"
ML_file "dynamic_unfold.ML"

simproc_setup dynamic_unfold ("x") = ‹Dynamic_Unfold.simproc›
declare [[simproc del: dynamic_unfold]]

lemma [code]: ― ‹TODO: work-around non-well-behaved simproc›
  ‹m < 0 ⟷ False›
  ‹m < Suc n ⟷ m ≤ n›
  by auto

setup ‹Code_Preproc.map_pre (Simplifier.add_proc @{simproc dynamic_unfold})›

end