aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c25
-rw-r--r--kernel/byterun/coq_float64.h48
-rw-r--r--kernel/byterun/coq_gc.h6
-rw-r--r--kernel/byterun/coq_interp.c1584
-rw-r--r--kernel/byterun/coq_memory.c12
-rw-r--r--kernel/byterun/coq_memory.h4
-rw-r--r--kernel/byterun/coq_uint63_emul.h15
-rw-r--r--kernel/byterun/coq_uint63_native.h23
-rw-r--r--kernel/byterun/coq_values.c4
-rw-r--r--kernel/byterun/coq_values.h20
-rw-r--r--kernel/byterun/dune5
11 files changed, 1040 insertions, 706 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 0865487c98..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,8 +42,9 @@ 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;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
@@ -63,11 +64,19 @@ void init_arity () {
arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
- arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1;
+ arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
+ arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
+ arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
+ arity[CHECKCLASSIFYFLOAT]=
+ arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
+ arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
+ arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
+ arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=
+ arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
/* 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;
@@ -125,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); \
@@ -150,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;
@@ -174,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_float64.h b/kernel/byterun/coq_float64.h
new file mode 100644
index 0000000000..c41079c8ff
--- /dev/null
+++ b/kernel/byterun/coq_float64.h
@@ -0,0 +1,48 @@
+#ifndef _COQ_FLOAT64_
+#define _COQ_FLOAT64_
+
+#include <math.h>
+
+#define DECLARE_FREL(name, e) \
+ int coq_##name(double x, double y) { \
+ return e; \
+ } \
+ \
+ value coq_##name##_byte(value x, value y) { \
+ return coq_##name(Double_val(x), Double_val(y)); \
+ }
+
+#define DECLARE_FBINOP(name, e) \
+ double coq_##name(double x, double y) { \
+ return e; \
+ } \
+ \
+ value coq_##name##_byte(value x, value y) { \
+ return caml_copy_double(coq_##name(Double_val(x), Double_val(y))); \
+ }
+
+#define DECLARE_FUNOP(name, e) \
+ double coq_##name(double x) { \
+ return e; \
+ } \
+ \
+ value coq_##name##_byte(value x) { \
+ return caml_copy_double(coq_##name(Double_val(x))); \
+ }
+
+DECLARE_FREL(feq, x == y)
+DECLARE_FREL(flt, x < y)
+DECLARE_FREL(fle, x <= y)
+DECLARE_FBINOP(fmul, x * y)
+DECLARE_FBINOP(fadd, x + y)
+DECLARE_FBINOP(fsub, x - y)
+DECLARE_FBINOP(fdiv, x / y)
+DECLARE_FUNOP(fsqrt, sqrt(x))
+DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
+DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
+
+value coq_is_double(value x) {
+ return Val_long(Is_double(x));
+}
+
+#endif /* _COQ_FLOAT64_ */
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 4b45608ae5..606cce0127 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -17,11 +17,15 @@
#include <signal.h>
#include <stdint.h>
#include <caml/memory.h>
+#include <caml/signals.h>
+#include <caml/version.h>
+#include <math.h>
#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
#include "coq_uint63_native.h"
@@ -47,7 +51,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
@@ -57,22 +61,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
@@ -93,7 +97,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.
*/
@@ -167,49 +171,47 @@ if (sp - num_args < coq_stack_threshold) { \
#endif
#endif
-#define CheckInt1() do{ \
- if (Is_uint63(accu)) pc++; \
- else{ \
- *--sp=accu; \
- accu = Field(coq_global_data, *pc++); \
- goto apply1; \
- } \
+#define CheckPrimArgs(cond, apply_lbl) do{ \
+ if (cond) pc++; \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
+ goto apply_lbl; \
+ } \
}while(0)
-#define CheckInt2() do{ \
- if (Is_uint63(accu) && Is_uint63(sp[0])) pc++; \
- else{ \
- *--sp=accu; \
- accu = Field(coq_global_data, *pc++); \
- goto apply2; \
- } \
- }while(0)
-
-
-
-#define CheckInt3() do{ \
- if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++; \
- else{ \
- *--sp=accu; \
- accu = Field(coq_global_data, *pc++); \
- goto apply3; \
- } \
- }while(0)
+#define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1)
+#define CheckInt2() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]), apply2)
+#define CheckInt3() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]) \
+ && Is_uint63(sp[1]), apply3)
+#define CheckFloat1() CheckPrimArgs(Is_double(accu), apply1)
+#define CheckFloat2() CheckPrimArgs(Is_double(accu) && Is_double(sp[0]), apply2)
#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
#define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
+/* Beware: we cannot use caml_copy_double here as it doesn't use
+ Alloc_small, hence doesn't protect the stack via
+ Setup_for_gc/Restore_after_gc. */
+#define Coq_copy_double(val) do{ \
+ double Coq_copy_double_f__ = (val); \
+ Alloc_small(accu, Double_wosize, Double_tag); \
+ Store_double_val(accu, Coq_copy_double_f__); \
+ }while(0);
+
#define Swap_accu_sp do{ \
value swap_accu_sp_tmp__ = accu; \
accu = *sp; \
*sp = swap_accu_sp_tmp__; \
}while(0)
+#if OCAML_VERSION < 41000
/* For signal handling, we hijack some code from the caml runtime */
-extern intnat caml_signals_are_pending;
-extern intnat caml_pending_signals[];
+extern intnat volatile caml_signals_are_pending;
+extern intnat volatile caml_pending_signals[];
extern void caml_process_pending_signals(void);
+#endif
/* The interpreter itself */
@@ -240,7 +242,7 @@ value coq_interprete
static void * coq_jumptable[] = {
# include "coq_jumptbl.h"
};
-#else
+#else
opcode_t curr_instr;
#endif
print_instr("Enter Interpreter");
@@ -271,193 +273,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) {
@@ -465,21 +467,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) {
@@ -503,16 +505,32 @@ value coq_interprete
}
/* Stack checks */
-
+
check_stack:
print_instr("check_stack");
CHECK_STACK(0);
/* We also check for signals */
+#if OCAML_VERSION >= 41000
+ {
+ value res = caml_process_pending_actions_exn();
+ if (Is_exception_result(res)) {
+ /* If there is an asynchronous exception, we reset the vm */
+ coq_sp = coq_stack_high;
+ caml_raise(Extract_exception(res));
+ }
+ }
+#else
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 */
+ intnat sigint = caml_pending_signals[SIGINT];
+ if (sigint) { coq_sp = coq_stack_high; }
+ caml_process_pending_signals();
+ if (sigint) {
+ caml_failwith("Coq VM: Fatal error: SIGINT signal detected "
+ "but no exception was raised");
+ }
}
+#endif
Next;
Instruct(ENSURESTACKCAPACITY) {
@@ -526,460 +544,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)) {
@@ -1025,135 +1043,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;
@@ -1170,47 +1188,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); */
@@ -1222,7 +1240,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++);
@@ -1232,27 +1250,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) {
@@ -1261,7 +1279,7 @@ value coq_interprete
}
Instruct (SUBINT63) {
print_instr("SUBINT63");
- /* returns the subtraction */
+ /* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
}
@@ -1269,35 +1287,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) {
@@ -1322,11 +1340,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
- else {
+ }
+ else {
Uint63_div(accu, *sp++);
}
- Next;
+ Next;
}
Instruct(CHECKMODINT63) {
@@ -1336,11 +1354,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
+ }
else {
Uint63_mod(accu,*sp++);
- }
- Next;
+ }
+ Next;
}
Instruct (CHECKDIVEUCLINT63) {
@@ -1368,7 +1386,7 @@ value coq_interprete
Field(accu, 1) = sp[0];
sp += 2;
}
- Next;
+ Next;
}
Instruct (CHECKDIV21INT63) {
@@ -1522,30 +1540,230 @@ 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;
+ }
+
+
+ Instruct (CHECKOPPFLOAT) {
+ print_instr("CHECKOPPFLOAT");
+ CheckFloat1();
+ Coq_copy_double(-Double_val(accu));
+ Next;
+ }
+
+ Instruct (CHECKABSFLOAT) {
+ print_instr("CHECKABSFLOAT");
+ CheckFloat1();
+ Coq_copy_double(fabs(Double_val(accu)));
+ Next;
+ }
+
+ Instruct (CHECKEQFLOAT) {
+ print_instr("CHECKEQFLOAT");
+ CheckFloat2();
+ accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
}
+ Instruct (CHECKLTFLOAT) {
+ print_instr("CHECKLTFLOAT");
+ CheckFloat2();
+ }
+ Instruct (LTFLOAT) {
+ print_instr("LTFLOAT");
+ accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLEFLOAT) {
+ print_instr("CHECKLEFLOAT");
+ CheckFloat2();
+ }
+ Instruct (LEFLOAT) {
+ print_instr("LEFLOAT");
+ accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKCOMPAREFLOAT) {
+ double x, y;
+ print_instr("CHECKCOMPAREFLOAT");
+ CheckFloat2();
+ x = Double_val(accu);
+ y = Double_val(*sp++);
+ if(x < y) {
+ accu = coq_FLt;
+ }
+ else if(x > y) {
+ accu = coq_FGt;
+ }
+ else if(x == y) {
+ accu = coq_FEq;
+ }
+ else { // nan value
+ accu = coq_FNotComparable;
+ }
+ Next;
+ }
+
+ Instruct (CHECKCLASSIFYFLOAT) {
+ double x;
+ print_instr("CHECKCLASSIFYFLOAT");
+ CheckFloat1();
+ x = Double_val(accu);
+ switch (fpclassify(x)) {
+ case FP_NORMAL:
+ accu = signbit(x) ? coq_NNormal : coq_PNormal;
+ break;
+ case FP_SUBNORMAL:
+ accu = signbit(x) ? coq_NSubn : coq_PSubn;
+ break;
+ case FP_ZERO:
+ accu = signbit(x) ? coq_NZero : coq_PZero;
+ break;
+ case FP_INFINITE:
+ accu = signbit(x) ? coq_NInf : coq_PInf;
+ break;
+ default: /* FP_NAN */
+ accu = coq_NaN;
+ break;
+ }
+ Next;
+ }
+
+ Instruct (CHECKADDFLOAT) {
+ print_instr("CHECKADDFLOAT");
+ CheckFloat2();
+ Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++)));
+ Next;
+ }
+
+ Instruct (CHECKSUBFLOAT) {
+ print_instr("CHECKSUBFLOAT");
+ CheckFloat2();
+ Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++)));
+ Next;
+ }
+
+ Instruct (CHECKMULFLOAT) {
+ print_instr("CHECKMULFLOAT");
+ CheckFloat2();
+ Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++)));
+ Next;
+ }
+
+ Instruct (CHECKDIVFLOAT) {
+ print_instr("CHECKDIVFLOAT");
+ CheckFloat2();
+ Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++)));
+ Next;
+ }
+
+ Instruct (CHECKSQRTFLOAT) {
+ print_instr("CHECKSQRTFLOAT");
+ CheckFloat1();
+ Coq_copy_double(coq_fsqrt(Double_val(accu)));
+ Next;
+ }
+
+ Instruct (CHECKFLOATOFINT63) {
+ print_instr("CHECKFLOATOFINT63");
+ CheckInt1();
+ Uint63_to_double(accu);
+ Next;
+ }
+
+ Instruct (CHECKFLOATNORMFRMANTISSA) {
+ double f;
+ print_instr("CHECKFLOATNORMFRMANTISSA");
+ CheckFloat1();
+ f = fabs(Double_val(accu));
+ if (f >= 0.5 && f < 1) {
+ Uint63_of_double(ldexp(f, DBL_MANT_DIG));
+ }
+ else {
+ Uint63_of_int(Val_int(0));
+ }
+ Next;
+ }
+
+ Instruct (CHECKFRSHIFTEXP) {
+ int exp;
+ double f;
+ print_instr("CHECKFRSHIFTEXP");
+ CheckFloat1();
+ /* frexp(infinity) incorrectly returns nan on mingw */
+#if defined(__MINGW32__) || defined(__MINGW64__)
+ if (fpclassify(Double_val(accu)) == FP_INFINITE) {
+ f = Double_val(accu);
+ } else
+#endif
+ f = frexp(Double_val(accu), &exp);
+ if (fpclassify(f) == FP_NORMAL) {
+ exp += FLOAT_EXP_SHIFT;
+ }
+ else {
+ exp = 0;
+ }
+ Coq_copy_double(f);
+ *--sp = accu;
+#ifdef ARCH_SIXTYFOUR
+ Alloc_small(accu, 2, coq_tag_pair);
+ Field(accu, 1) = Val_int(exp);
+#else
+ Uint63_of_int(Val_int(exp));
+ *--sp = accu;
+ Alloc_small(accu, 2, coq_tag_pair);
+ Field(accu, 1) = *sp++;
+#endif
+ Field(accu, 0) = *sp++;
+ Next;
+ }
+
+ Instruct (CHECKLDSHIFTEXP) {
+ print_instr("CHECKLDSHIFTEXP");
+ CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2);
+ Swap_accu_sp;
+ Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT));
+ accu = Int_val(accu);
+ Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT));
+ Next;
+ }
+
+ Instruct (CHECKNEXTUPFLOAT) {
+ print_instr("CHECKNEXTUPFLOAT");
+ CheckFloat1();
+ Coq_copy_double(coq_next_up(Double_val(accu)));
+ Next;
+ }
+
+ Instruct (CHECKNEXTDOWNFLOAT) {
+ print_instr("CHECKNEXTDOWNFLOAT");
+ CheckFloat1();
+ Coq_copy_double(coq_next_down(Double_val(accu)));
+ Next;
+ }
/* 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);*/
- failwith("Coq VM: Fatal error: bad opcode");
+ caml_failwith("Coq VM: Fatal error: bad opcode");
}
}
#endif
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_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 528cc6fc1f..143a6d098c 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -156,3 +156,18 @@ DECLARE_BINOP(mulc_ml)
*(h) = Field(uint63_return_value__, 0); \
accu = Field(uint63_return_value__, 1); \
}while(0)
+
+DECLARE_UNOP(to_float)
+#define Uint63_to_double(x) CALL_UNOP(to_float, x)
+
+DECLARE_UNOP(of_float)
+#define Uint63_of_double(f) do{ \
+ Coq_copy_double(f); \
+ CALL_UNOP(of_float, accu); \
+ }while(0)
+
+DECLARE_UNOP(of_int)
+#define Uint63_of_int(x) CALL_UNOP(of_int, x)
+
+DECLARE_BINOP(to_int_min)
+#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 9fbd3f83d8..5be7587091 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -138,3 +138,26 @@ value uint63_div21(value xh, value xl, value y, value* ql) {
}
}
#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))
+
+#define Uint63_to_double(x) Coq_copy_double((double) uint63_of_value(x))
+
+double coq_uint63_to_float(value x) {
+ return (double) uint63_of_value(x);
+}
+
+value coq_uint63_to_float_byte(value x) {
+ return caml_copy_double(coq_uint63_to_float(x));
+}
+
+#define Uint63_of_double(f) do{ \
+ accu = Val_long((uint64_t)(f)); \
+ }while(0)
+
+#define Uint63_of_int(x) (accu = (x))
+
+#define Uint63_to_int_min(n, m) do { \
+ if (uint63_lt((n),(m))) \
+ accu = (n); \
+ else \
+ accu = (m); \
+ }while(0)
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index e05f3fb82e..bbe91da628 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -39,8 +39,8 @@ 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 {
- if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+ else {
+ if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity");
return Val_int(1);
}
}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 0cf6ccf532..b027673ac7 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -14,6 +14,8 @@
#include <caml/alloc.h>
#include <caml/mlvalues.h>
+#include <float.h>
+
#define Default_tag 0
#define Accu_tag 0
@@ -29,8 +31,9 @@
/* 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)
-/* */
+/* coq values for primitive operations */
#define coq_tag_C1 2
#define coq_tag_C0 1
#define coq_tag_pair 1
@@ -39,5 +42,20 @@
#define coq_Eq Val_int(0)
#define coq_Lt Val_int(1)
#define coq_Gt Val_int(2)
+#define coq_FEq Val_int(0)
+#define coq_FLt Val_int(1)
+#define coq_FGt Val_int(2)
+#define coq_FNotComparable Val_int(3)
+#define coq_PNormal Val_int(0)
+#define coq_NNormal Val_int(1)
+#define coq_PSubn Val_int(2)
+#define coq_NSubn Val_int(3)
+#define coq_PZero Val_int(4)
+#define coq_NZero Val_int(5)
+#define coq_PInf Val_int(6)
+#define coq_NInf Val_int(7)
+#define coq_NaN Val_int(8)
+
+#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
#endif /* _COQ_VALUES_ */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 20bdf28e54..2998178be2 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -2,7 +2,10 @@
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq.vm)
- (c_names coq_fix_code coq_memory coq_values coq_interp))
+ (foreign_stubs
+ (language c)
+ (names coq_fix_code coq_memory coq_values coq_interp)
+ (flags (:include %{project_root}/config/dune.c_flags))))
(rule
(targets coq_instruct.h)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:02:42 +0000