From fae106f740d3d71555933cf416eec905c58f417e Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 23 Mar 2001 15:04:09 +0000 Subject: amelioration de la consommation memoire de la conversion en eta-expansant les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/esubst.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'kernel/esubst.ml') diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 7d24804cc..46be7a747 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -22,18 +22,19 @@ type lift = (* i.e under n binders *) (* compose a relocation of magnitude n *) -let rec el_shft n = function - | ELSHFT(el,k) -> el_shft (k+n) el - | el -> if n = 0 then el else ELSHFT(el,n) - +let rec el_shft_rec n = function + | ELSHFT(el,k) -> el_shft_rec (k+n) el + | el -> ELSHFT(el,n) +let el_shft n el = if n = 0 then el else el_shft_rec n el (* cross n binders *) -let rec el_liftn n = function - | ELID -> ELID - | ELLFT(k,el) -> el_liftn (n+k) el - | el -> if n=0 then el else ELLFT(n, el) +let rec el_liftn_rec n = function + | ELID -> ELID + | ELLFT(k,el) -> el_liftn_rec (n+k) el + | el -> ELLFT(n, el) +let el_liftn n el = if n = 0 then el else el_liftn_rec n el -let el_lift el = el_liftn 1 el +let el_lift el = el_liftn_rec 1 el (* relocation of de Bruijn n in an explicit lift *) let rec reloc_rel n = function -- cgit v1.2.3