From 49f26fdc202f9aba81c8a92ad1574df10940c883 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jun 2018 23:12:22 +0200
Subject: [PATCH] test and fix some more proof mode error messages
---
tests/proofmode.ref | 81 +++++++++++++++++++++++++++++++
tests/proofmode.v | 39 +++++++++++++--
theories/proofmode/ltac_tactics.v | 44 ++++++++++-------
3 files changed, 143 insertions(+), 21 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index aa47143c6..da7ba45eb 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -184,15 +184,21 @@ Tactic failure: iFrame: cannot frame Q.
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+"iAlways_spatial_non_empty"
+ : string
The command has indeed failed with message:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
Tactic failure: iModIntro: spatial context is non-empty.
+"iDestruct_bad_name"
+ : string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: "HQ" not found.
+"iIntros_dup_name"
+ : string
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
@@ -201,12 +207,87 @@ The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
+"iSplit_one_of_many"
+ : string
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+"iExact_fail"
+ : string
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
+The command has indeed failed with message:
+Ltac call to "iExact (constr)" failed.
+Tactic failure: iExact: "HQ" : Q does not match goal.
+The command has indeed failed with message:
+Ltac call to "iExact (constr)" failed.
+Tactic failure: iExact: "HP"
+not absorbing and the remaining hypotheses not affine.
+"iClear_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
+Tactic failure: iElaborateSelPat: "HP" not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)",
+"<iris.proofmode.ltac_tactics.iClear_go>" and
+"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
+Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
+"iSpecializeArgs_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializeArgs (constr) (open_constr)",
+"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
+"notypeclasses refine (uconstr)", last call failed.
+In environment
+PROP : sbi
+P : PROP
+The term "true" has type "bool" while it is expected to have type "nat".
+"iStartProof_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
+Tactic failure: iStartProof: not a BI assertion.
+"iPoseProof_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
+failed.
+Tactic failure: iPoseProof: not a BI assertion.
+The command has indeed failed with message:
+In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
+failed.
+Tactic failure: iRename: "H" not fresh.
+"iRevert_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
+Tactic failure: iElaborateSelPat: "H" not found.
+"iDestruct_fail"
+ : string
+The command has indeed failed with message:
+In nested Ltac calls to "iDestruct (open_constr) as (constr)",
+"iDestructCore (open_constr) as (constr) (tactic)",
+"iDestructCore (open_constr) as (constr) (tactic)" and
+"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+Tactic failure: iDestruct: "{HP}"
+should contain exactly one proper introduction pattern.
+The command has indeed failed with message:
+In nested Ltac calls to "iDestruct (open_constr) as (constr)",
+"iDestructCore (open_constr) as (constr) (tactic)",
+"iDestructCore (open_constr) as (constr) (tactic)" and
+"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
+invalid.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f771b38b0..a7e7e4227 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -553,14 +553,17 @@ Section error_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
+Check "iAlways_spatial_non_empty".
Lemma iAlways_spatial_non_empty P :
P -∗ □ emp.
Proof. iIntros "HP". Fail iAlways. Abort.
+Check "iDestruct_bad_name".
Lemma iDestruct_bad_name P :
P -∗ P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.
+Check "iIntros_dup_name".
Lemma iIntros_dup_name P Q :
P -∗ Q -∗ ∀ x y : (), P.
Proof.
@@ -568,16 +571,46 @@ Proof.
iIntros "HQ" (x). Fail iIntros (x).
Abort.
+Check "iSplit_one_of_many".
Lemma iSplit_one_of_many P :
P -∗ P -∗ P ∗ P.
Proof.
iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.
-Lemma iExact_not_found P :
- P -∗ P.
+Check "iExact_fail".
+Lemma iExact_fail P Q :
+ <affine> P -∗ Q -∗ <affine> P.
Proof.
- iIntros "HP". Fail iExact "HQ".
+ iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
Abort.
+Check "iClear_fail".
+Lemma iClear_fail P : P -∗ P.
+Proof. Fail iClear "HP". iIntros "HP". Fail iClear "HP". Abort.
+
+Check "iSpecializeArgs_fail".
+Lemma iSpecializeArgs_fail P :
+ (∀ x : nat, P) -∗ P.
+Proof. iIntros "HP". Fail iSpecialize ("HP" $! true). Abort.
+
+Check "iStartProof_fail".
+Lemma iStartProof_fail : 0 = 0.
+Proof. Fail iStartProof. Abort.
+
+Check "iPoseProof_fail".
+Lemma iPoseProof_fail P : P -∗ P.
+Proof.
+ Fail iPoseProof (eq_refl 0) as "H".
+ iIntros "H". Fail iPoseProof bi.and_intro as "H".
+Abort.
+
+Check "iRevert_fail".
+Lemma iRevert_fail P : P -∗ P.
+Proof. Fail iRevert "H". Abort.
+
+Check "iDestruct_fail".
+Lemma iDestruct_fail P : P -∗ <absorb> P.
+Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
+
End error_tests.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 4d5015b3c..c9ba1bb0e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -62,7 +62,7 @@ Tactic Notation "iStartProof" :=
lazymatch goal with
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
- [iSolveTC || fail "iStartProof: not a Bi entailment"
+ [iSolveTC || fail "iStartProof: not a BI assertion"
|apply tac_adequate]
end.
@@ -83,7 +83,7 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
[bi_car _], and hence trigger the canonical structures mechanism
to find the corresponding bi. *)
| |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
- [iSolveTC || fail "iStartProof: not a Bi entailment"
+ [iSolveTC || fail "iStartProof: not a BI assertion"
|apply tac_adequate]
end.
@@ -133,8 +133,12 @@ possible in Ltac2. *)
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
- [pm_reflexivity || fail "iRename:" H1 "not found"
- |pm_reflexivity || fail "iRename:" H2 "not fresh"|].
+ [pm_reflexivity ||
+ let H1 := pretty_ident H1 in
+ fail "iRename:" H1 "not found"
+ |pm_reflexivity ||
+ let H2 := pretty_ident H2 in
+ fail "iRename:" H2 "not fresh"|].
Local Inductive esel_pat :=
| ESelPure
@@ -172,18 +176,19 @@ Local Ltac iClearHyp H :=
let H := pretty_ident H in
fail "iClear:" H "not found"
|pm_reduce; iSolveTC ||
+ let H := pretty_ident H in
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iClear:" H ":" P "not affine and the goal not absorbing"
|].
+Local Ltac iClear_go Hs :=
+ lazymatch Hs with
+ | [] => idtac
+ | ESelPure :: ?Hs => clear; iClear_go Hs
+ | ESelIdent _ ?H :: ?Hs => iClearHyp H; iClear_go Hs
+ end.
Tactic Notation "iClear" constr(Hs) :=
- let rec go Hs :=
- lazymatch Hs with
- | [] => idtac
- | ESelPure :: ?Hs => clear; go Hs
- | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
- end in
- let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
+ iStartProof; let Hs := iElaborateSelPat Hs in iClear_go Hs.
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear Hs; clear xs.
@@ -192,11 +197,14 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
Tactic Notation "iExact" constr(H) :=
eapply tac_assumption with _ H _ _; (* (i:=H) *)
[pm_reflexivity ||
+ let H := pretty_ident H in
fail "iExact:" H "not found"
|iSolveTC ||
+ let H := pretty_ident H in
let P := match goal with |- FromAssumption _ ?P _ => P end in
fail "iExact:" H ":" P "does not match goal"
|pm_reduce; iSolveTC ||
+ let H := pretty_ident H in
fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
Tactic Notation "iAssumptionCore" :=
@@ -508,8 +516,7 @@ type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
at most places instead of `apply`. *)
-Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
- let rec go xs :=
+Local Ltac iSpecializeArgs_go H xs :=
lazymatch xs with
| hnil => idtac
| hcons ?x ?xs =>
@@ -523,9 +530,10 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- ∃ _ : ?A, _ =>
notypeclasses refine (@ex_intro A _ x (conj _ _))
- end; [shelve..|pm_reflexivity|go xs]]
- end in
- go xs.
+ end; [shelve..|pm_reflexivity|iSpecializeArgs_go H xs]]
+ end.
+Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
+ iSpecializeArgs_go H xs.
Ltac iSpecializePat_go H1 pats :=
let solve_to_wand H1 :=
@@ -737,7 +745,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) :=
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_emp_valid_1 tT _ _);
- [iSolveTC || fail "iPoseProof: not a BI assertion"
+ [iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]]
with go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
@@ -843,7 +851,7 @@ Tactic Notation "iRevert" constr(Hs) :=
fail "iRevert:" H "not found"
|pm_reduce; go Hs]
end in
- let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
+ iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
Tactic Notation "iRevert" "(" ident(x1) ")" :=
iForallRevert x1.
--
GitLab