source: extracted/rTLabs_semantics.ml @ 2890

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

Everything extracted again.

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