aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c15
-rw-r--r--kernel/byterun/coq_memory.c2
-rw-r--r--kernel/byterun/coq_values.h3
-rw-r--r--kernel/vmvalues.ml55
-rw-r--r--kernel/vmvalues.mli2
5 files changed, 34 insertions, 43 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 40ddcbb213..1b6da7dd6f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -193,6 +193,8 @@ if (sp - num_args < coq_stack_threshold) { \
#endif
#endif
+#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate)
+
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
else{ \
@@ -726,7 +728,7 @@ value coq_interprete
accu = block;
/* Construction of the accumulator */
num_args = coq_extra_args - rec_pos;
- Alloc_small(block, 3 + num_args, Accu_tag);
+ Alloc_small(block, 3 + num_args, Closure_tag);
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
Field(block, 2) = accu;
@@ -808,7 +810,7 @@ value coq_interprete
/* Creation des blocks accumulate */
for(i=0; i < nfunc; i++) {
- Alloc_small(accu, 3, Accu_tag);
+ Alloc_small(accu, 3, Closure_tag);
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
Field(accu, 2) = Val_int(1);
@@ -957,6 +959,7 @@ value coq_interprete
print_int(sizes & 0xFFFFFF);
if (Is_block(accu)) {
long index = Tag_val(accu);
+ if (index == Closure_tag) index = 0;
print_instr("block");
print_lint(index);
pc += pc[(sizes & 0xFFFFFF) + index];
@@ -1062,7 +1065,7 @@ value coq_interprete
Field(accu, 0) = Field(coq_global_data, *pc++);
Field(accu, 1) = *sp++;
/* Create accumulator */
- Alloc_small(block, 3, Accu_tag);
+ Alloc_small(block, 3, Closure_tag);
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
Field(block, 2) = accu;
@@ -1126,7 +1129,7 @@ value coq_interprete
mlsize_t i, size;
print_instr("ACCUMULATE");
size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+ Alloc_small(accu, size + coq_extra_args + 1, Closure_tag);
for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
for(i = size; i <= coq_extra_args + size; i++)
Field(accu, i) = *sp++;
@@ -1220,7 +1223,7 @@ value coq_interprete
Field(block, 1) = accu;
accu = block;
/* We create the accumulator */
- Alloc_small(block, 3, Accu_tag);
+ Alloc_small(block, 3, Closure_tag);
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
Field(block, 2) = accu;
@@ -1235,7 +1238,7 @@ value coq_interprete
Instruct(MAKEACCU) {
int i;
print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 4, Accu_tag);
+ Alloc_small(accu, coq_extra_args + 4, Closure_tag);
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
Field(accu, 2) = Field(coq_atom_tbl, *pc);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 6233675c66..ae5251c252 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -108,7 +108,7 @@ value init_coq_vm(value unit) /* ML */
init_coq_interpreter();
/* Some predefined pointer code.
- * It is typically contained in accumulator blocks whose tag is 0 and thus
+ * It is typically contained in accumulator blocks and thus might be
* scanned by the GC, so make it look like an OCaml block. */
value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \
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 <float.h>
#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)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 98a1b13373..0678f37a0b 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -34,8 +34,6 @@ let crazy_val = (val_of_obj (Obj.repr 0))
type tag = int
-let accu_tag = 0
-
let type_atom_tag = 2
let max_atom_tag = 2
let proj_tag = 3
@@ -225,8 +223,7 @@ type vswitch = {
(* + Cofixpoints : see cbytegen.ml *)
(* *)
(* + vblock's encode (non constant) constructors as in Ocaml, but *)
-(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *)
-(* accumulators. *)
+(* starting from 0 up. *)
(* *)
(* + vm_env is the type of the machine environments (i.e. a function or *)
(* a fixpoint) *)
@@ -391,29 +388,28 @@ external accumulate : unit -> tcode = "accumulate_code"
external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
let accumulate = accumulate ()
-let whd_val : values -> whd =
- fun v ->
- let o = Obj.repr v in
- if Obj.is_int o then Vconstr_const (Obj.obj o)
+let whd_val (v: values) =
+ let o = Obj.repr v in
+ if Obj.is_int o then Vconstr_const (Obj.obj o)
+ else
+ let tag = Obj.tag o in
+ if Int.equal tag 0 then
+ if Int.equal (Obj.size o) 1 then
+ Varray (Obj.obj o)
+ else Vprod (Obj.obj o)
+ else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then
+ whd_accu o []
+ else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then
+ (match kind_of_closure o with
+ | 0 -> Vfun(Obj.obj o)
+ | 1 -> Vfix(Obj.obj o, None)
+ | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o))
+ | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+ | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
+ else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+ else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
else
- let tag = Obj.tag o in
- if tag = accu_tag then
- if Int.equal (Obj.size o) 1 then
- Varray(Obj.obj o)
- else if is_accumulate (fun_code o) then whd_accu o []
- else Vprod(Obj.obj o)
- else
- if tag = Obj.closure_tag || tag = Obj.infix_tag then
- (match kind_of_closure o with
- | 0 -> Vfun(Obj.obj o)
- | 1 -> Vfix(Obj.obj o, None)
- | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o))
- | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
- | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
- else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
- else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
- else
- Vconstr_block(Obj.obj o)
+ Vconstr_block (Obj.obj o)
(**********************************************)
(* Constructors *******************************)
@@ -421,7 +417,7 @@ let whd_val : values -> whd =
let obj_of_atom : atom -> Obj.t =
fun a ->
- let res = Obj.new_block accu_tag 3 in
+ let res = Obj.new_block Obj.closure_tag 3 in
set_bytecode_field res 0 accumulate;
Obj.set_field res 1 (Obj.repr 2);
Obj.set_field res 2 (Obj.repr a);
@@ -632,10 +628,7 @@ let mk_cofix_body apply_varray k ndef vcf =
let c = Obj.field (Obj.repr vcfi) 0 in
Obj.set_field e 0 c;
let atom = Obj.new_block cofix_tag 1 in
- let self = Obj.new_block accu_tag 3 in
- set_bytecode_field self 0 accumulate;
- Obj.set_field self 1 (Obj.repr 2);
- Obj.set_field self 2 (Obj.repr atom);
+ let self = obj_of_atom (Obj.obj atom) in
apply_varray (Obj.obj e) [|Obj.obj self|] in
Array.init ndef cofix_body
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index ee3e2bd5fc..6632dc46b2 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -27,8 +27,6 @@ type to_update
type tag = int
-val accu_tag : tag
-
val type_atom_tag : tag
val max_atom_tag : tag
val proj_tag : tag
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:17:02 +0000