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/byterun | |
| 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/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 1 |
2 files changed, 2 insertions, 1 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)) |