source: extracted/joint_semantics.ml @ 2933

Last change on this file since 2933 was 2933, checked in by sacerdot, 6 years ago

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 106.7 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_25736 =
144  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
145    get_pc_from_label0 } = x_25736
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_25738 =
154  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
155    get_pc_from_label0 } = x_25738
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_25740 =
164  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
165    get_pc_from_label0 } = x_25740
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_25742 =
174  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
175    get_pc_from_label0 } = x_25742
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_25744 =
184  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
185    get_pc_from_label0 } = x_25744
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_25746 =
194  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
195    get_pc_from_label0 } = x_25746
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_25766 =
344  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
345    load_sp0; save_sp = save_sp0 } = x_25766
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_25768 =
354  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
355    load_sp0; save_sp = save_sp0 } = x_25768
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_25770 =
364  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
365    load_sp0; save_sp = save_sp0 } = x_25770
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_25772 =
374  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
375    load_sp0; save_sp = save_sp0 } = x_25772
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_25774 =
384  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
385    load_sp0; save_sp = save_sp0 } = x_25774
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_25776 =
394  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
395    load_sp0; save_sp = save_sp0 } = x_25776
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_25802 -> h_one_is x_25802
475| Both_is (x_25804, x_25803) -> h_both_is x_25804 x_25803
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_25809 -> h_one_is x_25809
483| Both_is (x_25811, x_25810) -> h_both_is x_25811 x_25810
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_25816 -> h_one_is x_25816
491| Both_is (x_25818, x_25817) -> h_both_is x_25818 x_25817
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_25823 -> h_one_is x_25823
499| Both_is (x_25825, x_25824) -> h_both_is x_25825 x_25824
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_25830 -> h_one_is x_25830
507| Both_is (x_25832, x_25831) -> h_both_is x_25832 x_25831
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_25837 -> h_one_is x_25837
515| Both_is (x_25839, x_25838) -> h_both_is x_25839 x_25838
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
595(** val state_rect_Type4 :
596    sem_state_params -> (__ Types.option -> internal_stack ->
597    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
598let rec state_rect_Type4 semp h_mk_state x_25887 =
599  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
600    m = m0 } = x_25887
601  in
602  h_mk_state st_frms0 istack0 carry0 regs0 m0
603
604(** val state_rect_Type5 :
605    sem_state_params -> (__ Types.option -> internal_stack ->
606    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
607let rec state_rect_Type5 semp h_mk_state x_25889 =
608  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
609    m = m0 } = x_25889
610  in
611  h_mk_state st_frms0 istack0 carry0 regs0 m0
612
613(** val state_rect_Type3 :
614    sem_state_params -> (__ Types.option -> internal_stack ->
615    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
616let rec state_rect_Type3 semp h_mk_state x_25891 =
617  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
618    m = m0 } = x_25891
619  in
620  h_mk_state st_frms0 istack0 carry0 regs0 m0
621
622(** val state_rect_Type2 :
623    sem_state_params -> (__ Types.option -> internal_stack ->
624    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
625let rec state_rect_Type2 semp h_mk_state x_25893 =
626  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
627    m = m0 } = x_25893
628  in
629  h_mk_state st_frms0 istack0 carry0 regs0 m0
630
631(** val state_rect_Type1 :
632    sem_state_params -> (__ Types.option -> internal_stack ->
633    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
634let rec state_rect_Type1 semp h_mk_state x_25895 =
635  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
636    m = m0 } = x_25895
637  in
638  h_mk_state st_frms0 istack0 carry0 regs0 m0
639
640(** val state_rect_Type0 :
641    sem_state_params -> (__ Types.option -> internal_stack ->
642    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
643let rec state_rect_Type0 semp h_mk_state x_25897 =
644  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
645    m = m0 } = x_25897
646  in
647  h_mk_state st_frms0 istack0 carry0 regs0 m0
648
649(** val st_frms : sem_state_params -> state -> __ Types.option **)
650let rec st_frms semp xxx =
651  xxx.st_frms
652
653(** val istack : sem_state_params -> state -> internal_stack **)
654let rec istack semp xxx =
655  xxx.istack
656
657(** val carry : sem_state_params -> state -> ByteValues.bebit **)
658let rec carry semp xxx =
659  xxx.carry
660
661(** val regs : sem_state_params -> state -> __ **)
662let rec regs semp xxx =
663  xxx.regs
664
665(** val m : sem_state_params -> state -> BEMem.bemem **)
666let rec m semp xxx =
667  xxx.m
668
669(** val state_inv_rect_Type4 :
670    sem_state_params -> state -> (__ Types.option -> internal_stack ->
671    ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
672let state_inv_rect_Type4 x1 hterm h1 =
673  let hcut = state_rect_Type4 x1 h1 hterm in hcut __
674
675(** val state_inv_rect_Type3 :
676    sem_state_params -> state -> (__ Types.option -> internal_stack ->
677    ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
678let state_inv_rect_Type3 x1 hterm h1 =
679  let hcut = state_rect_Type3 x1 h1 hterm in hcut __
680
681(** val state_inv_rect_Type2 :
682    sem_state_params -> state -> (__ Types.option -> internal_stack ->
683    ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
684let state_inv_rect_Type2 x1 hterm h1 =
685  let hcut = state_rect_Type2 x1 h1 hterm in hcut __
686
687(** val state_inv_rect_Type1 :
688    sem_state_params -> state -> (__ Types.option -> internal_stack ->
689    ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
690let state_inv_rect_Type1 x1 hterm h1 =
691  let hcut = state_rect_Type1 x1 h1 hterm in hcut __
692
693(** val state_inv_rect_Type0 :
694    sem_state_params -> state -> (__ Types.option -> internal_stack ->
695    ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
696let state_inv_rect_Type0 x1 hterm h1 =
697  let hcut = state_rect_Type0 x1 h1 hterm in hcut __
698
699(** val state_discr : sem_state_params -> state -> state -> __ **)
700let state_discr a1 x y =
701  Logic.eq_rect_Type2 x
702    (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4 } = x in
703    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
704
705(** val state_jmdiscr : sem_state_params -> state -> state -> __ **)
706let state_jmdiscr a1 x y =
707  Logic.eq_rect_Type2 x
708    (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4 } = x in
709    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
710
711(** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **)
712let sp p st =
713  p.load_sp st.regs
714
715type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
716                  last_pop : ByteValues.program_counter }
717
718(** val state_pc_rect_Type4 :
719    sem_state_params -> (state -> ByteValues.program_counter ->
720    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
721let rec state_pc_rect_Type4 semp h_mk_state_pc x_25913 =
722  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25913 in
723  h_mk_state_pc st_no_pc0 pc0 last_pop0
724
725(** val state_pc_rect_Type5 :
726    sem_state_params -> (state -> ByteValues.program_counter ->
727    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
728let rec state_pc_rect_Type5 semp h_mk_state_pc x_25915 =
729  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25915 in
730  h_mk_state_pc st_no_pc0 pc0 last_pop0
731
732(** val state_pc_rect_Type3 :
733    sem_state_params -> (state -> ByteValues.program_counter ->
734    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
735let rec state_pc_rect_Type3 semp h_mk_state_pc x_25917 =
736  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25917 in
737  h_mk_state_pc st_no_pc0 pc0 last_pop0
738
739(** val state_pc_rect_Type2 :
740    sem_state_params -> (state -> ByteValues.program_counter ->
741    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
742let rec state_pc_rect_Type2 semp h_mk_state_pc x_25919 =
743  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25919 in
744  h_mk_state_pc st_no_pc0 pc0 last_pop0
745
746(** val state_pc_rect_Type1 :
747    sem_state_params -> (state -> ByteValues.program_counter ->
748    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
749let rec state_pc_rect_Type1 semp h_mk_state_pc x_25921 =
750  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25921 in
751  h_mk_state_pc st_no_pc0 pc0 last_pop0
752
753(** val state_pc_rect_Type0 :
754    sem_state_params -> (state -> ByteValues.program_counter ->
755    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
756let rec state_pc_rect_Type0 semp h_mk_state_pc x_25923 =
757  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25923 in
758  h_mk_state_pc st_no_pc0 pc0 last_pop0
759
760(** val st_no_pc : sem_state_params -> state_pc -> state **)
761let rec st_no_pc semp xxx =
762  xxx.st_no_pc
763
764(** val pc : sem_state_params -> state_pc -> ByteValues.program_counter **)
765let rec pc semp xxx =
766  xxx.pc
767
768(** val last_pop :
769    sem_state_params -> state_pc -> ByteValues.program_counter **)
770let rec last_pop semp xxx =
771  xxx.last_pop
772
773(** val state_pc_inv_rect_Type4 :
774    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
775    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
776let state_pc_inv_rect_Type4 x1 hterm h1 =
777  let hcut = state_pc_rect_Type4 x1 h1 hterm in hcut __
778
779(** val state_pc_inv_rect_Type3 :
780    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
781    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
782let state_pc_inv_rect_Type3 x1 hterm h1 =
783  let hcut = state_pc_rect_Type3 x1 h1 hterm in hcut __
784
785(** val state_pc_inv_rect_Type2 :
786    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
787    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
788let state_pc_inv_rect_Type2 x1 hterm h1 =
789  let hcut = state_pc_rect_Type2 x1 h1 hterm in hcut __
790
791(** val state_pc_inv_rect_Type1 :
792    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
793    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
794let state_pc_inv_rect_Type1 x1 hterm h1 =
795  let hcut = state_pc_rect_Type1 x1 h1 hterm in hcut __
796
797(** val state_pc_inv_rect_Type0 :
798    sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
799    ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
800let state_pc_inv_rect_Type0 x1 hterm h1 =
801  let hcut = state_pc_rect_Type0 x1 h1 hterm in hcut __
802
803(** val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __ **)
804let state_pc_discr a1 x y =
805  Logic.eq_rect_Type2 x
806    (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
807    Obj.magic (fun _ dH -> dH __ __ __)) y
808
809(** val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __ **)
810let state_pc_jmdiscr a1 x y =
811  Logic.eq_rect_Type2 x
812    (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
813    Obj.magic (fun _ dH -> dH __ __ __)) y
814
815(** val dpi1__o__st_no_pc__o__inject :
816    sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0 **)
817let dpi1__o__st_no_pc__o__inject x0 x3 =
818  x3.Types.dpi1.st_no_pc
819
820(** val eject__o__st_no_pc__o__inject :
821    sem_state_params -> state_pc Types.sig0 -> state Types.sig0 **)
822let eject__o__st_no_pc__o__inject x0 x3 =
823  (Types.pi1 x3).st_no_pc
824
825(** val st_no_pc__o__inject :
826    sem_state_params -> state_pc -> state Types.sig0 **)
827let st_no_pc__o__inject x0 x2 =
828  x2.st_no_pc
829
830(** val dpi1__o__st_no_pc :
831    sem_state_params -> (state_pc, 'a1) Types.dPair -> state **)
832let dpi1__o__st_no_pc x0 x2 =
833  x2.Types.dpi1.st_no_pc
834
835(** val eject__o__st_no_pc :
836    sem_state_params -> state_pc Types.sig0 -> state **)
837let eject__o__st_no_pc x0 x2 =
838  (Types.pi1 x2).st_no_pc
839
840(** val exit_pc : ByteValues.program_counter **)
841let exit_pc =
842  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
843    ByteValues.pc_offset = Positive.One }
844
845(** val null_pc : Positive.pos -> ByteValues.program_counter **)
846let null_pc pos =
847  { ByteValues.pc_block = Pointers.dummy_block_code; ByteValues.pc_offset =
848    pos }
849
850(** val set_m : sem_state_params -> BEMem.bemem -> state -> state **)
851let set_m p m0 st =
852  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
853    st.regs; m = m0 }
854
855(** val set_regs : sem_state_params -> __ -> state -> state **)
856let set_regs p regs0 st =
857  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0;
858    m = st.m }
859
860(** val set_sp :
861    sem_state_params -> ByteValues.xpointer -> state -> state **)
862let set_sp p sp0 st =
863  let regs' = p.save_sp st.regs sp0 in
864  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs';
865  m = st.m }
866
867(** val set_carry :
868    sem_state_params -> ByteValues.bebit -> state -> state **)
869let set_carry p carry0 st =
870  { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs;
871    m = st.m }
872
873(** val set_istack : sem_state_params -> internal_stack -> state -> state **)
874let set_istack p is st =
875  { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m =
876    st.m }
877
878(** val set_pc :
879    sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc **)
880let set_pc p pc0 st =
881  { st_no_pc = st.st_no_pc; pc = pc0; last_pop = st.last_pop }
882
883(** val set_no_pc : sem_state_params -> state -> state_pc -> state_pc **)
884let set_no_pc p s st =
885  { st_no_pc = s; pc = st.pc; last_pop = st.last_pop }
886
887(** val set_last_pop :
888    sem_state_params -> ByteValues.program_counter -> (state,
889    ByteValues.program_counter) Types.prod -> state_pc **)
890let set_last_pop p s st =
891  { st_no_pc = st.Types.fst; pc = st.Types.snd; last_pop = s }
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 }
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_25978 =
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_25978
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_25980 =
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_25980
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_25982 =
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_25982
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_25984 =
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_25984
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_25986 =
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_25986
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_25988 =
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_25988
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 sem_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 sem_params_rect_Type4 :
1760    (Joint.params -> Joint.joint_closed_internal_function
1761    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1762    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1763let rec sem_params_rect_Type4 h_mk_sem_params x_26058 =
1764  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1765    point_of_offset = point_of_offset0 } = x_26058
1766  in
1767  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1768
1769(** val sem_params_rect_Type5 :
1770    (Joint.params -> Joint.joint_closed_internal_function
1771    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1772    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1773let rec sem_params_rect_Type5 h_mk_sem_params x_26060 =
1774  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1775    point_of_offset = point_of_offset0 } = x_26060
1776  in
1777  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1778
1779(** val sem_params_rect_Type3 :
1780    (Joint.params -> Joint.joint_closed_internal_function
1781    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1782    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1783let rec sem_params_rect_Type3 h_mk_sem_params x_26062 =
1784  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1785    point_of_offset = point_of_offset0 } = x_26062
1786  in
1787  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1788
1789(** val sem_params_rect_Type2 :
1790    (Joint.params -> Joint.joint_closed_internal_function
1791    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1792    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1793let rec sem_params_rect_Type2 h_mk_sem_params x_26064 =
1794  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1795    point_of_offset = point_of_offset0 } = x_26064
1796  in
1797  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1798
1799(** val sem_params_rect_Type1 :
1800    (Joint.params -> Joint.joint_closed_internal_function
1801    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1802    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1803let rec sem_params_rect_Type1 h_mk_sem_params x_26066 =
1804  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1805    point_of_offset = point_of_offset0 } = x_26066
1806  in
1807  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1808
1809(** val sem_params_rect_Type0 :
1810    (Joint.params -> Joint.joint_closed_internal_function
1811    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1812    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
1813let rec sem_params_rect_Type0 h_mk_sem_params x_26068 =
1814  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1815    point_of_offset = point_of_offset0 } = x_26068
1816  in
1817  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
1818
1819(** val spp : sem_params -> Joint.params **)
1820let rec spp xxx =
1821  xxx.spp
1822
1823(** val msu_pars :
1824    sem_params -> Joint.joint_closed_internal_function
1825    sem_unserialized_params **)
1826let rec msu_pars xxx =
1827  xxx.msu_pars
1828
1829(** val offset_of_point : sem_params -> __ -> Positive.pos **)
1830let rec offset_of_point xxx =
1831  xxx.offset_of_point
1832
1833(** val point_of_offset : sem_params -> Positive.pos -> __ **)
1834let rec point_of_offset xxx =
1835  xxx.point_of_offset
1836
1837(** val sem_params_inv_rect_Type4 :
1838    sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1839    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1840    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1841let sem_params_inv_rect_Type4 hterm h1 =
1842  let hcut = sem_params_rect_Type4 h1 hterm in hcut __
1843
1844(** val sem_params_inv_rect_Type3 :
1845    sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1846    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1847    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1848let sem_params_inv_rect_Type3 hterm h1 =
1849  let hcut = sem_params_rect_Type3 h1 hterm in hcut __
1850
1851(** val sem_params_inv_rect_Type2 :
1852    sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1853    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1854    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1855let sem_params_inv_rect_Type2 hterm h1 =
1856  let hcut = sem_params_rect_Type2 h1 hterm in hcut __
1857
1858(** val sem_params_inv_rect_Type1 :
1859    sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1860    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1861    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1862let sem_params_inv_rect_Type1 hterm h1 =
1863  let hcut = sem_params_rect_Type1 h1 hterm in hcut __
1864
1865(** val sem_params_inv_rect_Type0 :
1866    sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1867    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1868    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1869let sem_params_inv_rect_Type0 hterm h1 =
1870  let hcut = sem_params_rect_Type0 h1 hterm in hcut __
1871
1872(** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
1873let sem_params_jmdiscr x y =
1874  Logic.eq_rect_Type2 x
1875    (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset =
1876       a3 } = x
1877     in
1878    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1879
1880(** val spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
1881let spp__o__stmt_pars x0 =
1882  x0.spp.Joint.stmt_pars
1883
1884(** val spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params **)
1885let spp__o__stmt_pars__o__uns_pars x0 =
1886  Joint.stmt_pars__o__uns_pars x0.spp
1887
1888(** val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1889    sem_params -> Joint.unserialized_params **)
1890let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
1891  Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp
1892
1893(** val msu_pars__o__st_pars : sem_params -> sem_state_params **)
1894let msu_pars__o__st_pars x0 =
1895  x0.msu_pars.st_pars
1896
1897(** val pc_of_point :
1898    sem_params -> Pointers.block Types.sig0 -> __ ->
1899    ByteValues.program_counter **)
1900let pc_of_point p bl pt =
1901  { ByteValues.pc_block = bl; ByteValues.pc_offset = (p.offset_of_point pt) }
1902
1903(** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **)
1904let point_of_pc p ptr =
1905  p.point_of_offset ptr.ByteValues.pc_offset
1906
1907(** val fetch_statement :
1908    sem_params -> AST.ident List.list -> Joint.joint_function
1909    Globalenvs.genv_t -> ByteValues.program_counter -> ((AST.ident,
1910    Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
1911    Types.prod Errors.res **)
1912let fetch_statement p globals ge0 ptr =
1913  Obj.magic
1914    (Monad.m_bind2 (Monad.max_def Errors.res0)
1915      (Obj.magic (fetch_internal_function ge0 ptr.ByteValues.pc_block))
1916      (fun id fn ->
1917      let pt = point_of_pc p ptr in
1918      Monad.m_bind0 (Monad.max_def Errors.res0)
1919        (Obj.magic
1920          (Errors.opt_to_res
1921            (Errors.msg ErrorMessages.ProgramCounterOutOfCode)
1922            (p.spp.Joint.stmt_at globals (Types.pi1 fn).Joint.joint_if_code
1923              pt))) (fun stmt ->
1924        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1925          { Types.fst = id; Types.snd = fn }; Types.snd = stmt })))
1926
1927(** val pc_of_label :
1928    sem_params -> AST.ident List.list -> Joint.joint_function
1929    Globalenvs.genv_t -> Pointers.block Types.sig0 -> Graphs.label ->
1930    ByteValues.program_counter Errors.res **)
1931let pc_of_label p globals ge0 bl lbl =
1932  Obj.magic
1933    (Monad.m_bind2 (Monad.max_def Errors.res0)
1934      (Obj.magic (fetch_internal_function ge0 bl)) (fun i fn ->
1935      Monad.m_bind0 (Monad.max_def Errors.res0)
1936        (Obj.magic
1937          (Errors.opt_to_res (List.Cons ((Errors.MSG
1938            ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
1939            (PreIdentifiers.LabelTag, lbl)), List.Nil))))
1940            (p.spp.Joint.point_of_label globals
1941              (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt ->
1942        Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block =
1943          bl; ByteValues.pc_offset = (p.offset_of_point pt) })))
1944
1945(** val succ_pc :
1946    sem_params -> ByteValues.program_counter -> __ ->
1947    ByteValues.program_counter **)
1948let succ_pc p ptr nxt =
1949  let curr = point_of_pc p ptr in
1950  pc_of_point p ptr.ByteValues.pc_block (p.spp.Joint.point_of_succ curr nxt)
1951
1952(** val goto :
1953    sem_params -> AST.ident List.list -> Joint.joint_function
1954    Globalenvs.genv_t -> Graphs.label -> state_pc -> state_pc Errors.res **)
1955let goto p globals ge0 l st =
1956  Obj.magic
1957    (Monad.m_bind0 (Monad.max_def Errors.res0)
1958      (Obj.magic (pc_of_label p globals ge0 st.pc.ByteValues.pc_block l))
1959      (fun newpc ->
1960      Monad.m_return0 (Monad.max_def Errors.res0)
1961        (set_pc (msu_pars__o__st_pars p) newpc st)))
1962
1963(** val next : sem_params -> __ -> state_pc -> state_pc **)
1964let next p l st =
1965  let newpc = succ_pc p st.pc l in set_pc (msu_pars__o__st_pars p) newpc st
1966
1967(** val next_of_call_pc :
1968    sem_params -> AST.ident List.list -> Joint.joint_function
1969    Globalenvs.genv_t -> ByteValues.program_counter -> __ Errors.res **)
1970let next_of_call_pc p globals ge0 pc0 =
1971  Obj.magic
1972    (Monad.m_bind2 (Monad.max_def Errors.res0)
1973      (Obj.magic (fetch_statement p globals ge0 pc0)) (fun id_fn stmt ->
1974      match stmt with
1975      | Joint.Sequential (s, nxt) ->
1976        (match s with
1977         | Joint.COST_LABEL x ->
1978           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1979             ErrorMessages.NoSuccessor), List.Nil)))
1980         | Joint.CALL (x, x0, x1) ->
1981           Monad.m_return0 (Monad.max_def Errors.res0) nxt
1982         | Joint.COND (x, x0) ->
1983           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1984             ErrorMessages.NoSuccessor), List.Nil)))
1985         | Joint.Step_seq x ->
1986           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1987             ErrorMessages.NoSuccessor), List.Nil))))
1988      | Joint.Final x ->
1989        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1990          ErrorMessages.NoSuccessor), List.Nil)))
1991      | Joint.FCOND (x0, x1, x2) ->
1992        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1993          ErrorMessages.NoSuccessor), List.Nil)))))
1994
1995(** val eval_seq_no_pc :
1996    sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1997    -> state -> state Errors.res **)
1998let eval_seq_no_pc p globals ge0 curr_id seq st =
1999  match seq with
2000  | Joint.COMMENT x ->
2001prerr_endline "COMMENT";
2002    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2003  | Joint.MOVE dst_src ->
2004prerr_endline "MOVE";
2005    Obj.magic
2006      (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2007        p.msu_pars st dst_src)
2008  | Joint.POP dst ->
2009prerr_endline "POP";
2010    Obj.magic
2011      (Monad.m_bind2 (Monad.max_def Errors.res0)
2012        (Obj.magic (pop (msu_pars__o__st_pars p) st)) (fun v st' ->
2013        Obj.magic
2014          (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2015            p.msu_pars dst v st')))
2016  | Joint.PUSH src ->
2017prerr_endline "PUSH";
2018    Obj.magic
2019      (Monad.m_bind0 (Monad.max_def Errors.res0)
2020        (Obj.magic
2021          (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2022            p.msu_pars st src)) (fun v ->
2023        Obj.magic (push (msu_pars__o__st_pars p) st v)))
2024  | Joint.ADDRESS (id, ldest, hdest) ->
2025prerr_endline "ADDRESS";
2026    let addr_block =
2027      Option.opt_safe
2028        (Globalenvs.find_symbol
2029          (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
2030          id)
2031    in
2032    let { Types.fst = laddr; Types.snd = haddr } =
2033      ByteValues.beval_pair_of_pointer { Pointers.pblock = addr_block;
2034        Pointers.poff = Pointers.zero_offset }
2035    in
2036    Obj.magic
2037      (Monad.m_bind0 (Monad.max_def Errors.res0)
2038        (Obj.magic
2039          (dpl_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.msu_pars
2040            ldest laddr st)) (fun st' ->
2041        Obj.magic
2042          (dph_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.msu_pars
2043            hdest haddr st')))
2044  | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) ->
2045    Obj.magic
2046      (Monad.m_bind0 (Monad.max_def Errors.res0)
2047        (Obj.magic
2048          (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2049            p.msu_pars st sacc_a_reg)) (fun v1 ->
2050        Monad.m_bind0 (Monad.max_def Errors.res0)
2051          (Obj.magic
2052            (accb_arg_retrieve
2053              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) p.msu_pars st
2054              sacc_b_reg)) (fun v2 ->
2055          Monad.m_bind2 (Monad.max_def Errors.res0)
2056            (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' ->
2057            Monad.m_bind0 (Monad.max_def Errors.res0)
2058              (Obj.magic
2059                (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2060                  p.msu_pars dacc_a_reg v1' st)) (fun st' ->
2061              Obj.magic
2062                (accb_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2063                  p.msu_pars dacc_b_reg v2' st'))))))
2064  | Joint.OP1 (op, dacc_a, sacc_a) ->
2065prerr_endline "OP1";
2066    Obj.magic
2067      (Monad.m_bind0 (Monad.max_def Errors.res0)
2068        (Obj.magic
2069          (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2070            p.msu_pars st sacc_a)) (fun v ->
2071        Monad.m_bind0 (Monad.max_def Errors.res0)
2072          (Obj.magic (BackEndOps.be_op1 op v)) (fun v' ->
2073          Obj.magic
2074            (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2075              p.msu_pars dacc_a v' st))))
2076  | Joint.OP2 (op, dacc_a, sacc_a, src) ->
2077prerr_endline "OP2";
2078    Obj.magic
2079      (Monad.m_bind0 (Monad.max_def Errors.res0)
2080        (Obj.magic
2081          (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2082            p.msu_pars st sacc_a)) (fun v1 ->
2083        Monad.m_bind0 (Monad.max_def Errors.res0)
2084          (Obj.magic
2085            (snd_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2086              p.msu_pars st src)) (fun v2 ->
2087          Monad.m_bind2 (Monad.max_def Errors.res0)
2088            (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
2089            (fun v' carry0 ->
2090(if op = BackEndOps.Sub then
2091(if carry0 = ByteValues.BBbit Bool.True then prerr_endline "CARRY = 1" else prerr_endline "CARRY = 0"));
2092            Monad.m_bind0 (Monad.max_def Errors.res0)
2093              (Obj.magic
2094                (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2095                  p.msu_pars dacc_a v' st)) (fun st' ->
2096              Monad.m_return0 (Monad.max_def Errors.res0)
2097                (set_carry p.msu_pars.st_pars carry0 st'))))))
2098  | Joint.CLEAR_CARRY ->
2099prerr_endline "CLEAR_CARRY";
2100    Obj.magic
2101      (Monad.m_return0 (Monad.max_def Errors.res0)
2102        (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.False) st))
2103  | Joint.SET_CARRY ->
2104prerr_endline "SET_CARRY";
2105    Obj.magic
2106      (Monad.m_return0 (Monad.max_def Errors.res0)
2107        (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.True) st))
2108  | Joint.LOAD (dst, addrl, addrh) ->
2109prerr_endline "LOAD";
2110    Obj.magic
2111      (Monad.m_bind0 (Monad.max_def Errors.res0)
2112        (Obj.magic
2113          (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2114            p.msu_pars st addrh)) (fun vaddrh ->
2115        Monad.m_bind0 (Monad.max_def Errors.res0)
2116          (Obj.magic
2117            (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2118              p.msu_pars st addrl)) (fun vaddrl ->
2119          Monad.m_bind0 (Monad.max_def Errors.res0)
2120            (Obj.magic
2121              (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2122                vaddrh })) (fun vaddr ->
2123            Monad.m_bind0 (Monad.max_def Errors.res0)
2124              (Obj.magic
2125                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
2126                  (GenMem.beloadv st.m vaddr))) (fun v ->
2127              Obj.magic
2128                (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2129                  p.msu_pars dst v st))))))
2130  | Joint.STORE (addrl, addrh, src) ->
2131prerr_endline "STORE";
2132    Obj.magic
2133      (Monad.m_bind0 (Monad.max_def Errors.res0)
2134        (Obj.magic
2135          (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2136            p.msu_pars st addrh)) (fun vaddrh ->
2137        Monad.m_bind0 (Monad.max_def Errors.res0)
2138          (Obj.magic
2139            (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2140              p.msu_pars st addrl)) (fun vaddrl ->
2141          Monad.m_bind0 (Monad.max_def Errors.res0)
2142            (Obj.magic
2143              (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2144                vaddrh })) (fun vaddr ->
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) p.msu_pars
2149                  st src)) (fun v ->
2150              Monad.m_bind0 (Monad.max_def Errors.res0)
2151                (Obj.magic
2152                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
2153                    (GenMem.bestorev st.m vaddr v))) (fun m' ->
2154                Monad.m_return0 (Monad.max_def Errors.res0)
2155                  (set_m (msu_pars__o__st_pars p) m' st)))))))
2156  | Joint.Extension_seq c -> p.msu_pars.eval_ext_seq globals ge0 c curr_id st
2157
2158(** val code_block_of_block :
2159    Pointers.block -> Pointers.block Types.sig0 Types.option **)
2160let code_block_of_block bl =
2161  (match Pointers.block_region bl with
2162   | AST.XData -> (fun _ -> Types.None)
2163   | AST.Code -> (fun _ -> Types.Some bl)) __
2164
2165(** val block_of_funct_id :
2166    sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
2167    Pointers.block Types.sig0 Errors.res **)
2168let block_of_funct_id sp0 ge0 id =
2169  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2170    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
2171    (Obj.magic
2172      (Monad.m_bind0 (Monad.max_def Option.option)
2173        (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
2174        Obj.magic (code_block_of_block bl))))
2175
2176(** val block_of_call :
2177    sem_params -> AST.ident List.list -> Joint.joint_function
2178    Globalenvs.genv_t -> (PreIdentifiers.identifier, (__, __) Types.prod)
2179    Types.sum -> state -> __ **)
2180let block_of_call p globals ge0 f st =
2181  Monad.m_bind0 (Monad.max_def Errors.res0)
2182    (match f with
2183     | Types.Inl id ->
2184       Obj.magic
2185         (Errors.opt_to_res (List.Cons ((Errors.MSG
2186           ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
2187           (PreIdentifiers.SymbolTag, id)), List.Nil))))
2188           (Globalenvs.find_symbol ge0 id))
2189     | Types.Inr addr ->
2190       Monad.m_bind0 (Monad.max_def Errors.res0)
2191         (Obj.magic
2192           (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2193             p.msu_pars st addr.Types.fst)) (fun addr_l ->
2194         Monad.m_bind0 (Monad.max_def Errors.res0)
2195           (Obj.magic
2196             (dph_arg_retrieve
2197               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) p.msu_pars st
2198               addr.Types.snd)) (fun addr_h ->
2199           Monad.m_bind0 (Monad.max_def Errors.res0)
2200             (Obj.magic
2201               (ByteValues.pointer_of_bevals (List.Cons (addr_l, (List.Cons
2202                 (addr_h, List.Nil)))))) (fun ptr ->
2203             match BitVector.eq_bv Pointers.offset_size
2204                     (BitVector.zero Pointers.offset_size)
2205                     (Pointers.offv ptr.Pointers.poff) with
2206             | Bool.True ->
2207               Monad.m_return0 (Monad.max_def Errors.res0)
2208                 ptr.Pointers.pblock
2209             | Bool.False ->
2210               Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2211                 ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
2212                 ErrorMessages.BadPointer), List.Nil))))))))) (fun bl ->
2213    Obj.magic
2214      (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2215        (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil))))
2216        (code_block_of_block bl)))
2217
2218(** val eval_external_call :
2219    sem_params -> AST.external_function -> __ -> __ -> state -> __ **)
2220let eval_external_call p fn args dest st =
2221  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2222    (let x = IOMonad.err_to_io (p.msu_pars.fetch_external_args fn st args) in
2223    Obj.magic x) (fun params ->
2224    Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2225      (let x =
2226         IOMonad.err_to_io
2227           (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)
2228       in
2229      Obj.magic x) (fun evargs ->
2230      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2231        (Obj.magic
2232          (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
2233        (fun evres ->
2234        let vs = List.Cons
2235          ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil)
2236        in
2237        Obj.magic (IOMonad.err_to_io (p.msu_pars.set_result vs dest st)))))
2238
2239(** val eval_internal_call :
2240    sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2241    Joint.joint_internal_function -> __ -> state -> __ **)
2242let eval_internal_call p globals ge0 i fn args st =
2243  Monad.m_bind0 (Monad.max_def Errors.res0)
2244    (Obj.magic
2245      (Errors.opt_to_res (List.Cons ((Errors.MSG
2246        ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2247        (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i)))
2248    (fun stack_size ->
2249    Obj.magic
2250      (p.msu_pars.setup_call stack_size fn.Joint.joint_if_params args st))
2251
2252(** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **)
2253let is_inl = function
2254| Types.Inl x0 -> Bool.True
2255| Types.Inr x0 -> Bool.False
2256
2257(** val eval_call :
2258    sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2259    (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __ **)
2260let eval_call p globals ge0 f args dest nxt st =
2261  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2262    (let x =
2263       IOMonad.err_to_io
2264         (Obj.magic
2265           (block_of_call p globals
2266             (let p0 = p.spp in
2267             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
2268     in
2269    Obj.magic x) (fun bl ->
2270    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2271      (let x =
2272         IOMonad.err_to_io
2273           (fetch_function
2274             (let p0 = p.spp in
2275             let globals0 = globals in let g = ge0 in g.ge) bl)
2276       in
2277      Obj.magic x) (fun i fd ->
2278      match fd with
2279      | AST.Internal ifd ->
2280        Obj.magic
2281          (IOMonad.err_to_io
2282            (Obj.magic
2283              (Monad.m_bind0 (Monad.max_def Errors.res0)
2284                (Obj.magic
2285                  (p.msu_pars.save_frame
2286                    (kind_of_call
2287                      (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) f) dest
2288                    st)) (fun st' ->
2289                Monad.m_bind0 (Monad.max_def Errors.res0)
2290                  (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2291                    st') (fun st'' ->
2292                  let pc0 =
2293                    pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2294                  in
2295                  Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2296                    st''; pc = pc0; last_pop = st.last_pop })))))
2297      | AST.External efd ->
2298        Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2299          (eval_external_call p efd args dest st.st_no_pc) (fun st' ->
2300          Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { st_no_pc = st';
2301            pc = (succ_pc p st.pc nxt); last_pop = st.last_pop })))
2302
2303(** val eval_statement_no_pc :
2304    sem_params -> AST.ident List.list -> genv -> AST.ident ->
2305    Joint.joint_statement -> state -> state Errors.res **)
2306let eval_statement_no_pc p globals ge0 curr_id s st =
2307  match s with
2308  | Joint.Sequential (s0, next0) ->
2309    (match s0 with
2310     | Joint.COST_LABEL x ->
2311       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2312     | Joint.CALL (x, x0, x1) ->
2313       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2314     | Joint.COND (x, x0) ->
2315       Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2316     | Joint.Step_seq s1 -> eval_seq_no_pc p globals ge0 curr_id s1 st)
2317  | Joint.Final x ->
2318    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2319  | Joint.FCOND (x0, x1, x2) ->
2320    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2321
2322(** val eval_return :
2323    sem_params -> AST.ident List.list -> genv -> AST.ident -> __ -> state ->
2324    __ **)
2325let eval_return p globals ge0 curr_id curr_ret st =
2326prerr_endline "eval_return";
2327  Monad.m_bind0 (Monad.max_def Errors.res0)
2328    (Obj.magic (p.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
2329    (fun st' ->
2330    Monad.m_bind0 (Monad.max_def Errors.res0)
2331      (Obj.magic
2332        (next_of_call_pc p globals
2333          (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
2334          st'.Types.snd)) (fun nxt ->
2335      Monad.m_return0 (Monad.max_def Errors.res0)
2336        (next p nxt (set_last_pop p.msu_pars.st_pars st'.Types.snd st'))))
2337
2338(** val eval_tailcall :
2339    sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2340    (__, __) Types.prod) Types.sum -> __ -> AST.ident -> __ -> state_pc -> __ **)
2341let eval_tailcall p globals ge0 f args curr_f curr_ret st =
2342  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2343    (let x =
2344       IOMonad.err_to_io
2345         (Obj.magic
2346           (block_of_call p globals
2347             (let p0 = p.spp in
2348             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
2349     in
2350    Obj.magic x) (fun bl ->
2351    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2352      (let x =
2353         IOMonad.err_to_io
2354           (fetch_function
2355             (let p0 = p.spp in
2356             let globals0 = globals in let g = ge0 in g.ge) bl)
2357       in
2358      Obj.magic x) (fun i fd ->
2359      match fd with
2360      | AST.Internal ifd ->
2361        Obj.magic
2362          (IOMonad.err_to_io
2363            (Obj.magic
2364              (Monad.m_bind0 (Monad.max_def Errors.res0)
2365                (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2366                  st.st_no_pc) (fun st' ->
2367                let pc0 =
2368                  pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2369                in
2370                Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc = st';
2371                  pc = pc0; last_pop = st.last_pop }))))
2372      | AST.External efd ->
2373        Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2374          (eval_external_call p efd args curr_ret st.st_no_pc) (fun st' ->
2375          Obj.magic
2376            (IOMonad.err_to_io
2377              (Obj.magic
2378                (eval_return p globals ge0 curr_f curr_ret st.st_no_pc))))))
2379
2380(** val eval_statement_advance :
2381    sem_params -> AST.ident List.list -> genv -> AST.ident ->
2382    Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
2383    -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **)
2384let eval_statement_advance p g ge0 curr_id curr_fn s st =
2385  match s with
2386  | Joint.Sequential (s0, nxt) ->
2387    (match s0 with
2388     | Joint.COST_LABEL x ->
2389prerr_endline "COST";
2390       Obj.magic
2391         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
2392     | Joint.CALL (f, args, dest) ->
2393prerr_endline "CALL";
2394       Obj.magic (eval_call p g ge0 f args dest nxt st)
2395     | Joint.COND (a, l) ->
2396prerr_endline "COND";
2397       IOMonad.err_to_io
2398         (Obj.magic
2399           (Monad.m_bind0 (Monad.max_def Errors.res0)
2400             (Obj.magic
2401               (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2402                 p.msu_pars st.st_no_pc a)) (fun v ->
2403             Monad.m_bind0 (Monad.max_def Errors.res0)
2404               (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2405               match b with
2406               | Bool.True ->
2407                 Obj.magic
2408                   (goto p g
2409                     (let p0 = p.spp in
2410                     let globals = g in let g0 = ge0 in g0.ge) l st)
2411               | Bool.False ->
2412                 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
2413     | Joint.Step_seq x ->
2414       Obj.magic
2415         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st)))
2416  | Joint.Final s0 ->
2417    let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
2418    (match s0 with
2419     | Joint.GOTO l ->
2420prerr_endline "GOTO";
2421       IOMonad.err_to_io
2422         (goto p g
2423           (let p0 = p.spp in let globals = g in let g0 = ge0 in g0.ge) l st)
2424     | Joint.RETURN ->
2425prerr_endline "RETURN";
2426       IOMonad.err_to_io
2427         (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
2428     | Joint.TAILCALL (f, args) ->
2429prerr_endline "TAILCALL";
2430       Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
2431  | Joint.FCOND (a, lbltrue, lblfalse) ->
2432prerr_endline "FCOND";
2433    IOMonad.err_to_io
2434      (Obj.magic
2435        (Monad.m_bind0 (Monad.max_def Errors.res0)
2436          (Obj.magic
2437            (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
2438              p.msu_pars st.st_no_pc a)) (fun v ->
2439          Monad.m_bind0 (Monad.max_def Errors.res0)
2440            (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2441            match b with
2442            | Bool.True ->
2443              Obj.magic
2444                (goto p g
2445                  (let p0 = p.spp in
2446                  let globals = g in let g0 = ge0 in g0.ge) lbltrue st)
2447            | Bool.False ->
2448              Obj.magic
2449                (goto p g
2450                  (let p0 = p.spp in
2451                  let globals = g in let g0 = ge0 in g0.ge) lblfalse st)))))
2452
2453(** val eval_state :
2454    sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
2455    IO.io_in, state_pc) IOMonad.iO **)
2456let eval_state p globals ge0 st =
2457  Obj.magic
2458    (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
2459      (let x =
2460         IOMonad.err_to_io
2461           (fetch_statement p globals
2462             (let p0 = p.spp in
2463             let globals0 = globals in let g = ge0 in g.ge) st.pc)
2464       in
2465      Obj.magic x) (fun id fn s ->
2466prerr_endline ("ID == " ^ string_of_int (Glue.int_of_matitapos id));
2467       let res =
2468      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2469        (let x =
2470           IOMonad.err_to_io
2471             (eval_statement_no_pc p globals ge0 id s st.st_no_pc)
2472         in
2473        Obj.magic x) (fun st' ->
2474        let st'' = set_no_pc (msu_pars__o__st_pars p) st' st in
2475        Obj.magic (eval_statement_advance p globals ge0 id fn s st''))
2476    in
2477     match Obj.magic res with
2478     | Wrong e ->
2479        print_string "fun_";
2480        print_int (Glue.int_of_matitapos id);
2481        print_string ":";
2482        let point = pc_offset (pc (msu_pars__o__st_pars p) st) in
2483        print_int (Glue.int_of_matitapos point);
2484        print_string ":";
2485        res
2486     | _ -> res))
2487
2488(** val is_final :
2489    sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
2490    -> state_pc -> Integers.int Types.option **)
2491let is_final p globals ge0 exit st =
2492  Errors.res_to_opt
2493    (Obj.magic
2494      (Monad.m_bind3 (Monad.max_def Errors.res0)
2495        (Obj.magic
2496          (fetch_statement p globals
2497            (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
2498            st.pc)) (fun id fn s ->
2499        match s with
2500        | Joint.Sequential (x, x0) -> Obj.magic (Errors.Error List.Nil)
2501        | Joint.Final s' ->
2502          (match s' with
2503           | Joint.GOTO x -> Obj.magic (Errors.Error List.Nil)
2504           | Joint.RETURN ->
2505             let curr_ret = (Types.pi1 fn).Joint.joint_if_result in
2506             Monad.m_bind0 (Monad.max_def Errors.res0)
2507               (Obj.magic
2508                 (p.msu_pars.pop_frame globals ge0 id curr_ret st.st_no_pc))
2509               (fun st' ->
2510               match ByteValues.eq_program_counter st'.Types.snd exit with
2511               | Bool.True ->
2512                 Monad.m_bind0 (Monad.max_def Errors.res0)
2513                   (Obj.magic
2514                     (p.msu_pars.read_result globals
2515                       (let p0 = p.spp in
2516                       let globals0 = globals in let g = ge0 in g.ge)
2517                       curr_ret st.st_no_pc)) (fun vals ->
2518                   Obj.magic (ByteValues.word_of_list_beval vals))
2519               | Bool.False -> Obj.magic (Errors.Error List.Nil))
2520           | Joint.TAILCALL (x0, x1) -> Obj.magic (Errors.Error List.Nil))
2521        | Joint.FCOND (x0, x1, x2) -> Obj.magic (Errors.Error List.Nil))))
Note: See TracBrowser for help on using the repository browser.