From c543bdac98d5f14a9e8e7fb45ff3fb6acb437827 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Feb 2022 13:22:44 -0800 Subject: [PATCH] Better error messages Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [#378, #381, #384] != [#101, #106, #108] index 0: #378 != #101 (slice 0 44, [#377]) != (slice 0 44, [#98]) index 0: #377 != #98 (add 64, [#345, #375]) != (add 64, [#57, #96]) index 0: #345 != #57 (slice 0 44, [#337]) != (slice 0 44, [#44]) index 0: #337 != #44 (add 64, [#41, #334]) != (add 64, [#25, #41]) index 1: #334 != #25 (mul 64, [#1, #331]) != (mul 64, [#0, #1, #22]) [(add 64, [#329, #329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, #328]), (mul 64, [#7, #328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, #327])]), (mul 64, [(const 2, []), (add 64, [#0, #327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level? --- src/Assembly/Equivalence.v | 37 +++++++++++++++++++++---------------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index 671e448af34..1fde88471b0 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -158,17 +158,26 @@ Fixpoint remove_common_indices {T} (eqb : T -> T -> bool) (xs ys : list T) (star else ((start_idx, x) :: xs', ys') end. -Fixpoint explain_array_unification_error_without_commutativity +Definition show_expr_node_lite : Show Symbolic.expr + := fix show_expr_node_lite (e : Symbolic.expr) : string + := match e with + | ExprRef i => "#" ++ show i + | ExprApp (op, e) + => "(" ++ show op ++ ", " ++ @show_list _ show_expr_node_lite e ++ ")" + end%string. + +Fixpoint explain_array_unification_error_single (singular plural : string) (left_descr right_descr : string) (explain_idx_unification_error : idx -> idx -> list string) (describe_idx : idx -> list string) + (modulo_commutativity : bool) (asm_array PHOAS_array : list idx) (start_idx : nat) : list string - := let recr := explain_array_unification_error_without_commutativity singular plural left_descr right_descr explain_idx_unification_error describe_idx in + := let recr := explain_array_unification_error_single singular plural left_descr right_descr explain_idx_unification_error describe_idx modulo_commutativity in match asm_array, PHOAS_array with | [], [] - => ["Internal Error: Unifiable " ++ plural] + => ["Internal Error: Unifiable " ++ plural ++ (if modulo_commutativity then " modulo commutativity" else "")] | [], PHOAS_array => ((["The " ++ right_descr ++ " " ++ singular ++ " contains " ++ show (List.length PHOAS_array) ++ " more values than the " ++ left_descr ++ " " ++ singular ++ "."]%string) ++ List.flat_map describe_idx PHOAS_array)%list @@ -179,9 +188,13 @@ Fixpoint explain_array_unification_error_without_commutativity => if Decidable.dec (asm_value = PHOAS_value) then recr asm_array PHOAS_array (S start_idx) else - ((["index " ++ show start_idx ++ ": #" ++ show asm_value ++ " != #" ++ show PHOAS_value]%string) - ++ explain_idx_unification_error asm_value PHOAS_value - )%list + if modulo_commutativity && List.existsb (N.eqb asm_value) PHOAS_array + then + recr asm_array (PHOAS_value :: List.removen (N.eqb asm_value) PHOAS_array 1) (S start_idx) + else + ((["index " ++ show start_idx ++ ": " ++ show_expr_node_lite (ExprRef asm_value) ++ " != " ++ show_expr_node_lite (ExprRef PHOAS_value)]%string) + ++ explain_idx_unification_error asm_value PHOAS_value + )%list end%string%list%bool. Definition recursive_deps_list_step @@ -256,14 +269,6 @@ Definition indices_at_leaves_map (ls : list Symbolic.expr) : list idx Definition indices_at_leaves (e : Symbolic.expr) : list idx := indices_at_leaves_map [e]. -Definition show_expr_node_lite : Show Symbolic.expr - := fix show_expr_node_lite (e : Symbolic.expr) : string - := match e with - | ExprRef i => "#" ++ show i - | ExprApp (op, e) - => "(" ++ show op ++ ", " ++ @show_list _ show_expr_node_lite e ++ ")" - end%string. - Fixpoint make_iteratively_revealed_exprs (dag : dag) (max_depth : nat) @@ -341,7 +346,7 @@ Definition explain_array_unification_error (modulo_commutativity : bool) (asm_array PHOAS_array : list idx) : list string - := if modulo_commutativity + := if (modulo_commutativity && negb (List.length asm_array =? List.length PHOAS_array))%nat%bool then match remove_common_indices N.eqb asm_array PHOAS_array 0 with | ([], []) @@ -361,7 +366,7 @@ Definition explain_array_unification_error => iteratively_explain_array_unification_error_modulo_commutativity dag describe_idx asm_array PHOAS_array end%string%list%bool else - explain_array_unification_error_without_commutativity singular plural left_descr right_descr explain_idx_unification_error describe_idx asm_array PHOAS_array 0. + explain_array_unification_error_single singular plural left_descr right_descr explain_idx_unification_error describe_idx modulo_commutativity asm_array PHOAS_array 0. Definition explain_mismatch_from_state (left_descr right_descr : string)