aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c103
-rw-r--r--kernel/byterun/coq_values.h1
-rw-r--r--kernel/vmbytegen.ml14
-rw-r--r--kernel/vmvalues.ml16
4 files changed, 68 insertions, 66 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index b44ae34582..40ddcbb213 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -712,26 +712,26 @@ value coq_interprete
} else {
/* The recursif argument is an accumulator */
mlsize_t num_args, i;
+ value block;
/* Construction of fixpoint applied to its [rec_pos-1] first arguments */
Alloc_small(accu, rec_pos + 3, Closure_tag);
Code_val(accu) = pc; /* Point to the next RESTART instr. */
Field(accu, 1) = Val_int(2);
Field(accu, 2) = coq_env; // We store the fixpoint in the first field
- for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = sp[i]; // Storing args
- sp += rec_pos;
- *--sp = accu;
- /* Construction of the atom */
- Alloc_small(accu, 2, ATOM_FIX_TAG);
- Field(accu,1) = sp[0];
- Field(accu,0) = sp[1];
- sp++; sp[0] = accu;
- /* Construction of the accumulator */
+ for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = *sp++; // Storing args
+ /* Construction of the atom */
+ Alloc_small(block, 2, ATOM_FIX_TAG);
+ Field(block, 0) = *sp++;
+ Field(block, 1) = accu;
+ accu = block;
+ /* Construction of the accumulator */
num_args = coq_extra_args - rec_pos;
- Alloc_small(accu, 2+num_args, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = sp[0]; sp++;
- for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
- sp += num_args;
+ Alloc_small(block, 3 + num_args, Accu_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
+ for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++;
+ accu = block;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -808,9 +808,10 @@ value coq_interprete
/* Creation des blocks accumulate */
for(i=0; i < nfunc; i++) {
- Alloc_small(accu, 2, Accu_tag);
+ Alloc_small(accu, 3, Accu_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = Val_int(1);
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = Val_int(1);
*--sp=accu;
}
/* creation des fonction cofix */
@@ -818,22 +819,17 @@ value coq_interprete
p = sp;
size = nfunc + nvars + 3;
for (i=0; i < nfunc; i++) {
-
+ value block;
Alloc_small(accu, size, Closure_tag);
Code_val(accu) = pc+pc[i];
Field(accu, 1) = Val_int(2);
for (j = 0; j < nfunc; ++j) Field(accu, j + 2) = p[j];
Field(accu, size - 1) = p[nfunc];
for (j = nfunc + 1; j <= nfunc + nvars; ++j) Field(accu, j + 1) = p[j];
- *--sp = accu;
- /* creation du block contenant le cofix */
-
- Alloc_small(accu,1, ATOM_COFIX_TAG);
- Field(accu, 0) = sp[0];
- *sp = accu;
- /* mise a jour du block accumulate */
- caml_modify(&Field(p[i], 1),*sp);
- sp++;
+ Alloc_small(block, 1, ATOM_COFIX_TAG);
+ Field(block, 0) = accu;
+ /* update the accumulate block */
+ caml_modify(&Field(p[i], 2), block);
}
pc += nfunc;
accu = p[start];
@@ -1028,7 +1024,7 @@ value coq_interprete
print_instr("PROJ");
if (Is_accu (accu)) {
*--sp = accu; // Save matched block on stack
- accu = Field(accu, 1); // Save atom to accu register
+ accu = Field(accu, 2); // Save atom to accu register
switch (Tag_val(accu)) {
case ATOM_COFIX_TAG: // We are forcing a cofix
{
@@ -1040,11 +1036,11 @@ value coq_interprete
coq_env = Field(accu, 0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
sp[2] = Val_long(coq_extra_args); // Push number of args for return
- nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
// Push arguments to stack
CHECK_STACK(nargs + 1);
sp -= nargs;
- for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+ for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 3);
*--sp = accu; // Last argument is the pointer to the suspension
coq_extra_args = nargs;
pc = Code_val(coq_env); // Trigger evaluation
@@ -1066,9 +1062,10 @@ value coq_interprete
Field(accu, 0) = Field(coq_global_data, *pc++);
Field(accu, 1) = *sp++;
/* Create accumulator */
- Alloc_small(block, 2, Accu_tag);
+ Alloc_small(block, 3, Accu_tag);
Code_val(block) = accumulate;
- Field(block, 1) = accu;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
accu = block;
}
}
@@ -1142,7 +1139,7 @@ value coq_interprete
Instruct(MAKESWITCHBLOCK) {
print_instr("MAKESWITCHBLOCK");
*--sp = accu; // Save matched block on stack
- accu = Field(accu,1); // Save atom to accu register
+ accu = Field(accu, 2); // Save atom to accu register
switch (Tag_val(accu)) {
case ATOM_COFIX_TAG: // We are forcing a cofix
{
@@ -1156,11 +1153,11 @@ value coq_interprete
coq_env = Field(accu,0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
sp[2] = Val_long(coq_extra_args); // Push number of args for return
- nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
// Push arguments to stack
CHECK_STACK(nargs+1);
sp -= nargs;
- for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+ for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 3);
*--sp = accu; // Leftmost argument is the pointer to the suspension
print_lint(nargs);
coq_extra_args = nargs;
@@ -1181,6 +1178,7 @@ value coq_interprete
mlsize_t sz;
int i, annot;
code_t typlbl,swlbl;
+ value block;
print_instr("MAKESWITCHBLOCK");
typlbl = (code_t)pc + *pc;
@@ -1207,24 +1205,26 @@ value coq_interprete
*--sp = accu;
Alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = swlbl;
- *--sp = accu;
/* We create the switch zipper */
- Alloc_small(accu, 5, Default_tag);
- Field(accu, 0) = sp[1];
- Field(accu, 1) = sp[0];
- Field(accu, 2) = sp[3];
- Field(accu, 3) = sp[2];
- Field(accu, 4) = coq_env;
+ Alloc_small(block, 5, Default_tag);
+ Field(block, 0) = sp[0];
+ Field(block, 1) = accu;
+ Field(block, 2) = sp[2];
+ Field(block, 3) = sp[1];
+ Field(block, 4) = coq_env;
sp += 3;
- sp[0] = accu;
+ accu = block;
/* We create the atom */
- Alloc_small(accu, 2, ATOM_SWITCH_TAG);
- Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
- sp++;sp[0] = accu;
+ Alloc_small(block, 2, ATOM_SWITCH_TAG);
+ Field(block, 0) = *sp++;
+ Field(block, 1) = accu;
+ accu = block;
/* We create the accumulator */
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
+ Alloc_small(block, 3, Accu_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
+ accu = block;
}
}
Next;
@@ -1235,10 +1235,11 @@ value coq_interprete
Instruct(MAKEACCU) {
int i;
print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+ Alloc_small(accu, coq_extra_args + 4, Accu_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = Field(coq_atom_tbl, *pc);
- for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = Field(coq_atom_tbl, *pc);
+ for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
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)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index a826cf8193..375b1aface 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -74,23 +74,23 @@ open Environ
(* ^ *)
(* The [ai] blocks are functions that accumulate their arguments: *)
(* ai arg1 argp ---> *)
-(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
+(* ai' = [A_t | accumulate | envofs | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
(* If such a block is matched against, we have to force evaluation, *)
(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *)
(* (note that [ai'] is a pointer to the closure, passed as argument) *)
(* Once evaluation is completed [ai'] is updated with the result: *)
(* ai' <-- *)
-(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
+(* [A_t | accumulate | envofs | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
(* This representation is nice because the application of the cofix is *)
(* evaluated only once (it simulates a lazy evaluation) *)
(* Moreover, when cofix don't have arguments, it is possible to create *)
(* a cycle, e.g.: *)
(* cofix one := cons 1 one *)
-(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *)
+(* a1 = [A_t | accumulate | envofs | [Cfx_t|fcofix1] ] *)
(* fcofix1 = [clos_t | code | envofs | a1] *)
(* The result of evaluating [a1] is [cons_t | 1 | a1]. *)
(* When [a1] is updated : *)
-(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
+(* a1 = [A_t | accumulate | envofs | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
(* The cycle is created ... *)
(* *)
(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *)
@@ -394,16 +394,16 @@ let add_grabrec rec_arg arity lbl cont =
let cont_cofix arity =
(* accu = res *)
(* stk = ai::args::ra::... *)
- (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *)
+ (* ai = [At|accumulate|envofs|[Cfx_t|fcofix]|args] *)
[ Kpush;
Kpush; (* stk = res::res::ai::args::ra::... *)
Kacc 2;
- Kfield 1;
+ Kfield 2;
Kfield 0;
Kmakeblock(2, cofix_evaluated_tag);
Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
Kacc 2;
- Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *)
+ Ksetfield 2; (* ai = [At|accumulate|envofs|[Cfxe_t|fcofix|res]|args] *)
(* stk = res::ai::args::ra::... *)
Kacc 0; (* accu = res *)
Kreturn (arity+2) ]
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 177f67210c..98a1b13373 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -231,7 +231,7 @@ type vswitch = {
(* + vm_env is the type of the machine environments (i.e. a function or *)
(* a fixpoint) *)
(* *)
-(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
+(* + Accumulators : At_[accumulate | envofs=2 | accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *)
(* -- 10_[accu|proj name] : a projection blocked by an accu *)
@@ -328,9 +328,9 @@ let uni_lvl_val (v : values) : Univ.Level.t =
let rec whd_accu a stk =
let stk =
- if Int.equal (Obj.size a) 2 then stk
+ if Int.equal (Obj.size a) 3 then stk
else Zapp (Obj.obj a) :: stk in
- let at = Obj.field a 1 in
+ let at = Obj.field a 2 in
match Obj.tag at with
| i when Int.equal i type_atom_tag ->
begin match stk with
@@ -421,9 +421,10 @@ let whd_val : values -> whd =
let obj_of_atom : atom -> Obj.t =
fun a ->
- let res = Obj.new_block accu_tag 2 in
+ let res = Obj.new_block accu_tag 3 in
set_bytecode_field res 0 accumulate;
- Obj.set_field res 1 (Obj.repr a);
+ Obj.set_field res 1 (Obj.repr 2);
+ Obj.set_field res 2 (Obj.repr a);
res
(* obj_of_str_const : structured_constant -> Obj.t *)
@@ -631,9 +632,10 @@ 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 2 in
+ let self = Obj.new_block accu_tag 3 in
set_bytecode_field self 0 accumulate;
- Obj.set_field self 1 (Obj.repr atom);
+ Obj.set_field self 1 (Obj.repr 2);
+ Obj.set_field self 2 (Obj.repr atom);
apply_varray (Obj.obj e) [|Obj.obj self|] in
Array.init ndef cofix_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 06:50:25 +0000