[BR] Support arbitrary strings in other IPM arguments

iris/proofmode/ltac_tactics.v

@@ -2,7 +2,7 @@ From stdpp Require Import namespaces hlist pretty.
 From iris.bi Require Export bi telescopes.
 From iris.proofmode Require Import base intro_patterns spec_patterns
                                    sel_patterns coq_tactics reduction
-                                   string_ident.
+                                   string_ident strings.
 From iris.proofmode Require Export classes notation.
 From iris.prelude Require Import options.
 Export ident.
@@ -22,6 +22,20 @@ Ltac pretty_ident H :=
   | ?H => H
   end.
 
+(** [is_str t] succeeds if [t] can has a [to_str] instance. *)
+Ltac is_str t := assert_succeeds (let _ := open_constr:(to_str_str t) in idtac).
+
+(** [to_str t] tries to turn [t] into a name using [to_str] and returns the term
+    unchanged in case of failure. *)
+Ltac maybe_named t :=
+  match t with
+  | _ =>
+    let t := open_constr:(to_str_str t) in
+    let t := eval vm_compute in t in
+    constr:(INamed t)
+  | _ => t
+  end.
+
 (** * Misc *)
 
 Ltac iGetCtx :=
@@ -1010,11 +1024,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
     "with" open_constr(xs) open_constr(pat) "as" constr(p) :=
   let p := intro_pat_intuitionistic p in
   let pat := spec_pat.parse pat in
-  let H :=
-    lazymatch type of H with
-    | string => constr:(INamed H)
-    | _ => H
-    end in
+  let H := maybe_named H in
   iSpecializeArgs H xs; [..|
     lazymatch type of H with
     | ident =>
@@ -1065,13 +1075,15 @@ Tactic Notation "iSpecializeCore" open_constr(H)
 
 Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
   lazymatch type of t with
-  | string => iSpecializeCore t with hnil "" as p
   | ident => iSpecializeCore t with hnil "" as p
   | _ =>
-    lazymatch t with
-    | ITrm ?H ?xs ?pat => iSpecializeCore H with xs pat as p
-    | _ => fail "iSpecialize:" t "should be a proof mode term"
-    end
+    tryif is_str t then
+      iSpecializeCore t with hnil "" as p
+    else
+      lazymatch t with
+      | ITrm ?H ?xs ?pat => iSpecializeCore H with xs pat as p
+      | _ => fail "iSpecialize:" t "should be a proof mode term"
+      end
   end.
 
 Tactic Notation "iSpecialize" open_constr(t) :=
@@ -1090,7 +1102,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
     "as" constr(p) tactic3(tac) :=
   iStartProof;
   let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
-  let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
+  let t := maybe_named t in
   let spec_tac Htmp :=
     lazymatch lem with
     | ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
@@ -1196,7 +1208,7 @@ Tactic Notation "iSplit" :=
 
 Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
-  let Hs := String.words Hs in
+  let Hs := to_str_words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let Δ := iGetCtx in
   eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
@@ -1212,7 +1224,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
 
 Tactic Notation "iSplitR" constr(Hs) :=
   iStartProof;
-  let Hs := String.words Hs in
+  let Hs := to_str_words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let Δ := iGetCtx in
   eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
@@ -1481,7 +1493,7 @@ Tactic Notation "iDestructHyp" constr(H) "as"
 
 (** * Combinining hypotheses *)
 Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
-  let Hs := String.words Hs in
+  let Hs := to_str_words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
   let Δ := iGetCtx in
@@ -1502,7 +1514,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
   iCombine [H1;H2] as pat.
 
 Tactic Notation "iCombineGivesCore" constr(Hs) "gives" tactic3(tac) :=
-  let Hs := String.words Hs in
+  let Hs := to_str_words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
   let Δ := iGetCtx in
@@ -1534,7 +1546,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2)
 
 Tactic Notation "iCombineAsGivesCore" constr(Hs) "as" constr(pat1)
                                       "gives" tactic3(tac) :=
-  let Hs := String.words Hs in
+  let Hs := to_str_words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H1 := iFresh in
   let H2 := iFresh in
@@ -1690,8 +1702,11 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
      that is not supported by Ltac. *)
      let n := eval cbv in (Z.to_nat lem) in intro_destruct n
   | ident => tac lem
-  | string => tac constr:(INamed lem)
-  | _ => iPoseProofCore lem as p tac
+  | _ =>
+    tryif is_str lem then
+      tac constr:(INamed lem)
+    else
+      iPoseProofCore lem as p tac
   end.
 
 Ltac _iDestruct0 lem pat :=
@@ -2027,16 +2042,18 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
     | None => open_constr:(None)
     end in
   lazymatch type of select with
-  | string =>
-     notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
-     [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
   | ident  =>
      notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
      [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
   | namespace =>
      notypeclasses refine (tac_inv_elim _ _ H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
      [ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..]
-  | _ => fail "iInv: selector" select "is not of the right type "
+  | _ =>
+    tryif is_str select then
+      notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
+      [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
+    else
+      fail "iInv: selector" select "is not of the right type "
   end;
     [tc_solve ||
      let I := match goal with |- ElimInv _ ?I  _ _ _ _ _ => I end in

iris/proofmode/strings.v

@@ -10,8 +10,16 @@ Structure to_str := ToStr {
     to_str_str :> to_str_ty -> string
   }.
 #[global] Arguments ToStr [_]%_type_scope _.
-#[global] Arguments to_str_str [_] _.
+#[global] Arguments to_str_str {_} _.
 #[global] Add Printing Constructor to_str.
 
 (** Default instance for Coq's [string] type.  *)
 Canonical Structure stringTS : to_str := ToStr (fun (s : string) => s).
+
+(** A version of stdpp's [String.words] compatible with [to_str]. *)
+#[local] Definition to_str_words_list {TS : to_str} (ls : list TS) := to_str_str <$> ls.
+Ltac to_str_words s :=
+  match type of s with
+  | list _ => eval vm_compute in (to_str_words_list s)
+  | _ => eval vm_compute in (String.words (to_str_str s))
+  end.