27 open Hints_declaration
93 type 'f genv_t = { functions : 'f PositiveMap.positive_map;
94 nextfunction : Positive.pos;
95 symbols : Pointers.block Identifiers.identifier_map }
97 val genv_t_rect_Type4 :
98 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
99 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
101 val genv_t_rect_Type5 :
102 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
103 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
105 val genv_t_rect_Type3 :
106 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
107 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
109 val genv_t_rect_Type2 :
110 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
111 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
113 val genv_t_rect_Type1 :
114 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
115 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
117 val genv_t_rect_Type0 :
118 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
119 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
121 val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map
123 val nextfunction : 'a1 genv_t -> Positive.pos
125 val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map
127 val genv_t_inv_rect_Type4 :
128 'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
129 Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
131 val genv_t_inv_rect_Type3 :
132 'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
133 Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
135 val genv_t_inv_rect_Type2 :
136 'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
137 Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
139 val genv_t_inv_rect_Type1 :
140 'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
141 Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
143 val genv_t_inv_rect_Type0 :
144 'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
145 Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
147 val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __
149 val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __
151 val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t
153 val add_funct : (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t
155 val add_symbol : AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t
157 val empty_mem : GenMem.mem
159 val empty : 'a1 genv_t
162 'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t
164 val find_symbol : 'a1 genv_t -> AST.ident -> Pointers.block Types.option
166 val store_init_data :
167 'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
168 GenMem.mem Types.option
170 val size_init_data : AST.init_data -> Nat.nat
172 val store_init_data_list :
173 'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
174 List.list -> GenMem.mem Types.option
176 val size_init_data_list : AST.init_data List.list -> Nat.nat
179 ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod ->
180 ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
181 genv_t, GenMem.mem) Types.prod
184 ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
185 ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
186 GenMem.mem Errors.res
188 val globalenv_allocmem :
189 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1 genv_t,
190 GenMem.mem) Types.prod
193 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t
195 val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t
198 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
201 val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem
203 val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option
205 val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option
207 val symbol_for_block : 'a1 genv_t -> Pointers.block -> AST.ident Types.option
209 val symbol_of_function_block : 'a1 genv_t -> Pointers.block -> AST.ident
211 val symbol_of_function_block' :
212 'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident
214 val find_funct_ptr_id :
215 'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option
217 val opt_eq_from_res__o__ffpi_drop__o__inject :
218 Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
221 val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
222 Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
223 'a2) Types.dPair -> __ Types.sig0
225 val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
226 Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
227 Types.sig0 -> __ Types.sig0
229 val jmeq_to_eq__o__ffpi_drop__o__inject :
230 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
232 val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
233 Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
236 val dpi1__o__ffpi_drop__o__inject :
237 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
240 val eject__o__ffpi_drop__o__inject :
241 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
244 val ffpi_drop__o__inject :
245 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
247 val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident
249 val symbol_of_function_val' : 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident
252 'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option
254 val opt_eq_from_res__o__ffi_drop__o__inject :
255 Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
258 val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
259 Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2)
260 Types.dPair -> __ Types.sig0
262 val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
263 Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
264 Types.sig0 -> __ Types.sig0
266 val jmeq_to_eq__o__ffi_drop__o__inject :
267 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
269 val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
270 Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
273 val dpi1__o__ffi_drop__o__inject :
274 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
277 val eject__o__ffi_drop__o__inject :
278 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
281 val ffi_drop__o__inject :
282 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
284 val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
287 GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
288 GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1
290 val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
292 val related_globals_rect_Type4 :
293 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
296 val related_globals_rect_Type5 :
297 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
300 val related_globals_rect_Type3 :
301 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
304 val related_globals_rect_Type2 :
305 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
308 val related_globals_rect_Type1 :
309 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
312 val related_globals_rect_Type0 :
313 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
316 val related_globals_inv_rect_Type4 :
317 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
320 val related_globals_inv_rect_Type3 :
321 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
324 val related_globals_inv_rect_Type2 :
325 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
328 val related_globals_inv_rect_Type1 :
329 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
332 val related_globals_inv_rect_Type0 :
333 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
336 val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
338 val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
340 val related_globals_gen_rect_Type4 :
341 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
342 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
343 -> __ -> __ -> 'a3) -> 'a3
345 val related_globals_gen_rect_Type5 :
346 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
347 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
348 -> __ -> __ -> 'a3) -> 'a3
350 val related_globals_gen_rect_Type3 :
351 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
352 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
353 -> __ -> __ -> 'a3) -> 'a3
355 val related_globals_gen_rect_Type2 :
356 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
357 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
358 -> __ -> __ -> 'a3) -> 'a3
360 val related_globals_gen_rect_Type1 :
361 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
362 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
363 -> __ -> __ -> 'a3) -> 'a3
365 val related_globals_gen_rect_Type0 :
366 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
367 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
368 -> __ -> __ -> 'a3) -> 'a3
370 val related_globals_gen_inv_rect_Type4 :
371 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
372 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
373 -> __ -> __ -> __ -> 'a3) -> 'a3
375 val related_globals_gen_inv_rect_Type3 :
376 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
377 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
378 -> __ -> __ -> __ -> 'a3) -> 'a3
380 val related_globals_gen_inv_rect_Type2 :
381 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
382 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
383 -> __ -> __ -> __ -> 'a3) -> 'a3
385 val related_globals_gen_inv_rect_Type1 :
386 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
387 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
388 -> __ -> __ -> __ -> 'a3) -> 'a3
390 val related_globals_gen_inv_rect_Type0 :
391 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
392 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
393 -> __ -> __ -> __ -> 'a3) -> 'a3
395 val related_globals_gen_discr :
396 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
397 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
399 val related_globals_gen_jmdiscr :
400 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
401 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __