aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_fix_code.c14
-rw-r--r--kernel/byterun/coq_gc.h6
-rw-r--r--kernel/byterun/coq_interp.c1316
-rw-r--r--kernel/byterun/coq_memory.c12
-rw-r--r--kernel/byterun/coq_memory.h4
-rw-r--r--kernel/byterun/coq_values.c2
6 files changed, 677 insertions, 677 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 931b509f48..306643f758 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -12,7 +12,7 @@
for fast computation of bounded (31bits) integers */
#include <stdio.h>
-#include <stdlib.h>
+#include <stdlib.h>
#include <stdint.h>
#include <caml/config.h>
#include <caml/misc.h>
@@ -42,7 +42,7 @@ void init_arity () {
arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
- arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
+ arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
arity[LTFLOAT]=arity[LEFLOAT]=
arity[ISINT]=arity[AREINT2]=0;
@@ -76,7 +76,7 @@ void init_arity () {
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
arity[PROJ]=2;
- /* instruction with four operands */
+ /* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
@@ -134,7 +134,7 @@ value coq_is_accumulate_code(value code){
#ifdef ARCH_BIG_ENDIAN
#define Reverse_32(dst,src) { \
- char * _p, * _q; \
+ char * _p, * _q; \
char _a, _b; \
_p = (char *) (src); \
_q = (char *) (dst); \
@@ -159,9 +159,9 @@ value coq_tcode_of_code (value code) {
q = coq_stat_alloc(len);
Code_val(res) = q;
len /= sizeof(opcode_t);
- for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
+ for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
opcode_t instr;
- COPY32(&instr,p);
+ COPY32(&instr,p);
p++;
if (instr < 0 || instr > STOP){
instr = STOP;
@@ -183,7 +183,7 @@ value coq_tcode_of_code (value code) {
for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
} else {
uint32_t i, ar;
- ar = arity[instr];
+ ar = arity[instr];
for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
}
}
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index f06275862c..38eda4d11f 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -37,8 +37,8 @@ CAMLextern void minor_collection (void);
#define Make_header(wosize, tag, color) \
(((header_t) (((header_t) (wosize) << 10) \
- + (color) \
- + (tag_t) (tag))) \
+ + (color) \
+ + (tag_t) (tag))) \
)
#endif
@@ -53,7 +53,7 @@ CAMLextern void minor_collection (void);
} \
Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \
(result) = Val_hp (young_ptr); \
- }while(0)
+ }while(0)
#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ca1308696c..b78643e226 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -21,8 +21,8 @@
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
-#include "coq_memory.h"
-#include "coq_values.h"
+#include "coq_memory.h"
+#include "coq_values.h"
#include "coq_float64.h"
#ifdef ARCH_SIXTYFOUR
@@ -49,7 +49,7 @@ sp is a local copy of the global variable extern_sp. */
#ifdef THREADED_CODE
-# define Instruct(name) coq_lbl_##name:
+# define Instruct(name) coq_lbl_##name:
# if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
# define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
# else
@@ -59,22 +59,22 @@ sp is a local copy of the global variable extern_sp. */
# ifdef DEBUG
# define Next goto next_instr
# else
-# define Next goto *(void *)(coq_jumptbl_base + *pc++)
+# define Next goto *(void *)(coq_jumptbl_base + *pc++)
# endif
-#else
+#else
# define Instruct(name) case name:
# define Next break
-#endif
+#endif
/* #define _COQ_DEBUG_ */
-#ifdef _COQ_DEBUG_
+#ifdef _COQ_DEBUG_
# define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
# define print_int(i) /*if (drawinstr)*/ printf("%d\n",i)
# define print_lint(i) /*if (drawinstr)*/ printf("%ld\n",i)
-# else
-# define print_instr(s)
-# define print_int(i)
+# else
+# define print_instr(s)
+# define print_int(i)
# define print_lint(i)
#endif
@@ -95,7 +95,7 @@ if (sp - num_args < coq_stack_threshold) { \
Some compilers underestimate the use of the local variables representing
the abstract machine registers, and don't put them in hardware registers,
which slows down the interpreter considerably.
- For GCC, Xavier Leroy have hand-assigned hardware registers for
+ For GCC, Xavier Leroy have hand-assigned hardware registers for
several architectures.
*/
@@ -171,11 +171,11 @@ if (sp - num_args < coq_stack_threshold) { \
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
- else{ \
- *--sp=accu; \
- accu = Field(coq_global_data, *pc++); \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
goto apply_lbl; \
- } \
+ } \
}while(0)
#define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1)
@@ -238,7 +238,7 @@ value coq_interprete
static void * coq_jumptable[] = {
# include "coq_jumptbl.h"
};
-#else
+#else
opcode_t curr_instr;
#endif
print_instr("Enter Interpreter");
@@ -269,193 +269,193 @@ value coq_interprete
switch(curr_instr) {
#endif
/* Basic stack operations */
-
+
Instruct(ACC0){
- print_instr("ACC0");
- accu = sp[0]; Next;
+ print_instr("ACC0");
+ accu = sp[0]; Next;
}
Instruct(ACC1){
- print_instr("ACC1");
- accu = sp[1]; Next;
+ print_instr("ACC1");
+ accu = sp[1]; Next;
}
Instruct(ACC2){
- print_instr("ACC2");
- accu = sp[2]; Next;
+ print_instr("ACC2");
+ accu = sp[2]; Next;
}
Instruct(ACC3){
- print_instr("ACC3");
- accu = sp[3]; Next;
+ print_instr("ACC3");
+ accu = sp[3]; Next;
}
Instruct(ACC4){
- print_instr("ACC4");
- accu = sp[4]; Next;
+ print_instr("ACC4");
+ accu = sp[4]; Next;
}
Instruct(ACC5){
- print_instr("ACC5");
- accu = sp[5]; Next;
+ print_instr("ACC5");
+ accu = sp[5]; Next;
}
Instruct(ACC6){
- print_instr("ACC6");
- accu = sp[6]; Next;
+ print_instr("ACC6");
+ accu = sp[6]; Next;
}
Instruct(ACC7){
- print_instr("ACC7");
+ print_instr("ACC7");
accu = sp[7]; Next;
- }
+ }
Instruct(PUSH){
- print_instr("PUSH");
- *--sp = accu; Next;
+ print_instr("PUSH");
+ *--sp = accu; Next;
}
Instruct(PUSHACC0) {
- print_instr("PUSHACC0");
+ print_instr("PUSHACC0");
*--sp = accu; Next;
}
Instruct(PUSHACC1){
- print_instr("PUSHACC1");
+ print_instr("PUSHACC1");
*--sp = accu; accu = sp[1]; Next;
}
Instruct(PUSHACC2){
- print_instr("PUSHACC2");
+ print_instr("PUSHACC2");
*--sp = accu; accu = sp[2]; Next;
}
Instruct(PUSHACC3){
- print_instr("PUSHACC3");
- *--sp = accu; accu = sp[3]; Next;
+ print_instr("PUSHACC3");
+ *--sp = accu; accu = sp[3]; Next;
}
Instruct(PUSHACC4){
- print_instr("PUSHACC4");
- *--sp = accu; accu = sp[4]; Next;
+ print_instr("PUSHACC4");
+ *--sp = accu; accu = sp[4]; Next;
}
Instruct(PUSHACC5){
- print_instr("PUSHACC5");
- *--sp = accu; accu = sp[5]; Next;
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[5]; Next;
}
Instruct(PUSHACC6){
- print_instr("PUSHACC5");
- *--sp = accu; accu = sp[6]; Next;
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[6]; Next;
}
Instruct(PUSHACC7){
- print_instr("PUSHACC7");
- *--sp = accu; accu = sp[7]; Next;
+ print_instr("PUSHACC7");
+ *--sp = accu; accu = sp[7]; Next;
}
Instruct(PUSHACC){
- print_instr("PUSHACC");
- *--sp = accu;
+ print_instr("PUSHACC");
+ *--sp = accu;
}
/* Fallthrough */
-
+
Instruct(ACC){
- print_instr("ACC");
- accu = sp[*pc++];
+ print_instr("ACC");
+ accu = sp[*pc++];
Next;
}
-
+
Instruct(POP){
- print_instr("POP");
- sp += *pc++;
- Next;
+ print_instr("POP");
+ sp += *pc++;
+ Next;
}
/* Access in heap-allocated environment */
-
+
Instruct(ENVACC1){
- print_instr("ENVACC1");
- accu = Field(coq_env, 1); Next;
+ print_instr("ENVACC1");
+ accu = Field(coq_env, 1); Next;
}
Instruct(ENVACC2){
- print_instr("ENVACC2");
- accu = Field(coq_env, 2); Next;
+ print_instr("ENVACC2");
+ accu = Field(coq_env, 2); Next;
}
Instruct(ENVACC3){
- print_instr("ENVACC3");
- accu = Field(coq_env, 3); Next;
+ print_instr("ENVACC3");
+ accu = Field(coq_env, 3); Next;
}
Instruct(ENVACC4){
- print_instr("ENVACC4");
- accu = Field(coq_env, 4); Next;
+ print_instr("ENVACC4");
+ accu = Field(coq_env, 4); Next;
}
Instruct(PUSHENVACC1){
- print_instr("PUSHENVACC1");
- *--sp = accu; accu = Field(coq_env, 1); Next;
+ print_instr("PUSHENVACC1");
+ *--sp = accu; accu = Field(coq_env, 1); Next;
}
Instruct(PUSHENVACC2){
- print_instr("PUSHENVACC2");
- *--sp = accu; accu = Field(coq_env, 2); Next;
+ print_instr("PUSHENVACC2");
+ *--sp = accu; accu = Field(coq_env, 2); Next;
}
Instruct(PUSHENVACC3){
- print_instr("PUSHENVACC3");
- *--sp = accu; accu = Field(coq_env, 3); Next;
+ print_instr("PUSHENVACC3");
+ *--sp = accu; accu = Field(coq_env, 3); Next;
}
Instruct(PUSHENVACC4){
- print_instr("PUSHENVACC4");
- *--sp = accu; accu = Field(coq_env, 4); Next;
+ print_instr("PUSHENVACC4");
+ *--sp = accu; accu = Field(coq_env, 4); Next;
}
Instruct(PUSHENVACC){
- print_instr("PUSHENVACC");
- *--sp = accu;
+ print_instr("PUSHENVACC");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(ENVACC){
- print_instr("ENVACC");
- print_int(*pc);
- accu = Field(coq_env, *pc++);
+ print_instr("ENVACC");
+ print_int(*pc);
+ accu = Field(coq_env, *pc++);
Next;
}
/* Function application */
-
+
Instruct(PUSH_RETADDR) {
- print_instr("PUSH_RETADDR");
- sp -= 3;
- sp[0] = (value) (pc + *pc);
- sp[1] = coq_env;
- sp[2] = Val_long(coq_extra_args);
- coq_extra_args = 0;
- pc++;
- Next;
+ print_instr("PUSH_RETADDR");
+ sp -= 3;
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ sp[2] = Val_long(coq_extra_args);
+ coq_extra_args = 0;
+ pc++;
+ Next;
}
Instruct(APPLY) {
- print_instr("APPLY");
- coq_extra_args = *pc - 1;
- pc = Code_val(accu);
- coq_env = accu;
- goto check_stack;
+ print_instr("APPLY");
+ coq_extra_args = *pc - 1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
}
Instruct(APPLY1) {
value arg1;
apply1:
- print_instr("APPLY1");
+ print_instr("APPLY1");
arg1 = sp[0];
- sp -= 3;
- sp[0] = arg1;
- 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;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ 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;
+ goto check_stack;
}
Instruct(APPLY2) {
value arg1;
value arg2;
apply2:
- print_instr("APPLY2");
+ print_instr("APPLY2");
arg1 = sp[0];
arg2 = sp[1];
- sp -= 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = (value)pc;
- sp[3] = coq_env;
- sp[4] = Val_long(coq_extra_args);
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args = 1;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = (value)pc;
+ sp[3] = coq_env;
+ sp[4] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 1;
+ goto check_stack;
}
Instruct(APPLY3) {
@@ -463,21 +463,21 @@ value coq_interprete
value arg2;
value arg3;
apply3:
- print_instr("APPLY3");
+ print_instr("APPLY3");
arg1 = sp[0];
arg2 = sp[1];
arg3 = sp[2];
- sp -= 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = arg3;
- sp[3] = (value)pc;
- sp[4] = coq_env;
- sp[5] = Val_long(coq_extra_args);
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args = 2;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ sp[3] = (value)pc;
+ sp[4] = coq_env;
+ sp[5] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 2;
+ goto check_stack;
}
Instruct(APPLY4) {
@@ -501,15 +501,15 @@ value coq_interprete
}
/* Stack checks */
-
+
check_stack:
print_instr("check_stack");
CHECK_STACK(0);
/* We also check for signals */
if (caml_signals_are_pending) {
- /* If there's a Ctrl-C, we reset the vm */
- if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
- caml_process_pending_signals();
+ /* If there's a Ctrl-C, we reset the vm */
+ if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+ caml_process_pending_signals();
}
Next;
@@ -524,460 +524,460 @@ value coq_interprete
}
Instruct(APPTERM) {
- int nargs = *pc++;
- int slotsize = *pc;
- value * newsp;
- int i;
- print_instr("APPTERM");
- /* Slide the nargs bottom words of the current frame to the top
- of the frame, and discard the remainder of the frame */
- newsp = sp + slotsize - nargs;
- for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
- sp = newsp;
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args += nargs - 1;
- goto check_stack;
+ int nargs = *pc++;
+ int slotsize = *pc;
+ value * newsp;
+ int i;
+ print_instr("APPTERM");
+ /* Slide the nargs bottom words of the current frame to the top
+ of the frame, and discard the remainder of the frame */
+ newsp = sp + slotsize - nargs;
+ for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+ sp = newsp;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += nargs - 1;
+ goto check_stack;
}
Instruct(APPTERM1) {
- value arg1 = sp[0];
- print_instr("APPTERM1");
- sp = sp + *pc - 1;
- sp[0] = arg1;
- pc = Code_val(accu);
- coq_env = accu;
- goto check_stack;
+ value arg1 = sp[0];
+ print_instr("APPTERM1");
+ sp = sp + *pc - 1;
+ sp[0] = arg1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
}
Instruct(APPTERM2) {
- value arg1 = sp[0];
- value arg2 = sp[1];
- print_instr("APPTERM2");
- sp = sp + *pc - 2;
- sp[0] = arg1;
- sp[1] = arg2;
- pc = Code_val(accu);
- print_lint(accu);
- coq_env = accu;
- coq_extra_args += 1;
- goto check_stack;
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ print_instr("APPTERM2");
+ sp = sp + *pc - 2;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ pc = Code_val(accu);
+ print_lint(accu);
+ coq_env = accu;
+ coq_extra_args += 1;
+ goto check_stack;
}
Instruct(APPTERM3) {
- value arg1 = sp[0];
- value arg2 = sp[1];
- value arg3 = sp[2];
- print_instr("APPTERM3");
- sp = sp + *pc - 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = arg3;
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args += 2;
- goto check_stack;
- }
-
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ value arg3 = sp[2];
+ print_instr("APPTERM3");
+ sp = sp + *pc - 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += 2;
+ goto check_stack;
+ }
+
Instruct(RETURN) {
- 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]);
- sp += 3;
- }
- Next;
- }
-
+ 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]);
+ sp += 3;
+ }
+ Next;
+ }
+
Instruct(RESTART) {
- int num_args = Wosize_val(coq_env) - 2;
- int i;
- print_instr("RESTART");
+ int num_args = Wosize_val(coq_env) - 2;
+ int i;
+ print_instr("RESTART");
CHECK_STACK(num_args);
- sp -= num_args;
- for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
- coq_env = Field(coq_env, 1);
- coq_extra_args += num_args;
- Next;
+ sp -= num_args;
+ for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+ coq_env = Field(coq_env, 1);
+ coq_extra_args += num_args;
+ Next;
}
-
+
Instruct(GRAB) {
- int required = *pc++;
- print_instr("GRAB");
- /* printf("GRAB %d\n",required); */
- if (coq_extra_args >= required) {
- coq_extra_args -= required;
- } else {
- mlsize_t num_args, i;
- num_args = 1 + coq_extra_args; /* arg1 + extra args */
- Alloc_small(accu, num_args + 2, Closure_tag);
- Field(accu, 1) = coq_env;
- for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
- Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
- sp += num_args;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- }
- Next;
- }
-
- Instruct(GRABREC) {
- int rec_pos = *pc++; /* commence a zero */
- print_instr("GRABREC");
- if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
- pc++;/* On saute le Restart */
- } else {
- if (coq_extra_args < rec_pos) {
+ int required = *pc++;
+ print_instr("GRAB");
+ /* printf("GRAB %d\n",required); */
+ if (coq_extra_args >= required) {
+ coq_extra_args -= required;
+ } else {
+ mlsize_t num_args, i;
+ num_args = 1 + coq_extra_args; /* arg1 + extra args */
+ Alloc_small(accu, num_args + 2, Closure_tag);
+ Field(accu, 1) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+ Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ Next;
+ }
+
+ Instruct(GRABREC) {
+ int rec_pos = *pc++; /* commence a zero */
+ print_instr("GRABREC");
+ if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
+ pc++;/* On saute le Restart */
+ } else {
+ if (coq_extra_args < rec_pos) {
/* Partial application */
- mlsize_t num_args, i;
- num_args = 1 + coq_extra_args; /* arg1 + extra args */
- Alloc_small(accu, num_args + 2, Closure_tag);
- Field(accu, 1) = coq_env;
- for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
- Code_val(accu) = pc - 3;
- sp += num_args;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- } else {
- /* The recursif argument is an accumulator */
- mlsize_t num_args, i;
- /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
- Alloc_small(accu, rec_pos + 2, Closure_tag);
- Field(accu, 1) = coq_env; // We store the fixpoint in the first field
- for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
- Code_val(accu) = pc;
- 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 */
- 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;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- }
- }
- Next;
- }
-
+ mlsize_t num_args, i;
+ num_args = 1 + coq_extra_args; /* arg1 + extra args */
+ Alloc_small(accu, num_args + 2, Closure_tag);
+ Field(accu, 1) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+ Code_val(accu) = pc - 3;
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ } else {
+ /* The recursif argument is an accumulator */
+ mlsize_t num_args, i;
+ /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
+ Alloc_small(accu, rec_pos + 2, Closure_tag);
+ Field(accu, 1) = coq_env; // We store the fixpoint in the first field
+ for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
+ Code_val(accu) = pc;
+ 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 */
+ 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;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ }
+ Next;
+ }
+
Instruct(CLOSURE) {
- int nvars = *pc++;
- int i;
- print_instr("CLOSURE");
- print_int(nvars);
- if (nvars > 0) *--sp = accu;
- Alloc_small(accu, 1 + nvars, Closure_tag);
- Code_val(accu) = pc + *pc;
- pc++;
- for (i = 0; i < nvars; i++) {
- print_lint(sp[i]);
- Field(accu, i + 1) = sp[i];
- }
- sp += nvars;
- Next;
+ int nvars = *pc++;
+ int i;
+ print_instr("CLOSURE");
+ print_int(nvars);
+ if (nvars > 0) *--sp = accu;
+ Alloc_small(accu, 1 + nvars, Closure_tag);
+ Code_val(accu) = pc + *pc;
+ pc++;
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
+ sp += nvars;
+ Next;
}
Instruct(CLOSUREREC) {
- int nfuncs = *pc++;
- int nvars = *pc++;
- int start = *pc++;
- int i;
- value * p;
- print_instr("CLOSUREREC");
- if (nvars > 0) *--sp = accu;
- /* construction du vecteur de type */
+ int nfuncs = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i;
+ value * p;
+ print_instr("CLOSUREREC");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
Alloc_small(accu, nfuncs, Abstract_tag);
- for(i = 0; i < nfuncs; i++) {
- Field(accu,i) = (value)(pc+pc[i]);
- }
- pc += nfuncs;
- *--sp=accu;
- Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
- Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
- /* On remplie la partie pour les variables libres */
- p = &Field(accu, nfuncs * 2 - 1);
- for (i = 0; i < nvars; i++) {
- *p++ = *sp++;
- }
- p = &Field(accu, 0);
- *p = (value) (pc + pc[0]);
- p++;
- for (i = 1; i < nfuncs; i++) {
- *p = Make_header(i * 2, Infix_tag, Caml_white);
- p++; /* color irrelevant. */
- *p = (value) (pc + pc[i]);
- p++;
- }
- pc += nfuncs;
- accu = accu + 2 * start * sizeof(value);
- Next;
- }
-
- Instruct(CLOSURECOFIX){
- int nfunc = *pc++;
- int nvars = *pc++;
- int start = *pc++;
- int i, j , size;
- value * p;
- print_instr("CLOSURECOFIX");
- if (nvars > 0) *--sp = accu;
- /* construction du vecteur de type */
+ for(i = 0; i < nfuncs; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ pc += nfuncs;
+ *--sp=accu;
+ Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
+ Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
+ /* On remplie la partie pour les variables libres */
+ p = &Field(accu, nfuncs * 2 - 1);
+ for (i = 0; i < nvars; i++) {
+ *p++ = *sp++;
+ }
+ p = &Field(accu, 0);
+ *p = (value) (pc + pc[0]);
+ p++;
+ for (i = 1; i < nfuncs; i++) {
+ *p = Make_header(i * 2, Infix_tag, Caml_white);
+ p++; /* color irrelevant. */
+ *p = (value) (pc + pc[i]);
+ p++;
+ }
+ pc += nfuncs;
+ accu = accu + 2 * start * sizeof(value);
+ Next;
+ }
+
+ Instruct(CLOSURECOFIX){
+ int nfunc = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i, j , size;
+ value * p;
+ print_instr("CLOSURECOFIX");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
Alloc_small(accu, nfunc, Abstract_tag);
- for(i = 0; i < nfunc; i++) {
- Field(accu,i) = (value)(pc+pc[i]);
- }
- pc += nfunc;
- *--sp=accu;
+ for(i = 0; i < nfunc; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ pc += nfunc;
+ *--sp=accu;
/* Creation des blocks accumulate */
for(i=0; i < nfunc; i++) {
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = Val_int(1);
- *--sp=accu;
- }
- /* creation des fonction cofix */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = Val_int(1);
+ *--sp=accu;
+ }
+ /* creation des fonction cofix */
p = sp;
- size = nfunc + nvars + 2;
- for (i=0; i < nfunc; i++) {
-
- Alloc_small(accu, size, Closure_tag);
- Code_val(accu) = pc+pc[i];
- for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
- Field(accu, size - 1) = p[nfunc];
- for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
- *--sp = accu;
+ size = nfunc + nvars + 2;
+ for (i=0; i < nfunc; i++) {
+
+ Alloc_small(accu, size, Closure_tag);
+ Code_val(accu) = pc+pc[i];
+ for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+ Field(accu, size - 1) = p[nfunc];
+ for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = 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++;
- }
- pc += nfunc;
- accu = p[start];
+ 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++;
+ }
+ pc += nfunc;
+ accu = p[start];
sp = p + nfunc + 1 + nvars;
- print_instr("ici4");
- Next;
+ print_instr("ici4");
+ Next;
}
-
+
Instruct(PUSHOFFSETCLOSURE) {
- print_instr("PUSHOFFSETCLOSURE");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSURE");
+ *--sp = accu;
} /* fallthrough */
Instruct(OFFSETCLOSURE) {
- print_instr("OFFSETCLOSURE");
- accu = coq_env + *pc++ * sizeof(value); Next;
+ print_instr("OFFSETCLOSURE");
+ accu = coq_env + *pc++ * sizeof(value); Next;
}
Instruct(PUSHOFFSETCLOSUREM2) {
- print_instr("PUSHOFFSETCLOSUREM2");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSUREM2");
+ *--sp = accu;
} /* fallthrough */
Instruct(OFFSETCLOSUREM2) {
- print_instr("OFFSETCLOSUREM2");
- accu = coq_env - 2 * sizeof(value); Next;
+ print_instr("OFFSETCLOSUREM2");
+ accu = coq_env - 2 * sizeof(value); Next;
}
Instruct(PUSHOFFSETCLOSURE0) {
- print_instr("PUSHOFFSETCLOSURE0");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSURE0");
+ *--sp = accu;
}/* fallthrough */
Instruct(OFFSETCLOSURE0) {
- print_instr("OFFSETCLOSURE0");
- accu = coq_env; Next;
+ print_instr("OFFSETCLOSURE0");
+ accu = coq_env; Next;
}
Instruct(PUSHOFFSETCLOSURE2){
- print_instr("PUSHOFFSETCLOSURE2");
- *--sp = accu; /* fallthrough */
+ print_instr("PUSHOFFSETCLOSURE2");
+ *--sp = accu; /* fallthrough */
}
Instruct(OFFSETCLOSURE2) {
- print_instr("OFFSETCLOSURE2");
- accu = coq_env + 2 * sizeof(value); Next;
+ print_instr("OFFSETCLOSURE2");
+ accu = coq_env + 2 * sizeof(value); Next;
}
/* Access to global variables */
Instruct(PUSHGETGLOBAL) {
- print_instr("PUSH");
- *--sp = accu;
+ print_instr("PUSH");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(GETGLOBAL){
- print_instr("GETGLOBAL");
- print_int(*pc);
- accu = Field(coq_global_data, *pc);
+ print_instr("GETGLOBAL");
+ print_int(*pc);
+ accu = Field(coq_global_data, *pc);
pc++;
Next;
- }
+ }
/* Allocation of blocks */
Instruct(MAKEBLOCK) {
- mlsize_t wosize = *pc++;
- tag_t tag = *pc++;
- mlsize_t i;
- value block;
- print_instr("MAKEBLOCK, tag=");
- Alloc_small(block, wosize, tag);
- Field(block, 0) = accu;
- for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
- accu = block;
- Next;
+ mlsize_t wosize = *pc++;
+ tag_t tag = *pc++;
+ mlsize_t i;
+ value block;
+ print_instr("MAKEBLOCK, tag=");
+ Alloc_small(block, wosize, tag);
+ Field(block, 0) = accu;
+ for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK1) {
-
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK1, tag=");
- print_int(tag);
- Alloc_small(block, 1, tag);
- Field(block, 0) = accu;
- accu = block;
- Next;
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
+ Alloc_small(block, 1, tag);
+ Field(block, 0) = accu;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK2) {
-
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK2, tag=");
- print_int(tag);
- Alloc_small(block, 2, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- sp += 1;
- accu = block;
- Next;
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
+ Alloc_small(block, 2, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ sp += 1;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK3) {
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK3, tag=");
- print_int(tag);
- Alloc_small(block, 3, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- Field(block, 2) = sp[1];
- sp += 2;
- accu = block;
- Next;
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
+ Alloc_small(block, 3, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ sp += 2;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK4) {
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK4, tag=");
- print_int(tag);
- Alloc_small(block, 4, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- Field(block, 2) = sp[1];
- Field(block, 3) = sp[2];
- sp += 3;
- accu = block;
- Next;
- }
-
-
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
+ Alloc_small(block, 4, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ Field(block, 3) = sp[2];
+ sp += 3;
+ accu = block;
+ Next;
+ }
+
+
/* Access to components of blocks */
-
+
Instruct(SWITCH) {
- uint32_t sizes = *pc++;
- print_instr("SWITCH");
- print_int(sizes & 0xFFFFFF);
- if (Is_block(accu)) {
- long index = Tag_val(accu);
- print_instr("block");
- print_lint(index);
- pc += pc[(sizes & 0xFFFFFF) + index];
- } else {
- long index = Long_val(accu);
- print_instr("constant");
- print_lint(index);
- pc += pc[index];
- }
- Next;
+ uint32_t sizes = *pc++;
+ print_instr("SWITCH");
+ print_int(sizes & 0xFFFFFF);
+ if (Is_block(accu)) {
+ long index = Tag_val(accu);
+ print_instr("block");
+ print_lint(index);
+ pc += pc[(sizes & 0xFFFFFF) + index];
+ } else {
+ long index = Long_val(accu);
+ print_instr("constant");
+ print_lint(index);
+ pc += pc[index];
+ }
+ Next;
}
Instruct(PUSHFIELDS){
- int i;
- int size = *pc++;
- print_instr("PUSHFIELDS");
- sp -= size;
- for(i=0;i<size;i++)sp[i] = Field(accu,i);
- Next;
- }
-
+ int i;
+ int size = *pc++;
+ print_instr("PUSHFIELDS");
+ sp -= size;
+ for(i=0;i<size;i++)sp[i] = Field(accu,i);
+ Next;
+ }
+
Instruct(GETFIELD0){
- print_instr("GETFIELD0");
- accu = Field(accu, 0);
- Next;
+ print_instr("GETFIELD0");
+ accu = Field(accu, 0);
+ Next;
}
Instruct(GETFIELD1){
- print_instr("GETFIELD1");
- accu = Field(accu, 1);
- Next;
+ print_instr("GETFIELD1");
+ accu = Field(accu, 1);
+ Next;
}
Instruct(GETFIELD){
- print_instr("GETFIELD");
- accu = Field(accu, *pc);
- pc++;
- Next;
+ print_instr("GETFIELD");
+ accu = Field(accu, *pc);
+ pc++;
+ Next;
}
-
+
Instruct(SETFIELD0){
- print_instr("SETFIELD0");
- caml_modify(&Field(accu, 0),*sp);
- sp++;
- Next;
+ print_instr("SETFIELD0");
+ caml_modify(&Field(accu, 0),*sp);
+ sp++;
+ Next;
}
-
+
Instruct(SETFIELD1){
- print_instr("SETFIELD1");
- caml_modify(&Field(accu, 1),*sp);
- sp++;
- Next;
+ print_instr("SETFIELD1");
+ caml_modify(&Field(accu, 1),*sp);
+ sp++;
+ Next;
}
-
+
Instruct(SETFIELD){
- print_instr("SETFIELD");
- caml_modify(&Field(accu, *pc),*sp);
- sp++; pc++;
- Next;
+ print_instr("SETFIELD");
+ caml_modify(&Field(accu, *pc),*sp);
+ sp++; pc++;
+ Next;
}
Instruct(PROJ){
do_proj:
- print_instr("PROJ");
- if (Is_accu (accu)) {
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
*--sp = accu; // Save matched block on stack
accu = Field(accu, 1); // Save atom to accu register
switch (Tag_val(accu)) {
@@ -1023,135 +1023,135 @@ value coq_interprete
accu = block;
}
}
- } else {
+ } else {
accu = Field(accu, *pc);
pc += 2;
- }
- Next;
+ }
+ Next;
}
/* Integer constants */
Instruct(CONST0){
- print_instr("CONST0");
- accu = Val_int(0); Next;}
+ print_instr("CONST0");
+ accu = Val_int(0); Next;}
Instruct(CONST1){
- print_instr("CONST1");
- accu = Val_int(1); Next;}
+ print_instr("CONST1");
+ accu = Val_int(1); Next;}
Instruct(CONST2){
- print_instr("CONST2");
- accu = Val_int(2); Next;}
+ print_instr("CONST2");
+ accu = Val_int(2); Next;}
Instruct(CONST3){
- print_instr("CONST3");
- accu = Val_int(3); Next;}
-
+ print_instr("CONST3");
+ accu = Val_int(3); Next;}
+
Instruct(PUSHCONST0){
- print_instr("PUSHCONST0");
- *--sp = accu; accu = Val_int(0); Next;
+ print_instr("PUSHCONST0");
+ *--sp = accu; accu = Val_int(0); Next;
}
Instruct(PUSHCONST1){
- print_instr("PUSHCONST1");
- *--sp = accu; accu = Val_int(1); Next;
+ print_instr("PUSHCONST1");
+ *--sp = accu; accu = Val_int(1); Next;
}
Instruct(PUSHCONST2){
- print_instr("PUSHCONST2");
- *--sp = accu; accu = Val_int(2); Next;
+ print_instr("PUSHCONST2");
+ *--sp = accu; accu = Val_int(2); Next;
}
Instruct(PUSHCONST3){
- print_instr("PUSHCONST3");
- *--sp = accu; accu = Val_int(3); Next;
+ print_instr("PUSHCONST3");
+ *--sp = accu; accu = Val_int(3); Next;
}
Instruct(PUSHCONSTINT){
- print_instr("PUSHCONSTINT");
- *--sp = accu;
+ print_instr("PUSHCONSTINT");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(CONSTINT) {
- print_instr("CONSTINT");
- print_int(*pc);
- accu = Val_int(*pc);
- pc++;
- Next;
+ print_instr("CONSTINT");
+ print_int(*pc);
+ accu = Val_int(*pc);
+ pc++;
+ Next;
}
/* Special operations for reduction of open term */
Instruct(ACCUMULATE) {
- mlsize_t i, size;
- print_instr("ACCUMULATE");
- size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Accu_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++;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- Next;
- }
+ mlsize_t i, size;
+ print_instr("ACCUMULATE");
+ size = Wosize_val(coq_env);
+ Alloc_small(accu, size + coq_extra_args + 1, Accu_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++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
Instruct(MAKESWITCHBLOCK) {
- print_instr("MAKESWITCHBLOCK");
- *--sp = accu; // Save matched block on stack
- accu = Field(accu,1); // Save atom to accu register
- switch (Tag_val(accu)) {
- case ATOM_COFIX_TAG: // We are forcing a cofix
- {
- mlsize_t i, nargs;
- print_instr("COFIX_TAG");
- sp-=2;
- pc++;
+ print_instr("MAKESWITCHBLOCK");
+ *--sp = accu; // Save matched block on stack
+ accu = Field(accu,1); // Save atom to accu register
+ switch (Tag_val(accu)) {
+ case ATOM_COFIX_TAG: // We are forcing a cofix
+ {
+ mlsize_t i, nargs;
+ print_instr("COFIX_TAG");
+ sp-=2;
+ pc++;
// Push the return address
- sp[0] = (value) (pc + *pc);
- sp[1] = coq_env;
- 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)
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ 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)
// Push arguments to stack
CHECK_STACK(nargs+1);
- sp -= nargs;
- for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+ sp -= nargs;
+ for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
*--sp = accu; // Leftmost argument is the pointer to the suspension
- print_lint(nargs);
- coq_extra_args = nargs;
- pc = Code_val(coq_env); // Trigger evaluation
- goto check_stack;
- }
- case ATOM_COFIXEVALUATED_TAG:
- {
- print_instr("COFIX_EVAL_TAG");
- accu = Field(accu,1);
- pc++;
- pc = pc + *pc;
- sp++;
- Next;
- }
- default:
- {
- mlsize_t sz;
- int i, annot;
- code_t typlbl,swlbl;
- print_instr("MAKESWITCHBLOCK");
-
- typlbl = (code_t)pc + *pc;
- pc++;
- swlbl = (code_t)pc + *pc;
- pc++;
- annot = *pc++;
- sz = *pc++;
- *--sp=Field(coq_global_data, annot);
- /* We save the stack */
- if (sz == 0) accu = Atom(0);
- else {
- Alloc_small(accu, sz, Default_tag);
- if (Field(*sp, 2) == Val_true) {
- 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];
- }
- }
- *--sp = accu;
+ print_lint(nargs);
+ coq_extra_args = nargs;
+ pc = Code_val(coq_env); // Trigger evaluation
+ goto check_stack;
+ }
+ case ATOM_COFIXEVALUATED_TAG:
+ {
+ print_instr("COFIX_EVAL_TAG");
+ accu = Field(accu,1);
+ pc++;
+ pc = pc + *pc;
+ sp++;
+ Next;
+ }
+ default:
+ {
+ mlsize_t sz;
+ int i, annot;
+ code_t typlbl,swlbl;
+ print_instr("MAKESWITCHBLOCK");
+
+ typlbl = (code_t)pc + *pc;
+ pc++;
+ swlbl = (code_t)pc + *pc;
+ pc++;
+ annot = *pc++;
+ sz = *pc++;
+ *--sp=Field(coq_global_data, annot);
+ /* We save the stack */
+ if (sz == 0) accu = Atom(0);
+ else {
+ Alloc_small(accu, sz, Default_tag);
+ if (Field(*sp, 2) == Val_true) {
+ 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];
+ }
+ }
+ *--sp = accu;
/* Create bytecode wrappers */
Alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = typlbl;
@@ -1168,47 +1168,47 @@ value coq_interprete
Field(accu, 4) = coq_env;
sp += 3;
sp[0] = accu;
- /* 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;
- /* We create the accumulator */
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
- }
- }
- Next;
- }
-
-
-
+ /* 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;
+ /* We create the accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = *sp++;
+ }
+ }
+ Next;
+ }
+
+
+
Instruct(MAKEACCU) {
- int i;
- print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 3, 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++;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- Next;
- }
-
+ int i;
+ print_instr("MAKEACCU");
+ Alloc_small(accu, coq_extra_args + 3, 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++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
+
Instruct(MAKEPROD) {
- print_instr("MAKEPROD");
- *--sp=accu;
- Alloc_small(accu,2,0);
- Field(accu, 0) = sp[0];
- Field(accu, 1) = sp[1];
- sp += 2;
- Next;
+ print_instr("MAKEPROD");
+ *--sp=accu;
+ Alloc_small(accu,2,0);
+ Field(accu, 0) = sp[0];
+ Field(accu, 1) = sp[1];
+ sp += 2;
+ Next;
}
Instruct(BRANCH) {
- /* unconditional branching */
+ /* unconditional branching */
print_instr("BRANCH");
pc += *pc;
/* pc = (code_t)(pc+*pc); */
@@ -1220,7 +1220,7 @@ value coq_interprete
CheckInt2();
}
Instruct(ADDINT63) {
- /* Adds the integer in the accumulator with
+ /* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
print_instr("ADDINT63");
Uint63_add(accu, *sp++);
@@ -1230,27 +1230,27 @@ value coq_interprete
Instruct (CHECKADDCINT63) {
print_instr("CHECKADDCINT63");
CheckInt2();
- /* returns the sum with a carry */
+ /* returns the sum with a carry */
int c;
Uint63_add(accu, *sp);
Uint63_lt(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKADDCARRYCINT63) {
print_instr("ADDCARRYCINT63");
CheckInt2();
- /* returns the sum plus one with a carry */
+ /* returns the sum plus one with a carry */
int c;
Uint63_addcarry(accu, *sp);
Uint63_leq(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKSUBINT63) {
@@ -1259,7 +1259,7 @@ value coq_interprete
}
Instruct (SUBINT63) {
print_instr("SUBINT63");
- /* returns the subtraction */
+ /* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
}
@@ -1267,35 +1267,35 @@ value coq_interprete
Instruct (CHECKSUBCINT63) {
print_instr("SUBCINT63");
CheckInt2();
- /* returns the subtraction with a carry */
+ /* returns the subtraction with a carry */
int c;
Uint63_lt(c, accu, *sp);
Uint63_sub(accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKSUBCARRYCINT63) {
print_instr("SUBCARRYCINT63");
CheckInt2();
- /* returns the subtraction minus one with a carry */
+ /* returns the subtraction minus one with a carry */
int c;
Uint63_leq(c,accu,*sp);
Uint63_subcarry(accu,*sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKMULINT63) {
print_instr("MULINT63");
CheckInt2();
- /* returns the multiplication */
+ /* returns the multiplication */
Uint63_mul(accu,*sp++);
- Next;
+ Next;
}
Instruct (CHECKMULCINT63) {
@@ -1320,11 +1320,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
- else {
+ }
+ else {
Uint63_div(accu, *sp++);
}
- Next;
+ Next;
}
Instruct(CHECKMODINT63) {
@@ -1334,11 +1334,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
+ }
else {
Uint63_mod(accu,*sp++);
- }
- Next;
+ }
+ Next;
}
Instruct (CHECKDIVEUCLINT63) {
@@ -1366,7 +1366,7 @@ value coq_interprete
Field(accu, 1) = sp[0];
sp += 2;
}
- Next;
+ Next;
}
Instruct (CHECKDIV21INT63) {
@@ -1520,14 +1520,14 @@ value coq_interprete
Instruct (ISINT){
print_instr("ISINT");
accu = (Is_uint63(accu)) ? coq_true : coq_false;
- Next;
+ Next;
}
Instruct (AREINT2){
print_instr("AREINT2");
accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
sp++;
- Next;
+ Next;
}
@@ -1734,12 +1734,12 @@ value coq_interprete
/* Debugging and machine control */
Instruct(STOP){
- print_instr("STOP");
- coq_sp = sp;
+ print_instr("STOP");
+ coq_sp = sp;
CAMLreturn(accu);
}
-
-
+
+
#ifndef THREADED_CODE
default:
/*fprintf(stderr, "%d\n", *pc);*/
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a1c49bee95..91d6773b1f 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -9,7 +9,7 @@
/***********************************************************************/
#include <stdio.h>
-#include <string.h>
+#include <string.h>
#include <caml/alloc.h>
#include <caml/address_class.h>
#include "coq_gc.h"
@@ -31,7 +31,7 @@ int drawinstr;
long coq_saved_sp_offset;
value * coq_sp;
-/* Some predefined pointer code */
+/* Some predefined pointer code */
code_t accumulate;
/* functions over global environment */
@@ -80,7 +80,7 @@ void init_coq_stack()
coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
coq_max_stack_size = Coq_max_stack_size;
-}
+}
void init_coq_interpreter()
{
@@ -96,14 +96,14 @@ value init_coq_vm(value unit) /* ML */
fprintf(stderr,"already open \n");fflush(stderr);}
else {
drawinstr=0;
-#ifdef THREADED_CODE
+#ifdef THREADED_CODE
init_arity();
#endif /* THREADED_CODE */
/* Allocate the table of global and the stack */
init_coq_stack();
/* Initialing the interpreter */
init_coq_interpreter();
-
+
/* Some predefined pointer code.
* It is typically contained in accumulator blocks whose tag is 0 and thus
* scanned by the GC, so make it look like an OCaml block. */
@@ -117,7 +117,7 @@ value init_coq_vm(value unit) /* ML */
coq_prev_scan_roots_hook = scan_roots_hook;
scan_roots_hook = coq_scan_roots;
coq_vm_initialized = 1;
- }
+ }
return Val_unit;;
}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 1ea461c5e5..7f982d0477 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -39,7 +39,7 @@ extern int drawinstr;
/* interp state */
extern value * coq_sp;
-/* Some predefined pointer code */
+/* Some predefined pointer code */
extern code_t accumulate;
/* functions over global environment */
@@ -49,7 +49,7 @@ value coq_static_alloc(value size); /* ML */
value init_coq_vm(value unit); /* ML */
value re_init_coq_vm(value unit); /* ML */
-void realloc_coq_stack(asize_t required_space);
+void realloc_coq_stack(asize_t required_space);
value coq_set_transp_value(value transp); /* ML */
value get_coq_transp_value(value unit); /* ML */
#endif /* _COQ_MEMORY_ */
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index e05f3fb82e..3613bc07a6 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -39,7 +39,7 @@ value coq_closure_arity(value clos) {
if (Is_instruction(c,RESTART)) {
c++;
if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
- else {
+ else {
if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
return Val_int(1);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:49:31 +0000