19 open Hints_declaration
89 type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
91 step : (__ -> __ -> ('outty, 'inty,
92 (Events.trace, __) Types.prod)
95 (** val trans_system_rect_Type4 :
96 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
97 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
98 'a2) trans_system -> 'a3 **)
99 let rec trans_system_rect_Type4 h_mk_trans_system x_5925 =
100 let { is_final = is_final0; step = step0 } = x_5925 in
101 h_mk_trans_system __ __ is_final0 step0
103 (** val trans_system_rect_Type5 :
104 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
105 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
106 'a2) trans_system -> 'a3 **)
107 let rec trans_system_rect_Type5 h_mk_trans_system x_5927 =
108 let { is_final = is_final0; step = step0 } = x_5927 in
109 h_mk_trans_system __ __ is_final0 step0
111 (** val trans_system_rect_Type3 :
112 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
113 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
114 'a2) trans_system -> 'a3 **)
115 let rec trans_system_rect_Type3 h_mk_trans_system x_5929 =
116 let { is_final = is_final0; step = step0 } = x_5929 in
117 h_mk_trans_system __ __ is_final0 step0
119 (** val trans_system_rect_Type2 :
120 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
121 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
122 'a2) trans_system -> 'a3 **)
123 let rec trans_system_rect_Type2 h_mk_trans_system x_5931 =
124 let { is_final = is_final0; step = step0 } = x_5931 in
125 h_mk_trans_system __ __ is_final0 step0
127 (** val trans_system_rect_Type1 :
128 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
129 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
130 'a2) trans_system -> 'a3 **)
131 let rec trans_system_rect_Type1 h_mk_trans_system x_5933 =
132 let { is_final = is_final0; step = step0 } = x_5933 in
133 h_mk_trans_system __ __ is_final0 step0
135 (** val trans_system_rect_Type0 :
136 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
137 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
138 'a2) trans_system -> 'a3 **)
139 let rec trans_system_rect_Type0 h_mk_trans_system x_5935 =
140 let { is_final = is_final0; step = step0 } = x_5935 in
141 h_mk_trans_system __ __ is_final0 step0
143 type ('x, 'x0) global = __
145 type ('x, 'x0) state = __
148 ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option **)
149 let rec is_final xxx =
153 ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
154 Types.prod) IOMonad.iO **)
158 (** val trans_system_inv_rect_Type4 :
159 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
160 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
161 IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
162 let trans_system_inv_rect_Type4 hterm h1 =
163 let hcut = trans_system_rect_Type4 h1 hterm in hcut __
165 (** val trans_system_inv_rect_Type3 :
166 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
167 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
168 IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
169 let trans_system_inv_rect_Type3 hterm h1 =
170 let hcut = trans_system_rect_Type3 h1 hterm in hcut __
172 (** val trans_system_inv_rect_Type2 :
173 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
174 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
175 IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
176 let trans_system_inv_rect_Type2 hterm h1 =
177 let hcut = trans_system_rect_Type2 h1 hterm in hcut __
179 (** val trans_system_inv_rect_Type1 :
180 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
181 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
182 IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
183 let trans_system_inv_rect_Type1 hterm h1 =
184 let hcut = trans_system_rect_Type1 h1 hterm in hcut __
186 (** val trans_system_inv_rect_Type0 :
187 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
188 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
189 IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
190 let trans_system_inv_rect_Type0 hterm h1 =
191 let hcut = trans_system_rect_Type0 h1 hterm in hcut __
194 Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2,
195 (Events.trace, __) Types.prod) IOMonad.iO **)
196 let rec repeat n exec g s =
198 | Nat.O -> IOMonad.Value { Types.fst = Events.e0; Types.snd = s }
201 (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
202 (Obj.magic (exec.step g s)) (fun t1 s1 ->
203 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
204 (Obj.magic (repeat n' exec g s1)) (fun tn sn ->
205 Obj.magic (IOMonad.Value { Types.fst = (Events.eapp t1 tn);
209 ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
210 (Events.trace, 'a2 List.list) Types.prod Errors.res **)
211 let rec trace_map f = function
212 | List.Nil -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil }
213 | List.Cons (h, t) ->
215 (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h) (fun tr h' ->
216 Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (trace_map f t))
218 Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); Types.snd =
219 (List.Cons (h', t')) }))))
221 type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g :
222 __; avs_inv : (__ -> Bool.bool) }
224 (** val await_value_stuff_rect_Type4 :
225 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
226 await_value_stuff -> 'a1 **)
227 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6097 =
228 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6097
230 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
232 (** val await_value_stuff_rect_Type5 :
233 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
234 await_value_stuff -> 'a1 **)
235 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6099 =
236 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6099
238 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
240 (** val await_value_stuff_rect_Type3 :
241 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
242 await_value_stuff -> 'a1 **)
243 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6101 =
244 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6101
246 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
248 (** val await_value_stuff_rect_Type2 :
249 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
250 await_value_stuff -> 'a1 **)
251 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6103 =
252 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6103
254 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
256 (** val await_value_stuff_rect_Type1 :
257 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
258 await_value_stuff -> 'a1 **)
259 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6105 =
260 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6105
262 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
264 (** val await_value_stuff_rect_Type0 :
265 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
266 await_value_stuff -> 'a1 **)
267 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6107 =
268 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6107
270 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
276 (** val avs_exec : await_value_stuff -> (__, __) trans_system **)
277 let rec avs_exec xxx =
280 (** val avs_g : await_value_stuff -> __ **)
284 (** val avs_inv : await_value_stuff -> __ -> Bool.bool **)
285 let rec avs_inv xxx =
288 (** val await_value_stuff_inv_rect_Type4 :
289 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
290 Bool.bool) -> __ -> 'a1) -> 'a1 **)
291 let await_value_stuff_inv_rect_Type4 hterm h1 =
292 let hcut = await_value_stuff_rect_Type4 h1 hterm in hcut __
294 (** val await_value_stuff_inv_rect_Type3 :
295 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
296 Bool.bool) -> __ -> 'a1) -> 'a1 **)
297 let await_value_stuff_inv_rect_Type3 hterm h1 =
298 let hcut = await_value_stuff_rect_Type3 h1 hterm in hcut __
300 (** val await_value_stuff_inv_rect_Type2 :
301 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
302 Bool.bool) -> __ -> 'a1) -> 'a1 **)
303 let await_value_stuff_inv_rect_Type2 hterm h1 =
304 let hcut = await_value_stuff_rect_Type2 h1 hterm in hcut __
306 (** val await_value_stuff_inv_rect_Type1 :
307 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
308 Bool.bool) -> __ -> 'a1) -> 'a1 **)
309 let await_value_stuff_inv_rect_Type1 hterm h1 =
310 let hcut = await_value_stuff_rect_Type1 h1 hterm in hcut __
312 (** val await_value_stuff_inv_rect_Type0 :
313 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
314 Bool.bool) -> __ -> 'a1) -> 'a1 **)
315 let await_value_stuff_inv_rect_Type0 hterm h1 =
316 let hcut = await_value_stuff_rect_Type0 h1 hterm in hcut __
318 type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
319 and ('state, 'output, 'input) __execution =
320 | E_stop of Events.trace * Integers.int * 'state
321 | E_step of Events.trace * 'state * ('state, 'output, 'input) execution
322 | E_wrong of Errors.errmsg
323 | E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
325 (** val execution_inv_rect_Type4 :
326 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
327 -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
328 'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
329 execution) -> __ -> 'a4) -> 'a4 **)
330 let execution_inv_rect_Type4 hterm h1 h2 h3 h4 =
334 | E_stop (x, x0, x1) -> h1 x x0 x1
335 | E_step (x, x0, x1) -> h2 x x0 x1
337 | E_interact (x, x0) -> h4 x x0
341 (** val execution_inv_rect_Type3 :
342 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
343 -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
344 'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
345 execution) -> __ -> 'a4) -> 'a4 **)
346 let execution_inv_rect_Type3 hterm h1 h2 h3 h4 =
350 | E_stop (x, x0, x1) -> h1 x x0 x1
351 | E_step (x, x0, x1) -> h2 x x0 x1
353 | E_interact (x, x0) -> h4 x x0
357 (** val execution_inv_rect_Type2 :
358 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
359 -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
360 'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
361 execution) -> __ -> 'a4) -> 'a4 **)
362 let execution_inv_rect_Type2 hterm h1 h2 h3 h4 =
366 | E_stop (x, x0, x1) -> h1 x x0 x1
367 | E_step (x, x0, x1) -> h2 x x0 x1
369 | E_interact (x, x0) -> h4 x x0
373 (** val execution_inv_rect_Type1 :
374 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
375 -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
376 'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
377 execution) -> __ -> 'a4) -> 'a4 **)
378 let execution_inv_rect_Type1 hterm h1 h2 h3 h4 =
382 | E_stop (x, x0, x1) -> h1 x x0 x1
383 | E_step (x, x0, x1) -> h2 x x0 x1
385 | E_interact (x, x0) -> h4 x x0
389 (** val execution_inv_rect_Type0 :
390 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
391 -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
392 'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
393 execution) -> __ -> 'a4) -> 'a4 **)
394 let execution_inv_rect_Type0 hterm h1 h2 h3 h4 =
398 | E_stop (x, x0, x1) -> h1 x x0 x1
399 | E_step (x, x0, x1) -> h2 x x0 x1
401 | E_interact (x, x0) -> h4 x x0
405 (** val execution_discr :
406 ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
407 let execution_discr x y =
408 Logic.eq_rect_Type2 x
411 | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
412 | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
413 | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
414 | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
416 (** val execution_jmdiscr :
417 ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
418 let execution_jmdiscr x y =
419 Logic.eq_rect_Type2 x
422 | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
423 | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
424 | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
425 | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
427 (** val exec_inf_aux :
428 ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __)
429 Types.prod) IOMonad.iO -> (__, 'a1, 'a2) execution **)
430 let rec exec_inf_aux exec g = function
431 | IOMonad.Interact (out, k') ->
432 lazy (E_interact (out, (fun v -> exec_inf_aux exec g (k' v))))
434 let { Types.fst = t; Types.snd = s' } = v in
435 (match exec.is_final g s' with
437 lazy (E_step (t, s', (exec_inf_aux exec g (exec.step g s'))))
438 | Types.Some r -> lazy (E_stop (t, r, s')))
439 | IOMonad.Wrong m -> lazy (E_wrong m)
441 type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
442 make_global : (__ -> __);
443 make_initial_state : (__ -> __ Errors.res) }
445 (** val fullexec_rect_Type4 :
446 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
447 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
448 let rec fullexec_rect_Type4 h_mk_fullexec x_6125 =
449 let { es1 = es2; make_global = make_global0; make_initial_state =
450 make_initial_state0 } = x_6125
452 h_mk_fullexec __ es2 make_global0 make_initial_state0
454 (** val fullexec_rect_Type5 :
455 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
456 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
457 let rec fullexec_rect_Type5 h_mk_fullexec x_6127 =
458 let { es1 = es2; make_global = make_global0; make_initial_state =
459 make_initial_state0 } = x_6127
461 h_mk_fullexec __ es2 make_global0 make_initial_state0
463 (** val fullexec_rect_Type3 :
464 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
465 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
466 let rec fullexec_rect_Type3 h_mk_fullexec x_6129 =
467 let { es1 = es2; make_global = make_global0; make_initial_state =
468 make_initial_state0 } = x_6129
470 h_mk_fullexec __ es2 make_global0 make_initial_state0
472 (** val fullexec_rect_Type2 :
473 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
474 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
475 let rec fullexec_rect_Type2 h_mk_fullexec x_6131 =
476 let { es1 = es2; make_global = make_global0; make_initial_state =
477 make_initial_state0 } = x_6131
479 h_mk_fullexec __ es2 make_global0 make_initial_state0
481 (** val fullexec_rect_Type1 :
482 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
483 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
484 let rec fullexec_rect_Type1 h_mk_fullexec x_6133 =
485 let { es1 = es2; make_global = make_global0; make_initial_state =
486 make_initial_state0 } = x_6133
488 h_mk_fullexec __ es2 make_global0 make_initial_state0
490 (** val fullexec_rect_Type0 :
491 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
492 'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
493 let rec fullexec_rect_Type0 h_mk_fullexec x_6135 =
494 let { es1 = es2; make_global = make_global0; make_initial_state =
495 make_initial_state0 } = x_6135
497 h_mk_fullexec __ es2 make_global0 make_initial_state0
499 type ('x, 'x0) program = __
501 (** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
505 (** val make_global : ('a1, 'a2) fullexec -> __ -> __ **)
506 let rec make_global xxx =
509 (** val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res **)
510 let rec make_initial_state xxx =
511 xxx.make_initial_state
513 (** val fullexec_inv_rect_Type4 :
514 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
515 (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
516 let fullexec_inv_rect_Type4 hterm h1 =
517 let hcut = fullexec_rect_Type4 h1 hterm in hcut __
519 (** val fullexec_inv_rect_Type3 :
520 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
521 (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
522 let fullexec_inv_rect_Type3 hterm h1 =
523 let hcut = fullexec_rect_Type3 h1 hterm in hcut __
525 (** val fullexec_inv_rect_Type2 :
526 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
527 (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
528 let fullexec_inv_rect_Type2 hterm h1 =
529 let hcut = fullexec_rect_Type2 h1 hterm in hcut __
531 (** val fullexec_inv_rect_Type1 :
532 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
533 (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
534 let fullexec_inv_rect_Type1 hterm h1 =
535 let hcut = fullexec_rect_Type1 h1 hterm in hcut __
537 (** val fullexec_inv_rect_Type0 :
538 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
539 (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
540 let fullexec_inv_rect_Type0 hterm h1 =
541 let hcut = fullexec_rect_Type0 h1 hterm in hcut __
543 (** val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution **)
545 match fx.make_initial_state p with
547 exec_inf_aux fx.es1 (fx.make_global p) (IOMonad.Value { Types.fst =
548 Events.e0; Types.snd = s })
549 | Errors.Error m -> lazy (E_wrong m)
551 type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
553 (** val split_trace :
554 ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
555 'a2) execution) Types.prod Types.option **)
556 let rec split_trace x = function
557 | Nat.O -> Types.Some { Types.fst = List.Nil; Types.snd = x }
561 | E_stop (tr, r, s) ->
564 Types.Some { Types.fst = (List.Cons ({ Types.fst = tr; Types.snd =
565 s }, List.Nil)); Types.snd = x }
566 | Nat.S x0 -> Types.None)
567 | E_step (tr, s, x') ->
569 (Monad.m_bind2 (Monad.max_def Option.option)
570 (Obj.magic (split_trace x' n')) (fun pre x'' ->
571 Obj.magic (Types.Some { Types.fst = (List.Cons ({ Types.fst = tr;
572 Types.snd = s }, pre)); Types.snd = x'' })))
573 | E_wrong x0 -> Types.None
574 | E_interact (x0, x1) -> Types.None)
577 Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
578 Types.prod List.list, __) Types.prod Errors.res **)
579 let rec exec_steps n fx g s =
583 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
586 (match fx.es1.is_final g s with
588 (match fx.es1.step g s with
589 | IOMonad.Interact (x, x0) ->
590 Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
591 | IOMonad.Value trs ->
593 (Monad.m_bind2 (Monad.max_def Errors.res0)
594 (Obj.magic (exec_steps m fx g trs.Types.snd)) (fun tl s' ->
595 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
596 (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst },
597 tl)); Types.snd = s' }))
598 | IOMonad.Wrong m0 -> Errors.Error m0)
600 Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))
602 (** val gather_trace :
603 ('a1, Events.trace) Types.prod List.list -> Events.trace **)
604 let rec gather_trace = function
605 | List.Nil -> Events.e0
606 | List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)
608 (** val switch_trace_aux :
609 Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
610 (Events.trace, 'a1) Types.prod List.list **)
611 let rec switch_trace_aux tr l s' =
613 | List.Nil -> List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil)
614 | List.Cons (h, t) ->
615 List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst },
616 (switch_trace_aux h.Types.snd t s'))
618 (** val switch_trace :
619 ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
620 Types.prod List.list **)
621 let switch_trace l s' =
623 | List.Nil -> List.Nil
624 | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'