diff options
| author | Pierre-Marie Pédrot | 2020-05-14 13:58:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-22 12:46:20 +0200 |
| commit | 675b23dcf824d8a851881171a5628b239aad2201 (patch) | |
| tree | 90b800d6524b93c23c0adc6e0a941db7f421cc79 /kernel/cemitcodes.ml | |
| parent | e6d92a9765f84c80f8c6a102fe5480490c747313 (diff) | |
Remove redundant data from VM case switch.
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 6b4daabf0c..ed475dca7e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,6 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Constr open Vmvalues open Cbytecodes open Copcodes @@ -424,12 +423,11 @@ let subst_strcst s sc = | Const_float _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) +let subst_annot _ (a : annot_switch) = a + let subst_reloc s ri = match ri with - | Reloc_annot a -> - let (kn,i) = a.ci.ci_ind in - let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - Reloc_annot {a with ci = ci} + | Reloc_annot a -> Reloc_annot (subst_annot s a) | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) |