From 0ba144357be99f8df9af4676c34edc6b0276dfa2 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 20 Oct 2020 12:21:29 -0500
Subject: [PATCH] Improve more iDestruct error messages

---
 tests/proofmode.ref               | 15 ++++++++++-----
 tests/proofmode.v                 | 12 ++++++++++--
 theories/proofmode/ltac_tactics.v | 30 ++++++++++++++++++++++++------
 3 files changed, 44 insertions(+), 13 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 572cd8a09..bbaf4e297 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -631,15 +631,20 @@ Tactic failure: iElaborateSelPat: "H" not found.
 "iDestruct_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: iDestruct: "{HP}"
-should contain exactly one proper introduction pattern.
+Tactic failure: iDestruct: "[{HP}]" has just a single conjunct.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "// H" is not supported due to IDone.
 The command has indeed failed with message:
-Tactic failure: iDestruct: "[{HP}]" invalid.
+Tactic failure: iDestruct: "HP //"
+should contain exactly one proper introduction pattern.
 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.
+Tactic failure: iDestruct: "[HP|HQ|HR]" has too many disjuncts.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "[HP]" has just a single conjunct.
+The command has indeed failed with message:
+Tactic failure: iDestruct: in "[HP HQ|HR]" a disjunct has multiple patterns.
 "iOrDestruct_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c6d24d1a9..331ea7d5b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1226,10 +1226,18 @@ Check "iDestruct_fail".
 Lemma iDestruct_fail P : P -∗ <absorb> P.
 Proof.
   iIntros "HP".
-  Fail iDestruct "HP" as "{HP}".
   Fail iDestruct "HP" as "[{HP}]".
+  (* IDone is unsupported (see issue #380) *)
+  Fail iDestruct "HP" as "// H".
+  (* fails due to not having "one proper intro pattern" (see issue #380) *)
+  Fail iDestruct "HP" as "HP //".
+  (* both of these work *)
+  iDestruct "HP" as "HP /=".
+  iDestruct "HP" as "/= HP".
   Fail iDestruct "HP" as "[HP HQ HR]".
-  Fail iDestruct "HP" as "HP HQ HR".
+  Fail iDestruct "HP" as "[HP|HQ|HR]".
+  Fail iDestruct "HP" as "[HP]".
+  Fail iDestruct "HP" as "[HP HQ|HR]".
 Abort.
 
 Check "iOrDestruct_fail".
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c83c7dddf..0e5b695d0 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 *)
-(* pat0 is the unparsed pattern and is only used in error messages *)
+
+(** [pat0] is the unparsed pattern, and is only used in error messages *)
 Local Ltac iDestructHypGo Hz pat0 pat :=
   lazymatch pat with
   | IFresh =>
@@ -1431,12 +1432,29 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IFrame => iFrameHyp Hz
   | IIdent ?y => iRename Hz into y
   | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat0 pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat0 pat2
+
+  (* conjunctive patterns like [H1 H2] *)
+  | 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 pat0 pat1; iDestructHypGo Hy pat0 pat2
-  | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat0 pat1|iDestructHypGo Hz pat0 pat2]
+     let Hy := iFresh in iAndDestruct Hz as Hz Hy;
+     iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
+  | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
+
+  (* disjunctive patterns like [H1|H2] *)
+  | IList [[?pat1];[?pat2]] =>
+     iOrDestruct Hz as Hz Hz;
+     [iDestructHypGo Hz pat0 pat1|iDestructHypGo Hz pat0 pat2]
+  (* this matches a list of three or more disjunctions [H1|H2|H3] *)
+  | IList (_ :: _ :: _ :: _) => fail "iDestruct:" pat0 "has too many disjuncts"
+  (* the above patterns don't match [H1 H2|H3] *)
+  | IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"
+
   | IPure IGallinaAnon => iPure Hz as ?
   | IPure (IGallinaNamed ?s) => let x := string_to_ident s in
                                 iPure Hz as x
@@ -1445,7 +1463,7 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | 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"
+  | _ => fail "iDestruct:" pat0 "is not supported due to" pat
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
   lazymatch pats with
-- 
GitLab