# HG changeset patch # User Fabian Huch # Date 1709137554 -3600 # Node ID 3648e9c88d0cdfd8df96a246242539820dc295d2 # Parent 2e4518e8a36b110f24ff068cb915cb39a5221be5 add option for unify trace (now disabled by default as printing is excessive and rarely used); diff -r 2e4518e8a36b -r 3648e9c88d0c NEWS --- a/NEWS Wed Feb 28 15:19:15 2024 +0100 +++ b/NEWS Wed Feb 28 17:25:54 2024 +0100 @@ -62,6 +62,11 @@ transp_on_multp +*** Pure *** + +* Added configuration option for unifier tracing, which is now disabled by default. + + *** ML *** * ML antiquotation "try" provides variants of exception handling that diff -r 2e4518e8a36b -r 3648e9c88d0c src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Wed Feb 28 15:19:15 2024 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Wed Feb 28 17:25:54 2024 +0100 @@ -1826,6 +1826,7 @@ text \ \begin{tabular}{rcll} + @{attribute_def unify_trace} & : & \attribute\ & default \false\ \\ @{attribute_def unify_trace_simp} & : & \attribute\ & default \false\ \\ @{attribute_def unify_trace_types} & : & \attribute\ & default \false\ \\ @{attribute_def unify_trace_bound} & : & \attribute\ & default \50\ \\ @@ -1837,10 +1838,13 @@ but sometimes needs extra care to identify problems. These tracing options may help. + \<^descr> @{attribute unify_trace} controls whether unify trace messages will be + printed (controlled via more fine-grained tracing options below). + \<^descr> @{attribute unify_trace_simp} controls tracing of the simplification phase of higher-order unification. - \<^descr> @{attribute unify_trace_types} controls warnings of + \<^descr> @{attribute unify_trace_types} controls tracing of potential incompleteness, when unification is not considering all possible instantiations of schematic type variables. diff -r 2e4518e8a36b -r 3648e9c88d0c src/Doc/Logics/document/HOL.tex --- a/src/Doc/Logics/document/HOL.tex Wed Feb 28 15:19:15 2024 +0100 +++ b/src/Doc/Logics/document/HOL.tex Wed Feb 28 17:25:54 2024 +0100 @@ -176,9 +176,10 @@ Where function types are involved, Isabelle's unification code does not 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.unify_trace_types} to \texttt{true} causes Isabelle to report - omitted search paths during unification.\index{tracing!of unification} + possibly instantiating type variables. Setting \ttindex{Unify.unify_trace} + in combination with \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 2e4518e8a36b -r 3648e9c88d0c src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Feb 28 15:19:15 2024 +0100 +++ b/src/HOL/Tools/try0.ML Wed Feb 28 17:25:54 2024 +0100 @@ -109,12 +109,12 @@ ctxt |> Simplifier_Trace.disable |> Context_Position.set_visible false - |> Config.put Unify.unify_trace_bound (Config.get ctxt Unify.search_bound) + |> Config.put Unify.unify_trace false |> Config.put Argo_Tactic.trace "none" |> Proof_Context.background_theory (fn thy => thy |> Context_Position.set_visible_global false - |> Config.put_global Unify.unify_trace_bound (Config.get_global thy Unify.search_bound))); + |> Config.put_global Unify.unify_trace false)); fun generic_try0 mode timeout_opt quad st = let diff -r 2e4518e8a36b -r 3648e9c88d0c src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Feb 28 15:19:15 2024 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Feb 28 17:25:54 2024 +0100 @@ -631,6 +631,7 @@ register_config_bool Thm.show_tags #> register_config_bool Pattern.unify_trace_failure #> register_config_int Unify.search_bound #> + register_config_bool Unify.unify_trace #> register_config_int Unify.unify_trace_bound #> register_config_bool Unify.unify_trace_simp #> register_config_bool Unify.unify_trace_types #> diff -r 2e4518e8a36b -r 3648e9c88d0c src/Pure/unify.ML --- a/src/Pure/unify.ML Wed Feb 28 15:19:15 2024 +0100 +++ b/src/Pure/unify.ML Wed Feb 28 17:25:54 2024 +0100 @@ -12,6 +12,7 @@ signature UNIFY = sig val search_bound: int Config.T + val unify_trace: bool Config.T val unify_trace_bound: int Config.T val unify_trace_simp: bool Config.T val unify_trace_types: bool Config.T @@ -33,6 +34,8 @@ (* diagnostics *) +val unify_trace = Config.declare_bool ("unify_trace", \<^here>) (K false); + (*tracing starts above this depth, 0 for full*) val unify_trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50); @@ -42,6 +45,11 @@ (*announce potential incompleteness of type unification*) val unify_trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false); +fun cond_tracing ctxt msg = + if Config.get_generic ctxt unify_trace andalso Context_Position.is_visible_generic ctxt then + tracing (msg ()) + else (); + type binderlist = (string * typ) list; @@ -181,13 +189,11 @@ fun test_unify_types context (T, U) env = let - fun trace () = - if Context_Position.is_visible_generic context then - let val str_of = Syntax.string_of_typ (Context.proof_of context) - in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end - else (); + fun msg () = + let val str_of = Syntax.string_of_typ (Context.proof_of context) + in "Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T end val env' = unify_types context (T, U) env; - in if is_TVar T orelse is_TVar U then trace () else (); env' end; + in if is_TVar T orelse is_TVar U then cond_tracing context msg else (); env' end; (*Is the term eta-convertible to a single variable with the given rbinder? Examples: ?a ?f(B.0) ?g(B.1,B.0) @@ -568,17 +574,18 @@ In t \ u print u first because it may be rigid or flexible -- t is always flexible.*) fun print_dpairs context msg (env, dpairs) = - if Context_Position.is_visible_generic context then - let - fun pdp (rbinder, t, u) = - let - val ctxt = Context.proof_of context; - fun termT t = - Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); - val prt = Pretty.blk (0, [termT u, Pretty.str " \\<^sup>?", Pretty.brk 1, termT t]); - in tracing (Pretty.string_of prt) end; - in tracing msg; List.app pdp dpairs end - else (); + let + fun pdp (rbinder, t, u) = + let + val ctxt = Context.proof_of context; + fun termT t = + Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); + val prt = Pretty.blk (0, [termT u, Pretty.str " \\<^sup>?", Pretty.brk 1, termT t]); + in Pretty.string_of prt end; + in + cond_tracing context (fn () => msg); + List.app (fn dp => cond_tracing context (fn () => pdp dp)) dpairs + end; (*Unify the dpairs in the environment. @@ -602,8 +609,9 @@ [] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq) | dp :: frigid' => if tdepth > search_bound then - (if Context_Position.is_visible_generic context - then warning "Unification bound exceeded" else (); Seq.pull reseq) + (if Context_Position.is_visible_generic context then + warning "Unification bound exceeded -- see unify trace for details" + else (); Seq.pull reseq) else (if tdepth > unify_trace_bound then print_dpairs context "Enter MATCH" (env',flexrigid@flexflex) @@ -612,8 +620,8 @@ (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq)))) end handle CANTUNIFY => - (if tdepth > unify_trace_bound andalso Context_Position.is_visible_generic context - then tracing "Failure node" + (if tdepth > unify_trace_bound + then cond_tracing context (fn () => "Failure node") else (); Seq.pull reseq)); val dps = map (fn (t, u) => (binders, t, u)) tus; in add_unify 1 ((env, dps), Seq.empty) end;