diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-02 15:41:50 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 08:57:39 +0200 |
commit | b5aed34bb8bbdda27646720db29a8d47c79653b9 (patch) | |
tree | ab5ca6003048afc0b8d0c2c4d9bce7e7a079cce2 /kernel/byterun/coq_memory.c | |
parent | e128900aee63c972d7977fd47e3fd21649b63409 (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.c | 37 |
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; |