diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 40 |
1 files changed, 37 insertions, 3 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3dc1933a14..678f7c6ce6 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 @@ -426,10 +445,22 @@ let fold sigma f acc c = match kind sigma c with let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 +let eq_einstance sigma i1 i2 = + let i1 = EInstance.kind sigma (EInstance.make i1) in + let i2 = EInstance.kind sigma (EInstance.make i2) in + Univ.Instance.equal i1 i2 + +let eq_esorts sigma s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in + Sorts.equal s1 s2 + let eq_constr sigma c1 c2 = let kind c = kind_upto sigma c in + let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in + let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in let rec eq_constr nargs c1 c2 = - compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2 + compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2 in eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) @@ -442,8 +473,10 @@ let eq_constr_nounivs sigma c1 c2 = let compare_constr sigma cmp c1 c2 = let kind c = kind_upto sigma c in + let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in + let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let open UnivProblem in @@ -794,6 +827,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 = |