source: extracted/joint_semantics.ml @ 2960

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

New extraction, it diverges in RTL execution now.

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