source: extracted/smallstepExec.ml @ 2731

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

Exported again.

File size: 21.6 KB
RevLine 
[2601]1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Proper
32
[2649]33open ErrorMessages
34
[2601]35open Option
36
37open Setoids
38
39open Monad
40
41open Positive
42
43open PreIdentifiers
44
45open Errors
46
47open IOMonad
48
[2717]49open Exp
50
[2601]51open Arithmetic
52
53open Vector
54
55open FoldStuff
56
57open BitVector
58
59open Extranat
60
61open Integers
62
[2717]63open BitVectorTrie
64
[2601]65open CostLabel
66
67open PositiveMap
68
69open Deqsets
70
71open Lists
72
73open Identifiers
74
75open AST
76
77open Division
78
79open Z
80
81open BitVectorZ
82
83open Pointers
84
85open Coqlib
86
87open Values
88
89open Events
90
91type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
92                                                 Types.option);
93                                      step : (__ -> __ -> ('outty, 'inty,
94                                             (Events.trace, __) Types.prod)
95                                             IOMonad.iO) }
96
97(** val trans_system_rect_Type4 :
98    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
99    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
100    'a2) trans_system -> 'a3 **)
[2730]101let rec trans_system_rect_Type4 h_mk_trans_system x_8529 =
102  let { is_final = is_final0; step = step0 } = x_8529 in
[2601]103  h_mk_trans_system __ __ is_final0 step0
104
105(** val trans_system_rect_Type5 :
106    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
107    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
108    'a2) trans_system -> 'a3 **)
[2730]109let rec trans_system_rect_Type5 h_mk_trans_system x_8531 =
110  let { is_final = is_final0; step = step0 } = x_8531 in
[2601]111  h_mk_trans_system __ __ is_final0 step0
112
113(** val trans_system_rect_Type3 :
114    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
115    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
116    'a2) trans_system -> 'a3 **)
[2730]117let rec trans_system_rect_Type3 h_mk_trans_system x_8533 =
118  let { is_final = is_final0; step = step0 } = x_8533 in
[2601]119  h_mk_trans_system __ __ is_final0 step0
120
121(** val trans_system_rect_Type2 :
122    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
123    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
124    'a2) trans_system -> 'a3 **)
[2730]125let rec trans_system_rect_Type2 h_mk_trans_system x_8535 =
126  let { is_final = is_final0; step = step0 } = x_8535 in
[2601]127  h_mk_trans_system __ __ is_final0 step0
128
129(** val trans_system_rect_Type1 :
130    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
131    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
132    'a2) trans_system -> 'a3 **)
[2730]133let rec trans_system_rect_Type1 h_mk_trans_system x_8537 =
134  let { is_final = is_final0; step = step0 } = x_8537 in
[2601]135  h_mk_trans_system __ __ is_final0 step0
136
137(** val trans_system_rect_Type0 :
138    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
139    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
140    'a2) trans_system -> 'a3 **)
[2730]141let rec trans_system_rect_Type0 h_mk_trans_system x_8539 =
142  let { is_final = is_final0; step = step0 } = x_8539 in
[2601]143  h_mk_trans_system __ __ is_final0 step0
144
145type ('a,'b) global = __
146
147type ('a,'b) state = __
148
149(** val is_final :
150    ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option **)
151let rec is_final xxx =
152  xxx.is_final
153
154(** val step :
155    ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
156    Types.prod) IOMonad.iO **)
157let rec step xxx =
158  xxx.step
159
160(** val trans_system_inv_rect_Type4 :
161    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
162    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
163    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
164let trans_system_inv_rect_Type4 hterm h1 =
165  let hcut = trans_system_rect_Type4 h1 hterm in hcut __
166
167(** val trans_system_inv_rect_Type3 :
168    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
169    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
170    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
171let trans_system_inv_rect_Type3 hterm h1 =
172  let hcut = trans_system_rect_Type3 h1 hterm in hcut __
173
174(** val trans_system_inv_rect_Type2 :
175    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
176    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
177    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
178let trans_system_inv_rect_Type2 hterm h1 =
179  let hcut = trans_system_rect_Type2 h1 hterm in hcut __
180
181(** val trans_system_inv_rect_Type1 :
182    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
183    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
184    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
185let trans_system_inv_rect_Type1 hterm h1 =
186  let hcut = trans_system_rect_Type1 h1 hterm in hcut __
187
188(** val trans_system_inv_rect_Type0 :
189    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
190    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
191    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
192let trans_system_inv_rect_Type0 hterm h1 =
193  let hcut = trans_system_rect_Type0 h1 hterm in hcut __
194
195(** val repeat :
196    Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2,
197    (Events.trace, __) Types.prod) IOMonad.iO **)
198let rec repeat n exec g0 s =
199  match n with
200  | Nat.O -> IOMonad.Value { Types.fst = Events.e0; Types.snd = s }
201  | Nat.S n' ->
202    Obj.magic
203      (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
204        (Obj.magic (exec.step g0 s)) (fun t1 s1 ->
205        Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
206          (Obj.magic (repeat n' exec g0 s1)) (fun tn sn ->
207          Obj.magic (IOMonad.Value { Types.fst = (Events.eapp t1 tn);
208            Types.snd = sn }))))
209
210(** val trace_map :
211    ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
212    (Events.trace, 'a2 List.list) Types.prod Errors.res **)
213let rec trace_map f = function
214| List.Nil -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil }
215| List.Cons (h, t) ->
216  Obj.magic
217    (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h) (fun tr h' ->
218      Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (trace_map f t))
219        (fun tr' t' ->
220        Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); Types.snd =
221          (List.Cons (h', t')) }))))
222
223type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g : 
224                           __; avs_inv : (__ -> Bool.bool) }
225
226(** val await_value_stuff_rect_Type4 :
227    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
228    await_value_stuff -> 'a1 **)
[2730]229let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_8701 =
230  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8701
[2601]231  in
232  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
233
234(** val await_value_stuff_rect_Type5 :
235    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
236    await_value_stuff -> 'a1 **)
[2730]237let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_8703 =
238  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8703
[2601]239  in
240  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
241
242(** val await_value_stuff_rect_Type3 :
243    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
244    await_value_stuff -> 'a1 **)
[2730]245let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_8705 =
246  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8705
[2601]247  in
248  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
249
250(** val await_value_stuff_rect_Type2 :
251    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
252    await_value_stuff -> 'a1 **)
[2730]253let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_8707 =
254  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8707
[2601]255  in
256  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
257
258(** val await_value_stuff_rect_Type1 :
259    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
260    await_value_stuff -> 'a1 **)
[2730]261let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_8709 =
262  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8709
[2601]263  in
264  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
265
266(** val await_value_stuff_rect_Type0 :
267    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
268    await_value_stuff -> 'a1 **)
[2730]269let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_8711 =
270  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8711
[2601]271  in
272  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
273
274type avs_O = __
275
276type avs_I = __
277
278(** val avs_exec : await_value_stuff -> (__, __) trans_system **)
279let rec avs_exec xxx =
280  xxx.avs_exec
281
282(** val avs_g : await_value_stuff -> __ **)
283let rec avs_g xxx =
284  xxx.avs_g
285
286(** val avs_inv : await_value_stuff -> __ -> Bool.bool **)
287let rec avs_inv xxx =
288  xxx.avs_inv
289
290(** val await_value_stuff_inv_rect_Type4 :
291    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
292    Bool.bool) -> __ -> 'a1) -> 'a1 **)
293let await_value_stuff_inv_rect_Type4 hterm h1 =
294  let hcut = await_value_stuff_rect_Type4 h1 hterm in hcut __
295
296(** val await_value_stuff_inv_rect_Type3 :
297    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
298    Bool.bool) -> __ -> 'a1) -> 'a1 **)
299let await_value_stuff_inv_rect_Type3 hterm h1 =
300  let hcut = await_value_stuff_rect_Type3 h1 hterm in hcut __
301
302(** val await_value_stuff_inv_rect_Type2 :
303    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
304    Bool.bool) -> __ -> 'a1) -> 'a1 **)
305let await_value_stuff_inv_rect_Type2 hterm h1 =
306  let hcut = await_value_stuff_rect_Type2 h1 hterm in hcut __
307
308(** val await_value_stuff_inv_rect_Type1 :
309    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
310    Bool.bool) -> __ -> 'a1) -> 'a1 **)
311let await_value_stuff_inv_rect_Type1 hterm h1 =
312  let hcut = await_value_stuff_rect_Type1 h1 hterm in hcut __
313
314(** val await_value_stuff_inv_rect_Type0 :
315    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
316    Bool.bool) -> __ -> 'a1) -> 'a1 **)
317let await_value_stuff_inv_rect_Type0 hterm h1 =
318  let hcut = await_value_stuff_rect_Type0 h1 hterm in hcut __
319
320type await_value = __
321
322type assert0 = __
323
[2717]324type assert_nz = __
325
[2601]326type after_aux = __
327
328type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
329and ('state, 'output, 'input) __execution =
330| E_stop of Events.trace * Integers.int * 'state
331| E_step of Events.trace * 'state * ('state, 'output, 'input) execution
332| E_wrong of Errors.errmsg
333| E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
334
335(** val execution_inv_rect_Type4 :
336    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
337    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
338    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
339    execution) -> __ -> 'a4) -> 'a4 **)
340let execution_inv_rect_Type4 hterm h1 h2 h3 h4 =
341  let hcut =
342    match Lazy.force
343    hterm with
344    | E_stop (x, x0, x1) -> h1 x x0 x1
345    | E_step (x, x0, x1) -> h2 x x0 x1
346    | E_wrong x -> h3 x
347    | E_interact (x, x0) -> h4 x x0
348  in
349  hcut __
350
351(** val execution_inv_rect_Type3 :
352    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
353    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
354    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
355    execution) -> __ -> 'a4) -> 'a4 **)
356let execution_inv_rect_Type3 hterm h1 h2 h3 h4 =
357  let hcut =
358    match Lazy.force
359    hterm with
360    | E_stop (x, x0, x1) -> h1 x x0 x1
361    | E_step (x, x0, x1) -> h2 x x0 x1
362    | E_wrong x -> h3 x
363    | E_interact (x, x0) -> h4 x x0
364  in
365  hcut __
366
367(** val execution_inv_rect_Type2 :
368    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
369    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
370    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
371    execution) -> __ -> 'a4) -> 'a4 **)
372let execution_inv_rect_Type2 hterm h1 h2 h3 h4 =
373  let hcut =
374    match Lazy.force
375    hterm with
376    | E_stop (x, x0, x1) -> h1 x x0 x1
377    | E_step (x, x0, x1) -> h2 x x0 x1
378    | E_wrong x -> h3 x
379    | E_interact (x, x0) -> h4 x x0
380  in
381  hcut __
382
383(** val execution_inv_rect_Type1 :
384    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
385    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
386    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
387    execution) -> __ -> 'a4) -> 'a4 **)
388let execution_inv_rect_Type1 hterm h1 h2 h3 h4 =
389  let hcut =
390    match Lazy.force
391    hterm with
392    | E_stop (x, x0, x1) -> h1 x x0 x1
393    | E_step (x, x0, x1) -> h2 x x0 x1
394    | E_wrong x -> h3 x
395    | E_interact (x, x0) -> h4 x x0
396  in
397  hcut __
398
399(** val execution_inv_rect_Type0 :
400    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
401    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
402    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
403    execution) -> __ -> 'a4) -> 'a4 **)
404let execution_inv_rect_Type0 hterm h1 h2 h3 h4 =
405  let hcut =
406    match Lazy.force
407    hterm with
408    | E_stop (x, x0, x1) -> h1 x x0 x1
409    | E_step (x, x0, x1) -> h2 x x0 x1
410    | E_wrong x -> h3 x
411    | E_interact (x, x0) -> h4 x x0
412  in
413  hcut __
414
415(** val execution_discr :
416    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
417let execution_discr x y =
418  Logic.eq_rect_Type2 x
419    (match Lazy.force
420     x with
421     | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
422     | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
423     | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
424     | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
425
426(** val execution_jmdiscr :
427    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
428let execution_jmdiscr x y =
429  Logic.eq_rect_Type2 x
430    (match Lazy.force
431     x with
432     | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
433     | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
434     | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
435     | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
436
437(** val exec_inf_aux :
438    ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __)
439    Types.prod) IOMonad.iO -> (__, 'a1, 'a2) execution **)
440let rec exec_inf_aux exec g0 = function
441| IOMonad.Interact (out, k') ->
442  lazy (E_interact (out, (fun v -> exec_inf_aux exec g0 (k' v))))
443| IOMonad.Value v ->
444  let { Types.fst = t; Types.snd = s' } = v in
445  (match exec.is_final g0 s' with
446   | Types.None ->
447     lazy (E_step (t, s', (exec_inf_aux exec g0 (exec.step g0 s'))))
448   | Types.Some r -> lazy (E_stop (t, r, s')))
449| IOMonad.Wrong m -> lazy (E_wrong m)
450
451type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
452                                  make_global : (__ -> __);
453                                  make_initial_state : (__ -> __ Errors.res) }
454
455(** val fullexec_rect_Type4 :
456    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
457    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]458let rec fullexec_rect_Type4 h_mk_fullexec x_8729 =
[2601]459  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]460    make_initial_state0 } = x_8729
[2601]461  in
462  h_mk_fullexec __ es2 make_global0 make_initial_state0
463
464(** val fullexec_rect_Type5 :
465    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
466    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]467let rec fullexec_rect_Type5 h_mk_fullexec x_8731 =
[2601]468  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]469    make_initial_state0 } = x_8731
[2601]470  in
471  h_mk_fullexec __ es2 make_global0 make_initial_state0
472
473(** val fullexec_rect_Type3 :
474    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
475    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]476let rec fullexec_rect_Type3 h_mk_fullexec x_8733 =
[2601]477  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]478    make_initial_state0 } = x_8733
[2601]479  in
480  h_mk_fullexec __ es2 make_global0 make_initial_state0
481
482(** val fullexec_rect_Type2 :
483    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
484    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]485let rec fullexec_rect_Type2 h_mk_fullexec x_8735 =
[2601]486  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]487    make_initial_state0 } = x_8735
[2601]488  in
489  h_mk_fullexec __ es2 make_global0 make_initial_state0
490
491(** val fullexec_rect_Type1 :
492    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
493    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]494let rec fullexec_rect_Type1 h_mk_fullexec x_8737 =
[2601]495  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]496    make_initial_state0 } = x_8737
[2601]497  in
498  h_mk_fullexec __ es2 make_global0 make_initial_state0
499
500(** val fullexec_rect_Type0 :
501    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
502    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
[2730]503let rec fullexec_rect_Type0 h_mk_fullexec x_8739 =
[2601]504  let { es1 = es2; make_global = make_global0; make_initial_state =
[2730]505    make_initial_state0 } = x_8739
[2601]506  in
507  h_mk_fullexec __ es2 make_global0 make_initial_state0
508
509type ('a,'b) program0 = __
510
511(** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
512let rec es1 xxx =
513  xxx.es1
514
515(** val make_global : ('a1, 'a2) fullexec -> __ -> __ **)
516let rec make_global xxx =
517  xxx.make_global
518
519(** val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res **)
520let rec make_initial_state xxx =
521  xxx.make_initial_state
522
523(** val fullexec_inv_rect_Type4 :
524    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
525    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
526let fullexec_inv_rect_Type4 hterm h1 =
527  let hcut = fullexec_rect_Type4 h1 hterm in hcut __
528
529(** val fullexec_inv_rect_Type3 :
530    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
531    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
532let fullexec_inv_rect_Type3 hterm h1 =
533  let hcut = fullexec_rect_Type3 h1 hterm in hcut __
534
535(** val fullexec_inv_rect_Type2 :
536    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
537    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
538let fullexec_inv_rect_Type2 hterm h1 =
539  let hcut = fullexec_rect_Type2 h1 hterm in hcut __
540
541(** val fullexec_inv_rect_Type1 :
542    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
543    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
544let fullexec_inv_rect_Type1 hterm h1 =
545  let hcut = fullexec_rect_Type1 h1 hterm in hcut __
546
547(** val fullexec_inv_rect_Type0 :
548    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
549    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
550let fullexec_inv_rect_Type0 hterm h1 =
551  let hcut = fullexec_rect_Type0 h1 hterm in hcut __
552
553(** val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution **)
554let exec_inf fx p =
555  match fx.make_initial_state p with
556  | Errors.OK s ->
557    exec_inf_aux fx.es1 (fx.make_global p) (IOMonad.Value { Types.fst =
558      Events.e0; Types.snd = s })
559  | Errors.Error m -> lazy (E_wrong m)
560
[2649]561type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
562
563(** val split_trace :
564    ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
565    'a2) execution) Types.prod Types.option **)
566let rec split_trace x = function
567| Nat.O -> Types.Some { Types.fst = List.Nil; Types.snd = x }
568| Nat.S n' ->
569  (match Lazy.force
570   x with
571   | E_stop (tr, r, s) ->
572     (match n' with
573      | Nat.O ->
574        Types.Some { Types.fst = (List.Cons ({ Types.fst = tr; Types.snd =
575          s }, List.Nil)); Types.snd = x }
576      | Nat.S x0 -> Types.None)
577   | E_step (tr, s, x') ->
578     Obj.magic
579       (Monad.m_bind2 (Monad.max_def Option.option0)
580         (Obj.magic (split_trace x' n')) (fun pre x'' ->
581         Obj.magic (Types.Some { Types.fst = (List.Cons ({ Types.fst = tr;
582           Types.snd = s }, pre)); Types.snd = x'' })))
583   | E_wrong x0 -> Types.None
584   | E_interact (x0, x1) -> Types.None)
585
[2717]586(** val exec_steps :
587    Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
588    Types.prod List.list, __) Types.prod Errors.res **)
589let rec exec_steps n fx g0 s =
590  match n with
591  | Nat.O ->
592    Obj.magic
593      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
594        Types.snd = s })
595  | Nat.S m ->
596    (match fx.es1.is_final g0 s with
597     | Types.None ->
598       (match fx.es1.step g0 s with
599        | IOMonad.Interact (x, x0) ->
600          Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
601        | IOMonad.Value trs ->
602          Obj.magic
603            (Monad.m_bind2 (Monad.max_def Errors.res0)
604              (Obj.magic (exec_steps m fx g0 trs.Types.snd)) (fun tl s' ->
605              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
606                (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst },
607                tl)); Types.snd = s' }))
608        | IOMonad.Wrong m0 -> Errors.Error m0)
609     | Types.Some r ->
610       Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))
611
612(** val gather_trace :
613    ('a1, Events.trace) Types.prod List.list -> Events.trace **)
614let rec gather_trace = function
615| List.Nil -> Events.e0
616| List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)
617
618(** val switch_trace_aux :
619    Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
620    (Events.trace, 'a1) Types.prod List.list **)
621let rec switch_trace_aux tr l s' =
622  match l with
623  | List.Nil -> List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil)
624  | List.Cons (h, t) ->
625    List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst },
626      (switch_trace_aux h.Types.snd t s'))
627
628(** val switch_trace :
629    ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
630    Types.prod List.list **)
631let switch_trace l s' =
632  match l with
633  | List.Nil -> List.Nil
634  | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'
635
Note: See TracBrowser for help on using the repository browser.