From 19757d0cc64b221a3a333b12db14454a447dd7ee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 18 Nov 2018 14:57:43 +0100
Subject: Define an efficient representation of subscripted identifiers.

This is not used yet but it will become useful for efficiently generate
fresh identifiers.
---
 engine/nameops.mli | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'engine/nameops.mli')

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.
-- 
cgit v1.2.3