Define an efficient representation of subscripted identifiers.

This is not used yet but it will become useful for efficiently generate
fresh identifiers.

2 files changed, 119 insertions, 0 deletions

diff --git a/engine/nameops.ml b/engine/nameops.ml
index 2047772cfe..31914f9cfa 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -13,6 +13,51 @@ open Names
 
 (* Utilities *)
 
+module Subscript =
+struct
+
+type t = {
+  ss_zero : int;
+  (** Number of leading zeros of the subscript *)
+  ss_subs : int;
+  (** Digital value of the subscript, zero meaning empty *)
+}
+
+let rec overflow n =
+  Int.equal (n mod 10) 9 && (Int.equal (n / 10) 0 || overflow (n / 10))
+
+let zero = { ss_subs = 0; ss_zero = 0 }
+
+let succ s =
+  if Int.equal s.ss_subs 0 then
+    if Int.equal s.ss_zero 0 then
+      (* [] -> [0] *)
+      { ss_zero = 1; ss_subs = 0 }
+    else
+      (* [0...00] -> [0..01] *)
+      { ss_zero = s.ss_zero - 1; ss_subs = 1 }
+  else if overflow s.ss_subs then
+    if Int.equal s.ss_zero 0 then
+      (* [9...9] -> [10...0] *)
+      { ss_zero = 0; ss_subs = 1 + s.ss_subs }
+    else
+      (* [0...009...9] -> [0...010...0] *)
+      { ss_zero = s.ss_zero - 1; ss_subs = 1 + s.ss_subs }
+  else
+    (* [0...0n] -> [0...0{n+1}] *)
+    { ss_zero = s.ss_zero; ss_subs = s.ss_subs + 1 }
+
+let equal s1 s2 =
+  Int.equal s1.ss_zero s2.ss_zero && Int.equal s1.ss_subs s2.ss_subs
+
+let compare s1 s2 =
+  (* Lexicographic order is reversed in order to ensure that [succ] is strictly
+      increasing. *)
+  let c = Int.compare s1.ss_subs s2.ss_subs in
+  if Int.equal c 0 then Int.compare s1.ss_zero s2.ss_zero else c
+
+end
+
 let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
@@ -104,6 +149,46 @@ let has_subscript id =
   let id = Id.to_string id in
   is_digit (id.[String.length id - 1])
 
+let get_subscript id =
+  let id0 = id in
+  let id = Id.to_string id in
+  let len = String.length id in
+  let rec get_suf accu pos =
+    if pos < 0 then (pos, accu)
+    else
+      let c = id.[pos] in
+      if is_digit c then get_suf (Char.code c - Char.code '0' :: accu) (pos - 1)
+      else (pos, accu)
+  in
+  let (pos, suf) = get_suf [] (len - 1) in
+  if Int.equal pos (len - 1) then (id0, Subscript.zero)
+  else
+    let id = String.sub id 0 (pos + 1) in
+    let rec compute_zeros accu = function
+    | [] -> (accu, [])
+    | 0 :: l -> compute_zeros (succ accu) l
+    | _ :: _ as l -> (accu, l)
+    in
+    let (ss_zero, suf) = compute_zeros 0 suf in
+    let rec compute_suf accu = function
+    | [] -> accu
+    | n :: l -> compute_suf (10 * accu + n) l
+    in
+    let ss_subs = compute_suf 0 suf in
+    (Id.of_string id, { Subscript.ss_subs; ss_zero; })
+
+let add_subscript id ss =
+  if Subscript.equal Subscript.zero ss then id
+  else if Int.equal ss.Subscript.ss_subs 0 then
+    let id = Id.to_string id in
+    let pad = String.make ss.Subscript.ss_zero '0' in
+    Id.of_string (Printf.sprintf "%s%s" id pad)
+  else
+    let id = Id.to_string id in
+    let pad = String.make ss.Subscript.ss_zero '0' in
+    let suf = ss.Subscript.ss_subs in
+    Id.of_string (Printf.sprintf "%s%s%i" id pad suf)
+
 let forget_subscript id =
   let numstart = cut_ident false id in
   let newid = Bytes.make (numstart+1) '0' in
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.