1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: esubst.mli 8799 2006-05-09 21:15:07Z barras $ i*)
11
(*s Compact representation of explicit relocations. \\
12
[ELSHFT(l,n)] == lift of [n], then apply [lift l].
13
[ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
16
| ELSHFT of lift * int
19
val el_shft : int -> lift -> lift
20
val el_liftn : int -> lift -> lift
21
val el_lift : lift -> lift
22
val reloc_rel : int -> lift -> int
23
val is_lift_id : lift -> bool
25
(*s Explicit substitutions of type ['a]. *)
27
| ESID of int (* ESID(n) = %n END bounded identity *)
28
| CONS of 'a array * 'a subs
29
(* CONS([|t1..tn|],S) =
30
(S.t1...tn) parallel substitution
31
beware of the order *)
32
| SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
34
| LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
36
val subs_cons: 'a array * 'a subs -> 'a subs
37
val subs_shft: int * 'a subs -> 'a subs
38
val subs_lift: 'a subs -> 'a subs
39
val subs_liftn: int -> 'a subs -> 'a subs
40
val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
41
val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
42
val is_subs_id: 'a subs -> bool
43
val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs