aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-03 19:43:02 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-26 08:57:39 +0200
commitfd5dc5b37e765bdb864e874c451d42d03d737792 (patch)
tree464f48702d8b7116163f031a8f2c2bf2dec64823
parentb5aed34bb8bbdda27646720db29a8d47c79653b9 (diff)
Moving the VM global atom table to a ML reference.
-rw-r--r--kernel/byterun/coq_interp.c16
-rw-r--r--kernel/byterun/coq_interp.h7
-rw-r--r--kernel/byterun/coq_memory.c37
-rw-r--r--kernel/byterun/coq_memory.h3
-rw-r--r--kernel/csymtable.ml4
-rw-r--r--kernel/vm.ml6
-rw-r--r--kernel/vmvalues.ml21
-rw-r--r--kernel/vmvalues.mli3
8 files changed, 36 insertions, 61 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ced2a175d..cfeb0a9ee 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,10 +163,10 @@ extern void caml_process_pending_signals(void);
/* The interpreter itself */
value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args)
+(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args)
{
/* coq_accu is not allocated on the OCaml heap */
- CAMLparam1(coq_global_data);
+ CAMLparam2(coq_atom_tbl, coq_global_data);
/*Declaration des variables */
#ifdef PC_REG
@@ -1515,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) {
return Val_unit;
}
-value coq_interprete_ml(value tcode, value a, value g, value e, value ea) {
+value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
print_instr("coq_interprete");
- return coq_interprete((code_t)tcode, a, g, e, Long_val(ea));
+ return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea));
print_instr("end coq_interprete");
}
-value coq_eval_tcode (value tcode, value g, value e) {
- return coq_interprete_ml(tcode, Val_unit, g, e, 0);
+value coq_interprete_byte(value* argv, int argn){
+ return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
+}
+
+value coq_eval_tcode (value tcode, value t, value g, value e) {
+ return coq_interprete_ml(tcode, Val_unit, t, g, e, 0);
}
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 189c9a127..c04e9e00b 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -17,9 +17,10 @@ value coq_push_arguments(value args);
value coq_push_vstack(value stk);
-value coq_interprete_ml(value tcode, value a, value g, value e, value ea);
+value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea);
+value coq_interprete_byte(value* argv, int argn);
value coq_interprete
- (code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args);
+ (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args);
-value coq_eval_tcode (value tcode, value g, value e);
+value coq_eval_tcode (value tcode, value t, value g, value e);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 40dbda866..b2917a55e 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -24,9 +24,6 @@ value * coq_stack_threshold;
asize_t coq_max_stack_size = Coq_max_stack_size;
/* global_data */
-
-value coq_atom_tbl;
-
int drawinstr;
/* interp state */
@@ -57,8 +54,6 @@ static void (*coq_prev_scan_roots_hook) (scanning_action);
static void coq_scan_roots(scanning_action action)
{
register value * i;
- /* Scan the global variables */
- (*action)(coq_atom_tbl, &coq_atom_tbl);
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
(*action) (*i, i);
@@ -77,16 +72,10 @@ void init_coq_stack()
coq_max_stack_size = Coq_max_stack_size;
}
-void init_coq_atom_tbl(long requested_size){
- int i;
- coq_atom_tbl = alloc_shr(requested_size, 0);
- for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit;
-}
-
void init_coq_interpreter()
{
coq_sp = coq_stack_high;
- coq_interprete(NULL, Val_unit, Atom(0), Val_unit, 0);
+ coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0);
}
static int coq_vm_initialized = 0;
@@ -102,7 +91,6 @@ value init_coq_vm(value unit) /* ML */
#endif /* THREADED_CODE */
/* Allocate the table of global and the stack */
init_coq_stack();
- init_coq_atom_tbl(40);
/* Initialing the interpreter */
init_coq_interpreter();
@@ -146,29 +134,6 @@ void realloc_coq_stack(asize_t required_space)
#undef shift
}
-value get_coq_atom_tbl(value unit) /* ML */
-{
- return coq_atom_tbl;
-}
-
-value realloc_coq_atom_tbl(value size) /* ML */
-{
- mlsize_t requested_size, actual_size, i;
- value new_atom_tbl;
- requested_size = Long_val(size);
- actual_size = Wosize_val(coq_atom_tbl);
- if (requested_size >= actual_size) {
- requested_size = (requested_size + 0x100) & 0xFFFFFF00;
- new_atom_tbl = alloc_shr(requested_size, 0);
- for (i = 0; i < actual_size; i++)
- initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i));
- for (i = actual_size; i < requested_size; i++)
- Field (new_atom_tbl, i) = Val_long (0);
- coq_atom_tbl = new_atom_tbl;
- }
- return Val_unit;
-}
-
value coq_set_drawinstr(value unit)
{
drawinstr = 1;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 06711ad70..9375b15de 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -34,7 +34,6 @@ extern value * coq_stack_threshold;
/* global_data */
extern int coq_all_transp;
-extern value coq_atom_tbl;
extern int drawinstr;
/* interp state */
@@ -51,8 +50,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_atom_tbl(value unit); /* ML */
-value realloc_coq_atom_tbl(value size); /* ML */
value coq_set_transp_value(value transp); /* ML */
value get_coq_transp_value(value unit); /* ML */
#endif /* _COQ_MEMORY_ */
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index dfe3d8fb1..23b419473 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -26,7 +26,7 @@ open Cbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
-external eval_tcode : tcode -> vm_global -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode"
type global_data = { mutable glob_len : int; mutable glob_val : values array }
@@ -173,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) =
in
let tc = patch buff pl slots in
let vm_env = Array.map (slot_for_fv env) fv in
- eval_tcode tc (vm_global global_data.glob_val) vm_env
+ eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
and val_of_constr env c =
match compile ~fail_on_error:true env c with
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 160575ac7..d7eedc226 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -42,11 +42,11 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack"
(* interpreteur *)
-external coq_interprete : tcode -> values -> vm_global -> vm_env -> int -> values =
- "coq_interprete_ml"
+external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -> int -> values =
+ "coq_interprete_byte" "coq_interprete_ml"
let interprete code v env k =
- coq_interprete code v (Csymtable.get_global_data ()) env k
+ coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k
(* Functions over arguments *)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 6377e947f..cbe8c9187 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -410,13 +410,20 @@ let check_fix f1 f2 =
else false
else false
-external atom_rel : unit -> atom array = "get_coq_atom_tbl"
-external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+let atom_rel : atom array ref =
+ let init i = Aid (RelKey i) in
+ ref (Array.init 40 init)
+
+let get_atom_rel () = !atom_rel
+
+let realloc_atom_rel n =
+ let n = min (n + 0x100) Sys.max_array_length in
+ let init i = Aid (RelKey i) in
+ let ans = Array.init n init in
+ atom_rel := ans
let relaccu_tbl =
- let atom_rel = atom_rel() in
- let len = Array.length atom_rel in
- for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+ let len = Array.length !atom_rel in
ref (Array.init len mkAccuCode)
let relaccu_code i =
@@ -425,9 +432,7 @@ let relaccu_code i =
else
begin
realloc_atom_rel i;
- let atom_rel = atom_rel () in
- let nl = Array.length atom_rel in
- for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+ let nl = Array.length !atom_rel in
relaccu_tbl :=
Array.init nl
(fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 1fa889288..550791b2c 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -72,6 +72,9 @@ type atom =
| Aind of inductive
| Asort of Sorts.t
+val get_atom_rel : unit -> atom array
+(** Global table of rels *)
+
(** Zippers *)
type zipper =