From 2d63a61a991ab42f2124775b184898d7af6725dd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 08:34:25 +0200 Subject: Use the same memory layout as closures for accumulators. That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing. --- kernel/byterun/coq_values.h | 1 - 1 file changed, 1 deletion(-) (limited to 'kernel/byterun/coq_values.h') diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a19f9b56c1..bde6e14367 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,7 +30,6 @@ /* Les blocs accumulate */ #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) -- cgit v1.2.3 From 27695b52413f9fd6bcb60d77e0bdba538c16201f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 11:40:24 +0200 Subject: Use the closure tag for accumulators. The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction. --- kernel/byterun/coq_values.h | 3 --- 1 file changed, 3 deletions(-) (limited to 'kernel/byterun/coq_values.h') diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index bde6e14367..f07018711b 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -17,7 +17,6 @@ #include #define Default_tag 0 -#define Accu_tag 0 #define ATOM_ID_TAG 0 #define ATOM_INDUCTIVE_TAG 1 @@ -28,8 +27,6 @@ #define ATOM_COFIX_TAG 6 #define ATOM_COFIXEVALUATED_TAG 7 -/* Les blocs accumulate */ -#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -- cgit v1.2.3