# Module `Esubst`

Explicit substitutions

`type 'a subs`

`= private`

`|`

`ESID of int`

`|`

`CONS of 'a array * 'a subs`

`|`

`SHIFT of int * 'a subs`

`|`

`LIFT of int * 'a subs`

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)

`val subs_id : int -> 'a subs`

Derived constructors granting basic invariants

`val subs_cons : ('a array * 'a subs) -> 'a subs`

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

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

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

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

`subs_shift_cons(k,s,[|t1..tn|])`

builds (^k s).t1..tn

`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

`val comp : (('a subs * 'a) -> 'a) -> 'a subs -> 'a subs -> 'a subs`

Composition of substitutions:

`comp mk_clos s1 s2`

computes a substitution equivalent to applying s2 then s1. Argument mk_clos is used when a closure has to be created, i.e. when s1 is applied on an element of s2.

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

.

`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.