Merge PR #7082: Expliciting and taking advantage of a representation invariant in Esubst

2 files changed, 11 insertions, 5 deletions

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index a11a0dc00..91cc64523 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -19,6 +19,8 @@ open Util
 (*********************)
 
 (* Explicit lifts and basic operations *)
+(* Invariant to preserve in this module: no lift contains two consecutive
+    [ELSHFT] nor two consecutive [ELLFT]. *)
 type lift =
   | ELID
   | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
@@ -28,15 +30,15 @@ type lift =
 let el_id = ELID
 
 (* compose a relocation of magnitude n *)
-let rec el_shft_rec n = function
-  | ELSHFT(el,k) -> el_shft_rec (k+n) el
+let el_shft_rec n = function
+  | ELSHFT(el,k) -> ELSHFT(el,k+n)
   | el           -> ELSHFT(el,n)
 let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
 
 (* cross n binders *)
-let rec el_liftn_rec n = function
+let el_liftn_rec n = function
   | ELID        -> ELID
-  | ELLFT(k,el) -> el_liftn_rec (n+k) el
+  | ELLFT(k,el) -> ELLFT(n+k, el)
   | el          -> ELLFT(n, el)
 let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
 
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index b82d6fdf0..a674c425a 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
 (** {6 Compact representation } *)
 (** Compact representation of explicit relocations
     - [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-    - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+    - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders.
+
+    Invariant ensured by the private flag: no lift contains two consecutive
+    [ELSHFT] nor two consecutive [ELLFT].
+*)
 type lift = private
   | ELID
   | ELSHFT of lift * int