source: extracted/joint_semantics.ml @ 2951

Last change on this file since 2951 was 2951, checked in by sacerdot, 7 years ago

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 112.2 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Exp
40
41open Arithmetic
42
43open Vector
44
45open Div_and_mod
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Extranat
54
55open Integers
56
57open AST
58
59open ErrorMessages
60
61open Option
62
63open Setoids
64
65open Monad
66
67open Jmeq
68
69open Russell
70
71open Positive
72
73open PreIdentifiers
74
75open Bool
76
77open Relations
78
79open Nat
80
81open List
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Types
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open Events
100
101open IOMonad
102
103open IO
104
105open BEMem
106
107open String
108
109open Sets
110
111open Listb
112
113open LabelledObjects
114
115open BitVectorTrie
116
117open Graphs
118
119open I8051
120
121open Order
122
123open Registers
124
125open BackEndOps
126
127open Joint
128
129open I8051bis
130
131open ExtraGlobalenvs
132
133type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
134                     stack_sizes : (AST.ident -> Nat.nat Types.option);
135                     get_pc_from_label : (AST.ident -> Graphs.label ->
136                                         ByteValues.program_counter
137                                         Errors.res) }
138
139(** val genv_gen_rect_Type4 :
140    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
141    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
142    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
143let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_5376 =
144  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
145    get_pc_from_label0 } = x_5376
146  in
147  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
148
149(** val genv_gen_rect_Type5 :
150    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
151    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
152    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
153let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5378 =
154  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
155    get_pc_from_label0 } = x_5378
156  in
157  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
158
159(** val genv_gen_rect_Type3 :
160    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
161    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
162    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
163let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_5380 =
164  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
165    get_pc_from_label0 } = x_5380
166  in
167  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
168
169(** val genv_gen_rect_Type2 :
170    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
171    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
172    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
173let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_5382 =
174  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
175    get_pc_from_label0 } = x_5382
176  in
177  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
178
179(** val genv_gen_rect_Type1 :
180    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
181    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
182    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
183let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_5384 =
184  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
185    get_pc_from_label0 } = x_5384
186  in
187  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
188
189(** val genv_gen_rect_Type0 :
190    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
191    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
192    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
193let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_5386 =
194  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
195    get_pc_from_label0 } = x_5386
196  in
197  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
198
199(** val ge :
200    AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t **)
201let rec ge globals xxx =
202  xxx.ge
203
204(** val stack_sizes :
205    AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option **)
206let rec stack_sizes globals xxx =
207  xxx.stack_sizes
208
209(** val get_pc_from_label :
210    AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
211    ByteValues.program_counter Errors.res **)
212let rec get_pc_from_label globals xxx =
213  xxx.get_pc_from_label
214
215(** val genv_gen_inv_rect_Type4 :
216    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
217    -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
218    Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
219    'a2 **)
220let genv_gen_inv_rect_Type4 x2 hterm h1 =
221  let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __
222
223(** val genv_gen_inv_rect_Type3 :
224    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
225    -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
226    Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
227    'a2 **)
228let genv_gen_inv_rect_Type3 x2 hterm h1 =
229  let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __
230
231(** val genv_gen_inv_rect_Type2 :
232    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
233    -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
234    Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
235    'a2 **)
236let genv_gen_inv_rect_Type2 x2 hterm h1 =
237  let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __
238
239(** val genv_gen_inv_rect_Type1 :
240    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
241    -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
242    Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
243    'a2 **)
244let genv_gen_inv_rect_Type1 x2 hterm h1 =
245  let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __
246
247(** val genv_gen_inv_rect_Type0 :
248    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
249    -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
250    Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
251    'a2 **)
252let genv_gen_inv_rect_Type0 x2 hterm h1 =
253  let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __
254
255(** val genv_gen_discr :
256    AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
257let genv_gen_discr a2 x y =
258  Logic.eq_rect_Type2 x
259    (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
260    Obj.magic (fun _ dH -> dH __ __ __ __)) y
261
262(** val genv_gen_jmdiscr :
263    AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
264let genv_gen_jmdiscr a2 x y =
265  Logic.eq_rect_Type2 x
266    (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
267    Obj.magic (fun _ dH -> dH __ __ __ __)) y
268
269(** val dpi1__o__ge__o__inject :
270    AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
271    Globalenvs.genv_t Types.sig0 **)
272let dpi1__o__ge__o__inject x1 x4 =
273  x4.Types.dpi1.ge
274
275(** val eject__o__ge__o__inject :
276    AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
277    Globalenvs.genv_t Types.sig0 **)
278let eject__o__ge__o__inject x1 x4 =
279  (Types.pi1 x4).ge
280
281(** val ge__o__inject :
282    AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
283    Types.sig0 **)
284let ge__o__inject x1 x3 =
285  x3.ge
286
287(** val dpi1__o__ge :
288    AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
289    Globalenvs.genv_t **)
290let dpi1__o__ge x1 x3 =
291  x3.Types.dpi1.ge
292
293(** val eject__o__ge :
294    AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
295    Globalenvs.genv_t **)
296let eject__o__ge x1 x3 =
297  (Types.pi1 x3).ge
298
299type genv = Joint.joint_closed_internal_function genv_gen
300
301(** val dpi1__o__genv_to_genv_t__o__inject :
302    Joint.params -> AST.ident List.list -> (genv, 'a1) Types.dPair ->
303    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
304    Types.sig0 **)
305let dpi1__o__genv_to_genv_t__o__inject x0 x1 x4 =
306  x4.Types.dpi1.ge
307
308(** val eject__o__genv_to_genv_t__o__inject :
309    Joint.params -> AST.ident List.list -> genv Types.sig0 ->
310    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
311    Types.sig0 **)
312let eject__o__genv_to_genv_t__o__inject x0 x1 x4 =
313  (Types.pi1 x4).ge
314
315(** val genv_to_genv_t__o__inject :
316    Joint.params -> AST.ident List.list -> genv ->
317    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
318    Types.sig0 **)
319let genv_to_genv_t__o__inject x0 x1 x3 =
320  x3.ge
321
322(** val dpi1__o__genv_to_genv_t :
323    Joint.params -> AST.ident List.list -> (genv, 'a1) Types.dPair ->
324    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
325let dpi1__o__genv_to_genv_t x0 x1 x3 =
326  let p = x0 in let globals = x1 in let g = x3.Types.dpi1 in g.ge
327
328(** val eject__o__genv_to_genv_t :
329    Joint.params -> AST.ident List.list -> genv Types.sig0 ->
330    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
331let eject__o__genv_to_genv_t x0 x1 x3 =
332  let p = x0 in let globals = x1 in let g = Types.pi1 x3 in g.ge
333
334type sem_state_params = { empty_framesT : __;
335                          empty_regsT : (ByteValues.xpointer -> __);
336                          load_sp : (__ -> ByteValues.xpointer Errors.res);
337                          save_sp : (__ -> ByteValues.xpointer -> __) }
338
339(** val sem_state_params_rect_Type4 :
340    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
341    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
342    'a1) -> sem_state_params -> 'a1 **)
343let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_5406 =
344  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
345    load_sp0; save_sp = save_sp0 } = x_5406
346  in
347  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
348
349(** val sem_state_params_rect_Type5 :
350    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
351    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
352    'a1) -> sem_state_params -> 'a1 **)
353let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_5408 =
354  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
355    load_sp0; save_sp = save_sp0 } = x_5408
356  in
357  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
358
359(** val sem_state_params_rect_Type3 :
360    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
361    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
362    'a1) -> sem_state_params -> 'a1 **)
363let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_5410 =
364  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
365    load_sp0; save_sp = save_sp0 } = x_5410
366  in
367  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
368
369(** val sem_state_params_rect_Type2 :
370    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
371    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
372    'a1) -> sem_state_params -> 'a1 **)
373let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_5412 =
374  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
375    load_sp0; save_sp = save_sp0 } = x_5412
376  in
377  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
378
379(** val sem_state_params_rect_Type1 :
380    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
381    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
382    'a1) -> sem_state_params -> 'a1 **)
383let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_5414 =
384  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
385    load_sp0; save_sp = save_sp0 } = x_5414
386  in
387  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
388
389(** val sem_state_params_rect_Type0 :
390    (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
391    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
392    'a1) -> sem_state_params -> 'a1 **)
393let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_5416 =
394  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
395    load_sp0; save_sp = save_sp0 } = x_5416
396  in
397  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
398
399type framesT = __
400
401(** val empty_framesT : sem_state_params -> __ **)
402let rec empty_framesT xxx =
403  xxx.empty_framesT
404
405type regsT = __
406
407(** val empty_regsT : sem_state_params -> ByteValues.xpointer -> __ **)
408let rec empty_regsT xxx =
409  xxx.empty_regsT
410
411(** val load_sp :
412    sem_state_params -> __ -> ByteValues.xpointer Errors.res **)
413let rec load_sp xxx =
414  xxx.load_sp
415
416(** val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __ **)
417let rec save_sp xxx =
418  xxx.save_sp
419
420(** val sem_state_params_inv_rect_Type4 :
421    sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
422    -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
423    -> __ -> 'a1) -> 'a1 **)
424let sem_state_params_inv_rect_Type4 hterm h1 =
425  let hcut = sem_state_params_rect_Type4 h1 hterm in hcut __
426
427(** val sem_state_params_inv_rect_Type3 :
428    sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
429    -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
430    -> __ -> 'a1) -> 'a1 **)
431let sem_state_params_inv_rect_Type3 hterm h1 =
432  let hcut = sem_state_params_rect_Type3 h1 hterm in hcut __
433
434(** val sem_state_params_inv_rect_Type2 :
435    sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
436    -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
437    -> __ -> 'a1) -> 'a1 **)
438let sem_state_params_inv_rect_Type2 hterm h1 =
439  let hcut = sem_state_params_rect_Type2 h1 hterm in hcut __
440
441(** val sem_state_params_inv_rect_Type1 :
442    sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
443    -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
444    -> __ -> 'a1) -> 'a1 **)
445let sem_state_params_inv_rect_Type1 hterm h1 =
446  let hcut = sem_state_params_rect_Type1 h1 hterm in hcut __
447
448(** val sem_state_params_inv_rect_Type0 :
449    sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
450    -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
451    -> __ -> 'a1) -> 'a1 **)
452let sem_state_params_inv_rect_Type0 hterm h1 =
453  let hcut = sem_state_params_rect_Type0 h1 hterm in hcut __
454
455(** val sem_state_params_jmdiscr :
456    sem_state_params -> sem_state_params -> __ **)
457let sem_state_params_jmdiscr x y =
458  Logic.eq_rect_Type2 x
459    (let { empty_framesT = a1; empty_regsT = a3; load_sp = a4; save_sp =
460       a5 } = x
461     in
462    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
463
464type internal_stack =
465| Empty_is
466| One_is of ByteValues.beval
467| Both_is of ByteValues.beval * ByteValues.beval
468
469(** val internal_stack_rect_Type4 :
470    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
471    -> 'a1) -> internal_stack -> 'a1 **)
472let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
473| Empty_is -> h_empty_is
474| One_is x_5442 -> h_one_is x_5442
475| Both_is (x_5444, x_5443) -> h_both_is x_5444 x_5443
476
477(** val internal_stack_rect_Type5 :
478    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
479    -> 'a1) -> internal_stack -> 'a1 **)
480let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
481| Empty_is -> h_empty_is
482| One_is x_5449 -> h_one_is x_5449
483| Both_is (x_5451, x_5450) -> h_both_is x_5451 x_5450
484
485(** val internal_stack_rect_Type3 :
486    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
487    -> 'a1) -> internal_stack -> 'a1 **)
488let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
489| Empty_is -> h_empty_is
490| One_is x_5456 -> h_one_is x_5456
491| Both_is (x_5458, x_5457) -> h_both_is x_5458 x_5457
492
493(** val internal_stack_rect_Type2 :
494    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
495    -> 'a1) -> internal_stack -> 'a1 **)
496let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
497| Empty_is -> h_empty_is
498| One_is x_5463 -> h_one_is x_5463
499| Both_is (x_5465, x_5464) -> h_both_is x_5465 x_5464
500
501(** val internal_stack_rect_Type1 :
502    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
503    -> 'a1) -> internal_stack -> 'a1 **)
504let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
505| Empty_is -> h_empty_is
506| One_is x_5470 -> h_one_is x_5470
507| Both_is (x_5472, x_5471) -> h_both_is x_5472 x_5471
508
509(** val internal_stack_rect_Type0 :
510    'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
511    -> 'a1) -> internal_stack -> 'a1 **)
512let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
513| Empty_is -> h_empty_is
514| One_is x_5477 -> h_one_is x_5477
515| Both_is (x_5479, x_5478) -> h_both_is x_5479 x_5478
516
517(** val internal_stack_inv_rect_Type4 :
518    internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
519    (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
520let internal_stack_inv_rect_Type4 hterm h1 h2 h3 =
521  let hcut = internal_stack_rect_Type4 h1 h2 h3 hterm in hcut __
522
523(** val internal_stack_inv_rect_Type3 :
524    internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
525    (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
526let internal_stack_inv_rect_Type3 hterm h1 h2 h3 =
527  let hcut = internal_stack_rect_Type3 h1 h2 h3 hterm in hcut __
528
529(** val internal_stack_inv_rect_Type2 :
530    internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
531    (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
532let internal_stack_inv_rect_Type2 hterm h1 h2 h3 =
533  let hcut = internal_stack_rect_Type2 h1 h2 h3 hterm in hcut __
534
535(** val internal_stack_inv_rect_Type1 :
536    internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
537    (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
538let internal_stack_inv_rect_Type1 hterm h1 h2 h3 =
539  let hcut = internal_stack_rect_Type1 h1 h2 h3 hterm in hcut __
540
541(** val internal_stack_inv_rect_Type0 :
542    internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
543    (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
544let internal_stack_inv_rect_Type0 hterm h1 h2 h3 =
545  let hcut = internal_stack_rect_Type0 h1 h2 h3 hterm in hcut __
546
547(** val internal_stack_discr : internal_stack -> internal_stack -> __ **)
548let internal_stack_discr x y =
549  Logic.eq_rect_Type2 x
550    (match x with
551     | Empty_is -> Obj.magic (fun _ dH -> dH)
552     | One_is a0 -> Obj.magic (fun _ dH -> dH __)
553     | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
554
555(** val internal_stack_jmdiscr : internal_stack -> internal_stack -> __ **)
556let internal_stack_jmdiscr x y =
557  Logic.eq_rect_Type2 x
558    (match x with
559     | Empty_is -> Obj.magic (fun _ dH -> dH)
560     | One_is a0 -> Obj.magic (fun _ dH -> dH __)
561     | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
562
563(** val is_push :
564    internal_stack -> ByteValues.beval -> internal_stack Errors.res **)
565let is_push is bv =
566  match is with
567  | Empty_is ->
568    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (One_is bv))
569  | One_is bv' ->
570    Obj.magic
571      (Monad.m_return0 (Monad.max_def Errors.res0) (Both_is (bv', bv)))
572  | Both_is (x, x0) ->
573    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackFull),
574      List.Nil))
575
576(** val is_pop :
577    internal_stack -> (ByteValues.beval, internal_stack) Types.prod
578    Errors.res **)
579let is_pop = function
580| Empty_is ->
581  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackEmpty),
582    List.Nil))
583| One_is bv' ->
584  Obj.magic
585    (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
586      Types.snd = Empty_is })
587| Both_is (bv, bv') ->
588  Obj.magic
589    (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
590      Types.snd = (One_is bv) })
591
592type state = { st_frms : __ Types.option; istack : internal_stack;
593               carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
594               stack_usage : Nat.nat }
595
596(** val state_rect_Type4 :
597    sem_state_params -> (__ Types.option -> internal_stack ->
598    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
599let rec state_rect_Type4 semp h_mk_state x_5527 =
600  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
601    m = m0; stack_usage = stack_usage0 } = x_5527
602  in
603  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
604
605(** val state_rect_Type5 :
606    sem_state_params -> (__ Types.option -> internal_stack ->
607    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
608let rec state_rect_Type5 semp h_mk_state x_5529 =
609  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
610    m = m0; stack_usage = stack_usage0 } = x_5529
611  in
612  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
613
614(** val state_rect_Type3 :
615    sem_state_params -> (__ Types.option -> internal_stack ->
616    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
617let rec state_rect_Type3 semp h_mk_state x_5531 =
618  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
619    m = m0; stack_usage = stack_usage0 } = x_5531
620  in
621  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
622
623(** val state_rect_Type2 :
624    sem_state_params -> (__ Types.option -> internal_stack ->
625    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
626let rec state_rect_Type2 semp h_mk_state x_5533 =
627  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
628    m = m0; stack_usage = stack_usage0 } = x_5533
629  in
630  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
631
632(** val state_rect_Type1 :
633    sem_state_params -> (__ Types.option -> internal_stack ->
634    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
635let rec state_rect_Type1 semp h_mk_state x_5535 =
636  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
637    m = m0; stack_usage = stack_usage0 } = x_5535
638  in
639  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
640
641(** val state_rect_Type0 :
642    sem_state_params -> (__ Types.option -> internal_stack ->
643    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
644let rec state_rect_Type0 semp h_mk_state x_5537 =
645  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
646    m = m0; stack_usage = stack_usage0 } = x_5537
647  in
648  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
649
650(** val st_frms : sem_state_params -> state -> __ Types.option **)
651let rec st_frms semp xxx =
652  xxx.st_frms
653
654(** val istack : sem_state_params -> state -> internal_stack **)
655let rec istack semp xxx =
656  xxx.istack
657
658(** val carry : sem_state_params -> state -> ByteValues.bebit **)
659let rec carry semp xxx =
660  xxx.carry
661
662(** val regs : sem_state_params -> state -> __ **)
663let rec regs semp xxx =
664  xxx.regs
665
666(** val m : sem_state_params -> state -> BEMem.bemem **)
667let rec m semp xxx =
668  xxx.m
669
670(** val stack_usage : sem_state_params -> state -> Nat.nat **)
671let rec stack_usage semp xxx =
672  xxx.stack_usage
673
674(** val state_inv_rect_Type4 :
675    sem_state_params -> state -> (__ Types.option -> internal_stack ->
676    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
677let state_inv_rect_Type4 x1 hterm h1 =
678  let hcut = state_rect_Type4 x1 h1 hterm in hcut __
679
680(** val state_inv_rect_Type3 :
681    sem_state_params -> state -> (__ Types.option -> internal_stack ->
682    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
683let state_inv_rect_Type3 x1 hterm h1 =
684  let hcut = state_rect_Type3 x1 h1 hterm in hcut __
685
686(** val state_inv_rect_Type2 :
687    sem_state_params -> state -> (__ Types.option -> internal_stack ->
688    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
689let state_inv_rect_Type2 x1 hterm h1 =
690  let hcut = state_rect_Type2 x1 h1 hterm in hcut __
691
692(** val state_inv_rect_Type1 :
693    sem_state_params -> state -> (__ Types.option -> internal_stack ->
694    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
695let state_inv_rect_Type1 x1 hterm h1 =
696  let hcut = state_rect_Type1 x1 h1 hterm in hcut __
697
698(** val state_inv_rect_Type0 :
699    sem_state_params -> state -> (__ Types.option -> internal_stack ->
700    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
701let state_inv_rect_Type0 x1 hterm h1 =
702  let hcut = state_rect_Type0 x1 h1 hterm in hcut __
703
704(** val state_jmdiscr : sem_state_params -> state -> state -> __ **)
705let state_jmdiscr a1 x y =
706  Logic.eq_rect_Type2 x
707    (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4;
708       stack_usage = a5 } = x
709     in
710    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
711
712(** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **)
713let sp p st =
714  p.load_sp st.regs
715
716type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
717                  last_pop : ByteValues.program_counter }
718
719(** val state_pc_rect_Type4 :
720    sem_state_params -> (state -> ByteValues.program_counter ->
721    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
722let rec state_pc_rect_Type4 semp h_mk_state_pc x_5553 =
723  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5553 in
724  h_mk_state_pc st_no_pc0 pc0 last_pop0
725
726(** val state_pc_rect_Type5 :
727    sem_state_params -> (state -> ByteValues.program_counter ->
728    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
729let rec state_pc_rect_Type5 semp h_mk_state_pc x_5555 =
730  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5555 in
731  h_mk_state_pc st_no_pc0 pc0 last_pop0
732
733(** val state_pc_rect_Type3 :
734    sem_state_params -> (state -> ByteValues.program_counter ->
735    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
736let rec state_pc_rect_Type3 semp h_mk_state_pc x_5557 =
737  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5557 in
738  h_mk_state_pc st_no_pc0 pc0 last_pop0
739
740(** val state_pc_rect_Type2 :
741    sem_state_params -> (state -> ByteValues.program_counter ->
742    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
743let rec state_pc_rect_Type2 semp h_mk_state_pc x_5559 =
744  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5559 in
745  h_mk_state_pc st_no_pc0 pc0 last_pop0
746
747(** val state_pc_rect_Type1 :
748    sem_state_params -> (state -> ByteValues.program_counter ->
749    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
750let rec state_pc_rect_Type1 semp h_mk_state_pc x_5561 =
751  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5561 in
752  h_mk_state_pc st_no_pc0 pc0 last_pop0
753
754(** val state_pc_rect_Type0 :
755    sem_state_params -> (state -> ByteValues.program_counter ->
756    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
757let rec state_pc_rect_Type0 semp h_mk_state_pc x_5563 =
758  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5563 in
759  h_mk_state_pc st_no_pc0 pc0 last_pop0
760
761(** val st_no_pc : sem_state_params -> state_pc -> state **)
762let rec st_no_pc semp xxx =
763  xxx.st_no_pc
764
765(** val pc : sem_state_params -> state_pc -> ByteValues.program_counter **)
766let rec pc semp xxx =
767  xxx.pc
768
769(** val last_pop :
770    sem_state_params -> state_pc -> ByteValues.program_counter **)
771let rec last_pop semp xxx =
772  xxx.last_pop
773
774(** val state_pc_inv_rect_Type4 :
775    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
776    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
777let state_pc_inv_rect_Type4 x1 hterm h1 =
778  let hcut = state_pc_rect_Type4 x1 h1 hterm in hcut __
779
780(** val state_pc_inv_rect_Type3 :
781    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
782    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
783let state_pc_inv_rect_Type3 x1 hterm h1 =
784  let hcut = state_pc_rect_Type3 x1 h1 hterm in hcut __
785
786(** val state_pc_inv_rect_Type2 :
787    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
788    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
789let state_pc_inv_rect_Type2 x1 hterm h1 =
790  let hcut = state_pc_rect_Type2 x1 h1 hterm in hcut __
791
792(** val state_pc_inv_rect_Type1 :
793    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
794    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
795let state_pc_inv_rect_Type1 x1 hterm h1 =
796  let hcut = state_pc_rect_Type1 x1 h1 hterm in hcut __
797
798(** val state_pc_inv_rect_Type0 :
799    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
800    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
801let state_pc_inv_rect_Type0 x1 hterm h1 =
802  let hcut = state_pc_rect_Type0 x1 h1 hterm in hcut __
803
804(** val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __ **)
805let state_pc_discr a1 x y =
806  Logic.eq_rect_Type2 x
807    (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
808    Obj.magic (fun _ dH -> dH __ __ __)) y
809
810(** val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __ **)
811let state_pc_jmdiscr a1 x y =
812  Logic.eq_rect_Type2 x
813    (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
814    Obj.magic (fun _ dH -> dH __ __ __)) y
815
816(** val dpi1__o__st_no_pc__o__inject :
817    sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0 **)
818let dpi1__o__st_no_pc__o__inject x0 x3 =
819  x3.Types.dpi1.st_no_pc
820
821(** val eject__o__st_no_pc__o__inject :
822    sem_state_params -> state_pc Types.sig0 -> state Types.sig0 **)
823let eject__o__st_no_pc__o__inject x0 x3 =
824  (Types.pi1 x3).st_no_pc
825
826(** val st_no_pc__o__inject :
827    sem_state_params -> state_pc -> state Types.sig0 **)
828let st_no_pc__o__inject x0 x2 =
829  x2.st_no_pc
830
831(** val dpi1__o__st_no_pc :
832    sem_state_params -> (state_pc, 'a1) Types.dPair -> state **)
833let dpi1__o__st_no_pc x0 x2 =
834  x2.Types.dpi1.st_no_pc
835
836(** val eject__o__st_no_pc :
837    sem_state_params -> state_pc Types.sig0 -> state **)
838let eject__o__st_no_pc x0 x2 =
839  (Types.pi1 x2).st_no_pc
840
841(** val init_pc : ByteValues.program_counter **)
842let init_pc =
843  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
844    ByteValues.pc_offset = Positive.One }
845
846(** val null_pc : Positive.pos -> ByteValues.program_counter **)
847let null_pc pos =
848  { ByteValues.pc_block = Pointers.dummy_block_code; ByteValues.pc_offset =
849    pos }
850
851(** val set_m : sem_state_params -> BEMem.bemem -> state -> state **)
852let set_m p m0 st =
853  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
854    st.regs; m = m0; stack_usage = st.stack_usage }
855
856(** val set_regs : sem_state_params -> __ -> state -> state **)
857let set_regs p regs0 st =
858  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0;
859    m = st.m; stack_usage = st.stack_usage }
860
861(** val set_sp :
862    sem_state_params -> ByteValues.xpointer -> state -> state **)
863let set_sp p sp0 st =
864  let regs' = p.save_sp st.regs sp0 in
865  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs';
866  m = st.m; stack_usage = st.stack_usage }
867
868(** val set_carry :
869    sem_state_params -> ByteValues.bebit -> state -> state **)
870let set_carry p carry0 st =
871  { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs;
872    m = st.m; stack_usage = st.stack_usage }
873
874(** val set_istack : sem_state_params -> internal_stack -> state -> state **)
875let set_istack p is st =
876  { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m =
877    st.m; stack_usage = st.stack_usage }
878
879(** val set_pc :
880    sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc **)
881let set_pc p pc0 st =
882  { st_no_pc = st.st_no_pc; pc = pc0; last_pop = st.last_pop }
883
884(** val set_no_pc : sem_state_params -> state -> state_pc -> state_pc **)
885let set_no_pc p s st =
886  { st_no_pc = s; pc = st.pc; last_pop = st.last_pop }
887
888(** val set_last_pop :
889    sem_state_params -> state -> ByteValues.program_counter -> state_pc **)
890let set_last_pop p st pc0 =
891  { st_no_pc = st; pc = pc0; last_pop = pc0 }
892
893(** val set_frms : sem_state_params -> __ -> state -> state **)
894let set_frms p frms st =
895  { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
896    st.regs; m = st.m; stack_usage = st.stack_usage }
897
898(** val fetch_function :
899    'a1 Globalenvs.genv_t -> Pointers.block Types.sig0 -> (AST.ident, 'a1)
900    Types.prod Errors.res **)
901let fetch_function ge0 bl =
902  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
903    List.Nil))
904    (Obj.magic
905      (Monad.m_bind0 (Monad.max_def Option.option)
906        (Obj.magic (Globalenvs.symbol_for_block ge0 (Types.pi1 bl)))
907        (fun id ->
908        Monad.m_bind0 (Monad.max_def Option.option)
909          (Obj.magic (Globalenvs.find_funct_ptr ge0 (Types.pi1 bl)))
910          (fun fd ->
911          Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
912            Types.snd = fd }))))
913
914(** val fetch_internal_function :
915    'a1 AST.fundef Globalenvs.genv_t -> Pointers.block Types.sig0 ->
916    (AST.ident, 'a1) Types.prod Errors.res **)
917let fetch_internal_function ge0 bl =
918  Obj.magic
919    (Monad.m_bind2 (Monad.max_def Errors.res0)
920      (Obj.magic (fetch_function ge0 bl)) (fun id fd ->
921      match fd with
922      | AST.Internal ifd ->
923        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
924          Types.snd = ifd }
925      | AST.External x ->
926        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
927          ErrorMessages.BadFunction), List.Nil)))))
928
929type call_kind =
930| PTR
931| ID
932
933(** val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
934let rec call_kind_rect_Type4 h_PTR h_ID = function
935| PTR -> h_PTR
936| ID -> h_ID
937
938(** val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
939let rec call_kind_rect_Type5 h_PTR h_ID = function
940| PTR -> h_PTR
941| ID -> h_ID
942
943(** val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
944let rec call_kind_rect_Type3 h_PTR h_ID = function
945| PTR -> h_PTR
946| ID -> h_ID
947
948(** val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
949let rec call_kind_rect_Type2 h_PTR h_ID = function
950| PTR -> h_PTR
951| ID -> h_ID
952
953(** val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
954let rec call_kind_rect_Type1 h_PTR h_ID = function
955| PTR -> h_PTR
956| ID -> h_ID
957
958(** val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
959let rec call_kind_rect_Type0 h_PTR h_ID = function
960| PTR -> h_PTR
961| ID -> h_ID
962
963(** val call_kind_inv_rect_Type4 :
964    call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
965let call_kind_inv_rect_Type4 hterm h1 h2 =
966  let hcut = call_kind_rect_Type4 h1 h2 hterm in hcut __
967
968(** val call_kind_inv_rect_Type3 :
969    call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
970let call_kind_inv_rect_Type3 hterm h1 h2 =
971  let hcut = call_kind_rect_Type3 h1 h2 hterm in hcut __
972
973(** val call_kind_inv_rect_Type2 :
974    call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
975let call_kind_inv_rect_Type2 hterm h1 h2 =
976  let hcut = call_kind_rect_Type2 h1 h2 hterm in hcut __
977
978(** val call_kind_inv_rect_Type1 :
979    call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
980let call_kind_inv_rect_Type1 hterm h1 h2 =
981  let hcut = call_kind_rect_Type1 h1 h2 hterm in hcut __
982
983(** val call_kind_inv_rect_Type0 :
984    call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
985let call_kind_inv_rect_Type0 hterm h1 h2 =
986  let hcut = call_kind_rect_Type0 h1 h2 hterm in hcut __
987
988(** val call_kind_discr : call_kind -> call_kind -> __ **)
989let call_kind_discr x y =
990  Logic.eq_rect_Type2 x
991    (match x with
992     | PTR -> Obj.magic (fun _ dH -> dH)
993     | ID -> Obj.magic (fun _ dH -> dH)) y
994
995(** val call_kind_jmdiscr : call_kind -> call_kind -> __ **)
996let call_kind_jmdiscr x y =
997  Logic.eq_rect_Type2 x
998    (match x with
999     | PTR -> Obj.magic (fun _ dH -> dH)
1000     | ID -> Obj.magic (fun _ dH -> dH)) y
1001
1002(** val kind_of_call :
1003    Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum
1004    -> call_kind **)
1005let kind_of_call p = function
1006| Types.Inl x -> ID
1007| Types.Inr x -> PTR
1008
1009type 'f sem_unserialized_params = { st_pars : sem_state_params;
1010                                    acca_store_ : (__ -> ByteValues.beval ->
1011                                                  __ -> __ Errors.res);
1012                                    acca_retrieve_ : (__ -> __ ->
1013                                                     ByteValues.beval
1014                                                     Errors.res);
1015                                    acca_arg_retrieve_ : (__ -> __ ->
1016                                                         ByteValues.beval
1017                                                         Errors.res);
1018                                    accb_store_ : (__ -> ByteValues.beval ->
1019                                                  __ -> __ Errors.res);
1020                                    accb_retrieve_ : (__ -> __ ->
1021                                                     ByteValues.beval
1022                                                     Errors.res);
1023                                    accb_arg_retrieve_ : (__ -> __ ->
1024                                                         ByteValues.beval
1025                                                         Errors.res);
1026                                    dpl_store_ : (__ -> ByteValues.beval ->
1027                                                 __ -> __ Errors.res);
1028                                    dpl_retrieve_ : (__ -> __ ->
1029                                                    ByteValues.beval
1030                                                    Errors.res);
1031                                    dpl_arg_retrieve_ : (__ -> __ ->
1032                                                        ByteValues.beval
1033                                                        Errors.res);
1034                                    dph_store_ : (__ -> ByteValues.beval ->
1035                                                 __ -> __ Errors.res);
1036                                    dph_retrieve_ : (__ -> __ ->
1037                                                    ByteValues.beval
1038                                                    Errors.res);
1039                                    dph_arg_retrieve_ : (__ -> __ ->
1040                                                        ByteValues.beval
1041                                                        Errors.res);
1042                                    snd_arg_retrieve_ : (__ -> __ ->
1043                                                        ByteValues.beval
1044                                                        Errors.res);
1045                                    pair_reg_move_ : (__ -> __ -> __
1046                                                     Errors.res);
1047                                    save_frame : (call_kind -> __ -> state_pc
1048                                                 -> state Errors.res);
1049                                    setup_call : (Nat.nat -> __ -> __ ->
1050                                                 state -> state Errors.res);
1051                                    fetch_external_args : (AST.external_function
1052                                                          -> state -> __ ->
1053                                                          Values.val0
1054                                                          List.list
1055                                                          Errors.res);
1056                                    set_result : (Values.val0 List.list -> __
1057                                                 -> state -> state
1058                                                 Errors.res);
1059                                    call_args_for_main : __;
1060                                    call_dest_for_main : __;
1061                                    read_result : (AST.ident List.list -> 'f
1062                                                  AST.fundef
1063                                                  Globalenvs.genv_t -> __ ->
1064                                                  state -> ByteValues.beval
1065                                                  List.list Errors.res);
1066                                    eval_ext_seq : (AST.ident List.list -> 'f
1067                                                   genv_gen -> __ ->
1068                                                   AST.ident -> state ->
1069                                                   state Errors.res);
1070                                    pop_frame : (AST.ident List.list -> 'f
1071                                                genv_gen -> AST.ident -> __
1072                                                -> state -> (state,
1073                                                ByteValues.program_counter)
1074                                                Types.prod Errors.res) }
1075
1076(** val sem_unserialized_params_rect_Type4 :
1077    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1078    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1079    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1080    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1081    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1082    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1083    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1084    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1085    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1086    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1087    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1088    (AST.external_function -> state -> __ -> Values.val0 List.list
1089    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1090    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1091    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1092    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1093    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1094    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1095    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1096let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_5618 =
1097  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1098    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1099    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1100    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1101    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1102    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1103    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1104    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1105    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1106    set_result0; call_args_for_main = call_args_for_main0;
1107    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1108    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5618
1109  in
1110  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1111    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1112    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1113    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1114    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1115    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1116
1117(** val sem_unserialized_params_rect_Type5 :
1118    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1119    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1120    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1121    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1122    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1123    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1124    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1125    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1126    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1127    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1128    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1129    (AST.external_function -> state -> __ -> Values.val0 List.list
1130    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1131    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1132    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1133    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1134    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1135    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1136    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1137let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_5620 =
1138  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1139    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1140    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1141    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1142    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1143    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1144    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1145    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1146    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1147    set_result0; call_args_for_main = call_args_for_main0;
1148    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1149    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5620
1150  in
1151  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1152    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1153    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1154    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1155    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1156    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1157
1158(** val sem_unserialized_params_rect_Type3 :
1159    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1160    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1161    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1162    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1163    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1164    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1165    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1166    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1167    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1168    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1169    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1170    (AST.external_function -> state -> __ -> Values.val0 List.list
1171    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1172    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1173    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1174    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1175    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1176    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1177    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1178let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_5622 =
1179  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1180    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1181    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1182    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1183    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1184    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1185    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1186    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1187    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1188    set_result0; call_args_for_main = call_args_for_main0;
1189    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1190    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5622
1191  in
1192  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1193    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1194    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1195    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1196    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1197    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1198
1199(** val sem_unserialized_params_rect_Type2 :
1200    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1201    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1202    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1203    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1204    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1205    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1206    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1207    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1208    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1209    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1210    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1211    (AST.external_function -> state -> __ -> Values.val0 List.list
1212    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1213    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1214    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1215    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1216    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1217    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1218    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1219let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_5624 =
1220  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1221    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1222    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1223    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1224    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1225    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1226    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1227    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1228    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1229    set_result0; call_args_for_main = call_args_for_main0;
1230    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1231    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5624
1232  in
1233  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1234    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1235    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1236    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1237    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1238    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1239
1240(** val sem_unserialized_params_rect_Type1 :
1241    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1242    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1243    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1244    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1245    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1246    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1247    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1248    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1249    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1250    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1251    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1252    (AST.external_function -> state -> __ -> Values.val0 List.list
1253    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1254    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1255    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1256    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1257    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1258    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1259    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1260let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_5626 =
1261  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1262    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1263    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1264    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1265    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1266    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1267    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1268    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1269    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1270    set_result0; call_args_for_main = call_args_for_main0;
1271    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1272    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5626
1273  in
1274  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1275    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1276    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1277    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1278    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1279    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1280
1281(** val sem_unserialized_params_rect_Type0 :
1282    Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1283    -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1284    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1285    __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1286    -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1287    __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1288    -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1289    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1290    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1291    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1292    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1293    (AST.external_function -> state -> __ -> Values.val0 List.list
1294    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1295    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1296    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1297    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1298    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1299    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1300    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1301let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_5628 =
1302  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1303    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1304    accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1305    accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1306    dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1307    dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1308    dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1309    pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1310    setup_call0; fetch_external_args = fetch_external_args0; set_result =
1311    set_result0; call_args_for_main = call_args_for_main0;
1312    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1313    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5628
1314  in
1315  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1316    acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1317    dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1318    dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1319    setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1320    call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1321
1322(** val st_pars :
1323    Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1324    sem_state_params **)
1325let rec st_pars uns_pars xxx =
1326  xxx.st_pars
1327
1328(** val acca_store_ :
1329    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1330    ByteValues.beval -> __ -> __ Errors.res **)
1331let rec acca_store_ uns_pars xxx =
1332  xxx.acca_store_
1333
1334(** val acca_retrieve_ :
1335    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1336    ByteValues.beval Errors.res **)
1337let rec acca_retrieve_ uns_pars xxx =
1338  xxx.acca_retrieve_
1339
1340(** val acca_arg_retrieve_ :
1341    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1342    ByteValues.beval Errors.res **)
1343let rec acca_arg_retrieve_ uns_pars xxx =
1344  xxx.acca_arg_retrieve_
1345
1346(** val accb_store_ :
1347    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1348    ByteValues.beval -> __ -> __ Errors.res **)
1349let rec accb_store_ uns_pars xxx =
1350  xxx.accb_store_
1351
1352(** val accb_retrieve_ :
1353    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1354    ByteValues.beval Errors.res **)
1355let rec accb_retrieve_ uns_pars xxx =
1356  xxx.accb_retrieve_
1357
1358(** val accb_arg_retrieve_ :
1359    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1360    ByteValues.beval Errors.res **)
1361let rec accb_arg_retrieve_ uns_pars xxx =
1362  xxx.accb_arg_retrieve_
1363
1364(** val dpl_store_ :
1365    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1366    ByteValues.beval -> __ -> __ Errors.res **)
1367let rec dpl_store_ uns_pars xxx =
1368  xxx.dpl_store_
1369
1370(** val dpl_retrieve_ :
1371    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1372    ByteValues.beval Errors.res **)
1373let rec dpl_retrieve_ uns_pars xxx =
1374  xxx.dpl_retrieve_
1375
1376(** val dpl_arg_retrieve_ :
1377    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1378    ByteValues.beval Errors.res **)
1379let rec dpl_arg_retrieve_ uns_pars xxx =
1380  xxx.dpl_arg_retrieve_
1381
1382(** val dph_store_ :
1383    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1384    ByteValues.beval -> __ -> __ Errors.res **)
1385let rec dph_store_ uns_pars xxx =
1386  xxx.dph_store_
1387
1388(** val dph_retrieve_ :
1389    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1390    ByteValues.beval Errors.res **)
1391let rec dph_retrieve_ uns_pars xxx =
1392  xxx.dph_retrieve_
1393
1394(** val dph_arg_retrieve_ :
1395    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1396    ByteValues.beval Errors.res **)
1397let rec dph_arg_retrieve_ uns_pars xxx =
1398  xxx.dph_arg_retrieve_
1399
1400(** val snd_arg_retrieve_ :
1401    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1402    ByteValues.beval Errors.res **)
1403let rec snd_arg_retrieve_ uns_pars xxx =
1404  xxx.snd_arg_retrieve_
1405
1406(** val pair_reg_move_ :
1407    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1408    __ Errors.res **)
1409let rec pair_reg_move_ uns_pars xxx =
1410  xxx.pair_reg_move_
1411
1412(** val save_frame :
1413    Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind ->
1414    __ -> state_pc -> state Errors.res **)
1415let rec save_frame uns_pars xxx =
1416  xxx.save_frame
1417
1418(** val setup_call :
1419    Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
1420    -> __ -> state -> state Errors.res **)
1421let rec setup_call uns_pars xxx =
1422  xxx.setup_call
1423
1424(** val fetch_external_args :
1425    Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1426    AST.external_function -> state -> __ -> Values.val0 List.list Errors.res **)
1427let rec fetch_external_args uns_pars xxx =
1428  xxx.fetch_external_args
1429
1430(** val set_result :
1431    Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
1432    List.list -> __ -> state -> state Errors.res **)
1433let rec set_result uns_pars xxx =
1434  xxx.set_result
1435
1436(** val call_args_for_main :
1437    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1438let rec call_args_for_main uns_pars xxx =
1439  xxx.call_args_for_main
1440
1441(** val call_dest_for_main :
1442    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1443let rec call_dest_for_main uns_pars xxx =
1444  xxx.call_dest_for_main
1445
1446(** val read_result :
1447    Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1448    List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
1449    ByteValues.beval List.list Errors.res **)
1450let rec read_result uns_pars xxx =
1451  xxx.read_result
1452
1453(** val eval_ext_seq :
1454    Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1455    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res **)
1456let rec eval_ext_seq uns_pars xxx =
1457  xxx.eval_ext_seq
1458
1459(** val pop_frame :
1460    Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1461    List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
1462    ByteValues.program_counter) Types.prod Errors.res **)
1463let rec pop_frame uns_pars xxx =
1464  xxx.pop_frame
1465
1466(** val sem_unserialized_params_inv_rect_Type4 :
1467    Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1468    (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1469    (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1470    ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1471    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1472    ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1473    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1474    ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1475    Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1476    ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1477    -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1478    Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1479    (AST.external_function -> state -> __ -> Values.val0 List.list
1480    Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1481    -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1482    -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1483    List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1484    Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1485    state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1486    -> 'a2) -> 'a2 **)
1487let sem_unserialized_params_inv_rect_Type4 x1 hterm h1 =
1488  let hcut = sem_unserialized_params_rect_Type4 x1 h1 hterm in hcut __
1489
1490(** val sem_unserialized_params_inv_rect_Type3 :
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) -> __
1510    -> 'a2) -> 'a2 **)
1511let sem_unserialized_params_inv_rect_Type3 x1 hterm h1 =
1512  let hcut = sem_unserialized_params_rect_Type3 x1 h1 hterm in hcut __
1513
1514(** val sem_unserialized_params_inv_rect_Type2 :
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) -> __
1534    -> 'a2) -> 'a2 **)
1535let sem_unserialized_params_inv_rect_Type2 x1 hterm h1 =
1536  let hcut = sem_unserialized_params_rect_Type2 x1 h1 hterm in hcut __
1537
1538(** val sem_unserialized_params_inv_rect_Type1 :
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) -> __
1558    -> 'a2) -> 'a2 **)
1559let sem_unserialized_params_inv_rect_Type1 x1 hterm h1 =
1560  let hcut = sem_unserialized_params_rect_Type1 x1 h1 hterm in hcut __
1561
1562(** val sem_unserialized_params_inv_rect_Type0 :
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) -> __
1582    -> 'a2) -> 'a2 **)
1583let sem_unserialized_params_inv_rect_Type0 x1 hterm h1 =
1584  let hcut = sem_unserialized_params_rect_Type0 x1 h1 hterm in hcut __
1585
1586(** val sem_unserialized_params_jmdiscr :
1587    Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
1588    sem_unserialized_params -> __ **)
1589let sem_unserialized_params_jmdiscr a1 x y =
1590  Logic.eq_rect_Type2 x
1591    (let { st_pars = a0; acca_store_ = a10; acca_retrieve_ = a20;
1592       acca_arg_retrieve_ = a3; accb_store_ = a4; accb_retrieve_ = a5;
1593       accb_arg_retrieve_ = a6; dpl_store_ = a7; dpl_retrieve_ = a8;
1594       dpl_arg_retrieve_ = a9; dph_store_ = a100; dph_retrieve_ = a11;
1595       dph_arg_retrieve_ = a12; snd_arg_retrieve_ = a13; pair_reg_move_ =
1596       a14; save_frame = a15; setup_call = a16; fetch_external_args = a17;
1597       set_result = a18; call_args_for_main = a19; call_dest_for_main = a200;
1598       read_result = a21; eval_ext_seq = a22; pop_frame = a23 } = x
1599     in
1600    Obj.magic (fun _ dH ->
1601      dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __
1602        __)) y
1603
1604(** val helper_def_retrieve :
1605    (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ ->
1606    'a1 -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
1607    sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res **)
1608let helper_def_retrieve f up p st =
1609  Obj.magic f up __ p st.regs
1610
1611(** val helper_def_store :
1612    (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
1613    ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
1614    'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
1615    Errors.res **)
1616let helper_def_store f up p x v st =
1617  Obj.magic
1618    (Monad.m_bind0 (Monad.max_def Errors.res0)
1619      (Obj.magic f up __ p x v st.regs) (fun r ->
1620      Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st)))
1621
1622(** val acca_retrieve :
1623    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1624    -> ByteValues.beval Errors.res **)
1625let acca_retrieve up p x x0 =
1626  helper_def_retrieve (fun x1 _ -> acca_retrieve_ x1) up p x x0
1627
1628(** val acca_store :
1629    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1630    ByteValues.beval -> state -> state Errors.res **)
1631let acca_store up p x x0 x1 =
1632  helper_def_store (fun x2 _ -> acca_store_ x2) up p x x0 x1
1633
1634(** val acca_arg_retrieve :
1635    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1636    -> ByteValues.beval Errors.res **)
1637let acca_arg_retrieve up p x x0 =
1638  helper_def_retrieve (fun x1 _ -> acca_arg_retrieve_ x1) up p x x0
1639
1640(** val accb_store :
1641    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1642    ByteValues.beval -> state -> state Errors.res **)
1643let accb_store up p x x0 x1 =
1644  helper_def_store (fun x2 _ -> accb_store_ x2) up p x x0 x1
1645
1646(** val accb_retrieve :
1647    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1648    -> ByteValues.beval Errors.res **)
1649let accb_retrieve up p x x0 =
1650  helper_def_retrieve (fun x1 _ -> accb_retrieve_ x1) up p x x0
1651
1652(** val accb_arg_retrieve :
1653    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1654    -> ByteValues.beval Errors.res **)
1655let accb_arg_retrieve up p x x0 =
1656  helper_def_retrieve (fun x1 _ -> accb_arg_retrieve_ x1) up p x x0
1657
1658(** val dpl_store :
1659    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1660    ByteValues.beval -> state -> state Errors.res **)
1661let dpl_store up p x x0 x1 =
1662  helper_def_store (fun x2 _ -> dpl_store_ x2) up p x x0 x1
1663
1664(** val dpl_retrieve :
1665    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1666    -> ByteValues.beval Errors.res **)
1667let dpl_retrieve up p x x0 =
1668  helper_def_retrieve (fun x1 _ -> dpl_retrieve_ x1) up p x x0
1669
1670(** val dpl_arg_retrieve :
1671    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1672    -> ByteValues.beval Errors.res **)
1673let dpl_arg_retrieve up p x x0 =
1674  helper_def_retrieve (fun x1 _ -> dpl_arg_retrieve_ x1) up p x x0
1675
1676(** val dph_store :
1677    Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1678    ByteValues.beval -> state -> state Errors.res **)
1679let dph_store up p x x0 x1 =
1680  helper_def_store (fun x2 _ -> dph_store_ x2) up p x x0 x1
1681
1682(** val dph_retrieve :
1683    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1684    -> ByteValues.beval Errors.res **)
1685let dph_retrieve up p x x0 =
1686  helper_def_retrieve (fun x1 _ -> dph_retrieve_ x1) up p x x0
1687
1688(** val dph_arg_retrieve :
1689    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1690    -> ByteValues.beval Errors.res **)
1691let dph_arg_retrieve up p x x0 =
1692  helper_def_retrieve (fun x1 _ -> dph_arg_retrieve_ x1) up p x x0
1693
1694(** val snd_arg_retrieve :
1695    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1696    -> ByteValues.beval Errors.res **)
1697let snd_arg_retrieve up p x x0 =
1698  helper_def_retrieve (fun x1 _ -> snd_arg_retrieve_ x1) up p x x0
1699
1700(** val pair_reg_move :
1701    Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1702    -> __ **)
1703let pair_reg_move up p st pm =
1704  Monad.m_bind0 (Monad.max_def Errors.res0)
1705    (Obj.magic (p.pair_reg_move_ st.regs pm)) (fun r ->
1706    Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st))
1707
1708(** val push :
1709    sem_state_params -> state -> ByteValues.beval -> state Errors.res **)
1710let push p st v =
1711  Obj.magic
1712    (Monad.m_bind0 (Monad.max_def Errors.res0)
1713      (Obj.magic (is_push st.istack v)) (fun is ->
1714      Monad.m_return0 (Monad.max_def Errors.res0) (set_istack p is st)))
1715
1716(** val pop :
1717    sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1718    Errors.res **)
1719let pop p st =
1720  Obj.magic
1721    (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (is_pop st.istack))
1722      (fun bv is ->
1723      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv;
1724        Types.snd = (set_istack p is st) }))
1725
1726(** val push_ra :
1727    sem_state_params -> state -> ByteValues.program_counter -> state
1728    Errors.res **)
1729let push_ra p st l =
1730  let { Types.fst = addrl; Types.snd = addrh } =
1731    ByteValues.beval_pair_of_pc l
1732  in
1733  Obj.magic
1734    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (push p st addrl))
1735      (fun st' -> Obj.magic (push p st' addrh)))
1736
1737(** val pop_ra :
1738    sem_state_params -> state -> (state, ByteValues.program_counter)
1739    Types.prod Errors.res **)
1740let pop_ra p st =
1741  Obj.magic
1742    (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st))
1743      (fun addrh st' ->
1744      Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st'))
1745        (fun addrl st'' ->
1746        Monad.m_bind0 (Monad.max_def Errors.res0)
1747          (Obj.magic
1748            (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh,
1749              List.Nil)))))) (fun pr ->
1750          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st'';
1751            Types.snd = pr }))))
1752
1753type serialized_params = { spp : Joint.params;
1754                           msu_pars : Joint.joint_closed_internal_function
1755                                      sem_unserialized_params;
1756                           offset_of_point : (__ -> Positive.pos);
1757                           point_of_offset : (Positive.pos -> __) }
1758
1759(** val serialized_params_rect_Type4 :
1760    (Joint.params -> Joint.joint_closed_internal_function
1761    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1762    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1763let rec serialized_params_rect_Type4 h_mk_serialized_params x_5698 =
1764  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1765    point_of_offset = point_of_offset0 } = x_5698
1766  in
1767  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1768    __
1769
1770(** val serialized_params_rect_Type5 :
1771    (Joint.params -> Joint.joint_closed_internal_function
1772    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1773    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1774let rec serialized_params_rect_Type5 h_mk_serialized_params x_5700 =
1775  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1776    point_of_offset = point_of_offset0 } = x_5700
1777  in
1778  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1779    __
1780
1781(** val serialized_params_rect_Type3 :
1782    (Joint.params -> Joint.joint_closed_internal_function
1783    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1784    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1785let rec serialized_params_rect_Type3 h_mk_serialized_params x_5702 =
1786  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1787    point_of_offset = point_of_offset0 } = x_5702
1788  in
1789  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1790    __
1791
1792(** val serialized_params_rect_Type2 :
1793    (Joint.params -> Joint.joint_closed_internal_function
1794    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1795    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1796let rec serialized_params_rect_Type2 h_mk_serialized_params x_5704 =
1797  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1798    point_of_offset = point_of_offset0 } = x_5704
1799  in
1800  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1801    __
1802
1803(** val serialized_params_rect_Type1 :
1804    (Joint.params -> Joint.joint_closed_internal_function
1805    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1806    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1807let rec serialized_params_rect_Type1 h_mk_serialized_params x_5706 =
1808  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1809    point_of_offset = point_of_offset0 } = x_5706
1810  in
1811  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1812    __
1813
1814(** val serialized_params_rect_Type0 :
1815    (Joint.params -> Joint.joint_closed_internal_function
1816    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1817    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1818let rec serialized_params_rect_Type0 h_mk_serialized_params x_5708 =
1819  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1820    point_of_offset = point_of_offset0 } = x_5708
1821  in
1822  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1823    __
1824
1825(** val spp : serialized_params -> Joint.params **)
1826let rec spp xxx =
1827  xxx.spp
1828
1829(** val msu_pars :
1830    serialized_params -> Joint.joint_closed_internal_function
1831    sem_unserialized_params **)
1832let rec msu_pars xxx =
1833  xxx.msu_pars
1834
1835(** val offset_of_point : serialized_params -> __ -> Positive.pos **)
1836let rec offset_of_point xxx =
1837  xxx.offset_of_point
1838
1839(** val point_of_offset : serialized_params -> Positive.pos -> __ **)
1840let rec point_of_offset xxx =
1841  xxx.point_of_offset
1842
1843(** val serialized_params_inv_rect_Type4 :
1844    serialized_params -> (Joint.params ->
1845    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1846    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1847let serialized_params_inv_rect_Type4 hterm h1 =
1848  let hcut = serialized_params_rect_Type4 h1 hterm in hcut __
1849
1850(** val serialized_params_inv_rect_Type3 :
1851    serialized_params -> (Joint.params ->
1852    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1853    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1854let serialized_params_inv_rect_Type3 hterm h1 =
1855  let hcut = serialized_params_rect_Type3 h1 hterm in hcut __
1856
1857(** val serialized_params_inv_rect_Type2 :
1858    serialized_params -> (Joint.params ->
1859    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1860    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1861let serialized_params_inv_rect_Type2 hterm h1 =
1862  let hcut = serialized_params_rect_Type2 h1 hterm in hcut __
1863
1864(** val serialized_params_inv_rect_Type1 :
1865    serialized_params -> (Joint.params ->
1866    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1867    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1868let serialized_params_inv_rect_Type1 hterm h1 =
1869  let hcut = serialized_params_rect_Type1 h1 hterm in hcut __
1870
1871(** val serialized_params_inv_rect_Type0 :
1872    serialized_params -> (Joint.params ->
1873    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1874    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1875let serialized_params_inv_rect_Type0 hterm h1 =
1876  let hcut = serialized_params_rect_Type0 h1 hterm in hcut __
1877
1878(** val serialized_params_jmdiscr :
1879    serialized_params -> serialized_params -> __ **)
1880let serialized_params_jmdiscr x y =
1881  Logic.eq_rect_Type2 x
1882    (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset =
1883       a3 } = x
1884     in
1885    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1886
1887(** val spp__o__stmt_pars : serialized_params -> Joint.stmt_params **)
1888let spp__o__stmt_pars x0 =
1889  x0.spp.Joint.stmt_pars
1890
1891(** val spp__o__stmt_pars__o__uns_pars :
1892    serialized_params -> Joint.uns_params **)
1893let spp__o__stmt_pars__o__uns_pars x0 =
1894  Joint.stmt_pars__o__uns_pars x0.spp
1895
1896(** val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1897    serialized_params -> Joint.unserialized_params **)
1898let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
1899  Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp
1900
1901(** val msu_pars__o__st_pars : serialized_params -> sem_state_params **)
1902let msu_pars__o__st_pars x0 =
1903  x0.msu_pars.st_pars
1904
1905type sem_params = { spp' : serialized_params;
1906                    pre_main_generator : (Joint.joint_program ->
1907                                         Joint.joint_closed_internal_function) }
1908
1909(** val sem_params_rect_Type4 :
1910    (serialized_params -> (Joint.joint_program ->
1911    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1912let rec sem_params_rect_Type4 h_mk_sem_params x_5726 =
1913  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5726 in
1914  h_mk_sem_params spp'0 pre_main_generator0
1915
1916(** val sem_params_rect_Type5 :
1917    (serialized_params -> (Joint.joint_program ->
1918    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1919let rec sem_params_rect_Type5 h_mk_sem_params x_5728 =
1920  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5728 in
1921  h_mk_sem_params spp'0 pre_main_generator0
1922
1923(** val sem_params_rect_Type3 :
1924    (serialized_params -> (Joint.joint_program ->
1925    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1926let rec sem_params_rect_Type3 h_mk_sem_params x_5730 =
1927  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5730 in
1928  h_mk_sem_params spp'0 pre_main_generator0
1929
1930(** val sem_params_rect_Type2 :
1931    (serialized_params -> (Joint.joint_program ->
1932    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1933let rec sem_params_rect_Type2 h_mk_sem_params x_5732 =
1934  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5732 in
1935  h_mk_sem_params spp'0 pre_main_generator0
1936
1937(** val sem_params_rect_Type1 :
1938    (serialized_params -> (Joint.joint_program ->
1939    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1940let rec sem_params_rect_Type1 h_mk_sem_params x_5734 =
1941  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5734 in
1942  h_mk_sem_params spp'0 pre_main_generator0
1943
1944(** val sem_params_rect_Type0 :
1945    (serialized_params -> (Joint.joint_program ->
1946    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1947let rec sem_params_rect_Type0 h_mk_sem_params x_5736 =
1948  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5736 in
1949  h_mk_sem_params spp'0 pre_main_generator0
1950
1951(** val spp' : sem_params -> serialized_params **)
1952let rec spp' xxx =
1953  xxx.spp'
1954
1955(** val pre_main_generator :
1956    sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function **)
1957let rec pre_main_generator xxx =
1958  xxx.pre_main_generator
1959
1960(** val sem_params_inv_rect_Type4 :
1961    sem_params -> (serialized_params -> (Joint.joint_program ->
1962    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1963let sem_params_inv_rect_Type4 hterm h1 =
1964  let hcut = sem_params_rect_Type4 h1 hterm in hcut __
1965
1966(** val sem_params_inv_rect_Type3 :
1967    sem_params -> (serialized_params -> (Joint.joint_program ->
1968    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1969let sem_params_inv_rect_Type3 hterm h1 =
1970  let hcut = sem_params_rect_Type3 h1 hterm in hcut __
1971
1972(** val sem_params_inv_rect_Type2 :
1973    sem_params -> (serialized_params -> (Joint.joint_program ->
1974    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1975let sem_params_inv_rect_Type2 hterm h1 =
1976  let hcut = sem_params_rect_Type2 h1 hterm in hcut __
1977
1978(** val sem_params_inv_rect_Type1 :
1979    sem_params -> (serialized_params -> (Joint.joint_program ->
1980    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1981let sem_params_inv_rect_Type1 hterm h1 =
1982  let hcut = sem_params_rect_Type1 h1 hterm in hcut __
1983
1984(** val sem_params_inv_rect_Type0 :
1985    sem_params -> (serialized_params -> (Joint.joint_program ->
1986    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1987let sem_params_inv_rect_Type0 hterm h1 =
1988  let hcut = sem_params_rect_Type0 h1 hterm in hcut __
1989
1990(** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
1991let sem_params_jmdiscr x y =
1992  Logic.eq_rect_Type2 x
1993    (let { spp' = a0; pre_main_generator = a1 } = x in
1994    Obj.magic (fun _ dH -> dH __ __)) y
1995
1996(** val spp'__o__msu_pars :
1997    sem_params -> Joint.joint_closed_internal_function
1998    sem_unserialized_params **)
1999let spp'__o__msu_pars x0 =
2000  x0.spp'.msu_pars
2001
2002(** val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params **)
2003let spp'__o__msu_pars__o__st_pars x0 =
2004  msu_pars__o__st_pars x0.spp'
2005
2006(** val spp'__o__spp : sem_params -> Joint.params **)
2007let spp'__o__spp x0 =
2008  x0.spp'.spp
2009
2010(** val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
2011let spp'__o__spp__o__stmt_pars x0 =
2012  spp__o__stmt_pars x0.spp'
2013
2014(** val spp'__o__spp__o__stmt_pars__o__uns_pars :
2015    sem_params -> Joint.uns_params **)
2016let spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
2017  spp__o__stmt_pars__o__uns_pars x0.spp'
2018
2019(** val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
2020    sem_params -> Joint.unserialized_params **)
2021let spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2022  spp__o__stmt_pars__o__uns_pars__o__u_pars x0.spp'
2023
2024(** val pc_of_point :
2025    sem_params -> Pointers.block Types.sig0 -> __ ->
2026    ByteValues.program_counter **)
2027let pc_of_point p bl pt =
2028  { ByteValues.pc_block = bl; ByteValues.pc_offset =
2029    (p.spp'.offset_of_point pt) }
2030
2031(** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **)
2032let point_of_pc p ptr =
2033  p.spp'.point_of_offset ptr.ByteValues.pc_offset
2034
2035(** val fetch_statement :
2036    sem_params -> AST.ident List.list -> Joint.joint_function
2037    Globalenvs.genv_t -> ByteValues.program_counter -> ((AST.ident,
2038    Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
2039    Types.prod Errors.res **)
2040let fetch_statement p globals ge0 ptr =
2041  Obj.magic
2042    (Monad.m_bind2 (Monad.max_def Errors.res0)
2043      (Obj.magic (fetch_internal_function ge0 ptr.ByteValues.pc_block))
2044      (fun id fn ->
2045      let pt = point_of_pc p ptr in
2046      Monad.m_bind0 (Monad.max_def Errors.res0)
2047        (Obj.magic
2048          (Errors.opt_to_res
2049            (Errors.msg ErrorMessages.ProgramCounterOutOfCode)
2050            ((spp'__o__spp p).Joint.stmt_at globals
2051              (Types.pi1 fn).Joint.joint_if_code pt))) (fun stmt ->
2052        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
2053          { Types.fst = id; Types.snd = fn }; Types.snd = stmt })))
2054
2055(** val pc_of_label :
2056    sem_params -> AST.ident List.list -> Joint.joint_function
2057    Globalenvs.genv_t -> Pointers.block Types.sig0 -> Graphs.label ->
2058    ByteValues.program_counter Errors.res **)
2059let pc_of_label p globals ge0 bl lbl =
2060  Obj.magic
2061    (Monad.m_bind2 (Monad.max_def Errors.res0)
2062      (Obj.magic (fetch_internal_function ge0 bl)) (fun i fn ->
2063      Monad.m_bind0 (Monad.max_def Errors.res0)
2064        (Obj.magic
2065          (Errors.opt_to_res (List.Cons ((Errors.MSG
2066            ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
2067            (PreIdentifiers.LabelTag, lbl)), List.Nil))))
2068            ((spp'__o__spp p).Joint.point_of_label globals
2069              (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt ->
2070        Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block =
2071          bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) })))
2072
2073(** val succ_pc :
2074    sem_params -> ByteValues.program_counter -> __ ->
2075    ByteValues.program_counter **)
2076let succ_pc p ptr nxt =
2077  let curr = point_of_pc p ptr in
2078  pc_of_point p ptr.ByteValues.pc_block
2079    ((spp'__o__spp p).Joint.point_of_succ curr nxt)
2080
2081(** val goto :
2082    sem_params -> AST.ident List.list -> Joint.joint_function
2083    Globalenvs.genv_t -> Graphs.label -> state_pc -> state_pc Errors.res **)
2084let goto p globals ge0 l st =
2085  Obj.magic
2086    (Monad.m_bind0 (Monad.max_def Errors.res0)
2087      (Obj.magic (pc_of_label p globals ge0 st.pc.ByteValues.pc_block l))
2088      (fun newpc ->
2089      Monad.m_return0 (Monad.max_def Errors.res0)
2090        (set_pc (spp'__o__msu_pars__o__st_pars p) newpc st)))
2091
2092(** val next : sem_params -> __ -> state_pc -> state_pc **)
2093let next p l st =
2094  let newpc = succ_pc p st.pc l in
2095  set_pc (spp'__o__msu_pars__o__st_pars p) newpc st
2096
2097(** val next_of_call_pc :
2098    sem_params -> AST.ident List.list -> Joint.joint_function
2099    Globalenvs.genv_t -> ByteValues.program_counter -> __ Errors.res **)
2100let next_of_call_pc p globals ge0 pc0 =
2101  Obj.magic
2102    (Monad.m_bind2 (Monad.max_def Errors.res0)
2103      (Obj.magic (fetch_statement p globals ge0 pc0)) (fun id_fn stmt ->
2104      match stmt with
2105      | Joint.Sequential (s, nxt) ->
2106        (match s with
2107         | Joint.COST_LABEL x ->
2108           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2109             ErrorMessages.NoSuccessor), List.Nil)))
2110         | Joint.CALL (x, x0, x1) ->
2111           Monad.m_return0 (Monad.max_def Errors.res0) nxt
2112         | Joint.COND (x, x0) ->
2113           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2114             ErrorMessages.NoSuccessor), List.Nil)))
2115         | Joint.Step_seq x ->
2116           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2117             ErrorMessages.NoSuccessor), List.Nil))))
2118      | Joint.Final x ->
2119        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2120          ErrorMessages.NoSuccessor), List.Nil)))
2121      | Joint.FCOND (x0, x1, x2) ->
2122        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2123          ErrorMessages.NoSuccessor), List.Nil)))))
2124
2125(** val eval_seq_no_pc :
2126    sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
2127    -> state -> state Errors.res **)
2128let eval_seq_no_pc p globals ge0 curr_id seq st =
2129  match seq with
2130  | Joint.COMMENT x ->
2131    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2132  | Joint.MOVE dst_src ->
2133    Obj.magic
2134      (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2135        p.spp'.msu_pars st dst_src)
2136  | Joint.POP dst ->
2137    Obj.magic
2138      (Monad.m_bind2 (Monad.max_def Errors.res0)
2139        (Obj.magic (pop (spp'__o__msu_pars__o__st_pars p) st)) (fun v st' ->
2140        Obj.magic
2141          (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2142            (spp'__o__msu_pars p) dst v st')))
2143  | Joint.PUSH src ->
2144    Obj.magic
2145      (Monad.m_bind0 (Monad.max_def Errors.res0)
2146        (Obj.magic
2147          (acca_arg_retrieve
2148            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2149            p.spp'.msu_pars st src)) (fun v ->
2150        Obj.magic (push (spp'__o__msu_pars__o__st_pars p) st v)))
2151  | Joint.ADDRESS (id, ldest, hdest) ->
2152    let addr_block =
2153      Option.opt_safe
2154        (Globalenvs.find_symbol
2155          (let p0 = spp'__o__spp p in
2156          let globals0 = globals in let g = ge0 in g.ge) id)
2157    in
2158    let { Types.fst = laddr; Types.snd = haddr } =
2159      ByteValues.beval_pair_of_pointer { Pointers.pblock = addr_block;
2160        Pointers.poff = Pointers.zero_offset }
2161    in
2162    Obj.magic
2163      (Monad.m_bind0 (Monad.max_def Errors.res0)
2164        (Obj.magic
2165          (dpl_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2166            p.spp'.msu_pars ldest laddr st)) (fun st' ->
2167        Obj.magic
2168          (dph_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2169            p.spp'.msu_pars hdest haddr st')))
2170  | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) ->
2171    Obj.magic
2172      (Monad.m_bind0 (Monad.max_def Errors.res0)
2173        (Obj.magic
2174          (acca_arg_retrieve
2175            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2176            p.spp'.msu_pars st sacc_a_reg)) (fun v1 ->
2177        Monad.m_bind0 (Monad.max_def Errors.res0)
2178          (Obj.magic
2179            (accb_arg_retrieve
2180              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2181              p.spp'.msu_pars st sacc_b_reg)) (fun v2 ->
2182          Monad.m_bind2 (Monad.max_def Errors.res0)
2183            (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' ->
2184            Monad.m_bind0 (Monad.max_def Errors.res0)
2185              (Obj.magic
2186                (acca_store
2187                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2188                  p.spp'.msu_pars dacc_a_reg v1' st)) (fun st' ->
2189              Obj.magic
2190                (accb_store
2191                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2192                  p.spp'.msu_pars dacc_b_reg v2' st'))))))
2193  | Joint.OP1 (op, dacc_a, sacc_a) ->
2194    Obj.magic
2195      (Monad.m_bind0 (Monad.max_def Errors.res0)
2196        (Obj.magic
2197          (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2198            p.spp'.msu_pars st sacc_a)) (fun v ->
2199        Monad.m_bind0 (Monad.max_def Errors.res0)
2200          (Obj.magic (BackEndOps.be_op1 op v)) (fun v' ->
2201          Obj.magic
2202            (acca_store
2203              (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2204              p.spp'.msu_pars dacc_a v' st))))
2205  | Joint.OP2 (op, dacc_a, sacc_a, src) ->
2206    Obj.magic
2207      (Monad.m_bind0 (Monad.max_def Errors.res0)
2208        (Obj.magic
2209          (acca_arg_retrieve
2210            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2211            p.spp'.msu_pars st sacc_a)) (fun v1 ->
2212        Monad.m_bind0 (Monad.max_def Errors.res0)
2213          (Obj.magic
2214            (snd_arg_retrieve
2215              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2216              p.spp'.msu_pars st src)) (fun v2 ->
2217          Monad.m_bind2 (Monad.max_def Errors.res0)
2218            (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
2219            (fun v' carry0 ->
2220            Monad.m_bind0 (Monad.max_def Errors.res0)
2221              (Obj.magic
2222                (acca_store
2223                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2224                  p.spp'.msu_pars dacc_a v' st)) (fun st' ->
2225              Monad.m_return0 (Monad.max_def Errors.res0)
2226                (set_carry p.spp'.msu_pars.st_pars carry0 st'))))))
2227  | Joint.CLEAR_CARRY ->
2228    Obj.magic
2229      (Monad.m_return0 (Monad.max_def Errors.res0)
2230        (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2231          Bool.False) st))
2232  | Joint.SET_CARRY ->
2233    Obj.magic
2234      (Monad.m_return0 (Monad.max_def Errors.res0)
2235        (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2236          Bool.True) st))
2237  | Joint.LOAD (dst, addrl, addrh) ->
2238    Obj.magic
2239      (Monad.m_bind0 (Monad.max_def Errors.res0)
2240        (Obj.magic
2241          (dph_arg_retrieve
2242            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2243            p.spp'.msu_pars st addrh)) (fun vaddrh ->
2244        Monad.m_bind0 (Monad.max_def Errors.res0)
2245          (Obj.magic
2246            (dpl_arg_retrieve
2247              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2248              p.spp'.msu_pars st addrl)) (fun vaddrl ->
2249          Monad.m_bind0 (Monad.max_def Errors.res0)
2250            (Obj.magic
2251              (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2252                vaddrh })) (fun vaddr ->
2253            Monad.m_bind0 (Monad.max_def Errors.res0)
2254              (Obj.magic
2255                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
2256                  (GenMem.beloadv st.m vaddr))) (fun v ->
2257              Obj.magic
2258                (acca_store
2259                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2260                  p.spp'.msu_pars dst v st))))))
2261  | Joint.STORE (addrl, addrh, src) ->
2262    Obj.magic
2263      (Monad.m_bind0 (Monad.max_def Errors.res0)
2264        (Obj.magic
2265          (dph_arg_retrieve
2266            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2267            p.spp'.msu_pars st addrh)) (fun vaddrh ->
2268        Monad.m_bind0 (Monad.max_def Errors.res0)
2269          (Obj.magic
2270            (dpl_arg_retrieve
2271              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2272              p.spp'.msu_pars st addrl)) (fun vaddrl ->
2273          Monad.m_bind0 (Monad.max_def Errors.res0)
2274            (Obj.magic
2275              (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2276                vaddrh })) (fun vaddr ->
2277            Monad.m_bind0 (Monad.max_def Errors.res0)
2278              (Obj.magic
2279                (acca_arg_retrieve
2280                  (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2281                  p.spp'.msu_pars st src)) (fun v ->
2282              Monad.m_bind0 (Monad.max_def Errors.res0)
2283                (Obj.magic
2284                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
2285                    (GenMem.bestorev st.m vaddr v))) (fun m' ->
2286                Monad.m_return0 (Monad.max_def Errors.res0)
2287                  (set_m (spp'__o__msu_pars__o__st_pars p) m' st)))))))
2288  | Joint.Extension_seq c ->
2289    p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
2290
2291(** val code_block_of_block :
2292    Pointers.block -> Pointers.block Types.sig0 Types.option **)
2293let code_block_of_block bl =
2294  (match Pointers.block_region bl with
2295   | AST.XData -> (fun _ -> Types.None)
2296   | AST.Code -> (fun _ -> Types.Some bl)) __
2297
2298(** val block_of_funct_id :
2299    sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
2300    Pointers.block Types.sig0 Errors.res **)
2301let block_of_funct_id sp0 ge0 id =
2302  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2303    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
2304    (Obj.magic
2305      (Monad.m_bind0 (Monad.max_def Option.option)
2306        (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
2307        Obj.magic (code_block_of_block bl))))
2308
2309(** val block_of_call :
2310    sem_params -> AST.ident List.list -> Joint.joint_function
2311    Globalenvs.genv_t -> (PreIdentifiers.identifier, (__, __) Types.prod)
2312    Types.sum -> state -> __ **)
2313let block_of_call p globals ge0 f st =
2314  Monad.m_bind0 (Monad.max_def Errors.res0)
2315    (match f with
2316     | Types.Inl id ->
2317       Obj.magic
2318         (Errors.opt_to_res (List.Cons ((Errors.MSG
2319           ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
2320           (PreIdentifiers.SymbolTag, id)), List.Nil))))
2321           (Globalenvs.find_symbol ge0 id))
2322     | Types.Inr addr ->
2323       Monad.m_bind0 (Monad.max_def Errors.res0)
2324         (Obj.magic
2325           (dpl_arg_retrieve
2326             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2327             p.spp'.msu_pars st addr.Types.fst)) (fun addr_l ->
2328         Monad.m_bind0 (Monad.max_def Errors.res0)
2329           (Obj.magic
2330             (dph_arg_retrieve
2331               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2332               p.spp'.msu_pars st addr.Types.snd)) (fun addr_h ->
2333           Monad.m_bind0 (Monad.max_def Errors.res0)
2334             (Obj.magic
2335               (ByteValues.pointer_of_bevals (List.Cons (addr_l, (List.Cons
2336                 (addr_h, List.Nil)))))) (fun ptr ->
2337             match BitVector.eq_bv Pointers.offset_size
2338                     (BitVector.zero Pointers.offset_size)
2339                     (Pointers.offv ptr.Pointers.poff) with
2340             | Bool.True ->
2341               Monad.m_return0 (Monad.max_def Errors.res0)
2342                 ptr.Pointers.pblock
2343             | Bool.False ->
2344               Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2345                 ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
2346                 ErrorMessages.BadPointer), List.Nil))))))))) (fun bl ->
2347    Obj.magic
2348      (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2349        (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil))))
2350        (code_block_of_block bl)))
2351
2352(** val eval_external_call :
2353    sem_params -> AST.external_function -> __ -> __ -> state -> __ **)
2354let eval_external_call p fn args dest st =
2355  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2356    (let x =
2357       IOMonad.err_to_io
2358         ((spp'__o__msu_pars p).fetch_external_args fn st args)
2359     in
2360    Obj.magic x) (fun params ->
2361    Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2362      (let x =
2363         IOMonad.err_to_io
2364           (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)
2365       in
2366      Obj.magic x) (fun evargs ->
2367      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2368        (Obj.magic
2369          (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
2370        (fun evres ->
2371        let vs = List.Cons
2372          ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil)
2373        in
2374        Obj.magic
2375          (IOMonad.err_to_io ((spp'__o__msu_pars p).set_result vs dest st)))))
2376
2377(** val increment_stack_usage :
2378    sem_state_params -> Nat.nat -> state -> state **)
2379let increment_stack_usage p n st =
2380  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2381    st.regs; m = st.m; stack_usage = (Nat.plus n st.stack_usage) }
2382
2383(** val decrement_stack_usage :
2384    sem_state_params -> Nat.nat -> state -> state **)
2385let decrement_stack_usage p n st =
2386  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2387    st.regs; m = st.m; stack_usage = (Nat.minus st.stack_usage n) }
2388
2389(** val eval_internal_call :
2390    sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2391    Joint.joint_internal_function -> __ -> state -> __ **)
2392let eval_internal_call p globals ge0 i fn args st =
2393  Monad.m_bind0 (Monad.max_def Errors.res0)
2394    (Obj.magic
2395      (Errors.opt_to_res (List.Cons ((Errors.MSG
2396        ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2397        (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i)))
2398    (fun stack_size ->
2399    Monad.m_bind0 (Monad.max_def Errors.res0)
2400      (Obj.magic
2401        (p.spp'.msu_pars.setup_call stack_size fn.Joint.joint_if_params args
2402          st)) (fun st' ->
2403      Monad.m_return0 (Monad.max_def Errors.res0)
2404        (increment_stack_usage p.spp'.msu_pars.st_pars stack_size st')))
2405
2406(** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **)
2407let is_inl = function
2408| Types.Inl x0 -> Bool.True
2409| Types.Inr x0 -> Bool.False
2410
2411(** val eval_call :
2412    sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2413    (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __ **)
2414let eval_call p globals ge0 f args dest nxt st =
2415  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2416    (let x =
2417       IOMonad.err_to_io
2418         (Obj.magic
2419           (block_of_call p globals
2420             (let p0 = spp'__o__spp p in
2421             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
2422     in
2423    Obj.magic x) (fun bl ->
2424    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2425      (let x =
2426         IOMonad.err_to_io
2427           (fetch_function
2428             (let p0 = spp'__o__spp p in
2429             let globals0 = globals in let g = ge0 in g.ge) bl)
2430       in
2431      Obj.magic x) (fun i fd ->
2432      match fd with
2433      | AST.Internal ifd ->
2434        Obj.magic
2435          (IOMonad.err_to_io
2436            (Obj.magic
2437              (Monad.m_bind0 (Monad.max_def Errors.res0)
2438                (Obj.magic
2439                  (p.spp'.msu_pars.save_frame
2440                    (kind_of_call
2441                      (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) f)
2442                    dest st)) (fun st' ->
2443                Monad.m_bind0 (Monad.max_def Errors.res0)
2444                  (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2445                    st') (fun st'' ->
2446                  let pc0 =
2447                    pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2448                  in
2449                  Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2450                    st''; pc = pc0; last_pop = st.last_pop })))))
2451      | AST.External efd ->
2452        Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2453          (eval_external_call p efd args dest st.st_no_pc) (fun st' ->
2454          Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { st_no_pc = st';
2455            pc = (succ_pc p st.pc nxt); last_pop = st.last_pop })))
2456
2457(** val eval_statement_no_pc :
2458    sem_params -> AST.ident List.list -> genv -> AST.ident ->
2459    Joint.joint_statement -> state -> state Errors.res **)
2460let eval_statement_no_pc p globals ge0 curr_id s st =
2461  match s with
2462  | Joint.Sequential (s0, next0) ->
2463    (match s0 with
2464     | Joint.COST_LABEL x ->
2465       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2466     | Joint.CALL (x, x0, x1) ->
2467       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2468     | Joint.COND (x, x0) ->
2469       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2470     | Joint.Step_seq s1 -> eval_seq_no_pc p globals ge0 curr_id s1 st)
2471  | Joint.Final x ->
2472    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2473  | Joint.FCOND (x0, x1, x2) ->
2474    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2475
2476(** val eval_return :
2477    sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2478    __ -> state -> __ **)
2479let eval_return p globals ge0 curr_id curr_ret st =
2480  Monad.m_bind0 (Monad.max_def Errors.res0)
2481    (Obj.magic
2482      (Errors.opt_to_res (List.Cons ((Errors.MSG
2483        ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2484        (PreIdentifiers.SymbolTag, curr_id)), List.Nil))))
2485        (ge0.stack_sizes curr_id))) (fun stack_size ->
2486    Monad.m_bind2 (Monad.max_def Errors.res0)
2487      (Obj.magic (p.spp'.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
2488      (fun st' call_pc ->
2489      Monad.m_bind0 (Monad.max_def Errors.res0)
2490        (Obj.magic
2491          (next_of_call_pc p globals
2492            (let p0 = spp'__o__spp p in
2493            let globals0 = globals in let g = ge0 in g.ge) call_pc))
2494        (fun nxt ->
2495        let st'' =
2496          set_last_pop p.spp'.msu_pars.st_pars
2497            (decrement_stack_usage p.spp'.msu_pars.st_pars stack_size st')
2498            call_pc
2499        in
2500        Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st''))))
2501
2502(** val eval_tailcall :
2503    sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2504    (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __
2505    -> state_pc -> __ **)
2506let eval_tailcall p globals ge0 f args curr_f curr_ret st =
2507  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2508    (let x =
2509       IOMonad.err_to_io
2510         (Obj.magic
2511           (block_of_call p globals
2512             (let p0 = spp'__o__spp p in
2513             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
2514     in
2515    Obj.magic x) (fun bl ->
2516    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2517      (let x =
2518         IOMonad.err_to_io
2519           (fetch_function
2520             (let p0 = spp'__o__spp p in
2521             let globals0 = globals in let g = ge0 in g.ge) bl)
2522       in
2523      Obj.magic x) (fun i fd ->
2524      match fd with
2525      | AST.Internal ifd ->
2526        Obj.magic
2527          (IOMonad.err_to_io
2528            (Obj.magic
2529              (Monad.m_bind0 (Monad.max_def Errors.res0)
2530                (Obj.magic
2531                  (Errors.opt_to_res (List.Cons ((Errors.MSG
2532                    ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2533                    (PreIdentifiers.SymbolTag, curr_f)), List.Nil))))
2534                    (ge0.stack_sizes curr_f))) (fun stack_size ->
2535                let st' =
2536                  decrement_stack_usage (spp'__o__msu_pars__o__st_pars p)
2537                    stack_size st.st_no_pc
2538                in
2539                Monad.m_bind0 (Monad.max_def Errors.res0)
2540                  (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2541                    st') (fun st'' ->
2542                  let pc0 =
2543                    pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2544                  in
2545                  Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2546                    st''; pc = pc0; last_pop = st.last_pop })))))
2547      | AST.External efd ->
2548        Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2549          (eval_external_call p efd args curr_ret st.st_no_pc) (fun st' ->
2550          Obj.magic
2551            (IOMonad.err_to_io
2552              (Obj.magic
2553                (eval_return p globals ge0 curr_f curr_ret st.st_no_pc))))))
2554
2555(** val eval_statement_advance :
2556    sem_params -> AST.ident List.list -> genv -> AST.ident ->
2557    Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
2558    -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **)
2559let eval_statement_advance p g ge0 curr_id curr_fn s st =
2560  match s with
2561  | Joint.Sequential (s0, nxt) ->
2562    (match s0 with
2563     | Joint.COST_LABEL x ->
2564       Obj.magic
2565         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
2566     | Joint.CALL (f, args, dest) ->
2567       Obj.magic (eval_call p g ge0 f args dest nxt st)
2568     | Joint.COND (a, l) ->
2569       IOMonad.err_to_io
2570         (Obj.magic
2571           (Monad.m_bind0 (Monad.max_def Errors.res0)
2572             (Obj.magic
2573               (acca_retrieve
2574                 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2575                 p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2576             Monad.m_bind0 (Monad.max_def Errors.res0)
2577               (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2578               match b with
2579               | Bool.True ->
2580                 Obj.magic
2581                   (goto p g
2582                     (let p0 = spp'__o__spp p in
2583                     let globals = g in let g0 = ge0 in g0.ge) l st)
2584               | Bool.False ->
2585                 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
2586     | Joint.Step_seq x ->
2587       Obj.magic
2588         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st)))
2589  | Joint.Final s0 ->
2590    let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
2591    (match s0 with
2592     | Joint.GOTO l ->
2593       IOMonad.err_to_io
2594         (goto p g
2595           (let p0 = spp'__o__spp p in
2596           let globals = g in let g0 = ge0 in g0.ge) l st)
2597     | Joint.RETURN ->
2598       IOMonad.err_to_io
2599         (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
2600     | Joint.TAILCALL (f, args) ->
2601       Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
2602  | Joint.FCOND (a, lbltrue, lblfalse) ->
2603    IOMonad.err_to_io
2604      (Obj.magic
2605        (Monad.m_bind0 (Monad.max_def Errors.res0)
2606          (Obj.magic
2607            (acca_retrieve
2608              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2609              p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2610          Monad.m_bind0 (Monad.max_def Errors.res0)
2611            (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2612            match b with
2613            | Bool.True ->
2614              Obj.magic
2615                (goto p g
2616                  (let p0 = spp'__o__spp p in
2617                  let globals = g in let g0 = ge0 in g0.ge) lbltrue st)
2618            | Bool.False ->
2619              Obj.magic
2620                (goto p g
2621                  (let p0 = spp'__o__spp p in
2622                  let globals = g in let g0 = ge0 in g0.ge) lblfalse st)))))
2623
2624(** val eval_state :
2625    sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
2626    IO.io_in, state_pc) IOMonad.iO **)
2627let eval_state p globals ge0 st =
2628  Obj.magic
2629    (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
2630      (let x =
2631         IOMonad.err_to_io
2632           (fetch_statement p globals
2633             (let p0 = spp'__o__spp p in
2634             let globals0 = globals in let g = ge0 in g.ge) st.pc)
2635       in
2636      Obj.magic x) (fun id fn s ->
2637      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2638        (let x =
2639           IOMonad.err_to_io
2640             (eval_statement_no_pc p globals ge0 id s st.st_no_pc)
2641         in
2642        Obj.magic x) (fun st' ->
2643        let st'' = set_no_pc (spp'__o__msu_pars__o__st_pars p) st' st in
2644        Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))
2645
Note: See TracBrowser for help on using the repository browser.