Merge PR #13137: [ltac] Avoid magic numbers

Reviewed-by: herbelin

3 files changed, 31 insertions, 27 deletions

diff --git a/clib/cString.ml b/clib/cString.ml
index dcada4c18f..9d2c3729b2 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -25,6 +25,7 @@ sig
   val ordinal : int -> string
   val is_sub : string -> string -> int -> bool
   val is_prefix : string -> string -> bool
+  val is_suffix : string -> string -> bool
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
   module List : CList.MonoS with type elt = t
@@ -105,6 +106,9 @@ let is_sub p s off =
 let is_prefix p s =
   is_sub p s 0
 
+let is_suffix p s =
+  is_sub p s (String.length s - String.length p)
+
 let plural n s = if n<>1 then s^"s" else s
 
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
diff --git a/clib/cString.mli b/clib/cString.mli
index 0f78e66573..be8a202b64 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -54,6 +54,9 @@ sig
   val is_prefix : string -> string -> bool
   (** [is_prefix p s] tests whether [p] is a prefix of [s]. *)
 
+  val is_suffix : string -> string -> bool
+  (** [is_suffix suf s] tests whether [suf] is a suffix of [s]. *)
+
   (** {6 Generic operations} **)
 
   module Set : Set.S with type elt = t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index d58a76fe13..6823b6411f 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -31,18 +31,6 @@ type argument = Genarg.ArgT.any Extend.user_symbol
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
-let coincide s pat off =
-  let len = String.length pat in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = Char.code s.[off + !i] in
-    let d = Char.code pat.[!i] in
-    break := Int.equal c d;
-    incr i
-  done;
-  !break
-
 let atactic n =
   if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
   else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
@@ -70,28 +58,37 @@ let check_separator ?loc = function
 | Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
 
 let rec parse_user_entry ?loc s sep =
-  let l = String.length s in
-  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+  let open CString in
+  let matches pre suf s =
+    String.length s > (String.length pre + String.length suf) &&
+      is_prefix pre s && is_suffix suf s
+  in
+  let basename pre suf s =
+    let plen = String.length pre in
+    String.sub s plen (String.length s - (plen + String.length suf))
+  in
+  let tactic_len = String.length "tactic" in
+  if matches "ne_" "_list" s then
+    let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in
     check_separator ?loc sep;
     Ulist1 entry
-  else if l > 12 && coincide s "ne_" 0 &&
-                   coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
+  else if matches "ne_" "_list_sep" s then
+    let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in
     Ulist1sep (entry, get_separator sep)
-  else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+  else if matches "" "_list" s then
+    let entry = parse_user_entry ?loc (basename "" "_list" s) None in
     check_separator ?loc sep;
     Ulist0 entry
-  else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
+  else if matches "" "_list_sep" s then
+    let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in
     Ulist0sep (entry, get_separator sep)
-  else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+  else if matches "" "_opt" s then
+    let entry = parse_user_entry ?loc (basename "" "_opt" s) None in
     check_separator ?loc sep;
     Uopt entry
-  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
-    let n = Char.code s.[6] - 48 in
+  else if String.length s = tactic_len + 1 && is_prefix "tactic" s
+      && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then
+    let n = Char.code s.[tactic_len] - Char.code '0' in
     check_separator ?loc sep;
     Uentryl ("tactic", n)
   else
@@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function
   EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
 | Extend.Uentryl (s, n) ->
   let ArgT.Any tag = s in
-  assert (coincide (ArgT.repr tag) "tactic" 0);
+  assert (CString.is_suffix "tactic" (ArgT.repr tag));
   get_tacentry n lev
 
 (** Tactic grammar extensions *)