Commit 1c8a145a authored by Ralf Jung's avatar Ralf Jung

improve and test iApply error message

parent 1471ae26
Pipeline #9817 passed with stage
in 16 minutes and 21 seconds
......@@ -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.
......@@ -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.
......@@ -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 *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment