diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 97 |
1 files changed, 49 insertions, 48 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ccd49ca495..4dc584cfa8 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -606,7 +606,7 @@ let map_left2 f a g b = r, s end -let map_constr_with_binders_left_to_right sigma g f l c = +let map_constr_with_binders_left_to_right env sigma g f l c = let open RelDecl in let open EConstr in match EConstr.kind sigma c with @@ -650,14 +650,20 @@ let map_constr_with_binders_left_to_right sigma g f l c = let al' = List.map_left (f l) al in if List.for_all2 (==) al' al then c else mkEvar (e, al') - | Case (ci,p,iv,b,bl) -> + | Case (ci,u,pms,p,iv,b,bl) -> + 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 (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 @@ -677,25 +683,8 @@ let map_constr_with_binders_left_to_right sigma g f l c = if def' == def && t' == t && ty' == ty then c else mkArray(u,t',def',ty') -let map_under_context_with_full_binders sigma g f l n d = - let open EConstr in - let f l c = Unsafe.to_constr (f l (of_constr c)) in - let g d l = g (of_rel_decl d) l in - let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in - EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d) - -let map_branches_with_full_binders sigma g f l ci bl = - let tags = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in - if Array.for_all2 (==) bl' bl then bl else bl' - -let map_return_predicate_with_full_binders sigma g f l ci p = - let n = List.length ci.ci_pp_info.ind_tags in - let p' = map_under_context_with_full_binders sigma g f l n p in - if p' == p then p else p' - (* strong *) -let map_constr_with_full_binders_gen userview sigma g f l cstr = +let map_constr_with_full_binders env sigma g f l cstr = let open EConstr in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -727,20 +716,19 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = | Evar (e,al) -> let al' = List.map (f l) al in if List.for_all2 (==) al al' then cstr else mkEvar (e, al') - | Case (ci,p,iv,c,bl) when userview -> - let p' = map_return_predicate_with_full_binders sigma g f l ci p in - let iv' = map_invert (f l) iv in - let c' = f l c in - let bl' = map_branches_with_full_binders sigma g f l ci bl in - if p==p' && iv'==iv && c==c' && bl'==bl then cstr else - mkCase (ci, p', iv', c', bl') - | Case (ci,p,iv,c,bl) -> - let p' = f l p in + | Case (ci, u, pms, p, iv, c, bl) -> + 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 (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 @@ -761,12 +749,6 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let ty' = f l ty in if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty') -let map_constr_with_full_binders sigma g f = - map_constr_with_full_binders_gen false sigma g f - -let map_constr_with_full_binders_user_view sigma g f = - map_constr_with_full_binders_gen true sigma g f - (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions as @@ -774,12 +756,31 @@ let map_constr_with_full_binders_user_view sigma g f = index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_full_binders sigma g f n acc c = - let open EConstr in - let f l acc c = f l acc (of_constr c) in - let g d l = g (of_rel_decl d) l in - let c = Unsafe.to_constr (whd_evar sigma c) in - Constr.fold_with_full_binders g f n acc c +let fold_constr_with_full_binders env sigma g f n acc c = + let open EConstr.Vars in + let open Context.Rel.Declaration in + match EConstr.kind sigma c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | 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, _, 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 + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(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 + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty let fold_constr_with_binders sigma g f n acc c = let open EConstr in |