From a8b4394093e61b050406ca952a6d017ad1c737e4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 14 Mar 2019 16:14:45 -0400 Subject: Add constr_fail and constr_fail_with Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `*coq*` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully. --- src/Language.v | 24 ++++++++---------------- src/PushButtonSynthesis/Primitives.v | 21 +++++++++++---------- src/Rewriter.v | 15 ++++++--------- src/Util/ListUtil.v | 4 ++-- src/Util/Tactics.v | 1 + src/Util/Tactics/ConstrFail.v | 9 +++++++++ src/Util/Tactics/DebugPrint.v | 4 +++- 7 files changed, 40 insertions(+), 38 deletions(-) create mode 100644 src/Util/Tactics/ConstrFail.v (limited to 'src') diff --git a/src/Language.v b/src/Language.v index 81ca370db..4b112dfdb 100644 --- a/src/Language.v +++ b/src/Language.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Tactics.RunTacticAsConstr. Require Import Crypto.Util.Tactics.DebugPrint. +Require Import Crypto.Util.Tactics.ConstrFail. Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. Module Compilers. @@ -64,10 +65,10 @@ Module Compilers. Ltac debug_leave_reify_in_context_success e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac reify_in_context e ret). Ltac debug_leave_reify_in_context_failure e := let dummy := debug0 ltac:(fun _ => debug_leave_reify_failure_idtac reify_in_context e) in - constr:(I : I). + constr_fail. Ltac debug_leave_reify_base_type_failure e := let dummy := debug0 ltac:(fun _ => debug_leave_reify_failure_idtac reify_base_type e) in - constr:(I : I). + constr_fail. Tactic Notation "idtac_reify_in_context_case" ident(case) := idtac "reify_in_context:" case. Ltac debug_reify_in_context_case tac := @@ -392,10 +393,7 @@ Module Compilers. | zrange => type.zrange | interp (type.type_base ?T) => T | @einterp type interp (@Compilers.type.base type (type.type_base ?T)) => T - | _ => let __ := match goal with - | _ => fail 1 "Unrecognized type:" ty - end in - constr:(I : I) + | _ => constr_fail_with ltac:(fun _ => fail 1 "Unrecognized type:" ty) end. Ltac reify ty := let __ := Reify.debug_enter_reify_base_type ty in @@ -648,10 +646,7 @@ Module Compilers. lazymatch rb with | @Abs _ _ _ ?s ?d ?f => constr:(@LetIn base_type ident var s d ra f) - | ?rb => let __ := match goal with - | _ => fail 1 "Invalid non-Abs function reification of" b "to" rb - end in - constr:(I : I) + | ?rb => constr_fail_with ltac:(fun _ => fail 1 "Invalid non-Abs function reification of" b "to" rb) end | (fun x : ?T => ?f) => @@ -697,10 +692,7 @@ Module Compilers. remain. However, if this does come up, having a distinctive error message is much more useful for debugging than the generic "no matching clause" *) - let __ := match goal with - | _ => fail 1 "Failure to eliminate functional dependencies of" rf0 - end in - constr:(I : I) + constr_fail_with ltac:(fun _ => fail 1 "Failure to eliminate functional dependencies of" rf0) end end | _ @@ -738,7 +730,7 @@ Module Compilers. => let __ := match goal with | _ => fail 2 "Unrecognized term:" term' end in - constr:(I : I) + constr_fail end in match constr:(Set) with | _ => reify_rec term @@ -746,7 +738,7 @@ Module Compilers. | _ => idtac "Error: Failed to reify" term' "via unfolding"; fail 2 "Failed to reify" term' "via unfolding" end in - constr:(I : I) + constr_fail end) end) end diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 24a5592ed..575e4057a 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.HasBody. Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.ConstrFail. Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.CStringification. @@ -210,8 +211,8 @@ Module CorrectnessStringification. exact v) end) | ?T - => let __ := match goal with _ => idtac "Unrecognized bounds component:" T end in - constr:(I : I) + => constr_fail_with ltac:(fun _ => idtac "Unrecognized bounds component:" T; + fail 1 "Unrecognized bounds component:" T) end. Ltac with_assoc_list ctx correctness arg_var_names out_var_names cont := @@ -339,8 +340,8 @@ Module CorrectnessStringification. exact (" " ++ xn ++ res)) end) with | fun _ => ?f => f - | ?F => let __ := match goal with _ => idtac "Failed to eliminate functional dependencies in" F end in - constr:(I : I) + | ?F => constr_fail_with ltac:(fun _ => idtac "Failed to eliminate functional dependencies in" F; + fail 1 "Failed to eliminate functional dependencies in" F) end | ?v => let res := stringify_body ctx v in constr:(", " ++ res) @@ -422,8 +423,8 @@ Module CorrectnessStringification. | prod ?A ?B => let v := (eval cbn [fst snd] in (fst x = fst y /\ snd x = snd y)) in recurse v lvl - | ?T' => let __ := match goal with _ => idtac "Error: Unrecognized type for equality:" T' end in - constr:(I : I) + | ?T' => constr_fail_with ltac:(fun _ => idtac "Error: Unrecognized type for equality:" T'; + fail 1 "Error: Unrecognized type for equality:" T') end | eval (weight 8 1) _ ?v => let sv := recurse v 9 in @@ -500,12 +501,12 @@ Module CorrectnessStringification. | Z => show_Z () | nat => show_nat () | _ - => let __ := match goal with _ => idtac "Error: Unrecognized var:" v " in " ctx end in - constr:(I : I) + => constr_fail_with ltac:(fun _ => idtac "Error: Unrecognized var:" v " in " ctx; + fail 1 "Error: Unrecognized var:" v " in " ctx) end | false - => let __ := match goal with _ => idtac "Error: Unrecognized term:" v " in " ctx end in - constr:(I : I) + => constr_fail_with ltac:(fun _ => idtac "Error: Unrecognized term:" v " in " ctx; + fail 1 "Error: Unrecognized term:" v " in " ctx) end end end. diff --git a/src/Rewriter.v b/src/Rewriter.v index 01d7614e3..2ccfb342d 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -10,6 +10,7 @@ Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.Tactics.ConstrFail. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. Require Import Crypto.Language. @@ -1450,8 +1451,8 @@ Module Compilers. Ltac strip_functional_dependency term := lazymatch term with | fun _ => ?P => P - | _ => let __ := match goal with _ => idtac "Cannot eliminate functional dependencies of" term; fail 1 "Cannot eliminate functional dependencies of" term end in - constr:(I : I) + | _ => constr_fail_with ltac:(fun _ => idtac "Cannot eliminate functional dependencies of" term; + fail 1 "Cannot eliminate functional dependencies of" term) end. Ltac reify_under_forall_types' ty_ctx cur_i lem cont := @@ -1505,8 +1506,7 @@ Module Compilers. end) | @eq ?T ?A ?B => constr:((@eq T A B, side_conditions)) - | ?T => let __ := match goal with _ => fail 1 "Invalid type of equation:" T end in - constr:(I : I) + | ?T => constr_fail_with ltac:(fun _ => fail 1 "Invalid type of equation:" T) end. Ltac equation_to_parts lem := equation_to_parts' lem (@nil bool). @@ -1781,10 +1781,7 @@ Module Compilers. lazymatch rf0 with | (fun _ => ?f) => f | _ - => let __ := match goal with - | _ => fail 1 "Failure to eliminate functional dependencies of" rf0 - end in - constr:(I : I) + => constr_fail_with ltac:(fun _ => fail 1 "Failure to eliminate functional dependencies of" rf0) end | (@eq ?T ?A ?B, ?side_conditions) => let rA := expr.reify_in_context base.type ident ltac:(base.reify) reify_ident var_pos A value_ctx tt in @@ -2089,7 +2086,7 @@ Module Compilers. let next := match body with | context[@id ?t ?v] => lazymatch so_far with - | context[cons (existT _ _ v) _] => constr:(I : I) + | context[cons (existT _ _ v) _] => constr_fail | _ => constr:(@Some _ v) end | _ => constr:(@None unit) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index ac6575a4f..b7a5292d8 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -12,6 +12,7 @@ Require Export Crypto.Util.Tactics.BreakMatch. Require Export Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.Tactics.ConstrFail. Import ListNotations. Local Open Scope list_scope. @@ -1910,8 +1911,7 @@ Ltac expand_lists _ := let default_for A := match goal with | _ => (eval lazy in (_ : pointed A)) - | _ => let __ := match goal with _ => idtac "Warning: could not infer a default value for list type" A end in - constr:(I : I) + | _ => constr_fail_with ltac:(fun _ => idtac "Warning: could not infer a default value for list type" A) end in let T := lazymatch goal with |- _ = _ :> ?T => T end in let v := fresh in diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 7b378c9bf..30c3ec461 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -6,6 +6,7 @@ Require Export Crypto.Util.Tactics.ChangeInAll. Require Export Crypto.Util.Tactics.ClearAll. Require Export Crypto.Util.Tactics.ClearDuplicates. Require Export Crypto.Util.Tactics.ClearbodyAll. +Require Export Crypto.Util.Tactics.ConstrFail. Require Export Crypto.Util.Tactics.Contains. Require Export Crypto.Util.Tactics.ConvoyDestruct. Require Export Crypto.Util.Tactics.CPSId. diff --git a/src/Util/Tactics/ConstrFail.v b/src/Util/Tactics/ConstrFail.v new file mode 100644 index 000000000..fe8a05630 --- /dev/null +++ b/src/Util/Tactics/ConstrFail.v @@ -0,0 +1,9 @@ +(** A tactic that executes immediately (during expression evaluation / constr-construction) and fails. Ideally we can eventually give it a nicer error message. COQBUG(3913) *) + +Ltac constr_fail := + let __ := match goal with _ => fail 1 "Constr construction failed. Please look at the message log (*coq*, or run your tactic again inside Fail or try) to see more details" end in + (). + +Ltac constr_fail_with msg_tac := + let __ := match goal with _ => msg_tac () end in + constr_fail. diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v index 3ced23331..97edd0ad9 100644 --- a/src/Util/Tactics/DebugPrint.v +++ b/src/Util/Tactics/DebugPrint.v @@ -1,3 +1,5 @@ +Require Import Crypto.Util.Tactics.ConstrFail. + Ltac debuglevel := constr:(0%nat). Ltac solve_debugfail tac := @@ -36,7 +38,7 @@ Ltac constr_run_tac_fail tac := let dummy := match goal with | _ => tac () end in - constr:(I : I). + constr_fail. Ltac cidtac msg := constr_run_tac ltac:(fun _ => idtac msg). -- cgit v1.2.3