nouvelle implantation de la reduction

suppression de IsXtra du noyau


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 34 insertions, 0 deletions

diff --git a/kernel/esubst.mli b/kernel/esubst.mli
new file mode 100644
index 000000000..ea5df0a28
--- /dev/null
+++ b/kernel/esubst.mli
@@ -0,0 +1,34 @@
+
+(* $Id$ *)
+
+(*s 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. *)
+type lift =
+  | ELID
+  | ELSHFT of lift * int
+  | ELLFT of int * 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
+
+(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. 
+  [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
+  $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
+  [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+type 'a subs =
+  | ESID of int
+  | CONS of 'a * 'a subs
+  | SHIFT of int * 'a subs
+  | LIFT of int * 'a subs
+
+val subs_cons: 'a * '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 -> 'a subs
+val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
+val is_subs_id: 'a subs -> bool