From 055887ac67ed8bb7917408e23b1496f094d97ccd Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 9 Sep 2008 13:35:47 +0000
Subject: added comments in esubst.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11394 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/esubst.mli | 60 ++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 40 insertions(+), 20 deletions(-)

(limited to 'kernel/esubst.mli')

diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 68f5f2201..75d460ce6 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -8,6 +8,46 @@
 
 (*i $Id$ i*)
 
+(*s 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) *)
+type 'a subs =
+  | ESID of int
+  | CONS of 'a array * 'a subs
+  | SHIFT of int * 'a subs
+  | LIFT of 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
+(* [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
+val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
+
+(* [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 expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
+
+(* Tests whether a substitution behaves like the identity *)
+val is_subs_id: 'a subs -> bool
+
+(* 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.
+ *)
+val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
+
 (*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. *)
@@ -21,23 +61,3 @@ 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]. *)
-type 'a subs =
-  | ESID of int            (* ESID(n)    = %n END   bounded identity *)
-  | CONS of 'a array * 'a subs
-                           (* CONS([|t1..tn|],S)  =
-                              (S.t1...tn)    parallel substitution
-                              beware of the order *)
-  | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
-                           (*                        with n vars *)
-  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
-
-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
-val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
-val is_subs_id: 'a subs -> bool
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
-- 
cgit v1.2.3