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.