From 08f8c8759b6b5b08a86efcd083afc2333b02fd9e Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 20 Oct 2020 10:44:16 -0500
Subject: [PATCH] Use original pattern in iDestruct error messages
---
tests/proofmode.ref | 5 +++--
tests/proofmode.v | 1 +
theories/proofmode/ltac_tactics.v | 22 ++++++++++++----------
3 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index a37992615..572cd8a09 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -634,8 +634,9 @@ The command has indeed failed with message:
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
-Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
-invalid.
+Tactic failure: iDestruct: "[{HP}]" invalid.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "[HP HQ HR]" has too many conjuncts.
The command has indeed failed with message:
Tactic failure: iDestruct: "HP HQ HR"
should contain exactly one proper introduction pattern.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index a7c3a1dc4..c6d24d1a9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1228,6 +1228,7 @@ Proof.
iIntros "HP".
Fail iDestruct "HP" as "{HP}".
Fail iDestruct "HP" as "[{HP}]".
+ Fail iDestruct "HP" as "[HP HQ HR]".
Fail iDestruct "HP" as "HP HQ HR".
Abort.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 6cd5e2e4c..c83c7dddf 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1419,7 +1419,8 @@ Local Ltac string_to_ident s :=
end.
(** * Basic destruct tactic *)
-Local Ltac iDestructHypGo Hz pat :=
+(* pat0 is the unparsed pattern and is only used in error messages *)
+Local Ltac iDestructHypGo Hz pat0 pat :=
lazymatch pat with
| IFresh =>
lazymatch Hz with
@@ -1430,20 +1431,21 @@ Local Ltac iDestructHypGo Hz pat :=
| IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
- | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
- | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
+ | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat0 pat1
+ | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat0 pat2
| IList [[?pat1; ?pat2]] =>
- let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
- | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
+ let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
+ | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat0 pat1|iDestructHypGo Hz pat0 pat2]
+ | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
| IPure IGallinaAnon => iPure Hz as ?
| IPure (IGallinaNamed ?s) => let x := string_to_ident s in
iPure Hz as x
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
- | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
- | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat
- | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
- | _ => fail "iDestruct:" pat "invalid"
+ | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat0 pat
+ | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat0 pat
+ | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat0 pat
+ | _ => fail "iDestruct:" pat0 "invalid"
end.
Local Ltac iDestructHypFindPat Hgo pat found pats :=
lazymatch pats with
@@ -1457,7 +1459,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
| IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
| ?pat1 :: ?pats =>
lazymatch found with
- | false => iDestructHypGo Hgo pat1; iDestructHypFindPat Hgo pat true pats
+ | false => iDestructHypGo Hgo pat pat1; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
--
GitLab