diff options
| -rw-r--r-- | checker/closure.ml | 6 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 | ||||
| -rw-r--r-- | checker/term.ml | 2 | ||||
| -rw-r--r-- | kernel/closure.ml | 6 | ||||
| -rw-r--r-- | kernel/esubst.ml | 4 | ||||
| -rw-r--r-- | kernel/esubst.mli | 6 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 2 | ||||
| -rw-r--r-- | pretyping/cbv.ml | 4 |
10 files changed, 21 insertions, 15 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 2227e392e..033e2bd73 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -428,7 +428,7 @@ let optimise_closure env c = let (c',(_,s)) = compact_constr (0,[]) c 1 in let env' = Array.map (fun i -> clos_rel env i) (Array.of_list s) in - (subs_cons (env', ESID 0),c') + (subs_cons (env', subs_id 0),c') let mk_lambda env t = let (env,t) = optimise_closure env t in @@ -559,7 +559,7 @@ let term_of_fconstr = | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift ELID + term_of_fconstr_lift el_id @@ -806,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (ESID 0) +let inject = mk_clos (subs_id 0) let whd_stack infos m stk = let k = kni infos m stk in diff --git a/checker/reduction.ml b/checker/reduction.ml index efeaff07f..3aeaa1023 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -372,7 +372,7 @@ and convert_vect univ infos lft1 lft2 v1 v2 = let clos_fconv cv_pb env t1 t2 = let infos = create_clos_infos betaiotazeta env in let univ = universes env in - ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2) + ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2) let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then () diff --git a/checker/term.ml b/checker/term.ml index 7d2241228..ab40b6fa7 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -261,7 +261,7 @@ let rec exliftn el c = match c with (* Lifting the binding depth across k bindings *) let liftn k n = - match el_liftn (pred n) (el_shft k ELID) with + match el_liftn (pred n) (el_shft k el_id) with | ELID -> (fun c -> c) | el -> exliftn el diff --git a/kernel/closure.ml b/kernel/closure.ml index 8d4758cfd..143d6eb49 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -514,7 +514,7 @@ let optimise_closure env c = let (c',(_,s)) = compact_constr (0,[]) c 1 in let env' = Array.map (fun i -> clos_rel env i) (Array.of_list s) in - (subs_cons (env', ESID 0),c') + (subs_cons (env', subs_id 0),c') let mk_lambda env t = let (env,t) = optimise_closure env t in @@ -647,7 +647,7 @@ let term_of_fconstr = | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> mkFix fx | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> mkCoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift ELID + term_of_fconstr_lift el_id @@ -963,7 +963,7 @@ let whd_val info v = let norm_val info v = with_stats (lazy (kl info v)) -let inject = mk_clos (ESID 0) +let inject = mk_clos (subs_id 0) let whd_stack infos m stk = let k = kni infos m stk in diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 2e1b42d43..cbce04d62 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -23,6 +23,8 @@ type lift = | ELLFT of int * lift (* ELLFT(n,l) == apply l to de Bruijn > n *) (* i.e under n binders *) +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 @@ -69,6 +71,8 @@ type 'a subs = * Needn't be recursive if we always use these functions *) +let subs_id i = ESID i + let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s) let subs_liftn n = function diff --git a/kernel/esubst.mli b/kernel/esubst.mli index e605fa212..fe978261e 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -16,13 +16,14 @@ - 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 *) +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 @@ -54,11 +55,12 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** 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 = +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 diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c1c7f521a..1a286bb16 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -426,7 +426,7 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv = let clos_fconv trans cv_pb evars env t1 t2 = let infos = trans, create_clos_infos ~evars betaiotazeta env in - ccnv cv_pb infos ELID ELID (inject t1) (inject t2) empty_constraint + ccnv cv_pb infos el_id el_id (inject t1) (inject t2) empty_constraint let trans_fconv reds cv_pb evars env t1 t2 = if eq_constr t1 t2 then empty_constraint diff --git a/kernel/term.ml b/kernel/term.ml index 99a0e6bb3..83c417d95 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -787,7 +787,7 @@ let rec exliftn el c = match kind_of_term c with (* Lifting the binding depth across k bindings *) let liftn n k = - match el_liftn (pred k) (el_shft n ELID) with + match el_liftn (pred k) (el_shft n el_id) with | ELID -> (fun c -> c) | el -> exliftn el diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index fa56313d8..6ff673023 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -95,7 +95,7 @@ let lookup_map map = let protect_red map env sigma c = kl (create_clos_infos betadeltaiota env) - (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);; + (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 85112c288..cd8314573 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -356,14 +356,14 @@ and cbv_norm_value info = function (* reduction under binders *) (* with profiling *) let cbv_norm infos constr = - with_stats (lazy (cbv_norm_term infos (ESID 0) constr)) + with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)) type cbv_infos = cbv_value infos (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = create - (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c) + (fun old_info c -> cbv_stack_term old_info TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) |