source: extracted/smallstepExec.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

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