diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 22 | ||||
| -rw-r--r-- | engine/eConstr.mli | 7 | ||||
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 42 | ||||
| -rw-r--r-- | engine/termops.mli | 4 |
6 files changed, 71 insertions, 8 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3dc1933a14..2913645c1c 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -259,7 +259,17 @@ let decompose_prod_n_assum sigma n c = let existential_type = Evd.existential_type -let map sigma f c = match kind sigma c with +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)) +let map_branches f ci br = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br)) +let map_return_predicate f ci p = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p)) + +let map_gen userview sigma f c = match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c | Cast (b,k,t) -> @@ -296,6 +306,12 @@ let map sigma f c = match kind sigma c with let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') + | Case (ci,p,b,bl) when userview -> + let b' = f b in + let p' = map_return_predicate f ci p in + let bl' = map_branches f ci bl in + if b'==b && p'==p && bl'==bl then c + else mkCase (ci, p', b', bl') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in @@ -313,6 +329,9 @@ let map sigma f c = match kind sigma c with if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) +let map_user_view = map_gen true +let map = map_gen false + let map_with_binders sigma g f l c0 = match kind sigma c0 with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c0 @@ -794,6 +813,7 @@ struct let to_sorts = ESorts.unsafe_to_sorts let to_instance = EInstance.unsafe_to_instance let to_constr = unsafe_to_constr +let to_constr_array = unsafe_to_constr_array let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl let to_named_context = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index ecb36615f3..f897448557 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -224,7 +224,11 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) val map : Evd.evar_map -> (t -> t) -> t -> t +val map_user_view : Evd.evar_map -> (t -> t) -> t -> t val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t +val map_under_context : (t -> t) -> int -> t -> t +val map_branches : (t -> t) -> case_info -> t array -> t array +val map_return_predicate : (t -> t) -> case_info -> t -> t val iter : Evd.evar_map -> (t -> unit) -> t -> unit val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit @@ -315,6 +319,9 @@ sig val to_constr : t -> Constr.t (** Physical identity. Does not care for defined evars. *) + val to_constr_array : t array -> Constr.t array + (** Physical identity. Does not care for defined evars. *) + val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt (** Physical identity. Does not care for defined evars. *) diff --git a/engine/evd.ml b/engine/evd.ml index d1c7fef738..faf5f02353 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1267,7 +1267,9 @@ module MiniEConstr = struct let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind let of_constr c = c + let of_constr_array v = v let unsafe_to_constr c = c + let unsafe_to_constr_array v = v let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = diff --git a/engine/evd.mli b/engine/evd.mli index db2bd4eedf..1a5614988d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -657,10 +657,12 @@ module MiniEConstr : sig val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t val of_constr : Constr.t -> t + val of_constr_array : Constr.t array -> t array val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t val unsafe_to_constr : t -> Constr.t + val unsafe_to_constr_array : t array -> Constr.t array val unsafe_eq : (t, Constr.t) eq diff --git a/engine/termops.ml b/engine/termops.ml index e4c8ae66bc..156d1370e3 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -715,10 +715,26 @@ let map_constr_with_binders_left_to_right sigma g f l c = then c else mkCoFix (ln,(lna,tl',bl')) +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 sigma g f l cstr = +let map_constr_with_full_binders_gen userview sigma g f l cstr = let open EConstr in - let open RelDecl in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> cstr @@ -728,16 +744,16 @@ let map_constr_with_full_binders sigma g f l cstr = if c==c' && t==t' then cstr else mkCast (c', k, t') | Prod (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na, t)) l) c in + let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in if t==t' && c==c' then cstr else mkProd (na, t', c') | Lambda (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na, t)) l) c in + let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in if t==t' && c==c' then cstr else mkLambda (na, t', c') | LetIn (na,b,t,c) -> let b' = f l b in let t' = f l t in - let c' = f (g (LocalDef (na, b, t)) l) c in + let c' = f (g (RelDecl.LocalDef (na, b, t)) l) c in if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c') | App (c,al) -> let c' = f l c in @@ -749,6 +765,12 @@ let map_constr_with_full_binders sigma g f l cstr = | Evar (e,al) -> let al' = Array.map (f l) al in if Array.for_all2 (==) al al' then cstr else mkEvar (e, al') + | Case (ci,p,c,bl) when userview -> + let p' = map_return_predicate_with_full_binders sigma g f l ci p in + let c' = f l c in + let bl' = map_branches_with_full_binders sigma g f l ci bl in + if p==p' && c==c' && bl'==bl then cstr else + mkCase (ci, p', c', bl') | Case (ci,p,c,bl) -> let p' = f l p in let c' = f l c in @@ -758,7 +780,7 @@ let map_constr_with_full_binders sigma g f l cstr = | Fix (ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -766,12 +788,18 @@ let map_constr_with_full_binders sigma g f l cstr = | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl')) +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 diff --git a/engine/termops.mli b/engine/termops.mli index 80988989f1..b967bb6abb 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -63,6 +63,10 @@ val map_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +val map_constr_with_full_binders_user_view : + Evd.evar_map -> + (rel_declaration -> 'a -> 'a) -> + ('a -> constr -> constr) -> 'a -> constr -> constr (** [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 |