diff options
| author | Pierre-Marie Pédrot | 2019-11-21 09:23:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-22 08:35:57 +0100 |
| commit | b8b835cbb7ce5fa12a60184fd83fbde2082d51b3 (patch) | |
| tree | 195f3539dbd72866624506c800dec1d6da611bfd /pretyping | |
| parent | 83ab871c90c862ebb08bcc549701beec0afc6cce (diff) | |
Use the relevance flag in CClosure rel contexts in an efficient way.
Rels that exist inside the environment at the time of the closure creation
are fetched in the global environment, while we only use the local list of
relevance for FRels. All the infrastructure was implicitly relying on this
kind of behaviour before the introduction of SProp.
Fixes #11150: pattern is 10x slower in Coq 8.10.0
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f089b242a2..d2af957b54 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -264,16 +264,19 @@ let relevance_of_term env sigma c = if Environ.sprop_allowed env then let rec aux rels c = match kind sigma c with - | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Rel n -> + let len = Range.length rels in + if n <= len then Range.get rels (n - 1) + else Retypeops.relevance_of_rel env (n - len) | Var x -> Retypeops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> - aux (r::rels) codom + aux (Range.cons r rels) codom | Lambda ({binder_relevance=r}, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | LetIn ({binder_relevance=r}, _, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | App (c, _) -> aux rels c | Const (c,_) -> Retypeops.relevance_of_constant env c | Ind _ -> Sorts.Relevant @@ -287,7 +290,7 @@ let relevance_of_term env sigma c = | Meta _ | Evar _ -> Sorts.Relevant in - aux [] c + aux Range.empty c else Sorts.Relevant let relevance_of_type env sigma t = |