From 52547f53f8ff634878b45d4c2134d8b295e37195 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 14 Jun 2021 13:36:24 +0200
Subject: [PATCH] Improve error messages for sel/spec/intro pat.

---
 iris/proofmode/intro_patterns.v | 24 ++++++++++++++++++------
 iris/proofmode/sel_patterns.v   |  8 ++++++--
 iris/proofmode/spec_patterns.v  | 13 +++++++++----
 tests/proofmode.ref             |  8 ++++++--
 4 files changed, 39 insertions(+), 14 deletions(-)

diff --git a/iris/proofmode/intro_patterns.v b/iris/proofmode/intro_patterns.v
index 4847e2aca..b11191549 100644
--- a/iris/proofmode/intro_patterns.v
+++ b/iris/proofmode/intro_patterns.v
@@ -136,23 +136,32 @@ Ltac parse s :=
   | intro_pat => constr:([s])
   | list string =>
      lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | ident => constr:([IIdent s])
-  | ?X => fail "intro_pat.parse:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 Ltac parse_one s :=
   lazymatch type of s with
   | intro_pat => s
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
+     | Some [?pat] => pat
+     | _ => fail "intro_pat.parse_one: cannot parse" s "as an introduction pattern"
      end
-  | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse_one: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End intro_pat.
 
@@ -176,5 +185,8 @@ Ltac intro_pat_intuitionistic p :=
      eval cbv in (forallb intro_pat_intuitionistic pat)
   | ident => false
   | bool => p
-  | ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
+  | ?X => fail "intro_pat_intuitionistic: the term" p
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
diff --git a/iris/proofmode/sel_patterns.v b/iris/proofmode/sel_patterns.v
index 4f74efe1b..ea736320c 100644
--- a/iris/proofmode/sel_patterns.v
+++ b/iris/proofmode/sel_patterns.v
@@ -37,8 +37,12 @@ Ltac parse s :=
   | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "invalid sel_pat" s
+     | Some ?pats => pats
+     | _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
      end
-  | ?X => fail "sel_pat.parse:" s "has unexpected type" X
+  | ?X => fail "sel_pat.parse: the term" s
+     "is expected to be a selection pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End sel_pat.
diff --git a/iris/proofmode/spec_patterns.v b/iris/proofmode/spec_patterns.v
index 983b6d260..7b8032343 100644
--- a/iris/proofmode/spec_patterns.v
+++ b/iris/proofmode/spec_patterns.v
@@ -92,10 +92,15 @@ Ltac parse s :=
   lazymatch type of s with
   | list spec_pat => s
   | spec_pat => constr:([s])
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
-              end
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some ?pats => pats
+     | _ => fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
+     end
   | ident => constr:([SIdent s []])
-  | ?X => fail "spec_pat.parse:" s "has unexpected type" X
+  | ?X => fail "spec_pat.parse: the term" s
+     "is expected to be a specialization pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End spec_pat.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index bee3ca0f4..745fd6013 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -730,11 +730,15 @@ Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
 "iRevert_wrong_sel_pat"
      : string
 The command has indeed failed with message:
-Tactic failure: sel_pat.parse: n has unexpected type nat.
+Tactic failure: sel_pat.parse: the term n
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
 "iInduction_wrong_sel_pat"
      : string
 The command has indeed failed with message:
-Tactic failure: sel_pat.parse: m has unexpected type nat.
+Tactic failure: sel_pat.parse: the term m
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
 "test_pure_name"
      : string
 1 goal
-- 
GitLab