aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-14 16:14:45 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-03-31 09:31:15 -0400
commita8b4394093e61b050406ca952a6d017ad1c737e4 (patch)
treee75e2c0d33fd5a7fc4c46c3460b04530c30aa260
parentb18cfd89e1e8760185d9f50dd777c1c8096cf807 (diff)
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.
-rw-r--r--_CoqProject1
-rw-r--r--src/Language.v24
-rw-r--r--src/PushButtonSynthesis/Primitives.v21
-rw-r--r--src/Rewriter.v15
-rw-r--r--src/Util/ListUtil.v4
-rw-r--r--src/Util/Tactics.v1
-rw-r--r--src/Util/Tactics/ConstrFail.v9
-rw-r--r--src/Util/Tactics/DebugPrint.v4
8 files changed, 41 insertions, 38 deletions
diff --git a/_CoqProject b/_CoqProject
index 7fdf9a21c..8fadf2f12 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -219,6 +219,7 @@ src/Util/Tactics/ChangeInAll.v
src/Util/Tactics/ClearAll.v
src/Util/Tactics/ClearDuplicates.v
src/Util/Tactics/ClearbodyAll.v
+src/Util/Tactics/ConstrFail.v
src/Util/Tactics/Contains.v
src/Util/Tactics/ConvoyDestruct.v
src/Util/Tactics/DebugPrint.v
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).