diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 1 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 2 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 8 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 20 | ||||
| -rw-r--r-- | kernel/vmvalues.mli | 3 |
6 files changed, 14 insertions, 22 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 9921208e04..15cc451ea8 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1187,7 +1187,7 @@ value coq_interprete if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { + if (Is_tailrec_switch(*sp)) { for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; }else{ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 86ae6295fd..a19f9b56c1 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) +#define Is_tailrec_switch(v) (Field(v,1) == Val_true) /* coq array */ #define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7bff377238..bacc308e1f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont = done; let annot = - {ci = ci; rtbl = rtbl; tailcall = is_tailcall; + {rtbl = rtbl; tailcall = is_tailcall; max_stack_size = !max_stack_size - sz} in 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) 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 diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index f4070a02a3..f6efd49cfc 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr (** Values *) @@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } val eq_structured_constant : structured_constant -> structured_constant -> bool val hash_structured_constant : structured_constant -> int |