diff options
Diffstat (limited to 'kernel/esubst.mli')
-rw-r--r-- | kernel/esubst.mli | 61 |
1 files changed, 33 insertions, 28 deletions
diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 76c0d481..fe978261 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,61 +1,66 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: esubst.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** Explicit substitutions *) -(*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) +(** {6 Explicit substitutions } *) +(** 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 = +type 'a subs = private | ESID of int | CONS of 'a array * 'a subs | SHIFT of int * 'a subs | LIFT of int * 'a subs -(* Derived constructors granting basic invariants *) +(** Derived constructors granting basic invariants *) +val subs_id : int -> 'a subs 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 *) + +(** [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). - *) +(** [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 *) +(** 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. - *) +(** 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. *) -type lift = +(** {6 Compact representation } *) +(** 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 = private | ELID | ELSHFT of lift * int | ELLFT of int * lift +val el_id : lift val el_shft : int -> lift -> lift val el_liftn : int -> lift -> lift val el_lift : lift -> lift |