aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_memory.h
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/coq_memory.h')
-rw-r--r--kernel/byterun/coq_memory.h68
1 files changed, 68 insertions, 0 deletions
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
new file mode 100644
index 000000000..0884f06a8
--- /dev/null
+++ b/kernel/byterun/coq_memory.h
@@ -0,0 +1,68 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+#ifndef _COQ_MEMORY_
+#define _COQ_MEMORY_
+
+#include "config.h"
+#include "fail.h"
+#include "misc.h"
+#include "memory.h"
+#include "mlvalues.h"
+
+
+#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
+#define BOXED 1
+
+/* stack */
+
+extern value * coq_stack_low;
+extern value * coq_stack_high;
+extern value * coq_stack_threshold;
+
+/* global_data */
+
+extern value coq_global_data;
+extern value coq_global_transp;
+extern value coq_global_boxed;
+extern int default_transp;
+extern value coq_atom_tbl;
+/* interp state */
+
+extern value * coq_sp;
+extern value forcable;
+/* Some predefined pointer code */
+extern code_t accumulate;
+
+/* functions over global environment */
+
+value coq_static_alloc(value size); /* ML */
+value coq_static_free(value string); /* ML */
+
+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_global_transp(value unit); /* ML */
+value get_coq_global_boxed(value unit);
+value realloc_coq_global_boxed(value size); /* ML */
+value get_coq_atom_tbl(value unit); /* ML */
+value realloc_coq_atom_tbl(value size); /* ML */
+
+#endif /* _COQ_MEMORY_ */
+
+