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 /kernel/reduction.ml | |
| 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 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 10 |
1 files changed, 5 insertions, 5 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 |