83 open Hints_declaration
133 type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
134 stack_sizes : (AST.ident -> Nat.nat Types.option);
136 pc_from_label : (Pointers.block Types.sig0 -> 'f ->
138 ByteValues.program_counter Types.option) }
140 (** val genv_gen_rect_Type4 :
141 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
142 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
143 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
144 'a2) -> 'a1 genv_gen -> 'a2 **)
145 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_24476 =
146 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
147 pc_from_label = pc_from_label0 } = x_24476
149 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
151 (** val genv_gen_rect_Type5 :
152 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
153 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
154 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
155 'a2) -> 'a1 genv_gen -> 'a2 **)
156 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_24478 =
157 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
158 pc_from_label = pc_from_label0 } = x_24478
160 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
162 (** val genv_gen_rect_Type3 :
163 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
164 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
165 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
166 'a2) -> 'a1 genv_gen -> 'a2 **)
167 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_24480 =
168 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
169 pc_from_label = pc_from_label0 } = x_24480
171 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
173 (** val genv_gen_rect_Type2 :
174 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
175 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
176 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
177 'a2) -> 'a1 genv_gen -> 'a2 **)
178 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_24482 =
179 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
180 pc_from_label = pc_from_label0 } = x_24482
182 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
184 (** val genv_gen_rect_Type1 :
185 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
186 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
187 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
188 'a2) -> 'a1 genv_gen -> 'a2 **)
189 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_24484 =
190 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
191 pc_from_label = pc_from_label0 } = x_24484
193 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
195 (** val genv_gen_rect_Type0 :
196 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
197 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
198 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
199 'a2) -> 'a1 genv_gen -> 'a2 **)
200 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_24486 =
201 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
202 pc_from_label = pc_from_label0 } = x_24486
204 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
207 AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t **)
208 let rec ge globals xxx =
211 (** val stack_sizes :
212 AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option **)
213 let rec stack_sizes globals xxx =
216 (** val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1 **)
217 let rec premain globals xxx =
220 (** val pc_from_label :
221 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1
222 -> Graphs.label -> ByteValues.program_counter Types.option **)
223 let rec pc_from_label globals xxx =
226 (** val genv_gen_inv_rect_Type4 :
227 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
228 -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
229 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
230 Types.option) -> __ -> 'a2) -> 'a2 **)
231 let genv_gen_inv_rect_Type4 x2 hterm h1 =
232 let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __
234 (** val genv_gen_inv_rect_Type3 :
235 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
236 -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
237 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
238 Types.option) -> __ -> 'a2) -> 'a2 **)
239 let genv_gen_inv_rect_Type3 x2 hterm h1 =
240 let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __
242 (** val genv_gen_inv_rect_Type2 :
243 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
244 -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
245 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
246 Types.option) -> __ -> 'a2) -> 'a2 **)
247 let genv_gen_inv_rect_Type2 x2 hterm h1 =
248 let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __
250 (** val genv_gen_inv_rect_Type1 :
251 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
252 -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
253 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
254 Types.option) -> __ -> 'a2) -> 'a2 **)
255 let genv_gen_inv_rect_Type1 x2 hterm h1 =
256 let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __
258 (** val genv_gen_inv_rect_Type0 :
259 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
260 -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
261 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
262 Types.option) -> __ -> 'a2) -> 'a2 **)
263 let genv_gen_inv_rect_Type0 x2 hterm h1 =
264 let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __
266 (** val genv_gen_discr :
267 AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
268 let genv_gen_discr a2 x y =
269 Logic.eq_rect_Type2 x
270 (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
272 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
274 (** val genv_gen_jmdiscr :
275 AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
276 let genv_gen_jmdiscr a2 x y =
277 Logic.eq_rect_Type2 x
278 (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
280 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
282 (** val dpi1__o__ge__o__inject :
283 AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
284 Globalenvs.genv_t Types.sig0 **)
285 let dpi1__o__ge__o__inject x1 x4 =
288 (** val eject__o__ge__o__inject :
289 AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
290 Globalenvs.genv_t Types.sig0 **)
291 let eject__o__ge__o__inject x1 x4 =
294 (** val ge__o__inject :
295 AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
297 let ge__o__inject x1 x3 =
300 (** val dpi1__o__ge :
301 AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
302 Globalenvs.genv_t **)
303 let dpi1__o__ge x1 x3 =
306 (** val eject__o__ge :
307 AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
308 Globalenvs.genv_t **)
309 let eject__o__ge x1 x3 =
312 (** val pre_main_id : AST.ident **)
316 (** val fetch_function :
317 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
318 (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **)
319 let fetch_function g ge0 bl =
320 match Z.eqZb (Pointers.block_id (Types.pi1 bl))
321 (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with
324 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id;
325 Types.snd = (AST.Internal ge0.premain) })
327 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
330 (Monad.m_bind0 (Monad.max_def Option.option)
331 (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl)))
333 Monad.m_bind0 (Monad.max_def Option.option)
334 (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl)))
336 Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
339 (** val fetch_internal_function :
340 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
341 (AST.ident, 'a1) Types.prod Errors.res **)
342 let fetch_internal_function g ge0 bl =
344 (Monad.m_bind2 (Monad.max_def Errors.res0)
345 (Obj.magic (fetch_function g ge0 bl)) (fun id fd ->
347 | AST.Internal ifd ->
348 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
351 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
352 ErrorMessages.BadFunction), List.Nil)))))
354 (** val code_block_of_block :
355 Pointers.block -> Pointers.block Types.sig0 Types.option **)
356 let code_block_of_block bl =
357 (match Pointers.block_region bl with
358 | AST.XData -> (fun _ -> Types.None)
359 | AST.Code -> (fun _ -> Types.Some bl)) __
361 (** val block_of_funct_id :
362 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
363 Types.sig0 Errors.res **)
364 let block_of_funct_id ge0 id =
365 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
366 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
368 (Monad.m_bind0 (Monad.max_def Option.option)
369 (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
370 Obj.magic (code_block_of_block bl))))
372 (** val gen_pc_from_label :
373 AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
374 ByteValues.program_counter Errors.res **)
375 let gen_pc_from_label g ge0 id lbl =
377 (Monad.m_bind0 (Monad.max_def Errors.res0)
378 (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl ->
379 Monad.m_bind2 (Monad.max_def Errors.res0)
380 (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def ->
382 (Errors.opt_to_res (List.Cons ((Errors.MSG
383 ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
384 (PreIdentifiers.LabelTag, lbl)), List.Nil))))
385 (ge0.pc_from_label bl f_def lbl)))))
387 type genv = Joint.joint_closed_internal_function genv_gen
389 type sem_state_params = { empty_framesT : __;
390 empty_regsT : (ByteValues.xpointer -> __);
391 load_sp : (__ -> ByteValues.xpointer Errors.res);
392 save_sp : (__ -> ByteValues.xpointer -> __) }
394 (** val sem_state_params_rect_Type4 :
395 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
396 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
397 'a1) -> sem_state_params -> 'a1 **)
398 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_24507 =
399 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
400 load_sp0; save_sp = save_sp0 } = x_24507
402 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
404 (** val sem_state_params_rect_Type5 :
405 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
406 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
407 'a1) -> sem_state_params -> 'a1 **)
408 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_24509 =
409 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
410 load_sp0; save_sp = save_sp0 } = x_24509
412 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
414 (** val sem_state_params_rect_Type3 :
415 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
416 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
417 'a1) -> sem_state_params -> 'a1 **)
418 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_24511 =
419 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
420 load_sp0; save_sp = save_sp0 } = x_24511
422 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
424 (** val sem_state_params_rect_Type2 :
425 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
426 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
427 'a1) -> sem_state_params -> 'a1 **)
428 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_24513 =
429 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
430 load_sp0; save_sp = save_sp0 } = x_24513
432 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
434 (** val sem_state_params_rect_Type1 :
435 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
436 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
437 'a1) -> sem_state_params -> 'a1 **)
438 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_24515 =
439 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
440 load_sp0; save_sp = save_sp0 } = x_24515
442 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
444 (** val sem_state_params_rect_Type0 :
445 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
446 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
447 'a1) -> sem_state_params -> 'a1 **)
448 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_24517 =
449 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
450 load_sp0; save_sp = save_sp0 } = x_24517
452 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
456 (** val empty_framesT : sem_state_params -> __ **)
457 let rec empty_framesT xxx =
462 (** val empty_regsT : sem_state_params -> ByteValues.xpointer -> __ **)
463 let rec empty_regsT xxx =
467 sem_state_params -> __ -> ByteValues.xpointer Errors.res **)
468 let rec load_sp xxx =
471 (** val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __ **)
472 let rec save_sp xxx =
475 (** val sem_state_params_inv_rect_Type4 :
476 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
477 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
478 -> __ -> 'a1) -> 'a1 **)
479 let sem_state_params_inv_rect_Type4 hterm h1 =
480 let hcut = sem_state_params_rect_Type4 h1 hterm in hcut __
482 (** val sem_state_params_inv_rect_Type3 :
483 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
484 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
485 -> __ -> 'a1) -> 'a1 **)
486 let sem_state_params_inv_rect_Type3 hterm h1 =
487 let hcut = sem_state_params_rect_Type3 h1 hterm in hcut __
489 (** val sem_state_params_inv_rect_Type2 :
490 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
491 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
492 -> __ -> 'a1) -> 'a1 **)
493 let sem_state_params_inv_rect_Type2 hterm h1 =
494 let hcut = sem_state_params_rect_Type2 h1 hterm in hcut __
496 (** val sem_state_params_inv_rect_Type1 :
497 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
498 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
499 -> __ -> 'a1) -> 'a1 **)
500 let sem_state_params_inv_rect_Type1 hterm h1 =
501 let hcut = sem_state_params_rect_Type1 h1 hterm in hcut __
503 (** val sem_state_params_inv_rect_Type0 :
504 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
505 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
506 -> __ -> 'a1) -> 'a1 **)
507 let sem_state_params_inv_rect_Type0 hterm h1 =
508 let hcut = sem_state_params_rect_Type0 h1 hterm in hcut __
510 (** val sem_state_params_jmdiscr :
511 sem_state_params -> sem_state_params -> __ **)
512 let sem_state_params_jmdiscr x y =
513 Logic.eq_rect_Type2 x
514 (let { empty_framesT = a1; empty_regsT = a3; load_sp = a4; save_sp =
517 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
519 type internal_stack =
521 | One_is of ByteValues.beval
522 | Both_is of ByteValues.beval * ByteValues.beval
524 (** val internal_stack_rect_Type4 :
525 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
526 -> 'a1) -> internal_stack -> 'a1 **)
527 let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
528 | Empty_is -> h_empty_is
529 | One_is x_24543 -> h_one_is x_24543
530 | Both_is (x_24545, x_24544) -> h_both_is x_24545 x_24544
532 (** val internal_stack_rect_Type5 :
533 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
534 -> 'a1) -> internal_stack -> 'a1 **)
535 let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
536 | Empty_is -> h_empty_is
537 | One_is x_24550 -> h_one_is x_24550
538 | Both_is (x_24552, x_24551) -> h_both_is x_24552 x_24551
540 (** val internal_stack_rect_Type3 :
541 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
542 -> 'a1) -> internal_stack -> 'a1 **)
543 let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
544 | Empty_is -> h_empty_is
545 | One_is x_24557 -> h_one_is x_24557
546 | Both_is (x_24559, x_24558) -> h_both_is x_24559 x_24558
548 (** val internal_stack_rect_Type2 :
549 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
550 -> 'a1) -> internal_stack -> 'a1 **)
551 let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
552 | Empty_is -> h_empty_is
553 | One_is x_24564 -> h_one_is x_24564
554 | Both_is (x_24566, x_24565) -> h_both_is x_24566 x_24565
556 (** val internal_stack_rect_Type1 :
557 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
558 -> 'a1) -> internal_stack -> 'a1 **)
559 let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
560 | Empty_is -> h_empty_is
561 | One_is x_24571 -> h_one_is x_24571
562 | Both_is (x_24573, x_24572) -> h_both_is x_24573 x_24572
564 (** val internal_stack_rect_Type0 :
565 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
566 -> 'a1) -> internal_stack -> 'a1 **)
567 let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
568 | Empty_is -> h_empty_is
569 | One_is x_24578 -> h_one_is x_24578
570 | Both_is (x_24580, x_24579) -> h_both_is x_24580 x_24579
572 (** val internal_stack_inv_rect_Type4 :
573 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
574 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
575 let internal_stack_inv_rect_Type4 hterm h1 h2 h3 =
576 let hcut = internal_stack_rect_Type4 h1 h2 h3 hterm in hcut __
578 (** val internal_stack_inv_rect_Type3 :
579 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
580 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
581 let internal_stack_inv_rect_Type3 hterm h1 h2 h3 =
582 let hcut = internal_stack_rect_Type3 h1 h2 h3 hterm in hcut __
584 (** val internal_stack_inv_rect_Type2 :
585 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
586 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
587 let internal_stack_inv_rect_Type2 hterm h1 h2 h3 =
588 let hcut = internal_stack_rect_Type2 h1 h2 h3 hterm in hcut __
590 (** val internal_stack_inv_rect_Type1 :
591 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
592 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
593 let internal_stack_inv_rect_Type1 hterm h1 h2 h3 =
594 let hcut = internal_stack_rect_Type1 h1 h2 h3 hterm in hcut __
596 (** val internal_stack_inv_rect_Type0 :
597 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
598 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
599 let internal_stack_inv_rect_Type0 hterm h1 h2 h3 =
600 let hcut = internal_stack_rect_Type0 h1 h2 h3 hterm in hcut __
602 (** val internal_stack_discr : internal_stack -> internal_stack -> __ **)
603 let internal_stack_discr x y =
604 Logic.eq_rect_Type2 x
606 | Empty_is -> Obj.magic (fun _ dH -> dH)
607 | One_is a0 -> Obj.magic (fun _ dH -> dH __)
608 | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
610 (** val internal_stack_jmdiscr : internal_stack -> internal_stack -> __ **)
611 let internal_stack_jmdiscr x y =
612 Logic.eq_rect_Type2 x
614 | Empty_is -> Obj.magic (fun _ dH -> dH)
615 | One_is a0 -> Obj.magic (fun _ dH -> dH __)
616 | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
619 internal_stack -> ByteValues.beval -> internal_stack Errors.res **)
623 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (One_is bv))
626 (Monad.m_return0 (Monad.max_def Errors.res0) (Both_is (bv', bv)))
628 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackFull),
632 internal_stack -> (ByteValues.beval, internal_stack) Types.prod
634 let is_pop = function
636 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackEmpty),
640 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
641 Types.snd = Empty_is })
642 | Both_is (bv, bv') ->
644 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
645 Types.snd = (One_is bv) })
647 type state = { st_frms : __ Types.option; istack : internal_stack;
648 carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
649 stack_usage : Nat.nat }
651 (** val state_rect_Type4 :
652 sem_state_params -> (__ Types.option -> internal_stack ->
653 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
654 let rec state_rect_Type4 semp h_mk_state x_24628 =
655 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
656 m = m0; stack_usage = stack_usage0 } = x_24628
658 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
660 (** val state_rect_Type5 :
661 sem_state_params -> (__ Types.option -> internal_stack ->
662 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
663 let rec state_rect_Type5 semp h_mk_state x_24630 =
664 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
665 m = m0; stack_usage = stack_usage0 } = x_24630
667 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
669 (** val state_rect_Type3 :
670 sem_state_params -> (__ Types.option -> internal_stack ->
671 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
672 let rec state_rect_Type3 semp h_mk_state x_24632 =
673 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
674 m = m0; stack_usage = stack_usage0 } = x_24632
676 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
678 (** val state_rect_Type2 :
679 sem_state_params -> (__ Types.option -> internal_stack ->
680 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
681 let rec state_rect_Type2 semp h_mk_state x_24634 =
682 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
683 m = m0; stack_usage = stack_usage0 } = x_24634
685 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
687 (** val state_rect_Type1 :
688 sem_state_params -> (__ Types.option -> internal_stack ->
689 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
690 let rec state_rect_Type1 semp h_mk_state x_24636 =
691 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
692 m = m0; stack_usage = stack_usage0 } = x_24636
694 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
696 (** val state_rect_Type0 :
697 sem_state_params -> (__ Types.option -> internal_stack ->
698 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
699 let rec state_rect_Type0 semp h_mk_state x_24638 =
700 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
701 m = m0; stack_usage = stack_usage0 } = x_24638
703 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
705 (** val st_frms : sem_state_params -> state -> __ Types.option **)
706 let rec st_frms semp xxx =
709 (** val istack : sem_state_params -> state -> internal_stack **)
710 let rec istack semp xxx =
713 (** val carry : sem_state_params -> state -> ByteValues.bebit **)
714 let rec carry semp xxx =
717 (** val regs : sem_state_params -> state -> __ **)
718 let rec regs semp xxx =
721 (** val m : sem_state_params -> state -> BEMem.bemem **)
725 (** val stack_usage : sem_state_params -> state -> Nat.nat **)
726 let rec stack_usage semp xxx =
729 (** val state_inv_rect_Type4 :
730 sem_state_params -> state -> (__ Types.option -> internal_stack ->
731 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
732 let state_inv_rect_Type4 x1 hterm h1 =
733 let hcut = state_rect_Type4 x1 h1 hterm in hcut __
735 (** val state_inv_rect_Type3 :
736 sem_state_params -> state -> (__ Types.option -> internal_stack ->
737 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
738 let state_inv_rect_Type3 x1 hterm h1 =
739 let hcut = state_rect_Type3 x1 h1 hterm in hcut __
741 (** val state_inv_rect_Type2 :
742 sem_state_params -> state -> (__ Types.option -> internal_stack ->
743 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
744 let state_inv_rect_Type2 x1 hterm h1 =
745 let hcut = state_rect_Type2 x1 h1 hterm in hcut __
747 (** val state_inv_rect_Type1 :
748 sem_state_params -> state -> (__ Types.option -> internal_stack ->
749 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
750 let state_inv_rect_Type1 x1 hterm h1 =
751 let hcut = state_rect_Type1 x1 h1 hterm in hcut __
753 (** val state_inv_rect_Type0 :
754 sem_state_params -> state -> (__ Types.option -> internal_stack ->
755 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
756 let state_inv_rect_Type0 x1 hterm h1 =
757 let hcut = state_rect_Type0 x1 h1 hterm in hcut __
759 (** val state_jmdiscr : sem_state_params -> state -> state -> __ **)
760 let state_jmdiscr a1 x y =
761 Logic.eq_rect_Type2 x
762 (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4;
763 stack_usage = a5 } = x
765 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
767 (** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **)
771 type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
772 last_pop : ByteValues.program_counter }
774 (** val state_pc_rect_Type4 :
775 sem_state_params -> (state -> ByteValues.program_counter ->
776 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
777 let rec state_pc_rect_Type4 semp h_mk_state_pc x_24654 =
778 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24654 in
779 h_mk_state_pc st_no_pc0 pc0 last_pop0
781 (** val state_pc_rect_Type5 :
782 sem_state_params -> (state -> ByteValues.program_counter ->
783 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
784 let rec state_pc_rect_Type5 semp h_mk_state_pc x_24656 =
785 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24656 in
786 h_mk_state_pc st_no_pc0 pc0 last_pop0
788 (** val state_pc_rect_Type3 :
789 sem_state_params -> (state -> ByteValues.program_counter ->
790 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
791 let rec state_pc_rect_Type3 semp h_mk_state_pc x_24658 =
792 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24658 in
793 h_mk_state_pc st_no_pc0 pc0 last_pop0
795 (** val state_pc_rect_Type2 :
796 sem_state_params -> (state -> ByteValues.program_counter ->
797 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
798 let rec state_pc_rect_Type2 semp h_mk_state_pc x_24660 =
799 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24660 in
800 h_mk_state_pc st_no_pc0 pc0 last_pop0
802 (** val state_pc_rect_Type1 :
803 sem_state_params -> (state -> ByteValues.program_counter ->
804 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
805 let rec state_pc_rect_Type1 semp h_mk_state_pc x_24662 =
806 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24662 in
807 h_mk_state_pc st_no_pc0 pc0 last_pop0
809 (** val state_pc_rect_Type0 :
810 sem_state_params -> (state -> ByteValues.program_counter ->
811 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
812 let rec state_pc_rect_Type0 semp h_mk_state_pc x_24664 =
813 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24664 in
814 h_mk_state_pc st_no_pc0 pc0 last_pop0
816 (** val st_no_pc : sem_state_params -> state_pc -> state **)
817 let rec st_no_pc semp xxx =
820 (** val pc : sem_state_params -> state_pc -> ByteValues.program_counter **)
821 let rec pc semp xxx =
825 sem_state_params -> state_pc -> ByteValues.program_counter **)
826 let rec last_pop semp xxx =
829 (** val state_pc_inv_rect_Type4 :
830 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
831 ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
832 let state_pc_inv_rect_Type4 x1 hterm h1 =
833 let hcut = state_pc_rect_Type4 x1 h1 hterm in hcut __
835 (** val state_pc_inv_rect_Type3 :
836 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
837 ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
838 let state_pc_inv_rect_Type3 x1 hterm h1 =
839 let hcut = state_pc_rect_Type3 x1 h1 hterm in hcut __
841 (** val state_pc_inv_rect_Type2 :
842 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
843 ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
844 let state_pc_inv_rect_Type2 x1 hterm h1 =
845 let hcut = state_pc_rect_Type2 x1 h1 hterm in hcut __
847 (** val state_pc_inv_rect_Type1 :
848 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
849 ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
850 let state_pc_inv_rect_Type1 x1 hterm h1 =
851 let hcut = state_pc_rect_Type1 x1 h1 hterm in hcut __
853 (** val state_pc_inv_rect_Type0 :
854 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
855 ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
856 let state_pc_inv_rect_Type0 x1 hterm h1 =
857 let hcut = state_pc_rect_Type0 x1 h1 hterm in hcut __
859 (** val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __ **)
860 let state_pc_discr a1 x y =
861 Logic.eq_rect_Type2 x
862 (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
863 Obj.magic (fun _ dH -> dH __ __ __)) y
865 (** val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __ **)
866 let state_pc_jmdiscr a1 x y =
867 Logic.eq_rect_Type2 x
868 (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
869 Obj.magic (fun _ dH -> dH __ __ __)) y
871 (** val dpi1__o__st_no_pc__o__inject :
872 sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0 **)
873 let dpi1__o__st_no_pc__o__inject x0 x3 =
874 x3.Types.dpi1.st_no_pc
876 (** val eject__o__st_no_pc__o__inject :
877 sem_state_params -> state_pc Types.sig0 -> state Types.sig0 **)
878 let eject__o__st_no_pc__o__inject x0 x3 =
879 (Types.pi1 x3).st_no_pc
881 (** val st_no_pc__o__inject :
882 sem_state_params -> state_pc -> state Types.sig0 **)
883 let st_no_pc__o__inject x0 x2 =
886 (** val dpi1__o__st_no_pc :
887 sem_state_params -> (state_pc, 'a1) Types.dPair -> state **)
888 let dpi1__o__st_no_pc x0 x2 =
889 x2.Types.dpi1.st_no_pc
891 (** val eject__o__st_no_pc :
892 sem_state_params -> state_pc Types.sig0 -> state **)
893 let eject__o__st_no_pc x0 x2 =
894 (Types.pi1 x2).st_no_pc
896 (** val init_pc : ByteValues.program_counter **)
898 { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
899 ByteValues.pc_offset = Positive.One }
901 (** val null_pc : Positive.pos -> ByteValues.program_counter **)
903 { ByteValues.pc_block = Pointers.dummy_block_code; ByteValues.pc_offset =
906 (** val set_m : sem_state_params -> BEMem.bemem -> state -> state **)
908 { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
909 st.regs; m = m0; stack_usage = st.stack_usage }
911 (** val set_regs : sem_state_params -> __ -> state -> state **)
912 let set_regs p regs0 st =
913 { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0;
914 m = st.m; stack_usage = st.stack_usage }
917 sem_state_params -> ByteValues.xpointer -> state -> state **)
918 let set_sp p sp0 st =
919 let regs' = p.save_sp st.regs sp0 in
920 { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs';
921 m = st.m; stack_usage = st.stack_usage }
924 sem_state_params -> ByteValues.bebit -> state -> state **)
925 let set_carry p carry0 st =
926 { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs;
927 m = st.m; stack_usage = st.stack_usage }
929 (** val set_istack : sem_state_params -> internal_stack -> state -> state **)
930 let set_istack p is st =
931 { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m =
932 st.m; stack_usage = st.stack_usage }
935 sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc **)
936 let set_pc p pc0 st =
937 { st_no_pc = st.st_no_pc; pc = pc0; last_pop = st.last_pop }
939 (** val set_no_pc : sem_state_params -> state -> state_pc -> state_pc **)
940 let set_no_pc p s st =
941 { st_no_pc = s; pc = st.pc; last_pop = st.last_pop }
943 (** val set_last_pop :
944 sem_state_params -> state -> ByteValues.program_counter -> state_pc **)
945 let set_last_pop p st pc0 =
946 { st_no_pc = st; pc = pc0; last_pop = pc0 }
948 (** val set_frms : sem_state_params -> __ -> state -> state **)
949 let set_frms p frms st =
950 { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
951 st.regs; m = st.m; stack_usage = st.stack_usage }
957 (** val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
958 let rec call_kind_rect_Type4 h_PTR h_ID = function
962 (** val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
963 let rec call_kind_rect_Type5 h_PTR h_ID = function
967 (** val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
968 let rec call_kind_rect_Type3 h_PTR h_ID = function
972 (** val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
973 let rec call_kind_rect_Type2 h_PTR h_ID = function
977 (** val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
978 let rec call_kind_rect_Type1 h_PTR h_ID = function
982 (** val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
983 let rec call_kind_rect_Type0 h_PTR h_ID = function
987 (** val call_kind_inv_rect_Type4 :
988 call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
989 let call_kind_inv_rect_Type4 hterm h1 h2 =
990 let hcut = call_kind_rect_Type4 h1 h2 hterm in hcut __
992 (** val call_kind_inv_rect_Type3 :
993 call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
994 let call_kind_inv_rect_Type3 hterm h1 h2 =
995 let hcut = call_kind_rect_Type3 h1 h2 hterm in hcut __
997 (** val call_kind_inv_rect_Type2 :
998 call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
999 let call_kind_inv_rect_Type2 hterm h1 h2 =
1000 let hcut = call_kind_rect_Type2 h1 h2 hterm in hcut __
1002 (** val call_kind_inv_rect_Type1 :
1003 call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
1004 let call_kind_inv_rect_Type1 hterm h1 h2 =
1005 let hcut = call_kind_rect_Type1 h1 h2 hterm in hcut __
1007 (** val call_kind_inv_rect_Type0 :
1008 call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
1009 let call_kind_inv_rect_Type0 hterm h1 h2 =
1010 let hcut = call_kind_rect_Type0 h1 h2 hterm in hcut __
1012 (** val call_kind_discr : call_kind -> call_kind -> __ **)
1013 let call_kind_discr x y =
1014 Logic.eq_rect_Type2 x
1016 | PTR -> Obj.magic (fun _ dH -> dH)
1017 | ID -> Obj.magic (fun _ dH -> dH)) y
1019 (** val call_kind_jmdiscr : call_kind -> call_kind -> __ **)
1020 let call_kind_jmdiscr x y =
1021 Logic.eq_rect_Type2 x
1023 | PTR -> Obj.magic (fun _ dH -> dH)
1024 | ID -> Obj.magic (fun _ dH -> dH)) y
1026 (** val kind_of_call :
1027 Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum
1029 let kind_of_call p = function
1031 | Types.Inr x -> PTR
1033 type 'f sem_unserialized_params = { st_pars : sem_state_params;
1034 acca_store_ : (__ -> ByteValues.beval ->
1035 __ -> __ Errors.res);
1036 acca_retrieve_ : (__ -> __ ->
1039 acca_arg_retrieve_ : (__ -> __ ->
1042 accb_store_ : (__ -> ByteValues.beval ->
1043 __ -> __ Errors.res);
1044 accb_retrieve_ : (__ -> __ ->
1047 accb_arg_retrieve_ : (__ -> __ ->
1050 dpl_store_ : (__ -> ByteValues.beval ->
1051 __ -> __ Errors.res);
1052 dpl_retrieve_ : (__ -> __ ->
1055 dpl_arg_retrieve_ : (__ -> __ ->
1058 dph_store_ : (__ -> ByteValues.beval ->
1059 __ -> __ Errors.res);
1060 dph_retrieve_ : (__ -> __ ->
1063 dph_arg_retrieve_ : (__ -> __ ->
1066 snd_arg_retrieve_ : (__ -> __ ->
1069 pair_reg_move_ : (__ -> __ -> __
1071 save_frame : (call_kind -> __ -> state_pc
1072 -> state Errors.res);
1073 setup_call : (Nat.nat -> __ -> __ ->
1074 state -> state Errors.res);
1075 fetch_external_args : (AST.external_function
1080 set_result : (Values.val0 List.list -> __
1083 call_args_for_main : __;
1084 call_dest_for_main : __;
1085 read_result : (AST.ident List.list -> 'f
1087 Globalenvs.genv_t -> __ ->
1088 state -> ByteValues.beval
1089 List.list Errors.res);
1090 eval_ext_seq : (AST.ident List.list -> 'f
1092 AST.ident -> state ->
1094 pop_frame : (AST.ident List.list -> 'f
1095 genv_gen -> AST.ident -> __
1097 ByteValues.program_counter)
1098 Types.prod Errors.res) }
1100 (** val sem_unserialized_params_rect_Type4 :
1101 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1102 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1103 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1104 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1105 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1106 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1107 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1108 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1109 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1110 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1111 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1112 (AST.external_function -> state -> __ -> Values.val0 List.list
1113 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1114 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1115 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1116 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1117 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1118 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1119 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1120 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_24719 =
1121 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1122 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1123 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1124 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1125 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1126 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1127 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1128 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1129 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1130 set_result0; call_args_for_main = call_args_for_main0;
1131 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1132 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24719
1134 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1135 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1136 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1137 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1138 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1139 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1141 (** val sem_unserialized_params_rect_Type5 :
1142 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1143 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1144 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1145 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1146 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1147 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1148 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1149 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1150 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1151 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1152 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1153 (AST.external_function -> state -> __ -> Values.val0 List.list
1154 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1155 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1156 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1157 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1158 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1159 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1160 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1161 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_24721 =
1162 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1163 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1164 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1165 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1166 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1167 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1168 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1169 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1170 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1171 set_result0; call_args_for_main = call_args_for_main0;
1172 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1173 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24721
1175 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1176 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1177 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1178 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1179 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1180 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1182 (** val sem_unserialized_params_rect_Type3 :
1183 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1184 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1185 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1186 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1187 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1188 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1189 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1190 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1191 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1192 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1193 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1194 (AST.external_function -> state -> __ -> Values.val0 List.list
1195 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1196 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1197 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1198 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1199 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1200 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1201 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1202 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_24723 =
1203 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1204 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1205 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1206 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1207 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1208 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1209 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1210 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1211 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1212 set_result0; call_args_for_main = call_args_for_main0;
1213 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1214 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24723
1216 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1217 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1218 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1219 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1220 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1221 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1223 (** val sem_unserialized_params_rect_Type2 :
1224 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1225 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1226 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1227 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1228 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1229 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1230 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1231 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1232 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1233 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1234 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1235 (AST.external_function -> state -> __ -> Values.val0 List.list
1236 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1237 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1238 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1239 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1240 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1241 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1242 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1243 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_24725 =
1244 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1245 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1246 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1247 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1248 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1249 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1250 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1251 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1252 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1253 set_result0; call_args_for_main = call_args_for_main0;
1254 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1255 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24725
1257 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1258 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1259 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1260 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1261 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1262 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1264 (** val sem_unserialized_params_rect_Type1 :
1265 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1266 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1267 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1268 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1269 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1270 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1271 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1272 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1273 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1274 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1275 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1276 (AST.external_function -> state -> __ -> Values.val0 List.list
1277 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1278 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1279 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1280 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1281 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1282 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1283 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1284 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_24727 =
1285 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1286 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1287 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1288 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1289 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1290 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1291 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1292 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1293 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1294 set_result0; call_args_for_main = call_args_for_main0;
1295 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1296 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24727
1298 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1299 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1300 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1301 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1302 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1303 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1305 (** val sem_unserialized_params_rect_Type0 :
1306 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1307 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1308 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1309 __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1310 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1311 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1312 -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1313 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1314 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1315 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1316 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1317 (AST.external_function -> state -> __ -> Values.val0 List.list
1318 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1319 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1320 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1321 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1322 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1323 state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1324 'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1325 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_24729 =
1326 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1327 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1328 accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1329 accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1330 dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1331 dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1332 dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1333 pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1334 setup_call0; fetch_external_args = fetch_external_args0; set_result =
1335 set_result0; call_args_for_main = call_args_for_main0;
1336 call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1337 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24729
1339 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1340 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1341 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1342 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1343 setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1344 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1347 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1348 sem_state_params **)
1349 let rec st_pars uns_pars xxx =
1352 (** val acca_store_ :
1353 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1354 ByteValues.beval -> __ -> __ Errors.res **)
1355 let rec acca_store_ uns_pars xxx =
1358 (** val acca_retrieve_ :
1359 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1360 ByteValues.beval Errors.res **)
1361 let rec acca_retrieve_ uns_pars xxx =
1364 (** val acca_arg_retrieve_ :
1365 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1366 ByteValues.beval Errors.res **)
1367 let rec acca_arg_retrieve_ uns_pars xxx =
1368 xxx.acca_arg_retrieve_
1370 (** val accb_store_ :
1371 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1372 ByteValues.beval -> __ -> __ Errors.res **)
1373 let rec accb_store_ uns_pars xxx =
1376 (** val accb_retrieve_ :
1377 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1378 ByteValues.beval Errors.res **)
1379 let rec accb_retrieve_ uns_pars xxx =
1382 (** val accb_arg_retrieve_ :
1383 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1384 ByteValues.beval Errors.res **)
1385 let rec accb_arg_retrieve_ uns_pars xxx =
1386 xxx.accb_arg_retrieve_
1388 (** val dpl_store_ :
1389 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1390 ByteValues.beval -> __ -> __ Errors.res **)
1391 let rec dpl_store_ uns_pars xxx =
1394 (** val dpl_retrieve_ :
1395 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1396 ByteValues.beval Errors.res **)
1397 let rec dpl_retrieve_ uns_pars xxx =
1400 (** val dpl_arg_retrieve_ :
1401 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1402 ByteValues.beval Errors.res **)
1403 let rec dpl_arg_retrieve_ uns_pars xxx =
1404 xxx.dpl_arg_retrieve_
1406 (** val dph_store_ :
1407 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1408 ByteValues.beval -> __ -> __ Errors.res **)
1409 let rec dph_store_ uns_pars xxx =
1412 (** val dph_retrieve_ :
1413 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1414 ByteValues.beval Errors.res **)
1415 let rec dph_retrieve_ uns_pars xxx =
1418 (** val dph_arg_retrieve_ :
1419 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1420 ByteValues.beval Errors.res **)
1421 let rec dph_arg_retrieve_ uns_pars xxx =
1422 xxx.dph_arg_retrieve_
1424 (** val snd_arg_retrieve_ :
1425 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1426 ByteValues.beval Errors.res **)
1427 let rec snd_arg_retrieve_ uns_pars xxx =
1428 xxx.snd_arg_retrieve_
1430 (** val pair_reg_move_ :
1431 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1433 let rec pair_reg_move_ uns_pars xxx =
1436 (** val save_frame :
1437 Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind ->
1438 __ -> state_pc -> state Errors.res **)
1439 let rec save_frame uns_pars xxx =
1442 (** val setup_call :
1443 Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
1444 -> __ -> state -> state Errors.res **)
1445 let rec setup_call uns_pars xxx =
1448 (** val fetch_external_args :
1449 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1450 AST.external_function -> state -> __ -> Values.val0 List.list Errors.res **)
1451 let rec fetch_external_args uns_pars xxx =
1452 xxx.fetch_external_args
1454 (** val set_result :
1455 Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
1456 List.list -> __ -> state -> state Errors.res **)
1457 let rec set_result uns_pars xxx =
1460 (** val call_args_for_main :
1461 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1462 let rec call_args_for_main uns_pars xxx =
1463 xxx.call_args_for_main
1465 (** val call_dest_for_main :
1466 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1467 let rec call_dest_for_main uns_pars xxx =
1468 xxx.call_dest_for_main
1470 (** val read_result :
1471 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1472 List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
1473 ByteValues.beval List.list Errors.res **)
1474 let rec read_result uns_pars xxx =
1477 (** val eval_ext_seq :
1478 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1479 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res **)
1480 let rec eval_ext_seq uns_pars xxx =
1484 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1485 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
1486 ByteValues.program_counter) Types.prod Errors.res **)
1487 let rec pop_frame uns_pars xxx =
1490 (** val sem_unserialized_params_inv_rect_Type4 :
1491 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1492 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1493 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1494 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1495 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1496 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1497 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1498 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1499 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1500 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1501 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1502 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1503 (AST.external_function -> state -> __ -> Values.val0 List.list
1504 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1505 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1506 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1507 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1508 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1509 state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1511 let sem_unserialized_params_inv_rect_Type4 x1 hterm h1 =
1512 let hcut = sem_unserialized_params_rect_Type4 x1 h1 hterm in hcut __
1514 (** val sem_unserialized_params_inv_rect_Type3 :
1515 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1516 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1517 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1518 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1519 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1520 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1521 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1522 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1523 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1524 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1525 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1526 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1527 (AST.external_function -> state -> __ -> Values.val0 List.list
1528 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1529 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1530 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1531 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1532 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1533 state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1535 let sem_unserialized_params_inv_rect_Type3 x1 hterm h1 =
1536 let hcut = sem_unserialized_params_rect_Type3 x1 h1 hterm in hcut __
1538 (** val sem_unserialized_params_inv_rect_Type2 :
1539 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1540 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1541 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1542 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1543 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1544 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1545 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1546 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1547 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1548 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1549 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1550 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1551 (AST.external_function -> state -> __ -> Values.val0 List.list
1552 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1553 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1554 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1555 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1556 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1557 state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1559 let sem_unserialized_params_inv_rect_Type2 x1 hterm h1 =
1560 let hcut = sem_unserialized_params_rect_Type2 x1 h1 hterm in hcut __
1562 (** val sem_unserialized_params_inv_rect_Type1 :
1563 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1564 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1565 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1566 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1567 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1568 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1569 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1570 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1571 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1572 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1573 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1574 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1575 (AST.external_function -> state -> __ -> Values.val0 List.list
1576 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1577 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1578 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1579 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1580 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1581 state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1583 let sem_unserialized_params_inv_rect_Type1 x1 hterm h1 =
1584 let hcut = sem_unserialized_params_rect_Type1 x1 h1 hterm in hcut __
1586 (** val sem_unserialized_params_inv_rect_Type0 :
1587 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1588 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1589 (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1590 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1591 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1592 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1593 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1594 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1595 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1596 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1597 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1598 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1599 (AST.external_function -> state -> __ -> Values.val0 List.list
1600 Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1601 -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1602 -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1603 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1604 Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1605 state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1607 let sem_unserialized_params_inv_rect_Type0 x1 hterm h1 =
1608 let hcut = sem_unserialized_params_rect_Type0 x1 h1 hterm in hcut __
1610 (** val sem_unserialized_params_jmdiscr :
1611 Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
1612 sem_unserialized_params -> __ **)
1613 let sem_unserialized_params_jmdiscr a1 x y =
1614 Logic.eq_rect_Type2 x
1615 (let { st_pars = a0; acca_store_ = a10; acca_retrieve_ = a20;
1616 acca_arg_retrieve_ = a3; accb_store_ = a4; accb_retrieve_ = a5;
1617 accb_arg_retrieve_ = a6; dpl_store_ = a7; dpl_retrieve_ = a8;
1618 dpl_arg_retrieve_ = a9; dph_store_ = a100; dph_retrieve_ = a11;
1619 dph_arg_retrieve_ = a12; snd_arg_retrieve_ = a13; pair_reg_move_ =
1620 a14; save_frame = a15; setup_call = a16; fetch_external_args = a17;
1621 set_result = a18; call_args_for_main = a19; call_dest_for_main = a200;
1622 read_result = a21; eval_ext_seq = a22; pop_frame = a23 } = x
1624 Obj.magic (fun _ dH ->
1625 dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __
1628 (** val helper_def_retrieve :
1629 (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ ->
1630 'a1 -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
1631 sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res **)
1632 let helper_def_retrieve f up p st =
1633 Obj.magic f up __ p st.regs
1635 (** val helper_def_store :
1636 (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
1637 ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
1638 'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
1640 let helper_def_store f up p x v st =
1642 (Monad.m_bind0 (Monad.max_def Errors.res0)
1643 (Obj.magic f up __ p x v st.regs) (fun r ->
1644 Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st)))
1646 (** val acca_retrieve :
1647 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1648 -> ByteValues.beval Errors.res **)
1649 let acca_retrieve up p x x0 =
1650 helper_def_retrieve (fun x1 _ -> acca_retrieve_ x1) up p x x0
1652 (** val acca_store :
1653 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1654 ByteValues.beval -> state -> state Errors.res **)
1655 let acca_store up p x x0 x1 =
1656 helper_def_store (fun x2 _ -> acca_store_ x2) up p x x0 x1
1658 (** val acca_arg_retrieve :
1659 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1660 -> ByteValues.beval Errors.res **)
1661 let acca_arg_retrieve up p x x0 =
1662 helper_def_retrieve (fun x1 _ -> acca_arg_retrieve_ x1) up p x x0
1664 (** val accb_store :
1665 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1666 ByteValues.beval -> state -> state Errors.res **)
1667 let accb_store up p x x0 x1 =
1668 helper_def_store (fun x2 _ -> accb_store_ x2) up p x x0 x1
1670 (** val accb_retrieve :
1671 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1672 -> ByteValues.beval Errors.res **)
1673 let accb_retrieve up p x x0 =
1674 helper_def_retrieve (fun x1 _ -> accb_retrieve_ x1) up p x x0
1676 (** val accb_arg_retrieve :
1677 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1678 -> ByteValues.beval Errors.res **)
1679 let accb_arg_retrieve up p x x0 =
1680 helper_def_retrieve (fun x1 _ -> accb_arg_retrieve_ x1) up p x x0
1683 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1684 ByteValues.beval -> state -> state Errors.res **)
1685 let dpl_store up p x x0 x1 =
1686 helper_def_store (fun x2 _ -> dpl_store_ x2) up p x x0 x1
1688 (** val dpl_retrieve :
1689 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1690 -> ByteValues.beval Errors.res **)
1691 let dpl_retrieve up p x x0 =
1692 helper_def_retrieve (fun x1 _ -> dpl_retrieve_ x1) up p x x0
1694 (** val dpl_arg_retrieve :
1695 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1696 -> ByteValues.beval Errors.res **)
1697 let dpl_arg_retrieve up p x x0 =
1698 helper_def_retrieve (fun x1 _ -> dpl_arg_retrieve_ x1) up p x x0
1701 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1702 ByteValues.beval -> state -> state Errors.res **)
1703 let dph_store up p x x0 x1 =
1704 helper_def_store (fun x2 _ -> dph_store_ x2) up p x x0 x1
1706 (** val dph_retrieve :
1707 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1708 -> ByteValues.beval Errors.res **)
1709 let dph_retrieve up p x x0 =
1710 helper_def_retrieve (fun x1 _ -> dph_retrieve_ x1) up p x x0
1712 (** val dph_arg_retrieve :
1713 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1714 -> ByteValues.beval Errors.res **)
1715 let dph_arg_retrieve up p x x0 =
1716 helper_def_retrieve (fun x1 _ -> dph_arg_retrieve_ x1) up p x x0
1718 (** val snd_arg_retrieve :
1719 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1720 -> ByteValues.beval Errors.res **)
1721 let snd_arg_retrieve up p x x0 =
1722 helper_def_retrieve (fun x1 _ -> snd_arg_retrieve_ x1) up p x x0
1724 (** val pair_reg_move :
1725 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1727 let pair_reg_move up p st pm =
1728 Monad.m_bind0 (Monad.max_def Errors.res0)
1729 (Obj.magic (p.pair_reg_move_ st.regs pm)) (fun r ->
1730 Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st))
1733 sem_state_params -> state -> ByteValues.beval -> state Errors.res **)
1736 (Monad.m_bind0 (Monad.max_def Errors.res0)
1737 (Obj.magic (is_push st.istack v)) (fun is ->
1738 Monad.m_return0 (Monad.max_def Errors.res0) (set_istack p is st)))
1741 sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1745 (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (is_pop st.istack))
1747 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv;
1748 Types.snd = (set_istack p is st) }))
1751 sem_state_params -> state -> ByteValues.program_counter -> state
1753 let push_ra p st l =
1754 let { Types.fst = addrl; Types.snd = addrh } =
1755 ByteValues.beval_pair_of_pc l
1758 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (push p st addrl))
1759 (fun st' -> Obj.magic (push p st' addrh)))
1762 sem_state_params -> state -> (state, ByteValues.program_counter)
1763 Types.prod Errors.res **)
1766 (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st))
1768 Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st'))
1770 Monad.m_bind0 (Monad.max_def Errors.res0)
1772 (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh,
1773 List.Nil)))))) (fun pr ->
1774 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st'';
1775 Types.snd = pr }))))
1777 type serialized_params = { spp : Joint.params;
1778 msu_pars : Joint.joint_closed_internal_function
1779 sem_unserialized_params;
1780 offset_of_point : (__ -> Positive.pos);
1781 point_of_offset : (Positive.pos -> __) }
1783 (** val serialized_params_rect_Type4 :
1784 (Joint.params -> Joint.joint_closed_internal_function
1785 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1786 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1787 let rec serialized_params_rect_Type4 h_mk_serialized_params x_24799 =
1788 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1789 point_of_offset = point_of_offset0 } = x_24799
1791 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1794 (** val serialized_params_rect_Type5 :
1795 (Joint.params -> Joint.joint_closed_internal_function
1796 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1797 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1798 let rec serialized_params_rect_Type5 h_mk_serialized_params x_24801 =
1799 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1800 point_of_offset = point_of_offset0 } = x_24801
1802 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1805 (** val serialized_params_rect_Type3 :
1806 (Joint.params -> Joint.joint_closed_internal_function
1807 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1808 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1809 let rec serialized_params_rect_Type3 h_mk_serialized_params x_24803 =
1810 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1811 point_of_offset = point_of_offset0 } = x_24803
1813 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1816 (** val serialized_params_rect_Type2 :
1817 (Joint.params -> Joint.joint_closed_internal_function
1818 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1819 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1820 let rec serialized_params_rect_Type2 h_mk_serialized_params x_24805 =
1821 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1822 point_of_offset = point_of_offset0 } = x_24805
1824 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1827 (** val serialized_params_rect_Type1 :
1828 (Joint.params -> Joint.joint_closed_internal_function
1829 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1830 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1831 let rec serialized_params_rect_Type1 h_mk_serialized_params x_24807 =
1832 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1833 point_of_offset = point_of_offset0 } = x_24807
1835 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1838 (** val serialized_params_rect_Type0 :
1839 (Joint.params -> Joint.joint_closed_internal_function
1840 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1841 -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1842 let rec serialized_params_rect_Type0 h_mk_serialized_params x_24809 =
1843 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1844 point_of_offset = point_of_offset0 } = x_24809
1846 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1849 (** val spp : serialized_params -> Joint.params **)
1854 serialized_params -> Joint.joint_closed_internal_function
1855 sem_unserialized_params **)
1856 let rec msu_pars xxx =
1859 (** val offset_of_point : serialized_params -> __ -> Positive.pos **)
1860 let rec offset_of_point xxx =
1863 (** val point_of_offset : serialized_params -> Positive.pos -> __ **)
1864 let rec point_of_offset xxx =
1867 (** val serialized_params_inv_rect_Type4 :
1868 serialized_params -> (Joint.params ->
1869 Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1870 Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1871 let serialized_params_inv_rect_Type4 hterm h1 =
1872 let hcut = serialized_params_rect_Type4 h1 hterm in hcut __
1874 (** val serialized_params_inv_rect_Type3 :
1875 serialized_params -> (Joint.params ->
1876 Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1877 Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1878 let serialized_params_inv_rect_Type3 hterm h1 =
1879 let hcut = serialized_params_rect_Type3 h1 hterm in hcut __
1881 (** val serialized_params_inv_rect_Type2 :
1882 serialized_params -> (Joint.params ->
1883 Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1884 Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1885 let serialized_params_inv_rect_Type2 hterm h1 =
1886 let hcut = serialized_params_rect_Type2 h1 hterm in hcut __
1888 (** val serialized_params_inv_rect_Type1 :
1889 serialized_params -> (Joint.params ->
1890 Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1891 Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1892 let serialized_params_inv_rect_Type1 hterm h1 =
1893 let hcut = serialized_params_rect_Type1 h1 hterm in hcut __
1895 (** val serialized_params_inv_rect_Type0 :
1896 serialized_params -> (Joint.params ->
1897 Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1898 Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1899 let serialized_params_inv_rect_Type0 hterm h1 =
1900 let hcut = serialized_params_rect_Type0 h1 hterm in hcut __
1902 (** val serialized_params_jmdiscr :
1903 serialized_params -> serialized_params -> __ **)
1904 let serialized_params_jmdiscr x y =
1905 Logic.eq_rect_Type2 x
1906 (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset =
1909 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1911 (** val spp__o__stmt_pars : serialized_params -> Joint.stmt_params **)
1912 let spp__o__stmt_pars x0 =
1913 x0.spp.Joint.stmt_pars
1915 (** val spp__o__stmt_pars__o__uns_pars :
1916 serialized_params -> Joint.uns_params **)
1917 let spp__o__stmt_pars__o__uns_pars x0 =
1918 Joint.stmt_pars__o__uns_pars x0.spp
1920 (** val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1921 serialized_params -> Joint.unserialized_params **)
1922 let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
1923 Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp
1925 (** val msu_pars__o__st_pars : serialized_params -> sem_state_params **)
1926 let msu_pars__o__st_pars x0 =
1929 type sem_params = { spp' : serialized_params;
1930 pre_main_generator : (Joint.joint_program ->
1931 Joint.joint_closed_internal_function) }
1933 (** val sem_params_rect_Type4 :
1934 (serialized_params -> (Joint.joint_program ->
1935 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1936 let rec sem_params_rect_Type4 h_mk_sem_params x_24827 =
1937 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24827 in
1938 h_mk_sem_params spp'0 pre_main_generator0
1940 (** val sem_params_rect_Type5 :
1941 (serialized_params -> (Joint.joint_program ->
1942 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1943 let rec sem_params_rect_Type5 h_mk_sem_params x_24829 =
1944 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24829 in
1945 h_mk_sem_params spp'0 pre_main_generator0
1947 (** val sem_params_rect_Type3 :
1948 (serialized_params -> (Joint.joint_program ->
1949 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1950 let rec sem_params_rect_Type3 h_mk_sem_params x_24831 =
1951 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24831 in
1952 h_mk_sem_params spp'0 pre_main_generator0
1954 (** val sem_params_rect_Type2 :
1955 (serialized_params -> (Joint.joint_program ->
1956 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1957 let rec sem_params_rect_Type2 h_mk_sem_params x_24833 =
1958 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24833 in
1959 h_mk_sem_params spp'0 pre_main_generator0
1961 (** val sem_params_rect_Type1 :
1962 (serialized_params -> (Joint.joint_program ->
1963 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1964 let rec sem_params_rect_Type1 h_mk_sem_params x_24835 =
1965 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24835 in
1966 h_mk_sem_params spp'0 pre_main_generator0
1968 (** val sem_params_rect_Type0 :
1969 (serialized_params -> (Joint.joint_program ->
1970 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1971 let rec sem_params_rect_Type0 h_mk_sem_params x_24837 =
1972 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24837 in
1973 h_mk_sem_params spp'0 pre_main_generator0
1975 (** val spp' : sem_params -> serialized_params **)
1979 (** val pre_main_generator :
1980 sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function **)
1981 let rec pre_main_generator xxx =
1982 xxx.pre_main_generator
1984 (** val sem_params_inv_rect_Type4 :
1985 sem_params -> (serialized_params -> (Joint.joint_program ->
1986 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1987 let sem_params_inv_rect_Type4 hterm h1 =
1988 let hcut = sem_params_rect_Type4 h1 hterm in hcut __
1990 (** val sem_params_inv_rect_Type3 :
1991 sem_params -> (serialized_params -> (Joint.joint_program ->
1992 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1993 let sem_params_inv_rect_Type3 hterm h1 =
1994 let hcut = sem_params_rect_Type3 h1 hterm in hcut __
1996 (** val sem_params_inv_rect_Type2 :
1997 sem_params -> (serialized_params -> (Joint.joint_program ->
1998 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1999 let sem_params_inv_rect_Type2 hterm h1 =
2000 let hcut = sem_params_rect_Type2 h1 hterm in hcut __
2002 (** val sem_params_inv_rect_Type1 :
2003 sem_params -> (serialized_params -> (Joint.joint_program ->
2004 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
2005 let sem_params_inv_rect_Type1 hterm h1 =
2006 let hcut = sem_params_rect_Type1 h1 hterm in hcut __
2008 (** val sem_params_inv_rect_Type0 :
2009 sem_params -> (serialized_params -> (Joint.joint_program ->
2010 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
2011 let sem_params_inv_rect_Type0 hterm h1 =
2012 let hcut = sem_params_rect_Type0 h1 hterm in hcut __
2014 (** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
2015 let sem_params_jmdiscr x y =
2016 Logic.eq_rect_Type2 x
2017 (let { spp' = a0; pre_main_generator = a1 } = x in
2018 Obj.magic (fun _ dH -> dH __ __)) y
2020 (** val spp'__o__msu_pars :
2021 sem_params -> Joint.joint_closed_internal_function
2022 sem_unserialized_params **)
2023 let spp'__o__msu_pars x0 =
2026 (** val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params **)
2027 let spp'__o__msu_pars__o__st_pars x0 =
2028 msu_pars__o__st_pars x0.spp'
2030 (** val spp'__o__spp : sem_params -> Joint.params **)
2031 let spp'__o__spp x0 =
2034 (** val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
2035 let spp'__o__spp__o__stmt_pars x0 =
2036 spp__o__stmt_pars x0.spp'
2038 (** val spp'__o__spp__o__stmt_pars__o__uns_pars :
2039 sem_params -> Joint.uns_params **)
2040 let spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
2041 spp__o__stmt_pars__o__uns_pars x0.spp'
2043 (** val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
2044 sem_params -> Joint.unserialized_params **)
2045 let spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2046 spp__o__stmt_pars__o__uns_pars__o__u_pars x0.spp'
2048 (** val pc_of_point :
2049 sem_params -> Pointers.block Types.sig0 -> __ ->
2050 ByteValues.program_counter **)
2051 let pc_of_point p bl pt =
2052 { ByteValues.pc_block = bl; ByteValues.pc_offset =
2053 (p.spp'.offset_of_point pt) }
2055 (** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **)
2056 let point_of_pc p ptr =
2057 p.spp'.point_of_offset ptr.ByteValues.pc_offset
2059 (** val fetch_statement :
2060 sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
2061 -> ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
2062 Joint.joint_statement) Types.prod Errors.res **)
2063 let fetch_statement p globals ge0 ptr =
2065 (Monad.m_bind2 (Monad.max_def Errors.res0)
2067 (fetch_internal_function globals ge0 ptr.ByteValues.pc_block))
2069 let pt = point_of_pc p ptr in
2070 Monad.m_bind0 (Monad.max_def Errors.res0)
2073 (Errors.msg ErrorMessages.ProgramCounterOutOfCode)
2074 ((spp'__o__spp p).Joint.stmt_at globals
2075 (Types.pi1 fn).Joint.joint_if_code pt))) (fun stmt ->
2076 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
2077 { Types.fst = id; Types.snd = fn }; Types.snd = stmt })))
2079 (** val pc_of_label :
2080 sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
2081 Graphs.label -> ByteValues.program_counter Errors.res **)
2082 let pc_of_label p globals ge0 bl lbl =
2084 (Monad.m_bind2 (Monad.max_def Errors.res0)
2085 (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn ->
2086 Monad.m_bind0 (Monad.max_def Errors.res0)
2088 (Errors.opt_to_res (List.Cons ((Errors.MSG
2089 ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
2090 (PreIdentifiers.LabelTag, lbl)), List.Nil))))
2091 ((spp'__o__spp p).Joint.point_of_label globals
2092 (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt ->
2093 Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block =
2094 bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) })))
2097 sem_params -> ByteValues.program_counter -> __ ->
2098 ByteValues.program_counter **)
2099 let succ_pc p ptr nxt =
2100 let curr = point_of_pc p ptr in
2101 pc_of_point p ptr.ByteValues.pc_block
2102 ((spp'__o__spp p).Joint.point_of_succ curr nxt)
2105 sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
2106 state_pc Errors.res **)
2107 let goto p globals ge0 l st =
2109 (Monad.m_bind0 (Monad.max_def Errors.res0)
2110 (Obj.magic (pc_of_label p globals ge0 st.pc.ByteValues.pc_block l))
2112 Monad.m_return0 (Monad.max_def Errors.res0)
2113 (set_pc (spp'__o__msu_pars__o__st_pars p) newpc st)))
2115 (** val next : sem_params -> __ -> state_pc -> state_pc **)
2117 let newpc = succ_pc p st.pc l in
2118 set_pc (spp'__o__msu_pars__o__st_pars p) newpc st
2120 (** val next_of_call_pc :
2121 sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
2122 -> __ Errors.res **)
2123 let next_of_call_pc p globals ge0 pc0 =
2125 (Monad.m_bind2 (Monad.max_def Errors.res0)
2126 (Obj.magic (fetch_statement p globals ge0 pc0)) (fun id_fn stmt ->
2128 | Joint.Sequential (s, nxt) ->
2130 | Joint.COST_LABEL x ->
2131 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2132 ErrorMessages.NoSuccessor), List.Nil)))
2133 | Joint.CALL (x, x0, x1) ->
2134 Monad.m_return0 (Monad.max_def Errors.res0) nxt
2135 | Joint.COND (x, x0) ->
2136 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2137 ErrorMessages.NoSuccessor), List.Nil)))
2138 | Joint.Step_seq x ->
2139 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2140 ErrorMessages.NoSuccessor), List.Nil))))
2142 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2143 ErrorMessages.NoSuccessor), List.Nil)))
2144 | Joint.FCOND (x0, x1, x2) ->
2145 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2146 ErrorMessages.NoSuccessor), List.Nil)))))
2148 (** val eval_seq_no_pc :
2149 sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
2150 -> state -> state Errors.res **)
2151 let eval_seq_no_pc p globals ge0 curr_id seq st =
2153 | Joint.COMMENT x ->
2154 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2155 | Joint.MOVE dst_src ->
2157 (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2158 p.spp'.msu_pars st dst_src)
2161 (Monad.m_bind2 (Monad.max_def Errors.res0)
2162 (Obj.magic (pop (spp'__o__msu_pars__o__st_pars p) st)) (fun v st' ->
2164 (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2165 (spp'__o__msu_pars p) dst v st')))
2168 (Monad.m_bind0 (Monad.max_def Errors.res0)
2171 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2172 p.spp'.msu_pars st src)) (fun v ->
2173 Obj.magic (push (spp'__o__msu_pars__o__st_pars p) st v)))
2174 | Joint.ADDRESS (id, off, ldest, hdest) ->
2175 let addr_block = Option.opt_safe (Globalenvs.find_symbol ge0.ge id) in
2176 let { Types.fst = laddr; Types.snd = haddr } =
2177 ByteValues.beval_pair_of_pointer { Pointers.pblock = addr_block;
2178 Pointers.poff = off }
2181 (Monad.m_bind0 (Monad.max_def Errors.res0)
2183 (dpl_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2184 p.spp'.msu_pars ldest laddr st)) (fun st' ->
2186 (dph_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2187 p.spp'.msu_pars hdest haddr st')))
2188 | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) ->
2190 (Monad.m_bind0 (Monad.max_def Errors.res0)
2193 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2194 p.spp'.msu_pars st sacc_a_reg)) (fun v1 ->
2195 Monad.m_bind0 (Monad.max_def Errors.res0)
2198 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2199 p.spp'.msu_pars st sacc_b_reg)) (fun v2 ->
2200 Monad.m_bind2 (Monad.max_def Errors.res0)
2201 (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' ->
2202 Monad.m_bind0 (Monad.max_def Errors.res0)
2205 (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2206 p.spp'.msu_pars dacc_a_reg v1' st)) (fun st' ->
2209 (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2210 p.spp'.msu_pars dacc_b_reg v2' st'))))))
2211 | Joint.OP1 (op, dacc_a, sacc_a) ->
2213 (Monad.m_bind0 (Monad.max_def Errors.res0)
2215 (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2216 p.spp'.msu_pars st sacc_a)) (fun v ->
2217 Monad.m_bind0 (Monad.max_def Errors.res0)
2218 (Obj.magic (BackEndOps.be_op1 op v)) (fun v' ->
2221 (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2222 p.spp'.msu_pars dacc_a v' st))))
2223 | Joint.OP2 (op, dacc_a, sacc_a, src) ->
2225 (Monad.m_bind0 (Monad.max_def Errors.res0)
2228 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2229 p.spp'.msu_pars st sacc_a)) (fun v1 ->
2230 Monad.m_bind0 (Monad.max_def Errors.res0)
2233 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2234 p.spp'.msu_pars st src)) (fun v2 ->
2235 Monad.m_bind2 (Monad.max_def Errors.res0)
2236 (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
2238 Monad.m_bind0 (Monad.max_def Errors.res0)
2241 (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2242 p.spp'.msu_pars dacc_a v' st)) (fun st' ->
2243 Monad.m_return0 (Monad.max_def Errors.res0)
2244 (set_carry p.spp'.msu_pars.st_pars carry0 st'))))))
2245 | Joint.CLEAR_CARRY ->
2247 (Monad.m_return0 (Monad.max_def Errors.res0)
2248 (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2250 | Joint.SET_CARRY ->
2252 (Monad.m_return0 (Monad.max_def Errors.res0)
2253 (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2255 | Joint.LOAD (dst, addrl, addrh) ->
2257 (Monad.m_bind0 (Monad.max_def Errors.res0)
2260 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2261 p.spp'.msu_pars st addrh)) (fun vaddrh ->
2262 Monad.m_bind0 (Monad.max_def Errors.res0)
2265 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2266 p.spp'.msu_pars st addrl)) (fun vaddrl ->
2267 Monad.m_bind0 (Monad.max_def Errors.res0)
2269 (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2270 vaddrh })) (fun vaddr ->
2271 Monad.m_bind0 (Monad.max_def Errors.res0)
2273 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
2274 (GenMem.beloadv st.m vaddr))) (fun v ->
2277 (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2278 p.spp'.msu_pars dst v st))))))
2279 | Joint.STORE (addrl, addrh, src) ->
2281 (Monad.m_bind0 (Monad.max_def Errors.res0)
2284 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2285 p.spp'.msu_pars st addrh)) (fun vaddrh ->
2286 Monad.m_bind0 (Monad.max_def Errors.res0)
2289 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2290 p.spp'.msu_pars st addrl)) (fun vaddrl ->
2291 Monad.m_bind0 (Monad.max_def Errors.res0)
2293 (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2294 vaddrh })) (fun vaddr ->
2295 Monad.m_bind0 (Monad.max_def Errors.res0)
2298 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2299 p.spp'.msu_pars st src)) (fun v ->
2300 Monad.m_bind0 (Monad.max_def Errors.res0)
2302 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
2303 (GenMem.bestorev st.m vaddr v))) (fun m' ->
2304 Monad.m_return0 (Monad.max_def Errors.res0)
2305 (set_m (spp'__o__msu_pars__o__st_pars p) m' st)))))))
2306 | Joint.Extension_seq c ->
2307 p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
2309 (** val block_of_call :
2310 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2311 (__, __) Types.prod) Types.sum -> state -> __ **)
2312 let block_of_call p globals ge0 f st =
2313 Monad.m_bind0 (Monad.max_def Errors.res0)
2317 (Errors.opt_to_res (List.Cons ((Errors.MSG
2318 ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
2319 (PreIdentifiers.SymbolTag, id)), List.Nil))))
2320 (Globalenvs.find_symbol ge0.ge id))
2322 Monad.m_bind0 (Monad.max_def Errors.res0)
2325 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2326 p.spp'.msu_pars st addr.Types.fst)) (fun addr_l ->
2327 Monad.m_bind0 (Monad.max_def Errors.res0)
2330 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2331 p.spp'.msu_pars st addr.Types.snd)) (fun addr_h ->
2332 Monad.m_bind0 (Monad.max_def Errors.res0)
2334 (ByteValues.pointer_of_bevals (List.Cons (addr_l, (List.Cons
2335 (addr_h, List.Nil)))))) (fun ptr ->
2336 match BitVector.eq_bv Pointers.offset_size
2337 (BitVector.zero Pointers.offset_size)
2338 (Pointers.offv ptr.Pointers.poff) with
2340 Monad.m_return0 (Monad.max_def Errors.res0)
2343 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2344 ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
2345 ErrorMessages.BadPointer), List.Nil))))))))) (fun bl ->
2347 (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2348 (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil))))
2349 (code_block_of_block bl)))
2351 (** val eval_external_call :
2352 sem_params -> AST.external_function -> __ -> __ -> state -> __ **)
2353 let eval_external_call p fn args dest st =
2354 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2357 ((spp'__o__msu_pars p).fetch_external_args fn st args)
2359 Obj.magic x) (fun params ->
2360 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2363 (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)
2365 Obj.magic x) (fun evargs ->
2366 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2368 (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
2371 ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil)
2374 (IOMonad.err_to_io ((spp'__o__msu_pars p).set_result vs dest st)))))
2376 (** val increment_stack_usage :
2377 sem_state_params -> Nat.nat -> state -> state **)
2378 let increment_stack_usage p n st =
2379 { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2380 st.regs; m = st.m; stack_usage = (Nat.plus n st.stack_usage) }
2382 (** val decrement_stack_usage :
2383 sem_state_params -> Nat.nat -> state -> state **)
2384 let decrement_stack_usage p n st =
2385 { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2386 st.regs; m = st.m; stack_usage = (Nat.minus st.stack_usage n) }
2388 (** val eval_internal_call :
2389 sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2390 Joint.joint_internal_function -> __ -> state -> __ **)
2391 let eval_internal_call p globals ge0 i fn args st =
2392 Monad.m_bind0 (Monad.max_def Errors.res0)
2394 (Errors.opt_to_res (List.Cons ((Errors.MSG
2395 ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2396 (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i)))
2398 Monad.m_bind0 (Monad.max_def Errors.res0)
2400 (p.spp'.msu_pars.setup_call stack_size fn.Joint.joint_if_params args
2402 Monad.m_return0 (Monad.max_def Errors.res0)
2403 (increment_stack_usage p.spp'.msu_pars.st_pars stack_size st')))
2405 (** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **)
2406 let is_inl = function
2407 | Types.Inl x0 -> Bool.True
2408 | Types.Inr x0 -> Bool.False
2411 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2412 (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __ **)
2413 let eval_call p globals ge0 f args dest nxt st =
2414 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2417 (Obj.magic (block_of_call p globals ge0 f st.st_no_pc))
2419 Obj.magic x) (fun bl ->
2420 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2421 (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
2422 Obj.magic x) (fun i fd ->
2424 | AST.Internal ifd ->
2428 (Monad.m_bind0 (Monad.max_def Errors.res0)
2430 (p.spp'.msu_pars.save_frame
2432 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) f)
2433 dest st)) (fun st' ->
2434 Monad.m_bind0 (Monad.max_def Errors.res0)
2435 (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2438 pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2440 Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2441 st''; pc = pc0; last_pop = st.last_pop })))))
2442 | AST.External efd ->
2443 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2444 (eval_external_call p efd args dest st.st_no_pc) (fun st' ->
2445 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { st_no_pc = st';
2446 pc = (succ_pc p st.pc nxt); last_pop = st.last_pop })))
2448 (** val eval_statement_no_pc :
2449 sem_params -> AST.ident List.list -> genv -> AST.ident ->
2450 Joint.joint_statement -> state -> state Errors.res **)
2451 let eval_statement_no_pc p globals ge0 curr_id s st =
2453 | Joint.Sequential (s0, next0) ->
2455 | Joint.COST_LABEL x ->
2456 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2457 | Joint.CALL (x, x0, x1) ->
2458 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2459 | Joint.COND (x, x0) ->
2460 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2461 | Joint.Step_seq s1 -> eval_seq_no_pc p globals ge0 curr_id s1 st)
2463 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2464 | Joint.FCOND (x0, x1, x2) ->
2465 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2467 (** val eval_return :
2468 sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2469 __ -> state -> __ **)
2470 let eval_return p globals ge0 curr_id curr_ret st =
2471 Monad.m_bind0 (Monad.max_def Errors.res0)
2473 (Errors.opt_to_res (List.Cons ((Errors.MSG
2474 ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2475 (PreIdentifiers.SymbolTag, curr_id)), List.Nil))))
2476 (ge0.stack_sizes curr_id))) (fun stack_size ->
2477 Monad.m_bind2 (Monad.max_def Errors.res0)
2478 (Obj.magic (p.spp'.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
2480 Monad.m_bind0 (Monad.max_def Errors.res0)
2481 (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt ->
2483 set_last_pop p.spp'.msu_pars.st_pars
2484 (decrement_stack_usage p.spp'.msu_pars.st_pars stack_size st')
2487 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st''))))
2489 (** val eval_tailcall :
2490 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2491 (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __
2492 -> state_pc -> __ **)
2493 let eval_tailcall p globals ge0 f args curr_f curr_ret st =
2494 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2497 (Obj.magic (block_of_call p globals ge0 f st.st_no_pc))
2499 Obj.magic x) (fun bl ->
2500 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2501 (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
2502 Obj.magic x) (fun i fd ->
2504 | AST.Internal ifd ->
2508 (Monad.m_bind0 (Monad.max_def Errors.res0)
2510 (Errors.opt_to_res (List.Cons ((Errors.MSG
2511 ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2512 (PreIdentifiers.SymbolTag, curr_f)), List.Nil))))
2513 (ge0.stack_sizes curr_f))) (fun stack_size ->
2515 decrement_stack_usage (spp'__o__msu_pars__o__st_pars p)
2516 stack_size st.st_no_pc
2518 Monad.m_bind0 (Monad.max_def Errors.res0)
2519 (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2522 pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2524 Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2525 st''; pc = pc0; last_pop = st.last_pop })))))
2526 | AST.External efd ->
2527 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2528 (eval_external_call p efd args curr_ret st.st_no_pc) (fun st' ->
2532 (eval_return p globals ge0 curr_f curr_ret st.st_no_pc))))))
2534 (** val eval_statement_advance :
2535 sem_params -> AST.ident List.list -> genv -> AST.ident ->
2536 Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
2537 -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **)
2538 let eval_statement_advance p g ge0 curr_id curr_fn s st =
2540 | Joint.Sequential (s0, nxt) ->
2542 | Joint.COST_LABEL x ->
2544 (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
2545 | Joint.CALL (f, args, dest) ->
2546 Obj.magic (eval_call p g ge0 f args dest nxt st)
2547 | Joint.COND (a, l) ->
2550 (Monad.m_bind0 (Monad.max_def Errors.res0)
2553 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2554 p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2555 Monad.m_bind0 (Monad.max_def Errors.res0)
2556 (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2558 | Bool.True -> Obj.magic (goto p g ge0 l st)
2560 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
2561 | Joint.Step_seq x ->
2563 (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st)))
2565 let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
2567 | Joint.GOTO l -> IOMonad.err_to_io (goto p g ge0 l st)
2570 (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
2571 | Joint.TAILCALL (f, args) ->
2572 Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
2573 | Joint.FCOND (a, lbltrue, lblfalse) ->
2576 (Monad.m_bind0 (Monad.max_def Errors.res0)
2579 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2580 p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2581 Monad.m_bind0 (Monad.max_def Errors.res0)
2582 (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2584 | Bool.True -> Obj.magic (goto p g ge0 lbltrue st)
2585 | Bool.False -> Obj.magic (goto p g ge0 lblfalse st)))))
2587 (** val eval_state :
2588 sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
2589 IO.io_in, state_pc) IOMonad.iO **)
2590 let eval_state p globals ge0 st =
2592 (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
2593 (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in
2594 Obj.magic x) (fun id fn s ->
2595 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2598 (eval_statement_no_pc p globals ge0 id s st.st_no_pc)
2600 Obj.magic x) (fun st' ->
2601 let st'' = set_no_pc (spp'__o__msu_pars__o__st_pars p) st' st in
2602 Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))