From e3fb7049631f492d8685e270a1ee90e2dfe795cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 16 Mar 2017 21:05:50 +0100
Subject: [PATCH] Fix issue #80: better error message when hyps are missing.
---
theories/proofmode/tactics.v | 46 ++++++++++++++++++++++++++----------
1 file changed, 34 insertions(+), 12 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e5444b29..15c121dc 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -32,6 +32,15 @@ Ltac iFresh' H :=
end.
Ltac iFresh := iFresh' "~".
+Ltac iMissingHyps Hs :=
+ let Δ :=
+ lazymatch goal with
+ | |- of_envs ?Δ ⊢ _ => Δ
+ | |- context[ envs_split _ _ ?Δ ] => Δ
+ end in
+ let Hhyps := eval env_cbv in (envs_dom Δ) in
+ eval vm_compute in (list_difference Hs Hhyps).
+
Tactic Notation "iTypeOf" constr(H) tactic(tac):=
let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
lazymatch eval env_cbv in (envs_lookup H Δ) with
@@ -238,7 +247,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
Tactic Notation "iFrame" constr(Hs) :=
let rec go Hs :=
- match Hs with
+ lazymatch Hs with
| [] => idtac
| SelPure :: ?Hs => iFrameAnyPure; go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
@@ -357,7 +366,7 @@ Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
let rec go xs :=
- match xs with
+ lazymatch xs with
| hnil => idtac
| hcons ?x ?xs =>
eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *)
@@ -420,7 +429,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
| GSpatial => apply elim_modal_dummy
| GModal => apply _ || fail "iSpecialize: goal not a modality"
end
- |env_reflexivity || fail "iSpecialize:" Hs "not found"
+ |env_reflexivity ||
+ let Hs' := iMissingHyps Hs' in
+ fail "iSpecialize: hypotheses" Hs' "not found in the context"
|iFrame Hs_frame; done_if d (*goal*)
|go H1 pats]
| SAutoFrame GPersistent :: ?pats =>
@@ -674,8 +685,11 @@ Tactic Notation "iSplitL" constr(Hs) :=
[apply _ ||
let P := match goal with |- FromSep ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction"
- |env_reflexivity || fail "iSplitL: hypotheses" Hs
- "not found in the context"| |].
+ |env_reflexivity ||
+ let Hs := iMissingHyps Hs in
+ fail "iSplitL: hypotheses" Hs "not found in the context"
+ | |].
+
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
@@ -683,8 +697,10 @@ Tactic Notation "iSplitR" constr(Hs) :=
[apply _ ||
let P := match goal with |- FromSep ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction"
- |env_reflexivity || fail "iSplitR: hypotheses" Hs
- "not found in the context"| |].
+ |env_reflexivity ||
+ let Hs := iMissingHyps Hs in
+ fail "iSplitR: hypotheses" Hs "not found in the context"
+ | |].
Tactic Notation "iSplitL" := iSplitR "".
Tactic Notation "iSplitR" := iSplitL "".
@@ -709,7 +725,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H')
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
eapply tac_combine with _ _ Hs _ _ H _;
- [env_reflexivity || fail "iCombine:" Hs "not found"
+ [env_reflexivity ||
+ let Hs := iMissingHyps Hs in
+ fail "iCombine: hypotheses" Hs "not found in the context"
|apply _
|env_reflexivity || fail "iCombine:" H "not fresh"|].
@@ -1326,20 +1344,24 @@ Tactic Notation "iAssertCore" open_constr(Q)
| [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d)] =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
let p' := eval cbv in (match m with GModal => false | _ => p end) in
- match p' with
+ lazymatch p' with
| false =>
eapply tac_assert with _ _ _ lr Hs' H Q _;
[lazymatch m with
| GSpatial => apply elim_modal_dummy
| GModal => apply _ || fail "iAssert: goal not a modality"
end
- |env_reflexivity || fail "iAssert:" Hs "not found"
+ |env_reflexivity ||
+ let Hs' := iMissingHyps Hs' in
+ fail "iAssert: hypotheses" Hs' "not found in the context"
|env_reflexivity
|iFrame Hs_frame; done_if d (*goal*)
|tac H]
| true =>
eapply tac_assert_persistent with _ _ _ lr Hs' H Q;
- [env_reflexivity
+ [env_reflexivity ||
+ let Hs' := iMissingHyps Hs' in
+ fail "iAssert: hypotheses" Hs' "not found in the context"
|env_reflexivity
|apply _ || fail "iAssert:" Q "not persistent"
|done_if d (*goal*)
@@ -1350,7 +1372,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
let p := intro_pat_persistent p in
- match p with
+ lazymatch p with
| true => iAssertCore Q with "[#]" as p tac
| false => iAssertCore Q with "[]" as p tac
end.
--
GitLab