1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
|
/***********************************************************************/
/* */
/* Coq Compiler */
/* */
/* Benjamin Gregoire, projets Logical and Cristal */
/* INRIA Rocquencourt */
/* */
/* */
/***********************************************************************/
#include <stdio.h>
#include <string.h>
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_interp.h"
/* stack */
value * coq_stack_low;
value * coq_stack_high;
value * coq_stack_threshold;
asize_t coq_max_stack_size = Coq_max_stack_size;
/* global_data */
value coq_global_data;
int coq_all_transp;
value coq_atom_tbl;
int drawinstr;
/* interp state */
long coq_saved_sp_offset;
value * coq_sp;
/* Some predefined pointer code */
code_t accumulate;
/* functions over global environment */
void coq_stat_free (void * blk)
{
free (blk);
}
value coq_static_alloc(value size) /* ML */
{
return (value) coq_stat_alloc((asize_t) Long_val(size));
}
value accumulate_code(value unit) /* ML */
{
return (value) accumulate;
}
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_global_data, &coq_global_data);
(*action)(coq_atom_tbl, &coq_atom_tbl);
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
(*action) (*i, i);
};
/* Hook */
if (coq_prev_scan_roots_hook != NULL) (*coq_prev_scan_roots_hook)(action);
}
void init_coq_stack()
{
coq_stack_low = (value *) coq_stat_alloc(Coq_stack_size);
coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
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);
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, Val_unit, 0);
}
static int coq_vm_initialized = 0;
value init_coq_vm(value unit) /* ML */
{
int i;
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
drawinstr=0;
#ifdef THREADED_CODE
init_arity();
#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 */
coq_all_transp = 0;
init_coq_interpreter();
/* Some predefined pointer code */
accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
*accumulate = VALINSTR(ACCUMULATE);
/* Initialize GC */
if (coq_prev_scan_roots_hook == NULL)
coq_prev_scan_roots_hook = scan_roots_hook;
scan_roots_hook = coq_scan_roots;
coq_vm_initialized = 1;
}
return Val_unit;;
}
void realloc_coq_stack(asize_t required_space)
{
asize_t size;
value * new_low, * new_high, * new_sp;
value * p;
size = coq_stack_high - coq_stack_low;
do {
size *= 2;
} while (size < coq_stack_high - coq_sp + required_space);
new_low = (value *) coq_stat_alloc(size * sizeof(value));
new_high = new_low + size;
#define shift(ptr) \
((char *) new_high - ((char *) coq_stack_high - (char *) (ptr)))
new_sp = (value *) shift(coq_sp);
memmove((char *) new_sp,
(char *) coq_sp,
(coq_stack_high - coq_sp) * sizeof(value));
coq_stat_free(coq_stack_low);
coq_stack_low = new_low;
coq_stack_high = new_high;
coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
coq_sp = new_sp;
#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;
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_transp_value(value transp)
{
coq_all_transp = (transp == Val_true);
return Val_unit;
}
value get_coq_transp_value(value unit)
{
return Val_bool(coq_all_transp);
}
value coq_set_drawinstr(value unit)
{
drawinstr = 1;
return Val_unit;
}
|
