--- 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}
--- 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
--- 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 #>
--- 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;