source: driver/extracted/joint_semantics.ml @ 3106

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

New extraction

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