Merge PR #9078: Provide a faster bound name generation algorithm through a flag

Ack-by: jfehrle
Ack-by: ppedrot
Reviewed-by: vbgl

1 files changed, 34 insertions, 0 deletions

diff --git a/engine/nameops.mli b/engine/nameops.mli
index 0e75fed045..222573450b 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -24,8 +24,42 @@ val add_prefix : string -> Id.t -> Id.t
 
 (** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)
 
+module Subscript :
+sig
+  type t
+  (** Abstract datatype of subscripts. Isomorphic to a string of digits. *)
+
+  val zero : t
+  (** Empty subscript *)
+
+  val succ : t -> t
+  (** Guarantees that [x < succ x], but [succ x] might not be the smallest
+      element strictly above [x], generally it does not exist. Example mappings:
+      ""   ↦ "0"
+      "0"  ↦ "1"
+      "00" ↦ "01"
+      "1"  ↦ "2"
+      "01" ↦ "02"
+      "9"  ↦ "10"
+      "09" ↦ "10"
+      "99" ↦ "100"
+  *)
+
+  val compare : t -> t -> int
+  (** Well-founded order. *)
+
+  val equal : t -> t -> bool
+
+end
+
 val has_subscript       : Id.t -> bool
 
+val get_subscript : Id.t -> Id.t * Subscript.t
+(** Split an identifier into a base name and a subscript. *)
+
+val add_subscript : Id.t -> Subscript.t -> Id.t
+(** Append the subscript to the identifier. *)
+
 val increment_subscript : Id.t -> Id.t
 (** Return the same identifier as the original one but whose {i subscript} is incremented.
     If the original identifier does not have a suffix, [0] is appended to it.