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

4 files changed, 28 insertions, 29 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f2cb9a8aec..b7bd4eef9a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -302,7 +302,7 @@ let unfold_ref_with_args infos tab fl v =
 
 type conv_tab = {
   cnv_inf : clos_infos;
-  relevances : Sorts.relevance list;
+  relevances : Sorts.relevance Range.t;
   lft_tab : clos_tab;
   rgt_tab : clos_tab;
 }
@@ -313,16 +313,16 @@ type conv_tab = {
     passed to each respective side of the conversion function below. *)
 
 let push_relevance infos r =
-  { infos with relevances = r.Context.binder_relevance :: infos.relevances }
+  { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances }
 
 let push_relevances infos nas =
-  { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas }
+  { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas }
 
 let rec skip_pattern infos relevances n c1 c2 =
   if Int.equal n 0 then {infos with relevances}, c1, c2
   else match kind c1, kind c2 with
     | Lambda (x, _, c1), Lambda (_, _, c2) ->
-      skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2
+      skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
     | _ -> raise IrregularPatternShape
 
 let skip_pattern infos n c1 c2 =
@@ -705,7 +705,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let infos = create_clos_infos ~evars reds env in
   let infos = {
     cnv_inf = infos;
-    relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env);
+    relevances = Range.empty;
     lft_tab = create_tab ();
     rgt_tab = create_tab ();
   } in
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index 5c15257511..6a1b36ea94 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -39,16 +39,10 @@ let relevance_of_projection env p =
   let mib = lookup_mind mind env in
   Declareops.relevance_of_projection_repr mib (Projection.repr p)
 
-let rec relevance_of_rel_extra env extra n =
-  match extra with
-  | [] -> relevance_of_rel env n
-  | r :: _ when Int.equal n 1 -> r
-  | _ :: extra -> relevance_of_rel_extra env extra (n-1)
-
-let relevance_of_flex env extra lft = function
+let relevance_of_flex env = function
   | ConstKey (c,_) -> relevance_of_constant env c
   | VarKey x -> relevance_of_var env x
-  | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft)
+  | RelKey p -> relevance_of_rel env p
 
 let rec relevance_of_fterm env extra lft f =
   let open CClosure in
@@ -57,9 +51,9 @@ let rec relevance_of_fterm env extra lft f =
   | KnownI -> Sorts.Irrelevant
   | Unknown ->
     let r = match fterm_of f with
-      | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
+      | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1)
       | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
-      | FFlex key -> relevance_of_flex env extra lft key
+      | FFlex key -> relevance_of_flex env key
       | FInt _ | FFloat _ -> Sorts.Relevant
       | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
       | FConstruct (c,_) -> relevance_of_constructor env c
@@ -69,12 +63,12 @@ let rec relevance_of_fterm env extra lft f =
       | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
       | FCaseT (ci, _, _, _, _) -> ci.ci_relevance
       | FLambda (len, tys, bdy, e) ->
-        let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
+        let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
         let lft = Esubst.el_liftn len lft in
         let e = Esubst.subs_liftn len e in
         relevance_of_term_extra env extra lft e bdy
       | FLetIn (x, _, _, bdy, e) ->
-        relevance_of_term_extra env (x.binder_relevance :: extra)
+        relevance_of_term_extra env (Range.cons x.binder_relevance extra)
           (Esubst.el_lift lft) (Esubst.subs_lift e) bdy
       | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f
       | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c
@@ -88,16 +82,18 @@ let rec relevance_of_fterm env extra lft f =
 and relevance_of_term_extra env extra lft subs c =
   match kind c with
   | Rel n ->
-    (match Esubst.expand_rel n subs with
+    begin match Esubst.expand_rel n subs with
      | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f
-     | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft))
+     | Inr (n, None) -> Range.get extra (Esubst.reloc_rel n lft - 1)
+     | Inr (_, Some p) -> relevance_of_rel env p
+    end
   | Var x -> relevance_of_var env x
   | Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *)
   | Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c
   | Lambda ({binder_relevance=r;_}, _, bdy) ->
-    relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+    relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
   | LetIn ({binder_relevance=r;_}, _, _, bdy) ->
-    relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+    relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
   | App (c, _) -> relevance_of_term_extra env extra lft subs c
   | Const (c,_) -> relevance_of_constant env c
   | Construct (c,_) -> relevance_of_constructor env c
@@ -115,5 +111,5 @@ let relevance_of_fterm env extra lft c =
 
 let relevance_of_term env c =
   if Environ.sprop_allowed env
-  then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c
+  then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c
   else Sorts.Relevant
diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli
index f4497be44b..dd4513959f 100644
--- a/kernel/retypeops.mli
+++ b/kernel/retypeops.mli
@@ -14,14 +14,14 @@
 
 val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance
 
-val relevance_of_fterm : Environ.env -> Sorts.relevance list ->
+val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t ->
   Esubst.lift -> CClosure.fconstr ->
   Sorts.relevance
 
 
 (** Helpers *)
 open Names
-val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance
+val relevance_of_rel : Environ.env -> int -> Sorts.relevance
 val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance
 val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance
 val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance
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 =