source: extracted/rTLabs_semantics.ml @ 2731

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

Exported again.

File size: 85.2 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open ErrorMessages
22
23open Option
24
25open Setoids
26
27open Monad
28
29open Jmeq
30
31open Russell
32
33open Positive
34
35open PreIdentifiers
36
37open Errors
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open Globalenvs
96
97open BitVectorTrie
98
99open CostLabel
100
101open Events
102
103open IOMonad
104
105open IO
106
107open SmallstepExec
108
109open Graphs
110
111open Order
112
113open Registers
114
115open FrontEndOps
116
117open RTLabs_syntax
118
119type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
120
121type frame = { func : RTLabs_syntax.internal_function;
122               locals : Values.val0 Registers.register_env;
123               next : Graphs.label; sp : Pointers.block;
124               retdst : Registers.register Types.option }
125
126(** val frame_rect_Type4 :
127    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
128    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
129    -> 'a1) -> frame -> 'a1 **)
130let rec frame_rect_Type4 h_mk_frame x_1947 =
131  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
132    retdst0 } = x_1947
133  in
134  h_mk_frame func0 locals0 next0 __ sp0 retdst0
135
136(** val frame_rect_Type5 :
137    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
138    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
139    -> 'a1) -> frame -> 'a1 **)
140let rec frame_rect_Type5 h_mk_frame x_1949 =
141  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
142    retdst0 } = x_1949
143  in
144  h_mk_frame func0 locals0 next0 __ sp0 retdst0
145
146(** val frame_rect_Type3 :
147    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
148    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
149    -> 'a1) -> frame -> 'a1 **)
150let rec frame_rect_Type3 h_mk_frame x_1951 =
151  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
152    retdst0 } = x_1951
153  in
154  h_mk_frame func0 locals0 next0 __ sp0 retdst0
155
156(** val frame_rect_Type2 :
157    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
158    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
159    -> 'a1) -> frame -> 'a1 **)
160let rec frame_rect_Type2 h_mk_frame x_1953 =
161  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
162    retdst0 } = x_1953
163  in
164  h_mk_frame func0 locals0 next0 __ sp0 retdst0
165
166(** val frame_rect_Type1 :
167    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
168    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
169    -> 'a1) -> frame -> 'a1 **)
170let rec frame_rect_Type1 h_mk_frame x_1955 =
171  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
172    retdst0 } = x_1955
173  in
174  h_mk_frame func0 locals0 next0 __ sp0 retdst0
175
176(** val frame_rect_Type0 :
177    (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
178    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
179    -> 'a1) -> frame -> 'a1 **)
180let rec frame_rect_Type0 h_mk_frame x_1957 =
181  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
182    retdst0 } = x_1957
183  in
184  h_mk_frame func0 locals0 next0 __ sp0 retdst0
185
186(** val func : frame -> RTLabs_syntax.internal_function **)
187let rec func xxx =
188  xxx.func
189
190(** val locals : frame -> Values.val0 Registers.register_env **)
191let rec locals xxx =
192  xxx.locals
193
194(** val next : frame -> Graphs.label **)
195let rec next xxx =
196  xxx.next
197
198(** val sp : frame -> Pointers.block **)
199let rec sp xxx =
200  xxx.sp
201
202(** val retdst : frame -> Registers.register Types.option **)
203let rec retdst xxx =
204  xxx.retdst
205
206(** val frame_inv_rect_Type4 :
207    frame -> (RTLabs_syntax.internal_function -> Values.val0
208    Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
209    Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
210let frame_inv_rect_Type4 hterm h1 =
211  let hcut = frame_rect_Type4 h1 hterm in hcut __
212
213(** val frame_inv_rect_Type3 :
214    frame -> (RTLabs_syntax.internal_function -> Values.val0
215    Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
216    Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
217let frame_inv_rect_Type3 hterm h1 =
218  let hcut = frame_rect_Type3 h1 hterm in hcut __
219
220(** val frame_inv_rect_Type2 :
221    frame -> (RTLabs_syntax.internal_function -> Values.val0
222    Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
223    Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
224let frame_inv_rect_Type2 hterm h1 =
225  let hcut = frame_rect_Type2 h1 hterm in hcut __
226
227(** val frame_inv_rect_Type1 :
228    frame -> (RTLabs_syntax.internal_function -> Values.val0
229    Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
230    Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
231let frame_inv_rect_Type1 hterm h1 =
232  let hcut = frame_rect_Type1 h1 hterm in hcut __
233
234(** val frame_inv_rect_Type0 :
235    frame -> (RTLabs_syntax.internal_function -> Values.val0
236    Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
237    Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
238let frame_inv_rect_Type0 hterm h1 =
239  let hcut = frame_rect_Type0 h1 hterm in hcut __
240
241(** val frame_jmdiscr : frame -> frame -> __ **)
242let frame_jmdiscr x y =
243  Logic.eq_rect_Type2 x
244    (let { func = a0; locals = a1; next = a2; sp = a4; retdst = a5 } = x in
245    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
246
247(** val adv : Graphs.label -> frame -> frame **)
248let adv l f =
249  { func = f.func; locals = f.locals; next = l; sp = f.sp; retdst =
250    f.retdst }
251
252type state0 =
253| State of frame * frame List.list * GenMem.mem1
254| Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
255   * Values.val0 List.list * Registers.register Types.option
256   * frame List.list * GenMem.mem1
257| Returnstate of Values.val0 Types.option * Registers.register Types.option
258   * frame List.list * GenMem.mem1
259| Finalstate of Integers.int
260
261(** val state_rect_Type4 :
262    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
263    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
264    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
265    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
266    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
267    'a1 **)
268let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
269| State (f, fs, m) -> h_State f fs m
270| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
271| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
272| Finalstate r -> h_Finalstate r
273
274(** val state_rect_Type5 :
275    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
276    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
277    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
278    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
279    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
280    'a1 **)
281let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
282| State (f, fs, m) -> h_State f fs m
283| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
284| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
285| Finalstate r -> h_Finalstate r
286
287(** val state_rect_Type3 :
288    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
289    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
290    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
291    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
292    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
293    'a1 **)
294let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
295| State (f, fs, m) -> h_State f fs m
296| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
297| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
298| Finalstate r -> h_Finalstate r
299
300(** val state_rect_Type2 :
301    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
302    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
303    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
304    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
305    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
306    'a1 **)
307let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
308| State (f, fs, m) -> h_State f fs m
309| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
310| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
311| Finalstate r -> h_Finalstate r
312
313(** val state_rect_Type1 :
314    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
315    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
316    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
317    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
318    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
319    'a1 **)
320let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
321| State (f, fs, m) -> h_State f fs m
322| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
323| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
324| Finalstate r -> h_Finalstate r
325
326(** val state_rect_Type0 :
327    (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
328    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
329    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
330    -> (Values.val0 Types.option -> Registers.register Types.option -> frame
331    List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 ->
332    'a1 **)
333let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
334| State (f, fs, m) -> h_State f fs m
335| Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
336| Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
337| Finalstate r -> h_Finalstate r
338
339(** val state_inv_rect_Type4 :
340    state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
341    (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
342    List.list -> Registers.register Types.option -> frame List.list ->
343    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
344    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __
345    -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
346let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
347  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
348
349(** val state_inv_rect_Type3 :
350    state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
351    (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
352    List.list -> Registers.register Types.option -> frame List.list ->
353    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
354    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __
355    -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
356let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
357  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
358
359(** val state_inv_rect_Type2 :
360    state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
361    (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
362    List.list -> Registers.register Types.option -> frame List.list ->
363    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
364    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __
365    -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
366let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
367  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
368
369(** val state_inv_rect_Type1 :
370    state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
371    (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
372    List.list -> Registers.register Types.option -> frame List.list ->
373    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
374    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __
375    -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
376let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
377  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
378
379(** val state_inv_rect_Type0 :
380    state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
381    (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
382    List.list -> Registers.register Types.option -> frame List.list ->
383    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
384    Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __
385    -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
386let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
387  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
388
389(** val state_jmdiscr : state0 -> state0 -> __ **)
390let state_jmdiscr x y =
391  Logic.eq_rect_Type2 x
392    (match x with
393     | State (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
394     | Callstate (a0, a1, a2, a3, a4, a5) ->
395       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
396     | Returnstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
397     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
398
399(** val build_state :
400    frame -> frame List.list -> GenMem.mem1 -> Graphs.label -> state0 **)
401let build_state f fs m n =
402  State ((adv n f), fs, m)
403
404(** val next_instruction : frame -> RTLabs_syntax.statement **)
405let next_instruction f =
406  Identifiers.lookup_present PreIdentifiers.LabelTag
407    f.func.RTLabs_syntax.f_graph f.next
408
409(** val init_locals :
410    (Registers.register, AST.typ) Types.prod List.list -> Values.val0
411    Registers.register_env **)
412let init_locals =
413  List.foldr (fun idt en ->
414    let { Types.fst = id; Types.snd = ty } = idt in
415    Identifiers.add PreIdentifiers.RegisterTag en id Values.Vundef)
416    (Identifiers.empty_map PreIdentifiers.RegisterTag)
417
418(** val reg_store :
419    PreIdentifiers.identifier -> Values.val0 -> Values.val0
420    Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
421    Errors.res **)
422let reg_store reg v locals0 =
423  Identifiers.update0 PreIdentifiers.RegisterTag locals0 reg v
424
425(** val params_store :
426    (Registers.register, AST.typ) Types.prod List.list -> Values.val0
427    List.list -> Values.val0 Registers.register_env -> Values.val0
428    Registers.register_env Errors.res **)
429let rec params_store rs vs locals0 =
430  match rs with
431  | List.Nil ->
432    (match vs with
433     | List.Nil -> Errors.OK locals0
434     | List.Cons (x, x0) ->
435       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
436  | List.Cons (rt, rst) ->
437    (match vs with
438     | List.Nil ->
439       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
440     | List.Cons (v, vst) ->
441       let { Types.fst = r; Types.snd = ty } = rt in
442       let locals' = Identifiers.add PreIdentifiers.RegisterTag locals0 r v
443       in
444       params_store rst vst locals')
445
446(** val reg_retrieve :
447    Values.val0 Registers.register_env -> Registers.register -> Values.val0
448    Errors.res **)
449let reg_retrieve locals0 reg =
450  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
451    (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
452    (Identifiers.lookup0 PreIdentifiers.RegisterTag locals0 reg)
453
454(** val eval_statement :
455    genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0)
456    Types.prod) IOMonad.iO **)
457let eval_statement ge = function
458| State (f, fs, m) ->
459  let s = next_instruction f in
460  (match s with
461   | RTLabs_syntax.St_skip l ->
462     (fun _ ->
463       Obj.magic
464         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
465           Events.e0; Types.snd = (build_state f fs m l) }))
466   | RTLabs_syntax.St_cost (cl, l) ->
467     (fun _ ->
468       Obj.magic
469         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
470           (Events.echarge cl); Types.snd = (build_state f fs m l) }))
471   | RTLabs_syntax.St_const (x, r, cst, l) ->
472     (fun _ ->
473       IOMonad.err_to_io
474         (Obj.magic
475           (Monad.m_bind0 (Monad.max_def Errors.res0)
476             (Obj.magic
477               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
478                 (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge)
479                   f.sp cst))) (fun v ->
480             Monad.m_bind0 (Monad.max_def Errors.res0)
481               (Obj.magic (reg_store r v f.locals)) (fun locals0 ->
482               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
483                 Events.e0; Types.snd = (State ({ func = f.func; locals =
484                 locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) })))))
485   | RTLabs_syntax.St_op1 (x, x0, op0, dst, src, l) ->
486     (fun _ ->
487       IOMonad.err_to_io
488         (Obj.magic
489           (Monad.m_bind0 (Monad.max_def Errors.res0)
490             (Obj.magic (reg_retrieve f.locals src)) (fun v ->
491             Monad.m_bind0 (Monad.max_def Errors.res0)
492               (Obj.magic
493                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
494                   (FrontEndOps.eval_unop x0 x op0 v))) (fun v' ->
495               Monad.m_bind0 (Monad.max_def Errors.res0)
496                 (Obj.magic (reg_store dst v' f.locals)) (fun locals0 ->
497                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
498                   Events.e0; Types.snd = (State ({ func = f.func; locals =
499                   locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
500                   m)) }))))))
501   | RTLabs_syntax.St_op2 (x, x0, x1, op0, dst, src1, src2, l) ->
502     (fun _ ->
503       IOMonad.err_to_io
504         (Obj.magic
505           (Monad.m_bind0 (Monad.max_def Errors.res0)
506             (Obj.magic (reg_retrieve f.locals src1)) (fun v1 ->
507             Monad.m_bind0 (Monad.max_def Errors.res0)
508               (Obj.magic (reg_retrieve f.locals src2)) (fun v2 ->
509               Monad.m_bind0 (Monad.max_def Errors.res0)
510                 (Obj.magic
511                   (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
512                     (FrontEndOps.eval_binop m x0 x1 x op0 v1 v2)))
513                 (fun v' ->
514                 Monad.m_bind0 (Monad.max_def Errors.res0)
515                   (Obj.magic (reg_store dst v' f.locals)) (fun locals0 ->
516                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
517                     Events.e0; Types.snd = (State ({ func = f.func; locals =
518                     locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
519                     m)) })))))))
520   | RTLabs_syntax.St_load (chunk, addr, dst, l) ->
521     (fun _ ->
522       IOMonad.err_to_io
523         (Obj.magic
524           (Monad.m_bind0 (Monad.max_def Errors.res0)
525             (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr ->
526             Monad.m_bind0 (Monad.max_def Errors.res0)
527               (Obj.magic
528                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
529                   (FrontEndMem.loadv chunk m vaddr))) (fun v ->
530               Monad.m_bind0 (Monad.max_def Errors.res0)
531                 (Obj.magic (reg_store dst v f.locals)) (fun locals0 ->
532                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
533                   Events.e0; Types.snd = (State ({ func = f.func; locals =
534                   locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
535                   m)) }))))))
536   | RTLabs_syntax.St_store (chunk, addr, src, l) ->
537     (fun _ ->
538       IOMonad.err_to_io
539         (Obj.magic
540           (Monad.m_bind0 (Monad.max_def Errors.res0)
541             (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr ->
542             Monad.m_bind0 (Monad.max_def Errors.res0)
543               (Obj.magic (reg_retrieve f.locals src)) (fun v ->
544               Monad.m_bind0 (Monad.max_def Errors.res0)
545                 (Obj.magic
546                   (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
547                     (FrontEndMem.storev chunk m vaddr v))) (fun m' ->
548                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
549                   Events.e0; Types.snd = (build_state f fs m' l) }))))))
550   | RTLabs_syntax.St_call_id (id, args, dst, l) ->
551     (fun _ ->
552       IOMonad.err_to_io
553         (Obj.magic
554           (Monad.m_bind0 (Monad.max_def Errors.res0)
555             (Obj.magic
556               (Errors.opt_to_res (List.Cons ((Errors.MSG
557                 ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
558                 (PreIdentifiers.SymbolTag, id)), List.Nil))))
559                 (Globalenvs.find_symbol ge id))) (fun b ->
560             Monad.m_bind0 (Monad.max_def Errors.res0)
561               (Obj.magic
562                 (Errors.opt_to_res (List.Cons ((Errors.MSG
563                   ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
564                   (PreIdentifiers.SymbolTag, id)), List.Nil))))
565                   (Globalenvs.find_funct_ptr ge b))) (fun fd ->
566               Monad.m_bind0 (Monad.max_def Errors.res0)
567                 (Monad.m_list_map (Monad.max_def Errors.res0)
568                   (Obj.magic (reg_retrieve f.locals)) args) (fun vs ->
569                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
570                   Events.e0; Types.snd = (Callstate (id, fd, vs, dst,
571                   (List.Cons ((adv l f), fs)), m)) }))))))
572   | RTLabs_syntax.St_call_ptr (frs, args, dst, l) ->
573     (fun _ ->
574       IOMonad.err_to_io
575         (Obj.magic
576           (Monad.m_bind0 (Monad.max_def Errors.res0)
577             (Obj.magic (reg_retrieve f.locals frs)) (fun fv ->
578             Monad.m_bind2 (Monad.max_def Errors.res0)
579               (Obj.magic
580                 (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
581                   (Globalenvs.find_funct_id ge fv))) (fun fd id ->
582               Monad.m_bind0 (Monad.max_def Errors.res0)
583                 (Monad.m_list_map (Monad.max_def Errors.res0)
584                   (Obj.magic (reg_retrieve f.locals)) args) (fun vs ->
585                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
586                   Events.e0; Types.snd = (Callstate (id, fd, vs, dst,
587                   (List.Cons ((adv l f), fs)), m)) }))))))
588   | RTLabs_syntax.St_cond (src, ltrue, lfalse) ->
589     (fun _ ->
590       IOMonad.err_to_io
591         (Obj.magic
592           (Monad.m_bind0 (Monad.max_def Errors.res0)
593             (Obj.magic (reg_retrieve f.locals src)) (fun v ->
594             Monad.m_bind0 (Monad.max_def Errors.res0)
595               (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
596               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
597                 Events.e0; Types.snd =
598                 (build_state f fs m
599                   (match b with
600                    | Bool.True -> ltrue
601                    | Bool.False -> lfalse)) })))))
602   | RTLabs_syntax.St_return ->
603     (fun _ ->
604       IOMonad.err_to_io
605         (Obj.magic
606           (Monad.m_bind0 (Monad.max_def Errors.res0)
607             (match f.func.RTLabs_syntax.f_result with
608              | Types.None ->
609                Monad.m_return0 (Monad.max_def Errors.res0) Types.None
610              | Types.Some rt ->
611                let { Types.fst = r; Types.snd = ty } = rt in
612                Monad.m_bind0 (Monad.max_def Errors.res0)
613                  (Obj.magic (reg_retrieve f.locals r)) (fun v ->
614                  Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v)))
615             (fun v ->
616             Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
617               Events.e0; Types.snd = (Returnstate (v, f.retdst, fs,
618               (GenMem.free m f.sp))) }))))) __
619| Callstate (x, fd, params, dst, fs, m) ->
620  (match fd with
621   | AST.Internal fn ->
622     IOMonad.err_to_io
623       (Obj.magic
624         (Monad.m_bind0 (Monad.max_def Errors.res0)
625           (Obj.magic
626             (params_store fn.RTLabs_syntax.f_params params
627               (init_locals fn.RTLabs_syntax.f_locals))) (fun locals0 ->
628           let { Types.fst = m'; Types.snd = sp0 } =
629             GenMem.alloc m (Z.z_of_nat Nat.O)
630               (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
631           in
632           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
633             Events.e0; Types.snd = (State ({ func = fn; locals = locals0;
634             next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0; retdst =
635             dst }, fs, m')) })))
636   | AST.External fn ->
637     Obj.magic
638       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
639         (Obj.magic
640           (IOMonad.err_to_io
641             (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)))
642         (fun evargs ->
643         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
644           (Obj.magic
645             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
646           (fun evres ->
647           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
648             (Events.eextcall fn.AST.ef_id evargs
649               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
650             Types.snd = (Returnstate ((Types.Some
651             (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), dst, fs,
652             m)) }))))
653| Returnstate (v, dst, fs, m) ->
654  (match fs with
655   | List.Nil ->
656     (fun _ ->
657       (match v with
658        | Types.None ->
659          (fun _ ->
660            IOMonad.err_to_io (Errors.Error
661              (Errors.msg ErrorMessages.ReturnMismatch)))
662        | Types.Some v' ->
663          (fun _ ->
664            (match v' with
665             | Values.Vundef ->
666               (fun _ ->
667                 IOMonad.err_to_io (Errors.Error
668                   (Errors.msg ErrorMessages.ReturnMismatch)))
669             | Values.Vint (sz, r) ->
670               (fun _ ->
671                 IOMonad.err_to_io
672                   ((match sz with
673                     | AST.I8 ->
674                       (fun x -> Errors.Error
675                         (Errors.msg ErrorMessages.ReturnMismatch))
676                     | AST.I16 ->
677                       (fun x -> Errors.Error
678                         (Errors.msg ErrorMessages.ReturnMismatch))
679                     | AST.I32 ->
680                       (fun r5 ->
681                         Obj.magic
682                           (Monad.m_return0 (Monad.max_def Errors.res0)
683                             { Types.fst = Events.e0; Types.snd = (Finalstate
684                             r5) }))) r))
685             | Values.Vnull ->
686               (fun _ ->
687                 IOMonad.err_to_io (Errors.Error
688                   (Errors.msg ErrorMessages.ReturnMismatch)))
689             | Values.Vptr x ->
690               (fun _ ->
691                 IOMonad.err_to_io (Errors.Error
692                   (Errors.msg ErrorMessages.ReturnMismatch)))) __)) __)
693   | List.Cons (f, fs') ->
694     (fun _ ->
695       IOMonad.err_to_io
696         (Obj.magic
697           (Monad.m_bind0 (Monad.max_def Errors.res0)
698             (match dst with
699              | Types.None ->
700                (match v with
701                 | Types.None -> Obj.magic (Errors.OK f.locals)
702                 | Types.Some x ->
703                   Obj.magic (Errors.Error
704                     (Errors.msg ErrorMessages.ReturnMismatch)))
705              | Types.Some d ->
706                (match v with
707                 | Types.None ->
708                   Obj.magic (Errors.Error
709                     (Errors.msg ErrorMessages.ReturnMismatch))
710                 | Types.Some v' -> Obj.magic (reg_store d v' f.locals)))
711             (fun locals0 ->
712             Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
713               Events.e0; Types.snd = (State ({ func = f.func; locals =
714               locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs',
715               m)) }))))) __
716| Finalstate r ->
717  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.FinalState))
718
719(** val rTLabs_is_final : state0 -> Integers.int Types.option **)
720let rTLabs_is_final = function
721| State (x, x0, x1) -> Types.None
722| Callstate (x, x0, x1, x2, x3, x4) -> Types.None
723| Returnstate (x, x0, x1, x2) -> Types.None
724| Finalstate r -> Types.Some r
725
726(** val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
727let rTLabs_exec =
728  { SmallstepExec.is_final = (fun x -> Obj.magic rTLabs_is_final);
729    SmallstepExec.step = (Obj.magic eval_statement) }
730
731(** val make_global0 : RTLabs_syntax.rTLabs_program -> genv **)
732let make_global0 p =
733  Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
734
735(** val make_initial_state0 :
736    RTLabs_syntax.rTLabs_program -> state0 Errors.res **)
737let make_initial_state0 p =
738  let ge = make_global0 p in
739  Obj.magic
740    (Monad.m_bind0 (Monad.max_def Errors.res0)
741      (Obj.magic
742        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
743          List.Nil)) p)) (fun m ->
744      let main = p.AST.prog_main in
745      Monad.m_bind0 (Monad.max_def Errors.res0)
746        (Obj.magic
747          (Errors.opt_to_res (List.Cons ((Errors.MSG
748            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
749            (PreIdentifiers.SymbolTag, main)), List.Nil))))
750            (Globalenvs.find_symbol ge main))) (fun b ->
751        Monad.m_bind0 (Monad.max_def Errors.res0)
752          (Obj.magic
753            (Errors.opt_to_res (List.Cons ((Errors.MSG
754              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
755              (PreIdentifiers.SymbolTag, main)), List.Nil))))
756              (Globalenvs.find_funct_ptr ge b))) (fun f ->
757          Obj.magic (Errors.OK (Callstate (main, f, List.Nil, Types.None,
758            List.Nil, m)))))))
759
760(** val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
761let rTLabs_fullexec =
762  { SmallstepExec.es1 = rTLabs_exec; SmallstepExec.make_global =
763    (Obj.magic make_global0); SmallstepExec.make_initial_state =
764    (Obj.magic make_initial_state0) }
765
766(** val bind_ok :
767    'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
768    'a3) -> 'a3 **)
769let bind_ok clearme f v x =
770  (match clearme with
771   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
772   | Errors.Error m ->
773     (fun f0 v0 _ h _ ->
774       Obj.magic Errors.res_discr (Errors.Error m) (Errors.OK v0) __)) f v __
775    x __
776
777(** val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
778let jmeq_hackT x y auto =
779  auto __
780
781(** val func_block_of_exec :
782    genv -> state0 -> Events.trace -> AST.ident ->
783    RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
784    Registers.register Types.option -> frame List.list -> GenMem.mem1 ->
785    Pointers.block Types.sig0 **)
786let func_block_of_exec ge clearme t vf fd args dst fs m =
787  (match clearme with
788   | State (clearme0, x, x0) ->
789     (let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
790        dst0 } = clearme0
791      in
792     (fun fs0 m0 tr fid fd0 args0 dst' fs' m' ->
793     (match next_instruction { func = func0; locals = locals0; next = next0;
794              sp = sp0; retdst = dst0 } with
795      | RTLabs_syntax.St_skip l ->
796        (fun _ _ ->
797          jmeq_hackT (IOMonad.Value { Types.fst = Events.e0; Types.snd =
798            (build_state { func = func0; locals = locals0; next = next0; sp =
799              sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
800            tr; Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
801            (fun _ ->
802            Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
803              Events.e0; Types.snd =
804              (build_state { func = func0; locals = locals0; next = next0;
805                sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
806              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
807              dst', fs', m')) }) __ (fun _ ->
808              Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst = Events.e0;
809                Types.snd =
810                (build_state { func = func0; locals = locals0; next = next0;
811                  sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
812                Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) } __
813                (fun _ ->
814                Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
815                  Obj.magic state_jmdiscr (State
816                    ((adv l { func = func0; locals = locals0; next = next0;
817                       sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,
818                    fd0, args0, dst', fs', m')) __) tr __ __))))
819      | RTLabs_syntax.St_cost (c, l) ->
820        (fun _ _ ->
821          jmeq_hackT (IOMonad.Value { Types.fst = (Events.echarge c);
822            Types.snd =
823            (build_state { func = func0; locals = locals0; next = next0; sp =
824              sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
825            tr; Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
826            (fun _ ->
827            Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
828              (Events.echarge c); Types.snd =
829              (build_state { func = func0; locals = locals0; next = next0;
830                sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
831              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
832              dst', fs', m')) }) __ (fun _ ->
833              Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
834                (Events.echarge c); Types.snd =
835                (build_state { func = func0; locals = locals0; next = next0;
836                  sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
837                Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) } __
838                (fun _ ->
839                Logic.eq_rect_Type0 (List.Cons ((Events.EVcost c), List.Nil))
840                  (fun _ _ _ ->
841                  Obj.magic state_jmdiscr (State
842                    ((adv l { func = func0; locals = locals0; next = next0;
843                       sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,
844                    fd0, args0, dst', fs', m')) __) tr __ __))))
845      | RTLabs_syntax.St_const (t0, r, c, l) ->
846        (fun _ _ ->
847          IOMonad.bind_res_value
848            (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
849              (FrontEndOps.eval_constant t0 (Globalenvs.find_symbol ge) sp0
850                c)) (fun v ->
851            Obj.magic
852              (Monad.m_bind0 (Monad.max_def Errors.res0)
853                (Obj.magic (reg_store r v locals0)) (fun locals1 ->
854                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
855                  Events.e0; Types.snd = (State ({ func = func0; locals =
856                  locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
857            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
858            fs', m')) } (fun v _ _ ->
859            bind_ok (reg_store r v locals0) (fun x1 ->
860              Obj.magic
861                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
862                  Events.e0; Types.snd = (State ({ func = func0; locals = x1;
863                  next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
864              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
865              dst', fs', m')) } (fun locals' _ _ ->
866              jmeq_hackT
867                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
868                  Events.e0; Types.snd = (State ({ func = func0; locals =
869                  locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
870                (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
871                  (Callstate (fid, fd0, args0, dst', fs', m')) })) (fun _ ->
872                Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
873                  Events.e0; Types.snd = (State ({ func = func0; locals =
874                  locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
875                  (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
876                  fd0, args0, dst', fs', m')) }) __ (fun _ ->
877                  Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst = Events.e0;
878                    Types.snd = (State ({ func = func0; locals = locals';
879                    next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
880                    { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
881                    args0, dst', fs', m')) } __ (fun _ ->
882                    Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
883                      Obj.magic state_jmdiscr (State ({ func = func0;
884                        locals = locals'; next = l; sp = sp0; retdst =
885                        dst0 }, fs0, m0)) (Callstate (fid, fd0, args0, dst',
886                        fs', m')) __) tr __ __))))))
887      | RTLabs_syntax.St_op1 (t1, t2, op0, r5, r6, l) ->
888        (fun _ _ ->
889          IOMonad.bind_res_value (reg_retrieve locals0 r6) (fun v ->
890            Obj.magic
891              (Monad.m_bind0 (Monad.max_def Errors.res0)
892                (Obj.magic
893                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
894                    (FrontEndOps.eval_unop t2 t1 op0 v))) (fun v' ->
895                Monad.m_bind0 (Monad.max_def Errors.res0)
896                  (Obj.magic (reg_store r5 v' locals0)) (fun locals1 ->
897                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
898                    Events.e0; Types.snd = (State ({ func = func0; locals =
899                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
900            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
901            fs', m')) } (fun v _ _ ->
902            bind_ok
903              (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
904                (FrontEndOps.eval_unop t2 t1 op0 v)) (fun x1 ->
905              Obj.magic
906                (Monad.m_bind0 (Monad.max_def Errors.res0)
907                  (Obj.magic (reg_store r5 x1 locals0)) (fun locals1 ->
908                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
909                    Events.e0; Types.snd = (State ({ func = func0; locals =
910                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
911              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
912              dst', fs', m')) } (fun v' _ _ ->
913              bind_ok (reg_store r5 v' locals0) (fun x1 ->
914                Obj.magic
915                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
916                    Events.e0; Types.snd = (State ({ func = func0; locals =
917                    x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
918                { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
919                dst', fs', m')) } (fun loc _ _ ->
920                jmeq_hackT
921                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
922                    Events.e0; Types.snd = (State ({ func = func0; locals =
923                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
924                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
925                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
926                  (fun _ ->
927                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
928                    Events.e0; Types.snd = (State ({ func = func0; locals =
929                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
930                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
931                    fd0, args0, dst', fs', m')) }) __ (fun _ ->
932                    Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
933                      Events.e0; Types.snd = (State ({ func = func0; locals =
934                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
935                      { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
936                      args0, dst', fs', m')) } __ (fun _ ->
937                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
938                        Obj.magic state_jmdiscr (State ({ func = func0;
939                          locals = loc; next = l; sp = sp0; retdst = dst0 },
940                          fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
941                          m')) __) tr __ __)))))))
942      | RTLabs_syntax.St_op2 (t1, t2, t', op0, r5, r6, r7, l) ->
943        (fun _ _ ->
944          IOMonad.bind_res_value (reg_retrieve locals0 r6) (fun v1 ->
945            Obj.magic
946              (Monad.m_bind0 (Monad.max_def Errors.res0)
947                (Obj.magic (reg_retrieve locals0 r7)) (fun v2 ->
948                Monad.m_bind0 (Monad.max_def Errors.res0)
949                  (Obj.magic
950                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
951                      (FrontEndOps.eval_binop m0 t2 t' t1 op0 v1 v2)))
952                  (fun v' ->
953                  Monad.m_bind0 (Monad.max_def Errors.res0)
954                    (Obj.magic (reg_store r5 v' locals0)) (fun locals1 ->
955                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
956                      Events.e0; Types.snd = (State ({ func = func0; locals =
957                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
958                      m0)) }))))) { Types.fst = tr; Types.snd = (Callstate
959            (fid, fd0, args0, dst', fs', m')) } (fun v1 _ _ ->
960            bind_ok (reg_retrieve locals0 r7) (fun x1 ->
961              Obj.magic
962                (Monad.m_bind0 (Monad.max_def Errors.res0)
963                  (Obj.magic
964                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
965                      (FrontEndOps.eval_binop m0 t2 t' t1 op0 v1 x1)))
966                  (fun v' ->
967                  Monad.m_bind0 (Monad.max_def Errors.res0)
968                    (Obj.magic (reg_store r5 v' locals0)) (fun locals1 ->
969                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
970                      Events.e0; Types.snd = (State ({ func = func0; locals =
971                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
972                      m0)) })))) { Types.fst = tr; Types.snd = (Callstate
973              (fid, fd0, args0, dst', fs', m')) } (fun v2 _ _ ->
974              bind_ok
975                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
976                  (FrontEndOps.eval_binop m0 t2 t' t1 op0 v1 v2)) (fun x1 ->
977                Obj.magic
978                  (Monad.m_bind0 (Monad.max_def Errors.res0)
979                    (Obj.magic (reg_store r5 x1 locals0)) (fun locals1 ->
980                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
981                      Events.e0; Types.snd = (State ({ func = func0; locals =
982                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
983                      m0)) }))) { Types.fst = tr; Types.snd = (Callstate
984                (fid, fd0, args0, dst', fs', m')) } (fun v' _ _ ->
985                bind_ok (reg_store r5 v' locals0) (fun x1 ->
986                  Obj.magic
987                    (Monad.m_return0 (Monad.max_def Errors.res0)
988                      { Types.fst = Events.e0; Types.snd = (State ({ func =
989                      func0; locals = x1; next = l; sp = sp0; retdst =
990                      dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd =
991                  (Callstate (fid, fd0, args0, dst', fs', m')) }
992                  (fun loc _ _ ->
993                  jmeq_hackT
994                    (Monad.m_return0 (Monad.max_def Errors.res0)
995                      { Types.fst = Events.e0; Types.snd = (State ({ func =
996                      func0; locals = loc; next = l; sp = sp0; retdst =
997                      dst0 }, fs0, m0)) })
998                    (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
999                      (Callstate (fid, fd0, args0, dst', fs', m')) }))
1000                    (fun _ ->
1001                    Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1002                      Events.e0; Types.snd = (State ({ func = func0; locals =
1003                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
1004                      (Errors.OK { Types.fst = tr; Types.snd = (Callstate
1005                      (fid, fd0, args0, dst', fs', m')) }) __ (fun _ ->
1006                      Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1007                        Events.e0; Types.snd = (State ({ func = func0;
1008                        locals = loc; next = l; sp = sp0; retdst = dst0 },
1009                        fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate
1010                        (fid, fd0, args0, dst', fs', m')) } __ (fun _ ->
1011                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1012                          Obj.magic state_jmdiscr (State ({ func = func0;
1013                            locals = loc; next = l; sp = sp0; retdst =
1014                            dst0 }, fs0, m0)) (Callstate (fid, fd0, args0,
1015                            dst', fs', m')) __) tr __ __))))))))
1016      | RTLabs_syntax.St_load (ch, r5, r6, l) ->
1017        (fun _ _ ->
1018          IOMonad.bind_res_value (reg_retrieve locals0 r5) (fun vaddr ->
1019            Obj.magic
1020              (Monad.m_bind0 (Monad.max_def Errors.res0)
1021                (Obj.magic
1022                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
1023                    (FrontEndMem.loadv ch m0 vaddr))) (fun v ->
1024                Monad.m_bind0 (Monad.max_def Errors.res0)
1025                  (Obj.magic (reg_store r6 v locals0)) (fun locals1 ->
1026                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1027                    Events.e0; Types.snd = (State ({ func = func0; locals =
1028                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
1029            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
1030            fs', m')) } (fun v _ _ ->
1031            bind_ok
1032              (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
1033                (FrontEndMem.loadv ch m0 v)) (fun x1 ->
1034              Obj.magic
1035                (Monad.m_bind0 (Monad.max_def Errors.res0)
1036                  (Obj.magic (reg_store r6 x1 locals0)) (fun locals1 ->
1037                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1038                    Events.e0; Types.snd = (State ({ func = func0; locals =
1039                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
1040              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1041              dst', fs', m')) } (fun v' _ _ ->
1042              bind_ok (reg_store r6 v' locals0) (fun x1 ->
1043                Obj.magic
1044                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1045                    Events.e0; Types.snd = (State ({ func = func0; locals =
1046                    x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
1047                { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1048                dst', fs', m')) } (fun loc _ _ ->
1049                jmeq_hackT
1050                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1051                    Events.e0; Types.snd = (State ({ func = func0; locals =
1052                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
1053                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1054                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1055                  (fun _ ->
1056                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1057                    Events.e0; Types.snd = (State ({ func = func0; locals =
1058                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
1059                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
1060                    fd0, args0, dst', fs', m')) }) __ (fun _ ->
1061                    Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1062                      Events.e0; Types.snd = (State ({ func = func0; locals =
1063                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
1064                      { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
1065                      args0, dst', fs', m')) } __ (fun _ ->
1066                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1067                        Obj.magic state_jmdiscr (State ({ func = func0;
1068                          locals = loc; next = l; sp = sp0; retdst = dst0 },
1069                          fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
1070                          m')) __) tr __ __)))))))
1071      | RTLabs_syntax.St_store (ch, r5, r6, l) ->
1072        (fun _ _ ->
1073          IOMonad.bind_res_value (reg_retrieve locals0 r5) (fun vaddr ->
1074            Obj.magic
1075              (Monad.m_bind0 (Monad.max_def Errors.res0)
1076                (Obj.magic (reg_retrieve locals0 r6)) (fun v ->
1077                Monad.m_bind0 (Monad.max_def Errors.res0)
1078                  (Obj.magic
1079                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1080                      (FrontEndMem.storev ch m0 vaddr v))) (fun m'0 ->
1081                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1082                    Events.e0; Types.snd =
1083                    (build_state { func = func0; locals = locals0; next =
1084                      next0; sp = sp0; retdst = dst0 } fs0 m'0 l) }))))
1085            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
1086            fs', m')) } (fun v _ _ ->
1087            bind_ok (reg_retrieve locals0 r6) (fun x1 ->
1088              Obj.magic
1089                (Monad.m_bind0 (Monad.max_def Errors.res0)
1090                  (Obj.magic
1091                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1092                      (FrontEndMem.storev ch m0 v x1))) (fun m'0 ->
1093                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1094                    Events.e0; Types.snd =
1095                    (build_state { func = func0; locals = locals0; next =
1096                      next0; sp = sp0; retdst = dst0 } fs0 m'0 l) })))
1097              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1098              dst', fs', m')) } (fun v' _ _ ->
1099              bind_ok
1100                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1101                  (FrontEndMem.storev ch m0 v v')) (fun x1 ->
1102                Obj.magic
1103                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1104                    Events.e0; Types.snd =
1105                    (build_state { func = func0; locals = locals0; next =
1106                      next0; sp = sp0; retdst = dst0 } fs0 x1 l) }))
1107                { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1108                dst', fs', m')) } (fun loc _ _ ->
1109                jmeq_hackT
1110                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1111                    Events.e0; Types.snd =
1112                    (build_state { func = func0; locals = locals0; next =
1113                      next0; sp = sp0; retdst = dst0 } fs0 loc l) })
1114                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1115                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1116                  (fun _ ->
1117                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1118                    Events.e0; Types.snd =
1119                    (build_state { func = func0; locals = locals0; next =
1120                      next0; sp = sp0; retdst = dst0 } fs0 loc l) })
1121                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
1122                    fd0, args0, dst', fs', m')) }) __ (fun _ ->
1123                    Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1124                      Events.e0; Types.snd =
1125                      (build_state { func = func0; locals = locals0; next =
1126                        next0; sp = sp0; retdst = dst0 } fs0 loc l) }
1127                      { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
1128                      args0, dst', fs', m')) } __ (fun _ ->
1129                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1130                        Obj.magic state_jmdiscr (State
1131                          ((adv l { func = func0; locals = locals0; next =
1132                             next0; sp = sp0; retdst = dst0 }), fs0, loc))
1133                          (Callstate (fid, fd0, args0, dst', fs', m')) __) tr
1134                        __ __)))))))
1135      | RTLabs_syntax.St_call_id (x1, rs, or2, l) ->
1136        (fun _ _ ->
1137          IOMonad.bind_res_value
1138            (Errors.opt_to_res (List.Cons ((Errors.MSG
1139              ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1140              (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1141              (Globalenvs.find_symbol ge x1)) (fun b ->
1142            Obj.magic
1143              (Monad.m_bind0 (Monad.max_def Errors.res0)
1144                (Obj.magic
1145                  (Errors.opt_to_res (List.Cons ((Errors.MSG
1146                    ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1147                    (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1148                    (Globalenvs.find_funct_ptr ge b))) (fun fd1 ->
1149                Monad.m_bind0 (Monad.max_def Errors.res0)
1150                  (Monad.m_list_map (Monad.max_def Errors.res0)
1151                    (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1152                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1153                    Events.e0; Types.snd = (Callstate (x1, fd1, vs, or2,
1154                    (List.Cons
1155                    ((adv l { func = func0; locals = locals0; next = next0;
1156                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
1157            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
1158            fs', m')) } (fun v _ _ ->
1159            bind_ok
1160              (Errors.opt_to_res (List.Cons ((Errors.MSG
1161                ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1162                (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1163                (Globalenvs.find_funct_ptr ge v)) (fun x2 ->
1164              Obj.magic
1165                (Monad.m_bind0 (Monad.max_def Errors.res0)
1166                  (Monad.m_list_map (Monad.max_def Errors.res0)
1167                    (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1168                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1169                    Events.e0; Types.snd = (Callstate (x1, x2, vs, or2,
1170                    (List.Cons
1171                    ((adv l { func = func0; locals = locals0; next = next0;
1172                       sp = sp0; retdst = dst0 }), fs0)), m0)) })))
1173              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1174              dst', fs', m')) } (fun fd' _ _ ->
1175              bind_ok
1176                (Obj.magic
1177                  (Monad.m_list_map (Monad.max_def Errors.res0)
1178                    (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 ->
1179                Obj.magic
1180                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1181                    Events.e0; Types.snd = (Callstate (x1, fd', x2, or2,
1182                    (List.Cons
1183                    ((adv l { func = func0; locals = locals0; next = next0;
1184                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))
1185                { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1186                dst', fs', m')) } (fun vs _ _ ->
1187                jmeq_hackT
1188                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1189                    Events.e0; Types.snd = (Callstate (x1, fd', vs, or2,
1190                    (List.Cons
1191                    ((adv l { func = func0; locals = locals0; next = next0;
1192                       sp = sp0; retdst = dst0 }), fs0)), m0)) })
1193                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1194                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1195                  (fun _ ->
1196                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1197                    List.Nil; Types.snd = (Callstate (x1, fd', vs, or2,
1198                    (List.Cons ({ func = func0; locals = locals0; next = l;
1199                    sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK
1200                    { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
1201                    args0, dst', fs', m')) }) __ (fun _ ->
1202                    Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1203                      List.Nil; Types.snd = (Callstate (x1, fd', vs, or2,
1204                      (List.Cons ({ func = func0; locals = locals0; next = l;
1205                      sp = sp0; retdst = dst0 }, fs0)), m0)) } { Types.fst =
1206                      tr; Types.snd = (Callstate (fid, fd0, args0, dst', fs',
1207                      m')) } __ (fun _ ->
1208                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1209                        Obj.magic state_jmdiscr (Callstate (x1, fd', vs, or2,
1210                          (List.Cons ({ func = func0; locals = locals0;
1211                          next = l; sp = sp0; retdst = dst0 }, fs0)), m0))
1212                          (Callstate (fid, fd0, args0, dst', fs', m')) __
1213                          (fun _ ->
1214                          Extralib.eq_rect_Type0_r1 fid (fun _ _ _ _ _ _ _ ->
1215                            Extralib.eq_rect_Type0_r1 fd0 (fun _ _ _ _ _ ->
1216                              Extralib.eq_rect_Type0_r1 args0
1217                                (fun _ _ _ _ _ ->
1218                                Extralib.eq_rect_Type0_r1 dst'
1219                                  (fun _ _ _ _ _ ->
1220                                  Logic.eq_rect_Type0 (List.Cons ({ func =
1221                                    func0; locals = locals0; next = l; sp =
1222                                    sp0; retdst = dst0 }, fs0))
1223                                    (fun _ _ _ _ ->
1224                                    Extralib.eq_rect_Type0_r1 m'
1225                                      (fun _ _ _ ->
1226                                      Logic.streicherK (Errors.OK
1227                                        { Types.fst = List.Nil; Types.snd =
1228                                        (Callstate (fid, fd0, args0, dst',
1229                                        (List.Cons ({ func = func0; locals =
1230                                        locals0; next = l; sp = sp0; retdst =
1231                                        dst0 }, fs0)), m')) })
1232                                        (Logic.streicherK { Types.fst =
1233                                          List.Nil; Types.snd = (Callstate
1234                                          (fid, fd0, args0, dst', (List.Cons
1235                                          ({ func = func0; locals = locals0;
1236                                          next = l; sp = sp0; retdst =
1237                                          dst0 }, fs0)), m')) }
1238                                          (Logic.streicherK (Callstate (fid,
1239                                            fd0, args0, dst', (List.Cons
1240                                            ({ func = func0; locals =
1241                                            locals0; next = l; sp = sp0;
1242                                            retdst = dst0 }, fs0)), m')) v)))
1243                                      m0 __ __ __) fs' __ __ __) or2 __ __ __
1244                                  __) vs __ __ __ __) fd' __ __ __ __) x1 __
1245                            __ __ __ __ __)) tr __ __)))))))
1246      | RTLabs_syntax.St_call_ptr (x1, rs, or2, l) ->
1247        (fun _ _ ->
1248          IOMonad.bind_res_value (reg_retrieve locals0 x1) (fun fv ->
1249            Obj.magic
1250              (Monad.m_bind2 (Monad.max_def Errors.res0)
1251                (Obj.magic
1252                  (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
1253                    (Globalenvs.find_funct_id ge fv))) (fun fd1 id ->
1254                Monad.m_bind0 (Monad.max_def Errors.res0)
1255                  (Monad.m_list_map (Monad.max_def Errors.res0)
1256                    (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1257                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1258                    Events.e0; Types.snd = (Callstate (id, fd1, vs, or2,
1259                    (List.Cons
1260                    ((adv l { func = func0; locals = locals0; next = next0;
1261                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
1262            { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
1263            fs', m')) } (fun v _ _ ->
1264            bind_ok
1265              (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
1266                (Globalenvs.find_funct_id ge v)) (fun x2 ->
1267              Obj.magic
1268                (Monad.m_bind0 (Monad.max_def Errors.res0)
1269                  (Monad.m_list_map (Monad.max_def Errors.res0)
1270                    (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1271                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1272                    Events.e0; Types.snd = (Callstate (x2.Types.snd,
1273                    x2.Types.fst, vs, or2, (List.Cons
1274                    ((adv l { func = func0; locals = locals0; next = next0;
1275                       sp = sp0; retdst = dst0 }), fs0)), m0)) })))
1276              { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1277              dst', fs', m')) } (fun fd' _ _ ->
1278              bind_ok
1279                (Obj.magic
1280                  (Monad.m_list_map (Monad.max_def Errors.res0)
1281                    (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 ->
1282                Obj.magic
1283                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1284                    Events.e0; Types.snd = (Callstate (fd'.Types.snd,
1285                    fd'.Types.fst, x2, or2, (List.Cons
1286                    ((adv l { func = func0; locals = locals0; next = next0;
1287                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))
1288                { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
1289                dst', fs', m')) } (fun vs _ _ ->
1290                jmeq_hackT
1291                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1292                    Events.e0; Types.snd = (Callstate (fd'.Types.snd,
1293                    fd'.Types.fst, vs, or2, (List.Cons
1294                    ((adv l { func = func0; locals = locals0; next = next0;
1295                       sp = sp0; retdst = dst0 }), fs0)), m0)) })
1296                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1297                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1298                  (fun _ ->
1299                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1300                    List.Nil; Types.snd = (Callstate (fd'.Types.snd,
1301                    fd'.Types.fst, vs, or2, (List.Cons ({ func = func0;
1302                    locals = locals0; next = l; sp = sp0; retdst = dst0 },
1303                    fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd =
1304                    (Callstate (fid, fd0, args0, dst', fs', m')) }) __
1305                    (fun _ ->
1306                    Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1307                      List.Nil; Types.snd = (Callstate (fd'.Types.snd,
1308                      fd'.Types.fst, vs, or2, (List.Cons ({ func = func0;
1309                      locals = locals0; next = l; sp = sp0; retdst = dst0 },
1310                      fs0)), m0)) } { Types.fst = tr; Types.snd = (Callstate
1311                      (fid, fd0, args0, dst', fs', m')) } __ (fun _ ->
1312                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1313                        Obj.magic state_jmdiscr (Callstate (fd'.Types.snd,
1314                          fd'.Types.fst, vs, or2, (List.Cons ({ func = func0;
1315                          locals = locals0; next = l; sp = sp0; retdst =
1316                          dst0 }, fs0)), m0)) (Callstate (fid, fd0, args0,
1317                          dst', fs', m')) __ (fun _ ->
1318                          Logic.eq_rect_Type0 fd'.Types.snd (fun _ _ _ _ ->
1319                            Logic.eq_rect_Type0 fd'.Types.fst (fun _ _ _ _ ->
1320                              Extralib.eq_rect_Type0_r1 args0
1321                                (fun _ _ _ _ _ ->
1322                                Extralib.eq_rect_Type0_r1 dst'
1323                                  (fun _ _ _ _ _ ->
1324                                  Logic.eq_rect_Type0 (List.Cons ({ func =
1325                                    func0; locals = locals0; next = l; sp =
1326                                    sp0; retdst = dst0 }, fs0))
1327                                    (fun _ _ _ _ ->
1328                                    Extralib.eq_rect_Type0_r1 m'
1329                                      (fun _ _ _ ->
1330                                      Logic.streicherK (Errors.OK
1331                                        { Types.fst = List.Nil; Types.snd =
1332                                        (Callstate (fd'.Types.snd,
1333                                        fd'.Types.fst, args0, dst',
1334                                        (List.Cons ({ func = func0; locals =
1335                                        locals0; next = l; sp = sp0; retdst =
1336                                        dst0 }, fs0)), m')) })
1337                                        (Logic.streicherK { Types.fst =
1338                                          List.Nil; Types.snd = (Callstate
1339                                          (fd'.Types.snd, fd'.Types.fst,
1340                                          args0, dst', (List.Cons ({ func =
1341                                          func0; locals = locals0; next = l;
1342                                          sp = sp0; retdst = dst0 }, fs0)),
1343                                          m')) }
1344                                          (Logic.streicherK (Callstate
1345                                            (fd'.Types.snd, fd'.Types.fst,
1346                                            args0, dst', (List.Cons ({ func =
1347                                            func0; locals = locals0; next =
1348                                            l; sp = sp0; retdst = dst0 },
1349                                            fs0)), m'))
1350                                            ((match v with
1351                                              | Values.Vundef ->
1352                                                (fun _ ->
1353                                                  Obj.magic Errors.res_discr
1354                                                    (Errors.Error (List.Cons
1355                                                    ((Errors.MSG
1356                                                    ErrorMessages.BadFunction),
1357                                                    List.Nil))) (Errors.OK
1358                                                    fd') __)
1359                                              | Values.Vint (a, b) ->
1360                                                (fun _ ->
1361                                                  Obj.magic Errors.res_discr
1362                                                    (Errors.Error (List.Cons
1363                                                    ((Errors.MSG
1364                                                    ErrorMessages.BadFunction),
1365                                                    List.Nil))) (Errors.OK
1366                                                    fd') __)
1367                                              | Values.Vnull ->
1368                                                (fun _ ->
1369                                                  Obj.magic Errors.res_discr
1370                                                    (Errors.Error (List.Cons
1371                                                    ((Errors.MSG
1372                                                    ErrorMessages.BadFunction),
1373                                                    List.Nil))) (Errors.OK
1374                                                    fd') __)
1375                                              | Values.Vptr clearme1 ->
1376                                                let { Pointers.pblock = b;
1377                                                  Pointers.poff = off } =
1378                                                  clearme1
1379                                                in
1380                                                let { Types.fst = fd'';
1381                                                  Types.snd = fid' } = fd'
1382                                                in
1383                                                (fun _ -> b)) __)))) m0 __ __
1384                                      __) fs' __ __ __) or2 __ __ __ __) vs
1385                                __ __ __ __) fd0 __ __ __) fid __ __ __)) tr
1386                        __ __)))))))
1387      | RTLabs_syntax.St_cond (r, l1, l2) ->
1388        (fun _ _ ->
1389          IOMonad.bind_res_value (reg_retrieve locals0 r) (fun v ->
1390            Obj.magic
1391              (Monad.m_bind0 (Monad.max_def Errors.res0)
1392                (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
1393                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1394                  Events.e0; Types.snd =
1395                  (build_state { func = func0; locals = locals0; next =
1396                    next0; sp = sp0; retdst = dst0 } fs0 m0
1397                    (match b with
1398                     | Bool.True -> l1
1399                     | Bool.False -> l2)) }))) { Types.fst = tr; Types.snd =
1400            (Callstate (fid, fd0, args0, dst', fs', m')) } (fun v _ _ ->
1401            bind_ok (Values.eval_bool_of_val v) (fun x1 ->
1402              Obj.magic
1403                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1404                  Events.e0; Types.snd =
1405                  (build_state { func = func0; locals = locals0; next =
1406                    next0; sp = sp0; retdst = dst0 } fs0 m0
1407                    (match x1 with
1408                     | Bool.True -> l1
1409                     | Bool.False -> l2)) })) { Types.fst = tr; Types.snd =
1410              (Callstate (fid, fd0, args0, dst', fs', m')) } (fun b _ _ ->
1411              jmeq_hackT
1412                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1413                  Events.e0; Types.snd =
1414                  (build_state { func = func0; locals = locals0; next =
1415                    next0; sp = sp0; retdst = dst0 } fs0 m0
1416                    (match b with
1417                     | Bool.True -> l1
1418                     | Bool.False -> l2)) })
1419                (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1420                  (Callstate (fid, fd0, args0, dst', fs', m')) })) (fun _ ->
1421                Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1422                  Events.e0; Types.snd =
1423                  (build_state { func = func0; locals = locals0; next =
1424                    next0; sp = sp0; retdst = dst0 } fs0 m0
1425                    (match b with
1426                     | Bool.True -> l1
1427                     | Bool.False -> l2)) }) (Errors.OK { Types.fst = tr;
1428                  Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
1429                  __ (fun _ ->
1430                  Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst = Events.e0;
1431                    Types.snd =
1432                    (build_state { func = func0; locals = locals0; next =
1433                      next0; sp = sp0; retdst = dst0 } fs0 m0
1434                      (match b with
1435                       | Bool.True -> l1
1436                       | Bool.False -> l2)) } { Types.fst = tr; Types.snd =
1437                    (Callstate (fid, fd0, args0, dst', fs', m')) } __
1438                    (fun _ ->
1439                    Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1440                      Obj.magic state_jmdiscr (State
1441                        ((adv
1442                           (match b with
1443                            | Bool.True -> l1
1444                            | Bool.False -> l2) { func = func0; locals =
1445                           locals0; next = next0; sp = sp0; retdst = dst0 }),
1446                        fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
1447                        m')) __) tr __ __))))))
1448      | RTLabs_syntax.St_return ->
1449        (fun _ _ ->
1450          IOMonad.bind_res_value
1451            (match func0.RTLabs_syntax.f_result with
1452             | Types.None ->
1453               Obj.magic
1454                 (Monad.m_return0 (Monad.max_def Errors.res0) Types.None)
1455             | Types.Some rt ->
1456               let { Types.fst = r; Types.snd = ty } = rt in
1457               Obj.magic
1458                 (Monad.m_bind0 (Monad.max_def Errors.res0)
1459                   (Obj.magic (reg_retrieve locals0 r)) (fun v ->
1460                   Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v))))
1461            (fun v ->
1462            Obj.magic
1463              (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1464                Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1465                (GenMem.free m0 sp0))) })) { Types.fst = tr; Types.snd =
1466            (Callstate (fid, fd0, args0, dst', fs', m')) } (fun v ->
1467            match func0.RTLabs_syntax.f_result with
1468            | Types.None ->
1469              (fun _ _ ->
1470                jmeq_hackT
1471                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1472                    Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1473                    (GenMem.free m0 sp0))) })
1474                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1475                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1476                  (fun _ ->
1477                  Obj.magic Errors.res_discr (Errors.OK Types.None)
1478                    (Errors.OK v) __
1479                    (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1480                      Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1481                      (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
1482                      Types.snd = (Callstate (fid, fd0, args0, dst', fs',
1483                      m')) }) __ (fun _ ->
1484                      Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1485                        Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1486                        (GenMem.free m0 sp0))) } { Types.fst = tr;
1487                        Types.snd = (Callstate (fid, fd0, args0, dst', fs',
1488                        m')) } __ (fun _ ->
1489                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1490                          Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
1491                            (GenMem.free m0 sp0))) (Callstate (fid, fd0,
1492                            args0, dst', fs', m')) __) tr __ __)))))
1493            | Types.Some clearme1 ->
1494              let { Types.fst = r; Types.snd = t0 } = clearme1 in
1495              (fun _ ->
1496              bind_ok (reg_retrieve locals0 r) (fun x1 ->
1497                Obj.magic
1498                  (Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some
1499                    x1))) v (fun v0 _ _ _ ->
1500                jmeq_hackT
1501                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1502                    Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1503                    (GenMem.free m0 sp0))) })
1504                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1505                    (Callstate (fid, fd0, args0, dst', fs', m')) }))
1506                  (fun _ ->
1507                  Obj.magic Errors.res_discr (Errors.OK (Types.Some v0))
1508                    (Errors.OK v) __
1509                    (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1510                      Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1511                      (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
1512                      Types.snd = (Callstate (fid, fd0, args0, dst', fs',
1513                      m')) }) __ (fun _ ->
1514                      Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1515                        Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1516                        (GenMem.free m0 sp0))) } { Types.fst = tr;
1517                        Types.snd = (Callstate (fid, fd0, args0, dst', fs',
1518                        m')) } __ (fun _ ->
1519                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1520                          Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
1521                            (GenMem.free m0 sp0))) (Callstate (fid, fd0,
1522                            args0, dst', fs', m')) __) tr __ __))))))))) __))
1523       x x0
1524   | Callstate (vf0, clearme0, x, x0, x1, x2) ->
1525     (match clearme0 with
1526      | AST.Internal fn ->
1527        (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ ->
1528          IOMonad.bind_res_value
1529            (params_store fn.RTLabs_syntax.f_params args0
1530              (init_locals fn.RTLabs_syntax.f_locals)) (fun locals0 ->
1531            let { Types.fst = m'0; Types.snd = sp0 } =
1532              GenMem.alloc m0 (Z.z_of_nat Nat.O)
1533                (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
1534            in
1535            Obj.magic
1536              (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1537                Events.e0; Types.snd = (State ({ func = fn; locals = locals0;
1538                next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0;
1539                retdst = retdst0 }, stk, m'0)) })) { Types.fst = tr;
1540            Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }
1541            (fun loc _ ->
1542            let { Types.fst = m'0; Types.snd = b } =
1543              GenMem.alloc m0 (Z.z_of_nat Nat.O)
1544                (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
1545            in
1546            (fun _ ->
1547            jmeq_hackT (Errors.OK { Types.fst = Events.e0; Types.snd = (State
1548              ({ func = fn; locals = loc; next =
1549              (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1550              retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr;
1551              Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1552              (fun _ ->
1553              Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1554                Events.e0; Types.snd = (State ({ func = fn; locals = loc;
1555                next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1556                retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr;
1557                Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1558                __ (fun _ ->
1559                Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst = Events.e0;
1560                  Types.snd = (State ({ func = fn; locals = loc; next =
1561                  (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1562                  retdst0 }, stk, m'0)) } { Types.fst = tr; Types.snd =
1563                  (Callstate (vf', fd', args', dst', fs', m')) } __ (fun _ ->
1564                  Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1565                    Obj.magic state_jmdiscr (State ({ func = fn; locals =
1566                      loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp =
1567                      b; retdst = retdst0 }, stk, m'0)) (Callstate (vf', fd',
1568                      args', dst', fs', m')) __) tr __ __))))))
1569      | AST.External fn ->
1570        (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ ->
1571          IOMonad.bindIO_value
1572            (IOMonad.err_to_io
1573              (IO.check_eventval_list args0 fn.AST.ef_sig.AST.sig_args))
1574            (fun evargs ->
1575            Obj.magic
1576              (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1577                (Obj.magic
1578                  (IO.do_io fn.AST.ef_id evargs
1579                    (AST.proj_sig_res fn.AST.ef_sig))) (fun evres ->
1580                Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
1581                  (Events.eextcall fn.AST.ef_id evargs
1582                    (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
1583                  Types.snd = (Returnstate ((Types.Some
1584                  (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
1585                  retdst0, stk, m0)) }))) { Types.fst = tr; Types.snd =
1586            (Callstate (vf', fd', args', dst', fs', m')) } (fun evargs _ _ ->
1587            Obj.magic IOMonad.iO_discr (IOMonad.Interact ({ IO.io_function =
1588              fn.AST.ef_id; IO.io_args = evargs; IO.io_in_typ =
1589              (AST.proj_sig_res fn.AST.ef_sig) }, (fun res1 ->
1590              IOMonad.bindIO (IOMonad.Value res1) (fun evres ->
1591                Obj.magic
1592                  (Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
1593                    { Types.fst =
1594                    (Events.eextcall fn.AST.ef_id evargs
1595                      (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
1596                    Types.snd = (Returnstate ((Types.Some
1597                    (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
1598                    retdst0, stk, m0)) }))))) (IOMonad.Value { Types.fst =
1599              tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1600              __))) x x0 x1 x2
1601   | Returnstate (v, r, clearme0, x) ->
1602     (match clearme0 with
1603      | List.Nil ->
1604        (fun m0 tr vf' fd' args' dst' fs' m' ->
1605          match v with
1606          | Types.None ->
1607            (fun _ ->
1608              Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1609                ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1610                (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf',
1611                fd', args', dst', fs', m')) }) __)
1612          | Types.Some clearme1 ->
1613            (match clearme1 with
1614             | Values.Vundef ->
1615               (fun _ ->
1616                 Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1617                   ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1618                   (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1619                   (vf', fd', args', dst', fs', m')) }) __)
1620             | Values.Vint (clearme2, x0) ->
1621               (match clearme2 with
1622                | AST.I8 ->
1623                  (fun r5 _ ->
1624                    jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG
1625                      ErrorMessages.ReturnMismatch), List.Nil)))
1626                      (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1627                      (vf', fd', args', dst', fs', m')) }) (fun _ ->
1628                      Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons
1629                        ((Errors.MSG ErrorMessages.ReturnMismatch),
1630                        List.Nil))) (IOMonad.Value { Types.fst = tr;
1631                        Types.snd = (Callstate (vf', fd', args', dst', fs',
1632                        m')) }) __))
1633                | AST.I16 ->
1634                  (fun r5 _ ->
1635                    jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG
1636                      ErrorMessages.ReturnMismatch), List.Nil)))
1637                      (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1638                      (vf', fd', args', dst', fs', m')) }) (fun _ ->
1639                      Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons
1640                        ((Errors.MSG ErrorMessages.ReturnMismatch),
1641                        List.Nil))) (IOMonad.Value { Types.fst = tr;
1642                        Types.snd = (Callstate (vf', fd', args', dst', fs',
1643                        m')) }) __))
1644                | AST.I32 ->
1645                  (fun r5 _ ->
1646                    jmeq_hackT (IOMonad.Value { Types.fst = List.Nil;
1647                      Types.snd = (Finalstate r5) }) (IOMonad.Value
1648                      { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1649                      args', dst', fs', m')) }) (fun _ ->
1650                      Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value
1651                        { Types.fst = List.Nil; Types.snd = (Finalstate
1652                        r5) }) (IOMonad.Value { Types.fst = tr; Types.snd =
1653                        (Callstate (vf', fd', args', dst', fs', m')) }) __
1654                        (fun _ ->
1655                        Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst =
1656                          List.Nil; Types.snd = (Finalstate r5) }
1657                          { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1658                          args', dst', fs', m')) } __ (fun _ ->
1659                          Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1660                            Obj.magic state_jmdiscr (Finalstate r5)
1661                              (Callstate (vf', fd', args', dst', fs', m')) __)
1662                            tr __ __))))) x0
1663             | Values.Vnull ->
1664               (fun _ ->
1665                 Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1666                   ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1667                   (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1668                   (vf', fd', args', dst', fs', m')) }) __)
1669             | Values.Vptr a ->
1670               (fun _ ->
1671                 Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1672                   ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1673                   (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1674                   (vf', fd', args', dst', fs', m')) }) __)))
1675      | List.Cons (f, fs0) ->
1676        (fun m0 tr vf' fd' args' dst' fs' m' _ ->
1677          IOMonad.bind_res_value
1678            (match r with
1679             | Types.None ->
1680               (match v with
1681                | Types.None -> Errors.OK f.locals
1682                | Types.Some x0 ->
1683                  Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
1684             | Types.Some d ->
1685               (match v with
1686                | Types.None ->
1687                  Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
1688                | Types.Some v' -> reg_store d v' f.locals)) (fun locals0 ->
1689            Obj.magic
1690              (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1691                Events.e0; Types.snd = (State ({ func = f.func; locals =
1692                locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs0,
1693                m0)) })) { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1694            args', dst', fs', m')) } (fun loc _ _ ->
1695            jmeq_hackT
1696              (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1697                Events.e0; Types.snd = (State ({ func = f.func; locals = loc;
1698                next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) })
1699              (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate
1700                (vf', fd', args', dst', fs', m')) })) (fun _ ->
1701              Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1702                Events.e0; Types.snd = (State ({ func = f.func; locals = loc;
1703                next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) })
1704                (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf',
1705                fd', args', dst', fs', m')) }) __ (fun _ ->
1706                Obj.magic Globalenvs.prod_jmdiscr0 { Types.fst = Events.e0;
1707                  Types.snd = (State ({ func = f.func; locals = loc; next =
1708                  f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) }
1709                  { Types.fst = tr; Types.snd = (Callstate (vf', fd', args',
1710                  dst', fs', m')) } __ (fun _ ->
1711                  Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1712                    Obj.magic state_jmdiscr (State ({ func = f.func; locals =
1713                      loc; next = f.next; sp = f.sp; retdst = f.retdst },
1714                      fs0, m0)) (Callstate (vf', fd', args', dst', fs', m'))
1715                      __) tr __ __)))))) x
1716   | Finalstate r ->
1717     (fun tr vf' fd' args' dst' fs' m' _ ->
1718       Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG
1719         ErrorMessages.FinalState), List.Nil))) (IOMonad.Value { Types.fst =
1720         tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __))
1721    t vf fd args dst fs m __
1722
Note: See TracBrowser for help on using the repository browser.