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/vmvalues.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/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 20 |
1 files changed, 7 insertions, 13 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index ec429d5f9e..de604176cb 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names open Univ -open Constr (********************************************) (* Initialization of the abstract machine ***) @@ -61,8 +60,9 @@ type structured_constant = type reloc_table = (tag * int) array +(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *) type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } let rec eq_structured_values v1 v2 = v1 == v2 || @@ -123,22 +123,16 @@ let hash_structured_constant c = | Const_float f -> combinesmall 7 (Float64.hash f) let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && CArray.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall + (asw1.tailcall : bool) == asw2.tailcall && + Int.equal asw1.max_stack_size asw2.max_stack_size let hash_annot_switch asw = let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 + let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h2 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 asw.max_stack_size let pp_sort s = let open Sorts in |