From 5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 12 Jun 2017 17:44:29 +0200 Subject: use map_constr more efficiently --- kernel/vars.ml | 42 ++++++++++++++++++++++++++++++------------ 1 file changed, 30 insertions(+), 12 deletions(-) (limited to 'kernel/vars.ml') diff --git a/kernel/vars.ml b/kernel/vars.ml index 89c17b850..baf8fa31f 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -316,18 +316,36 @@ let subst_univs_level_context s = Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = - let f u = Univ.subst_instance_instance subst u in - let rec aux t = - match kind t with - | Const (c, u) -> mkConstU (c, f u) - | Ind (i, u) -> mkIndU (i, f u) - | Construct (c, u) -> mkConstructU (c, f u) - | Sort (Sorts.Type u) -> - let u' = Univ.subst_instance_universe subst u in - mkSort (Sorts.sort_of_univ u') - | _ -> Constr.map aux t - in - aux c + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let rec aux t = + match kind t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstU (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkIndU (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstructU (c, u')) + | Sort (Sorts.Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (mkSort (Sorts.sort_of_univ u')) + | _ -> Constr.map aux t + in + aux c (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) -- cgit v1.2.3