diff options
Diffstat (limited to 'kernel/byterun')
-rw-r--r-- | kernel/byterun/coq_interp.c | 17 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.h | 8 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.c | 37 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.h | 4 |
4 files changed, 14 insertions, 52 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index af89712d5..ced2a175d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -163,8 +163,11 @@ extern void caml_process_pending_signals(void); /* The interpreter itself */ value coq_interprete -(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args) +(code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args) { + /* coq_accu is not allocated on the OCaml heap */ + CAMLparam1(coq_global_data); + /*Declaration des variables */ #ifdef PC_REG register code_t pc PC_REG; @@ -196,7 +199,7 @@ value coq_interprete coq_instr_table = (char **) coq_jumptable; coq_instr_base = coq_Jumptbl_base; #endif - return Val_unit; + CAMLreturn(Val_unit); } #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) coq_jumptbl_base = coq_Jumptbl_base; @@ -1460,7 +1463,7 @@ value coq_interprete Instruct(STOP){ print_instr("STOP"); coq_sp = sp; - return accu; + CAMLreturn(accu); } @@ -1512,12 +1515,12 @@ value coq_push_vstack(value stk, value max_stack_size) { return Val_unit; } -value coq_interprete_ml(value tcode, value a, value e, value ea) { +value coq_interprete_ml(value tcode, value a, value g, value e, value ea) { print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + return coq_interprete((code_t)tcode, a, g, e, Long_val(ea)); print_instr("end coq_interprete"); } -value coq_eval_tcode (value tcode, value e) { - return coq_interprete_ml(tcode, Val_unit, e, 0); +value coq_eval_tcode (value tcode, value g, value e) { + return coq_interprete_ml(tcode, Val_unit, g, e, 0); } diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 60865c32e..189c9a127 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -17,11 +17,9 @@ value coq_push_arguments(value args); value coq_push_vstack(value stk); -value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete_ml(value tcode, value a, value g, value e, value ea); value coq_interprete - (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); - -value coq_eval_tcode (value tcode, value e); - + (code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args); +value coq_eval_tcode (value tcode, value g, value e); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 45cfae509..40dbda866 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -25,7 +25,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size; /* global_data */ -value coq_global_data; value coq_atom_tbl; int drawinstr; @@ -59,7 +58,6 @@ static void coq_scan_roots(scanning_action action) { register value * i; /* Scan the global variables */ - (*action)(coq_global_data, &coq_global_data); (*action)(coq_atom_tbl, &coq_atom_tbl); /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { @@ -79,14 +77,6 @@ void init_coq_stack() coq_max_stack_size = Coq_max_stack_size; } -void init_coq_global_data(long requested_size) -{ - int i; - coq_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_data, i) = Val_unit; -} - void init_coq_atom_tbl(long requested_size){ int i; coq_atom_tbl = alloc_shr(requested_size, 0); @@ -96,7 +86,7 @@ void init_coq_atom_tbl(long requested_size){ void init_coq_interpreter() { coq_sp = coq_stack_high; - coq_interprete(NULL, Val_unit, Val_unit, 0); + coq_interprete(NULL, Val_unit, Atom(0), Val_unit, 0); } static int coq_vm_initialized = 0; @@ -112,7 +102,6 @@ value init_coq_vm(value unit) /* ML */ #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); - init_coq_global_data(Coq_global_data_Size); init_coq_atom_tbl(40); /* Initialing the interpreter */ init_coq_interpreter(); @@ -157,35 +146,11 @@ void realloc_coq_stack(asize_t required_space) #undef shift } -value get_coq_global_data(value unit) /* ML */ -{ - return coq_global_data; -} - value get_coq_atom_tbl(value unit) /* ML */ { return coq_atom_tbl; } -value realloc_coq_global_data(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_global_data; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_data); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_global_data, i), Field(coq_global_data, i)); - for (i = actual_size; i < requested_size; i++){ - Field (new_global_data, i) = Val_long (0); - } - coq_global_data = new_global_data; - } - return Val_unit; -} - value realloc_coq_atom_tbl(value size) /* ML */ { mlsize_t requested_size, actual_size, i; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index cec34f566..06711ad70 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -20,7 +20,6 @@ #define Coq_stack_size (4096 * sizeof(value)) #define Coq_stack_threshold (256 * sizeof(value)) -#define Coq_global_data_Size (4096 * sizeof(value)) #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 @@ -34,7 +33,6 @@ extern value * coq_stack_threshold; /* global_data */ -extern value coq_global_data; extern int coq_all_transp; extern value coq_atom_tbl; @@ -53,8 +51,6 @@ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); -value get_coq_global_data(value unit); /* ML */ -value realloc_coq_global_data(value size); /* ML */ value get_coq_atom_tbl(value unit); /* ML */ value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ |