aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_memory.c
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-02 15:41:50 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-26 08:57:39 +0200
commitb5aed34bb8bbdda27646720db29a8d47c79653b9 (patch)
treeab5ca6003048afc0b8d0c2c4d9bce7e7a079cce2 /kernel/byterun/coq_memory.c
parente128900aee63c972d7977fd47e3fd21649b63409 (diff)
Moving the VM global data to a ML reference.
Diffstat (limited to 'kernel/byterun/coq_memory.c')
-rw-r--r--kernel/byterun/coq_memory.c37
1 files changed, 1 insertions, 36 deletions
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;