# Module `Esubst`

Explicit substitutions

`type 'a subs`

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.

`val subs_id : int -> 'a subs`

Assuming |Γ| = n, Γ ⊢ subs_id n : Γ

`val subs_cons : 'a -> 'a subs -> 'a subs`

Assuming Γ ⊢ σ : Δ and Γ ⊢ t : A

`σ`

, then Γ ⊢ subs_cons t σ : Δ, A

`val subs_shft : (int * 'a subs) -> 'a subs`

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ

`val subs_liftn : int -> 'a subs -> 'a subs`

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ

`val expand_rel : int -> 'a subs -> (int * 'a, int * int option) Util.union`

`expand_rel k subs`

expands de Bruijn`k`

in the explicit substitution`subs`

. The result is either (Inl(lams,v)) when the variable is substituted by value`v`

under lams binders (i.e. v *has* to be shifted by lams), or (Inr (k',p)) when the variable k is just relocated as k'; p is None if the variable points inside subs and Some(k) if the variable points k bindings beyond subs (cf argument of ESID).

`val is_subs_id : 'a subs -> bool`

Tests whether a substitution behaves like the identity

`type lift`

`= private`

`|`

`ELID`

`|`

`ELSHFT of lift * int`

`|`

`ELLFT of int * lift`

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.

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_*`

.

`val el_id : lift`

`val el_shft : int -> lift -> lift`

`val el_liftn : int -> lift -> lift`

`val el_lift : lift -> lift`

`val reloc_rel : int -> lift -> int`

`val is_lift_id : lift -> bool`

`val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs`

Lift applied to substitution:

`lift_subst mk_clos el s`

computes a 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 σ : Ξ.

`module Internal : sig ... end`

Debugging utilities