aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-06-12 17:44:29 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:51:20 +0200
commit5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f (patch)
tree9c71c3f6b678ccbfdcb882fc6a951ad303f7850a /checker
parentab0c49baa8d57ed92a79e7d0b0737267042210f8 (diff)
use map_constr more efficiently
Diffstat (limited to 'checker')
-rw-r--r--checker/term.ml42
1 files changed, 30 insertions, 12 deletions
diff --git a/checker/term.ml b/checker/term.ml
index c0f8e0106..dea3d3e65 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -413,18 +413,36 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
let subst_instance_constr subst c =
- let f u = Univ.subst_instance_instance subst u in
- let rec aux t =
- match t with
- | Const (c, u) -> Const (c, f u)
- | Ind (i, u) -> Ind (i, f u)
- | Construct (c, u) -> Construct (c, f u)
- | Sort (Type u) ->
- let u' = Univ.subst_instance_universe subst u in
- Sort (sort_of_univ u')
- | _ -> map_constr 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 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 (Const (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 (Ind (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 (Construct (c, u'))
+ | Sort (Type u) ->
+ let u' = Univ.subst_instance_universe subst u in
+ if u' == u then t else
+ (Sort (sort_of_univ u'))
+ | _ -> map_constr aux t
+ in
+ aux c
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx