# HG changeset patch # User Fabian Huch # Date 1709129955 -3600 # Node ID 2e4518e8a36b110f24ff068cb915cb39a5221be5 # Parent 513829904bebff0cb84638e8a7bf926598addd5b tuned unify trace option names; diff -r 513829904beb -r 2e4518e8a36b src/Doc/Logics/document/HOL.tex --- a/src/Doc/Logics/document/HOL.tex Wed Feb 28 23:50:22 2024 +0100 +++ b/src/Doc/Logics/document/HOL.tex Wed Feb 28 15:19:15 2024 +0100 @@ -177,7 +177,7 @@ guarantee to find instantiations for type variables automatically. Be prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, possibly instantiating type variables. Setting - \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report + \ttindex{Unify.unify_trace_types} to \texttt{true} causes Isabelle to report omitted search paths during unification.\index{tracing!of unification} \end{warn} diff -r 513829904beb -r 2e4518e8a36b src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Feb 28 23:50:22 2024 +0100 +++ b/src/HOL/Tools/try0.ML Wed Feb 28 15:19:15 2024 +0100 @@ -109,12 +109,12 @@ ctxt |> Simplifier_Trace.disable |> Context_Position.set_visible false - |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound) + |> Config.put Unify.unify_trace_bound (Config.get ctxt Unify.search_bound) |> Config.put Argo_Tactic.trace "none" |> Proof_Context.background_theory (fn thy => thy |> Context_Position.set_visible_global false - |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))); + |> Config.put_global Unify.unify_trace_bound (Config.get_global thy Unify.search_bound))); fun generic_try0 mode timeout_opt quad st = let diff -r 513829904beb -r 2e4518e8a36b src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Feb 28 23:50:22 2024 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Feb 28 15:19:15 2024 +0100 @@ -630,10 +630,10 @@ register_config_bool Thm.show_hyps #> register_config_bool Thm.show_tags #> register_config_bool Pattern.unify_trace_failure #> - register_config_int Unify.trace_bound #> register_config_int Unify.search_bound #> - register_config_bool Unify.trace_simp #> - register_config_bool Unify.trace_types #> + register_config_int Unify.unify_trace_bound #> + register_config_bool Unify.unify_trace_simp #> + register_config_bool Unify.unify_trace_types #> register_config_int Raw_Simplifier.simp_depth_limit #> register_config_int Raw_Simplifier.simp_trace_depth_limit #> register_config_bool Raw_Simplifier.simp_debug #> diff -r 513829904beb -r 2e4518e8a36b src/Pure/unify.ML --- a/src/Pure/unify.ML Wed Feb 28 23:50:22 2024 +0100 +++ b/src/Pure/unify.ML Wed Feb 28 15:19:15 2024 +0100 @@ -11,10 +11,10 @@ signature UNIFY = sig - val trace_bound: int Config.T val search_bound: int Config.T - val trace_simp: bool Config.T - val trace_types: bool Config.T + val unify_trace_bound: int Config.T + val unify_trace_simp: bool Config.T + val unify_trace_types: bool Config.T val hounifiers: (string * typ) list -> Context.generic * Envir.env * ((term * term) list) -> (Envir.env * (term * term) list) Seq.seq val unifiers: Context.generic * Envir.env * ((term * term) list) -> @@ -27,17 +27,20 @@ (*Unification options*) -(*tracing starts above this depth, 0 for full*) -val trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50); - (*unification quits above this depth*) val search_bound = Config.declare_int ("unify_search_bound", \<^here>) (K 60); + +(* diagnostics *) + +(*tracing starts above this depth, 0 for full*) +val unify_trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50); + (*print dpairs before calling SIMPL*) -val trace_simp = Config.declare_bool ("unify_trace_simp", \<^here>) (K false); +val unify_trace_simp = Config.declare_bool ("unify_trace_simp", \<^here>) (K false); (*announce potential incompleteness of type unification*) -val trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false); +val unify_trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false); type binderlist = (string * typ) list; @@ -325,7 +328,7 @@ let fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq = let - val trace_types = Config.get_generic context trace_types; + val unify_trace_types = Config.get_generic context unify_trace_types; (*Produce copies of uarg and cons them in front of uargs*) fun copycons uarg (uargs, (env, dpairs)) = Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed')) @@ -342,7 +345,7 @@ fun projenv (head, (Us, bary), targ, tail) = let val env = - if trace_types then test_unify_types context (base, bary) env + if unify_trace_types then test_unify_types context (base, bary) env else unify_types context (base, bary) env in Seq.make (fn () => @@ -584,14 +587,14 @@ fun hounifiers binders (context, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq = let - val trace_bound = Config.get_generic context trace_bound; + val unify_trace_bound = Config.get_generic context unify_trace_bound; + val unify_trace_simp = Config.get_generic context unify_trace_simp; val search_bound = Config.get_generic context search_bound; - val trace_simp = Config.get_generic context trace_simp; fun add_unify tdepth ((env, dpairs), reseq) = Seq.make (fn () => let val (env', flexflex, flexrigid) = - (if tdepth > trace_bound andalso trace_simp + (if tdepth > unify_trace_bound andalso unify_trace_simp then print_dpairs context "Enter SIMPL" (env, dpairs) else (); SIMPL context (env, dpairs)); in @@ -602,14 +605,14 @@ (if Context_Position.is_visible_generic context then warning "Unification bound exceeded" else (); Seq.pull reseq) else - (if tdepth > trace_bound then + (if tdepth > unify_trace_bound then print_dpairs context "Enter MATCH" (env',flexrigid@flexflex) else (); Seq.pull (Seq.it_right (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq)))) end handle CANTUNIFY => - (if tdepth > trace_bound andalso Context_Position.is_visible_generic context + (if tdepth > unify_trace_bound andalso Context_Position.is_visible_generic context then tracing "Failure node" else (); Seq.pull reseq)); val dps = map (fn (t, u) => (binders, t, u)) tus;