From 30798e6d63dcaac08e2ff259f44b15e421029a33 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 6 May 2024 06:06:03 +0200 Subject: [PATCH 1/3] An attempt to make printing of unsatisfiable constraints more readable. It includes more uniformity (same no-quotes for hypotheses and evars) and better space management when going to the next line. --- engine/termops.ml | 4 ++-- test-suite/output/ClassMissingInstance.out | 6 ++---- test-suite/output/bug_13942.out | 8 ++------ vernac/himsg.ml | 9 +++++---- 4 files changed, 11 insertions(+), 16 deletions(-) diff --git a/engine/termops.ml b/engine/termops.ml index 70b3de4777b0..38c4616a062c 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -337,12 +337,12 @@ let pr_evar_constraints sigma pbs = naming/renaming. *) Namegen.make_all_name_different env sigma in - print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++ + hov 2 (hov 2 (print_env_short env sigma) ++ spc () ++ str "|-" ++ spc () ++ Internal.print_kconstr env sigma t1 ++ spc () ++ str (match pbty with | Conversion.CONV -> "==" | Conversion.CUMUL -> "<=") ++ - spc () ++ Internal.print_kconstr env sigma t2 + spc () ++ Internal.print_kconstr env sigma t2) in prlist_with_sep fnl pr_evconstr pbs diff --git a/test-suite/output/ClassMissingInstance.out b/test-suite/output/ClassMissingInstance.out index 69941eea510e..dd2374ad918e 100644 --- a/test-suite/output/ClassMissingInstance.out +++ b/test-suite/output/ClassMissingInstance.out @@ -1,8 +1,6 @@ File "./output/ClassMissingInstance.v", line 7, characters 0-28: The command has indeed failed with message: Unable to satisfy the following constraints: +?arg_2 : Foo 1 -?arg_2 : "Foo 1" - -?arg_20 : "Foo 2" - +?arg_20 : Foo 2 diff --git a/test-suite/output/bug_13942.out b/test-suite/output/bug_13942.out index 67a9f4603986..b7fd9561edc4 100644 --- a/test-suite/output/bug_13942.out +++ b/test-suite/output/bug_13942.out @@ -119,14 +119,11 @@ ifalse : Choose false -> Union (M B) itrue : Choose true -> Union (M B) ib : Insert K B (M B) i : Choose false -> Union (M A) +?hi : Insert K ?A (M ?A) -?hi : "Insert K ?A (M ?A)" - -?hu : "Union (M ?A)" - +?hu : Union (M ?A) File "./output/bug_13942.v", line 145, characters 16-18: The command has indeed failed with message: - Could not find an instance for "Union (M B)" in environment: K : Type @@ -143,7 +140,6 @@ fi fu : B : B File "./output/bug_13942.v", line 307, characters 20-31: The command has indeed failed with message: - Could not find an instance for "Insert K K (M A)" in environment: K : Type diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 4bf964bfcc42..ba252bc2a265 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -682,7 +682,7 @@ let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr env sigma (Evd.evar_concl evi) with | Some _ -> let env = Evd.evar_filtered_env env evi in - fnl () ++ str "Could not find an instance for " ++ + str "Could not find an instance for " ++ pr_leconstr_env env sigma (Evd.evar_concl evi) ++ pr_trailing_ne_context_of env sigma | _ -> mt() @@ -975,10 +975,11 @@ let pr_constraints printenv env sigma evars cstrs = pr_ne_context_of (str "In environment:") env' sigma else mt () in + let env = Global.env () in let evs = - prlist - (fun (ev, evi) -> fnl () ++ pr_existential_key (Global.env ()) sigma ev ++ - str " : " ++ pr_leconstr_env env' sigma (Evd.evar_concl evi) ++ fnl ()) l + prlist_with_sep (fun () -> fnl () ++ fnl ()) + (fun (ev, evi) -> hov 2 (pr_existential_key env sigma ev ++ + str " :" ++ spc () ++ Printer.pr_leconstr_env env' sigma (Evd.evar_concl evi))) l in h (pe ++ evs ++ pr_evar_constraints sigma cstrs) else From 6f9ff6e3fc20624a4b4d6befff6856043e75201b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 6 May 2024 06:22:18 +0200 Subject: [PATCH 2/3] Do not print unresolved constraints when there are only evars. --- test-suite/output/ClassMissingInstance.out | 2 +- test-suite/output/bug_13942.out | 2 +- vernac/himsg.ml | 8 ++++++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/test-suite/output/ClassMissingInstance.out b/test-suite/output/ClassMissingInstance.out index dd2374ad918e..6683ae007465 100644 --- a/test-suite/output/ClassMissingInstance.out +++ b/test-suite/output/ClassMissingInstance.out @@ -1,6 +1,6 @@ File "./output/ClassMissingInstance.v", line 7, characters 0-28: The command has indeed failed with message: -Unable to satisfy the following constraints: +Could not find an instance for the following existential variables: ?arg_2 : Foo 1 ?arg_20 : Foo 2 diff --git a/test-suite/output/bug_13942.out b/test-suite/output/bug_13942.out index b7fd9561edc4..bd71e5140ed5 100644 --- a/test-suite/output/bug_13942.out +++ b/test-suite/output/bug_13942.out @@ -108,7 +108,7 @@ More precisely: i : Union (M A) File "./output/bug_13942.v", line 140, characters 2-20: The command has indeed failed with message: -Unable to satisfy the following constraints: +Could not find an instance for the following existential variables: In environment: K : Type M : Type -> Type diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba252bc2a265..7d9a02690e8c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1000,8 +1000,12 @@ let explain_unsatisfiable_constraints env sigma constr comp = in match constr with | None -> - str "Unable to satisfy the following constraints:" ++ fnl () ++ - pr_constraints true env sigma undef constraints + if List.is_empty constraints then + str "Could not find an instance for the following existential variables:" ++ fnl () ++ + pr_constraints true env sigma undef constraints + else + str "Unable to satisfy the following constraints:" ++ fnl () ++ + pr_constraints true env sigma undef constraints | Some (ev, k) -> let cstr = let remaining = Evar.Map.remove ev undef in From bd854794efc470e4b727ca6f378047e15b77876c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 May 2024 12:55:53 +0200 Subject: [PATCH 3/3] When printing unresolved constraints, print "In environment" beforehand. --- test-suite/output/bug_13942.out | 2 +- vernac/himsg.ml | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/test-suite/output/bug_13942.out b/test-suite/output/bug_13942.out index bd71e5140ed5..b6bb3a0c6edc 100644 --- a/test-suite/output/bug_13942.out +++ b/test-suite/output/bug_13942.out @@ -108,7 +108,6 @@ More precisely: i : Union (M A) File "./output/bug_13942.v", line 140, characters 2-20: The command has indeed failed with message: -Could not find an instance for the following existential variables: In environment: K : Type M : Type -> Type @@ -119,6 +118,7 @@ ifalse : Choose false -> Union (M B) itrue : Choose true -> Union (M B) ib : Insert K B (M B) i : Choose false -> Union (M A) +Could not find an instance for the following existential variables: ?hi : Insert K ?A (M ?A) ?hu : Union (M ?A) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 7d9a02690e8c..a78edad48d2f 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -963,7 +963,7 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1 pr_leconstr_env env sigma t1 ++ strbrk " at position " ++ pr_position (cl1,pos1) ++ str "." -let pr_constraints printenv env sigma evars cstrs = +let pr_constraints printenv msg env sigma evars cstrs = let (ev, evi) = Evar.Map.choose evars in if Evar.Map.for_all (fun ev' evi' -> eq_named_context_val (Evd.evar_hyps evi) (Evd.evar_hyps evi')) evars @@ -981,7 +981,7 @@ let pr_constraints printenv env sigma evars cstrs = (fun (ev, evi) -> hov 2 (pr_existential_key env sigma ev ++ str " :" ++ spc () ++ Printer.pr_leconstr_env env' sigma (Evd.evar_concl evi))) l in - h (pe ++ evs ++ pr_evar_constraints sigma cstrs) + h (pe ++ str msg ++ fnl () ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter env sigma @@ -1001,17 +1001,17 @@ let explain_unsatisfiable_constraints env sigma constr comp = match constr with | None -> if List.is_empty constraints then - str "Could not find an instance for the following existential variables:" ++ fnl () ++ - pr_constraints true env sigma undef constraints + let msg = "Could not find an instance for the following existential variables:" in + pr_constraints true msg env sigma undef constraints else - str "Unable to satisfy the following constraints:" ++ fnl () ++ - pr_constraints true env sigma undef constraints + let msg = "Unable to satisfy the following constraints:" in + pr_constraints true msg env sigma undef constraints | Some (ev, k) -> let cstr = let remaining = Evar.Map.remove ev undef in if not (Evar.Map.is_empty remaining) then - str "With the following constraints:" ++ fnl () ++ - pr_constraints false env sigma remaining constraints + let msg = "With the following constraints:" in + pr_constraints false msg env sigma remaining constraints else mt () in let info = Evar.Map.find ev undef in