diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 36 |
1 files changed, 23 insertions, 13 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index d331ecc458..4dc584cfa8 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -651,15 +651,19 @@ let map_constr_with_binders_left_to_right env sigma g f l c = if List.for_all2 (==) al' al then c else mkEvar (e, al') | Case (ci,u,pms,p,iv,b,bl) -> - (* FIXME: skip annotations? *) - let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in + let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in + let f_ctx (nas, _ as r) (ctx, c) = + let c' = f (List.fold_right g ctx l) c in + if c' == c then r else (nas, c') + in (* In v8 concrete syntax, predicate is after the term to match! *) let b' = f l b in + let pms' = Array.map_left (f l) pms in + let p' = f_ctx p p0 in let iv' = map_invert (f l) iv in - let p' = f l p in - let bl' = Array.map_left (f l) bl in - if b' == b && p' == p && iv' == iv && bl' == bl then c - else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl')) + let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in + if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c + else mkCase (ci, u, pms', p', iv', b', bl') | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in let (tl', bl') = map_left2 (f l) tl (f l') bl in @@ -713,13 +717,18 @@ let map_constr_with_full_binders env sigma g f l cstr = let al' = List.map (f l) al in if List.for_all2 (==) al al' then cstr else mkEvar (e, al') | Case (ci, u, pms, p, iv, c, bl) -> - let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in - let p' = f l p in + let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in + let f_ctx (nas, _ as r) (ctx, c) = + let c' = f (List.fold_right g ctx l) c in + if c' == c then r else (nas, c') + in + let pms' = Array.Smart.map (f l) pms in + let p' = f_ctx p p0 in let iv' = map_invert (f l) iv in let c' = f l c in - let bl' = Array.map (f l) bl in - if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else - mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl')) + let bl' = Array.map2 f_ctx bl bl0 in + if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else + mkCase (ci, u, pms', p', iv', c', bl') | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in let l' = fold_rec_types g fx l in @@ -760,8 +769,9 @@ let fold_constr_with_full_binders env sigma g f n acc c = | Proj (_,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l | Case (ci, u, pms, p, iv, c, bl) -> - let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in - Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + let (ci, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in + let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in + Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) p) iv) c) bl | Fix (_,(lna,tl,bl)) -> let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in |