aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_interp.c57
-rw-r--r--kernel/byterun/coq_memory.c16
-rw-r--r--kernel/byterun/coq_values.c1
-rw-r--r--kernel/byterun/coq_values.h10
4 files changed, 40 insertions, 44 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0a121dc32e..dc571699ef 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -341,6 +341,7 @@ value coq_interprete
/* Fallthrough */
Instruct(ENVACC){
print_instr("ENVACC");
+ print_int(*pc);
accu = Field(coq_env, *pc++);
Next;
}
@@ -371,6 +372,10 @@ value coq_interprete
sp[1] = (value)pc;
sp[2] = coq_env;
sp[3] = Val_long(coq_extra_args);
+ print_instr("call stack=");
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ print_lint(sp[3]);
pc = Code_val(accu);
coq_env = accu;
coq_extra_args = 0;
@@ -458,6 +463,7 @@ value coq_interprete
sp[0] = arg1;
sp[1] = arg2;
pc = Code_val(accu);
+ print_lint(accu);
coq_env = accu;
coq_extra_args += 1;
goto check_stacks;
@@ -481,11 +487,18 @@ value coq_interprete
print_instr("RETURN");
print_int(*pc);
sp += *pc++;
+ print_instr("stack=");
+ print_lint(sp[0]);
+ print_lint(sp[1]);
+ print_lint(sp[2]);
if (coq_extra_args > 0) {
+ print_instr("extra args > 0");
+ print_lint(coq_extra_args);
coq_extra_args--;
pc = Code_val(accu);
coq_env = accu;
} else {
+ print_instr("extra args = 0");
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -585,7 +598,10 @@ value coq_interprete
Alloc_small(accu, 1 + nvars, Closure_tag);
Code_val(accu) = pc + *pc;
pc++;
- for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
sp += nvars;
Next;
}
@@ -720,6 +736,7 @@ value coq_interprete
/* Fallthrough */
Instruct(GETGLOBAL){
print_instr("GETGLOBAL");
+ print_int(*pc);
accu = Field(coq_global_data, *pc);
pc++;
Next;
@@ -732,7 +749,7 @@ value coq_interprete
tag_t tag = *pc++;
mlsize_t i;
value block;
- print_instr("MAKEBLOCK");
+ print_instr("MAKEBLOCK, tag=");
Alloc_small(block, wosize, tag);
Field(block, 0) = accu;
for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -743,7 +760,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK1");
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
Alloc_small(block, 1, tag);
Field(block, 0) = accu;
accu = block;
@@ -753,7 +771,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK2");
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
Alloc_small(block, 2, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -764,7 +783,8 @@ value coq_interprete
Instruct(MAKEBLOCK3) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK3");
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
Alloc_small(block, 3, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -776,7 +796,8 @@ value coq_interprete
Instruct(MAKEBLOCK4) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK4");
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
Alloc_small(block, 4, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -844,7 +865,6 @@ value coq_interprete
}
Instruct(SETFIELD1){
- int i, j, size, size_aux;
print_instr("SETFIELD1");
caml_modify(&Field(accu, 1),*sp);
sp++;
@@ -884,19 +904,17 @@ value coq_interprete
Instruct(PROJ){
print_instr("PROJ");
if (Is_accu (accu)) {
+ value block;
/* Skip over the index of projected field */
pc++;
- /* Save the argument on the stack */
- *--sp = accu;
/* Create atom */
- Alloc_small(accu, 2, ATOM_PROJ_TAG);
- Field(accu, 0) = Field(coq_global_data, *pc);
- Field(accu, 1) = sp[0];
- sp[0] = accu;
+ Alloc_small(block, 2, ATOM_PROJ_TAG);
+ Field(block, 0) = Field(coq_global_data, *pc);
+ Field(block, 1) = accu;
/* Create accumulator */
Alloc_small(accu, 2, Accu_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
+ Field(accu, 1) = block;
} else {
accu = Field(accu, *pc++);
}
@@ -943,6 +961,7 @@ value coq_interprete
/* Fallthrough */
Instruct(CONSTINT) {
print_instr("CONSTINT");
+ print_int(*pc);
accu = Val_int(*pc);
pc++;
Next;
@@ -1110,7 +1129,6 @@ value coq_interprete
/* returns the sum plus one with a carry */
uint32_t s;
s = (uint32_t)accu + (uint32_t)*sp++ + 1;
- value block;
if( (uint32_t)s <= (uint32_t)accu ) {
/* carry */
Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1252,16 +1270,17 @@ value coq_interprete
shiftby = uint32_of_value(accu);
if (shiftby > 31) {
if (shiftby < 62) {
- *sp++;
- accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+ sp++;
+ accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
}
else {
+ sp+=2;
accu = (value)(1);
}
}
else{
/* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
- accu = (value)(((*sp++)^1) << shiftby);
+ accu = (value)((((uint32_t)*sp++)^1) << shiftby);
/* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
}
@@ -1270,7 +1289,7 @@ value coq_interprete
Instruct (COMPAREINT31) {
/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
- /* assumes Inudctive _ : _ := Eq | Lt | Gt */
+ /* assumes Inductive _ : _ := Eq | Lt | Gt */
print_instr("COMPAREINT31");
if ((uint32_t)accu == (uint32_t)*sp) {
accu = 1; /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829ab0..c9bcdc32ff 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
value coq_global_data;
-int coq_all_transp;
value coq_atom_tbl;
int drawinstr;
@@ -104,7 +103,6 @@ static int coq_vm_initialized = 0;
value init_coq_vm(value unit) /* ML */
{
- int i;
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
@@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
init_coq_global_data(Coq_global_data_Size);
init_coq_atom_tbl(40);
/* Initialing the interpreter */
- coq_all_transp = 0;
init_coq_interpreter();
/* Some predefined pointer code */
@@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
{
asize_t size;
value * new_low, * new_high, * new_sp;
- value * p;
size = coq_stack_high - coq_stack_low;
do {
size *= 2;
@@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size) /* ML */
return Val_unit;
}
-
-value coq_set_transp_value(value transp)
-{
- coq_all_transp = (transp == Val_true);
- return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
- return Val_bool(coq_all_transp);
-}
-
value coq_set_drawinstr(value unit)
{
drawinstr = 1;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b27c..528babebfc 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
value coq_kind_of_closure(value v) {
opcode_t * c;
- int res;
int is_app = 0;
c = Code_val(v);
if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1590a2141d..bb0f0eb5e4 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,23 +17,17 @@
#define Default_tag 0
#define Accu_tag 0
-
-
#define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
#define ATOM_PROJ_TAG 3
#define ATOM_FIX_TAG 4
#define ATOM_SWITCH_TAG 5
#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_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#endif /* _COQ_VALUES_ */
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:40:46 +0000