diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-27 12:12:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-27 13:25:54 +0200 |
| commit | 4fba4b00257e8ddbc94f71115d139bfc2483944d (patch) | |
| tree | 77338ae34ec87c6697e6bcfc94792c7c25899af1 | |
| parent | 01b7de3a673eb89cea61442c4db721aad9520c9f (diff) | |
Expliciting and taking advantage of a representation invariant in Esubst.
| -rw-r--r-- | kernel/esubst.ml | 10 | ||||
| -rw-r--r-- | kernel/esubst.mli | 6 |
2 files changed, 11 insertions, 5 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml index a11a0dc00..91cc64523 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -19,6 +19,8 @@ open Util (*********************) (* Explicit lifts and basic operations *) +(* Invariant to preserve in this module: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. *) type lift = | ELID | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *) @@ -28,15 +30,15 @@ type lift = let el_id = ELID (* compose a relocation of magnitude n *) -let rec el_shft_rec n = function - | ELSHFT(el,k) -> el_shft_rec (k+n) el +let el_shft_rec n = function + | ELSHFT(el,k) -> ELSHFT(el,k+n) | el -> ELSHFT(el,n) let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) -let rec el_liftn_rec n = function +let el_liftn_rec n = function | ELID -> ELID - | ELLFT(k,el) -> el_liftn_rec (n+k) el + | ELLFT(k,el) -> ELLFT(n+k, el) | el -> ELLFT(n, el) let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el diff --git a/kernel/esubst.mli b/kernel/esubst.mli index b82d6fdf0..a674c425a 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** {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. *) + - [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]. +*) type lift = private | ELID | ELSHFT of lift * int |