Experimenting documentation of the Vars.subst functions.

Related questions:
- What balance to find between precision and conciseness?
- What convention to follow for typesetting the different components
  of the documentation is unclear?

New tentative type substl to emphasize that substitutions (for substl)
are represented the other way round compared to instances for
application (applist), though there are represented the same way
(i.e. most recent/dependent component on top) as instances of evars
(mkEvar).

Also removing unused subst*_named_decl functions (at least
substnl_named_decl is somehow non-sense).

2 files changed, 60 insertions, 31 deletions

diff --git a/kernel/vars.ml b/kernel/vars.ml
index a800e2531..f8c0a65e6 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -151,6 +151,11 @@ let make_subst = function
   done;
   subst
 
+(* The type of substitutions, with term substituting most recent
+    binder at the head *)
+
+type substl = Constr.t list
+
 let substnl laml n c = substn_many (make_subst laml) n c
 let substl laml c = substn_many (make_subst laml) 0 c
 let subst1 lam c = substn_many [|make_substituend lam|] 0 c
@@ -159,13 +164,6 @@ let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r
 let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r
 let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r
 
-let substnl_named_decl laml k d =
-  map_named_declaration (fun c -> substnl laml k c) d
-let substl_named_decl laml d =
-  map_named_declaration (fun c -> substnl laml 0 c) d
-let subst1_named_decl lam d =
-  map_named_declaration (fun c -> subst1 lam c) d
-
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
@@ -197,15 +195,10 @@ let replace_vars var_alist x =
     in
     substrec 0 x
 
-(*
-let repvarkey = Profile.declare_profile "replace_vars";;
-let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;;
-*)
-
-(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
+(* (subst_var str t) substitute (Var str) by (Rel 1) in t *)
 let subst_var str t = replace_vars [(str, Constr.mkRel 1)] t
 
-(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+(* (subst_vars [id1;...;idn] t) substitute (Var idj) by (Rel j) in t *)
 let substn_vars p vars c =
   let _,subst =
     List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars
diff --git a/kernel/vars.mli b/kernel/vars.mli
index c0fbeeb6e..ab10ba93b 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -42,33 +42,69 @@ val liftn : int -> int -> constr -> constr
 (** [lift n c] lifts by [n] the positive indexes in [c] *)
 val lift : int -> constr -> constr
 
-(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
+(** The type [substl] is the type of substitutions [u₁..un] of type
+    some context Δ and defined in some environment Γ. Typing of
+    substitutions is defined by:
+    - Γ ⊢ ∅ : ∅,
+    - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ u{_n} : An\[u₁..u{_n-1}\] implies
+      Γ ⊢ u₁..u{_n} : Δ,x{_n}:A{_n}
+    - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ un : A{_n}\[u₁..u{_n-1}\] implies
+      Γ ⊢ u₁..u{_n} : Δ,x{_n}:=c{_n}:A{_n} when Γ ⊢ u{_n} ≡ c{_n}\[u₁..u{_n-1}\]
+
+    Note that [u₁..un] is represented as a list with [un] at the head of
+    the list, i.e. as [[un;...;u₁]]. *)
+
+type substl = constr list
+
+(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
-    accordingly indexes in [a1],...,[an] and [c] *)
-val substnl : constr list -> int -> constr -> constr
-val substl : constr list -> constr -> constr
+    accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if
+    Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then
+    Γ, Γ' ⊢ [substnl [a₁;...;an] k c] : [substnl [a₁;...;an] k T]. *)
+val substnl : substl -> int -> constr -> constr
+
+(** [substl σ c] is a short-hand for [substnl σ 0 c] *)
+val substl : substl -> constr -> constr
+
+(** [substl a c] is a short-hand for [substnl [a] 0 c] *)
 val subst1 : constr -> constr -> constr
 
-val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
-val substl_decl : constr list -> rel_declaration -> rel_declaration
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+(** [substnl_decl [a₁;...;an] k Ω] substitutes in parallel [a₁], ..., [an]
+    for respectively [Rel(k+1)], ..., [Rel(k+n)] in [Ω]; it relocates
+    accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if
+    Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then
+    Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *)
+val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+
+(** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *)
+val substl_decl : substl -> rel_declaration -> rel_declaration
 
-val substnl_named_decl : constr list -> int -> named_declaration -> named_declaration
-val subst1_named_decl : constr -> named_declaration -> named_declaration
-val substl_named_decl : constr list -> named_declaration -> named_declaration
+(** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *)
+val subst1_decl : constr -> rel_declaration -> rel_declaration
 
+(** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by
+    [cj] in [t]. *)
 val replace_vars : (Id.t * constr) list -> constr -> constr
-(** (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-val subst_var : Id.t -> constr -> constr
 
-(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
-   if two names are identical, the one of least indice is kept *)
-val subst_vars : Id.t list -> constr -> constr
+(** [substn_vars k [id₁;...;idn] t] substitutes [Var idj] by [Rel j+k-1] in [t].
+   If two names are identical, the one of least index is kept. In terms of
+   typing, if Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ t:T, together with id{_j}:T{_j} and
+   Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ T{_j}\[id{_j+1}..id{_n}:=x{_j+1}..x{_n}\] ≡ Uj,
+   then Γ\\{id₁,...,id{_n}\},x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ [substn_vars
+   (|Γ'|+1) [id₁;...;idn] t] : [substn_vars (|Γ'|+1) [id₁;...;idn]
+   T]. *)
 
-(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
-   if two names are identical, the one of least indice is kept *)
 val substn_vars : int -> Id.t list -> constr -> constr
 
+(** [subst_vars [id1;...;idn] t] is a short-hand for [substn_vars
+   [id1;...;idn] 1 t]: it substitutes [Var idj] by [Rel j] in [t]. If
+   two names are identical, the one of least index is kept. *)
+val subst_vars : Id.t list -> constr -> constr
+
+(** [subst_var id t] is a short-hand for [substn_vars [id] 1 t]: it
+    substitutes [Var id] by [Rel 1] in [t]. *)
+val subst_var : Id.t -> constr -> constr
+
 (** {3 Substitution of universes} *)
 
 open Univ