Document Esubst API and implementation.

2 files changed, 83 insertions, 12 deletions

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 8a9b24afd2..b3b4a49f4d 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -63,11 +63,27 @@ let rec is_lift_id = function
 (* Variant of skewed lists enriched w.r.t. a monoid. See the Range module.
 
   In addition to the indexed data, every node contains a monoid element, in our
-  case, integers. It corresponds to the number of partial lifts to apply when
-  reaching this subtree. The total lift is obtained by summing all the partial
-  lifts encountered in the tree traversal. For efficiency, we also cache the
-  sum of partial lifts of the whole subtree as the last argument of the [Node]
-  constructor. *)
+  case, integers. It corresponds to the number of partial shifts to apply when
+  reaching this subtree. The total shift is obtained by summing all the partial
+  shifts encountered in the tree traversal. For efficiency, we also cache the
+  sum of partial shifts of the whole subtree as the last argument of the [Node]
+  constructor.
+
+  A more intuitive but inefficient representation of this data structure would
+  be a list of terms interspeded with shifts, as in
+
+  type 'a subst = NIL | CONS of 'a or_var * 'a subst | SHIFT of 'a subst
+
+  On this inefficient representation, the typing rules would be:
+
+  · ⊢ NIL : ·
+  Γ ⊢ σ : Δ and Γ ⊢ t : A{σ} implies Γ ⊢ CONS (t, σ) : Δ, A
+  Γ ⊢ σ : Δ implies Γ, A ⊢ SHIFT σ : Δ
+
+  The efficient representation is isomorphic to this naive variant, except that
+  shifts are grouped together, and we use skewed lists instead of lists.
+
+*)
 
 type mon = int
 let mul n m = n + m
@@ -78,9 +94,36 @@ type 'a or_var = Arg of 'a | Var of int
 type 'a tree =
 | Leaf of mon * 'a or_var
 | Node of mon * 'a or_var * 'a tree * 'a tree * mon
+(*
+  Invariants:
+  - All trees are complete.
+  - Define get_shift inductively as [get_shift (Leaf (w, _)) := w] and
+    [get_shift (Node (w, _, t1, t2, _)) := w + t1 + t2] then for every tree
+    of the form Node (_, _, t1, t2, sub), we must have
+    sub = get_shift t1 + get_shift t2.
+
+  In the naive semantics:
+
+  Leaf (w, x) := SHIFT^w (CONS (x, NIL))
+  Node (w, x, t1, t2, _) := SHIFT^w (CONS (x, t1 @ t2))
+
+*)
 
 type 'a subs = Nil of mon * int | Cons of int * 'a tree * 'a subs
+(*
+  In the naive semantics mentioned above, we have the following.
+
+  Nil (w, n) stands for SHIFT^w (ID n) where ID n is a compact form of identity
+  substitution, defined inductively as
+
+  ID 0 := NIL
+  ID (S n) := CONS (Var 1, SHIFT (ID n))
+
+  Cons (h, t, s) stands for (t @ s) and h is the total number of values in the
+  tree t. In particular, it is always of the form 2^n - 1 for some n.
+*)
 
+(* Returns the number of shifts contained in the whole tree. *)
 let eval = function
 | Leaf (w, _) -> w
 | Node (w1, _, _, _, w2) -> mul w1 w2
@@ -158,6 +201,11 @@ let subs_id n = Nil (0, n)
 
 let subs_shft (n, s) = write n s
 
+(* pop is the n-ary tailrec variant of a function whose typing rules would be
+   given as follows. Assume Γ ⊢ e : Δ, A, then
+   - Γ := Ξ, A, Ω for some Ξ and Ω with |Ω| := fst (pop e)
+   - Ξ ⊢ snd (pop e) : Δ
+*)
 let rec pop n i e =
   if Int.equal n 0 then i, e
   else match e with
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 9ad422275e..8ff29ab07a 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -11,20 +11,37 @@
 (** Explicit substitutions *)
 
 (** {6 Explicit substitutions } *)
-(** Explicit substitutions of type ['a].
-    - ESID(n)             = %n END   bounded identity
-    - CONS([|t1..tn|],S)  = (S.t1...tn)    parallel substitution
-        (beware of the order: indice 1 is substituted by tn)
-    - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
-    - LIFT(n,S)           = (%n S) stands for ((^n o S).n...1)
-         (corresponds to S crossing n binders) *)
+(** Explicit substitutions for some type of terms ['a].
+
+    Assuming terms enjoy a notion of typability Γ ⊢ t : A, where Γ is a
+    telescope and A a type, substitutions can be typed as Γ ⊢ σ : Δ, where
+    as a first approximation σ is a list of terms u₁; ...; uₙ s.t.
+    Δ := (x₁ : A₁), ..., (xₙ : Aₙ) and Γ ⊢ uᵢ : Aᵢ{u₁...uᵢ₋₁} for all 1 ≤ i ≤ n.
+
+    Substitutions can be applied to terms as follows, and furthermore
+    if Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ t{σ} : A{σ}.
+
+    We make the typing rules explicit below, but we omit the explicit De Bruijn
+    fidgetting and leave relocations implicit in terms and types.
+
+*)
 type 'a subs
 
 (** Derived constructors granting basic invariants *)
+
+(** Assuming |Γ| = n, Γ ⊢ subs_id n : Γ *)
 val subs_id : int -> 'a subs
+
+(** Assuming Γ ⊢ σ : Δ and Γ ⊢ t : A{σ}, then Γ ⊢ subs_cons t σ : Δ, A *)
 val subs_cons: 'a -> 'a subs -> 'a subs
+
+(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ *)
 val subs_shft: int * 'a subs -> 'a subs
+
+(** Unary variant of {!subst_liftn}. *)
 val subs_lift: 'a subs -> 'a subs
+
+(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ *)
 val subs_liftn: int -> 'a subs -> 'a subs
 
 (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
@@ -52,6 +69,10 @@ val is_subs_id: 'a subs -> bool
 
     Invariant ensured by the private flag: no lift contains two consecutive
     [ELSHFT] nor two consecutive [ELLFT].
+
+    Relocations are a particular kind of substitutions that only contain
+    variables. In particular, [el_*] enjoys the same typing rules as the
+    equivalent substitution function [subs_*].
 *)
 type lift = private
   | ELID
@@ -69,5 +90,7 @@ val is_lift_id : lift -> bool
     substitution equivalent to applying el then s. Argument
     mk_clos is used when a closure has to be created, i.e. when
     el is applied on an element of s.
+
+    That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.
 *)
 val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs