From 1c8a145a1d894e75b3707db5e91ec188827fe028 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Jun 2018 22:24:42 +0200
Subject: [PATCH] improve and test iApply error message
---
tests/proofmode.ref | 13 +++++++++
tests/proofmode.v | 4 +++
theories/proofmode/ltac_tactics.v | 44 +++++++++++++++----------------
3 files changed, 39 insertions(+), 22 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 47449bd3a..34c19e80b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -330,3 +330,16 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
+"iApply_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iApply (open_constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"goal_tac" (bound to
+fun _ => <ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp) and
+"<ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp", last
+call failed.
+Tactic failure: iApply: cannot apply P.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 307f56eb7..dc0a46417 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -636,4 +636,8 @@ Check "iDestruct_fail".
Lemma iDestruct_fail P : P -∗ <absorb> P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
+Check "iApply_fail".
+Lemma iApply_fail P Q : P -∗ Q.
+Proof. iIntros "HP". Fail iApply "HP". Abort.
+
End error_tests.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 12643fbd3..f5eea3e90 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -769,6 +769,26 @@ The tactic [iApply] uses laxy type class inference, so that evars can first be
instantiated by matching with the goal, whereas [iDestruct] does not, because
eliminations may not be performed when type classes have not been resolved.
*)
+Local Ltac iPoseProofCore_go Htmp t goal_tac :=
+ lazymatch type of t with
+ | ident =>
+ eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
+ [pm_reflexivity ||
+ let t := pretty_ident t in
+ fail "iPoseProof:" t "not found"
+ |pm_reflexivity ||
+ let Htmp := pretty_ident Htmp in
+ fail "iPoseProof:" Htmp "not fresh"
+ |goal_tac ()]
+ | _ =>
+ eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
+ [iIntoEmpValid t
+ |pm_reflexivity ||
+ let Htmp := pretty_ident Htmp in
+ fail "iPoseProof:" Htmp "not fresh"
+ |goal_tac ()]
+ end;
+ try iSolveTC.
Tactic Notation "iPoseProofCore" open_constr(lem)
"as" constr(p) constr(lazy_tc) tactic(tac) :=
iStartProof;
@@ -780,29 +800,9 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
| _ => idtac
end in
- let go goal_tac :=
- lazymatch type of t with
- | ident =>
- eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
- [pm_reflexivity ||
- let t := pretty_ident t in
- fail "iPoseProof:" t "not found"
- |pm_reflexivity ||
- let Htmp := pretty_ident Htmp in
- fail "iPoseProof:" Htmp "not fresh"
- |goal_tac ()]
- | _ =>
- eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
- [iIntoEmpValid t
- |pm_reflexivity ||
- let Htmp := pretty_ident Htmp in
- fail "iPoseProof:" Htmp "not fresh"
- |goal_tac ()]
- end;
- try iSolveTC in
lazymatch eval compute in lazy_tc with
- | true => go ltac:(fun _ => spec_tac (); last (tac Htmp))
- | false => go spec_tac; last (tac Htmp)
+ | true => iPoseProofCore_go Htmp t ltac:(fun _ => spec_tac (); last (tac Htmp))
+ | false => iPoseProofCore_go Htmp t spec_tac; last (tac Htmp)
end.
(** * Apply *)
--
GitLab