diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/termops.ml | 33 |
2 files changed, 25 insertions, 16 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index cfc4bea85f..40e48998d6 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -296,6 +296,8 @@ let decompose_prod_n_assum sigma n c = let existential_type = Evd.existential_type +let lift n c = of_constr (Vars.lift n (unsafe_to_constr c)) + let map_under_context f n c = let f c = unsafe_to_constr (f (of_constr c)) in of_constr (Constr.map_under_context f n (unsafe_to_constr c)) @@ -453,11 +455,11 @@ let iter_with_full_binders sigma g f n c = | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in Array.iter (f n') bl | CoFix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in Array.iter (f n') bl let iter_with_binders sigma g f n c = @@ -712,7 +714,7 @@ let to_rel_decl = unsafe_to_rel_decl type substl = t list (** Operations that commute with evar-normalization *) -let lift n c = of_constr (Vars.lift n (to_constr c)) +let lift = lift let liftn n m c = of_constr (Vars.liftn n m (to_constr c)) let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c)) diff --git a/engine/termops.ml b/engine/termops.ml index ada6311067..64048777ad 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -721,18 +721,16 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let bl' = Array.map (f l) bl in if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else mkCase (ci, p', c', bl') - | Fix (ln,(lna,tl,bl)) -> + | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> + | CoFix(ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -759,7 +757,10 @@ let fold_constr_with_full_binders sigma g f n acc c = Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = - fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_constr_with_binders g f n acc c (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at @@ -780,13 +781,19 @@ let iter_constr_with_full_binders sigma g f l c = | Evar (_,args) -> Array.iter (f l) args | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl | Fix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl + let l' = Array.fold_left2_i (fun i l na t -> + g (LocalAssum (na, EConstr.Vars.lift i t)) l) + l lna tl + in + Array.iter (f l) tl; + Array.iter (f l') bl | CoFix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl + let l' = Array.fold_left2_i (fun i l na t -> + g (LocalAssum (na, EConstr.Vars.lift i t)) l) + l lna tl + in + Array.iter (f l) tl; + Array.iter (f l') bl (***************************) (* occurs check functions *) |