source: driver/extracted/smallstepExec.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 21.5 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 Exp
50
51open Arithmetic
52
53open Vector
54
55open FoldStuff
56
57open BitVector
58
59open Extranat
60
61open Integers
62
63open CostLabel
64
65open PositiveMap
66
67open Deqsets
68
69open Lists
70
71open Identifiers
72
73open AST
74
75open Division
76
77open Z
78
79open BitVectorZ
80
81open Pointers
82
83open Coqlib
84
85open Values
86
87open Events
88
89type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
90                                                 Types.option);
91                                      step : (__ -> __ -> ('outty, 'inty,
92                                             (Events.trace, __) Types.prod)
93                                             IOMonad.iO) }
94
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 **)
99let 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
102
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 **)
107let 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
110
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 **)
115let 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
118
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 **)
123let 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
126
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 **)
131let 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
134
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 **)
139let 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
142
143type ('x, 'x0) global = __
144
145type ('x, 'x0) state = __
146
147(** val is_final :
148    ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option **)
149let rec is_final xxx =
150  xxx.is_final
151
152(** val step :
153    ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
154    Types.prod) IOMonad.iO **)
155let rec step xxx =
156  xxx.step
157
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 **)
162let trans_system_inv_rect_Type4 hterm h1 =
163  let hcut = trans_system_rect_Type4 h1 hterm in hcut __
164
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 **)
169let trans_system_inv_rect_Type3 hterm h1 =
170  let hcut = trans_system_rect_Type3 h1 hterm in hcut __
171
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 **)
176let trans_system_inv_rect_Type2 hterm h1 =
177  let hcut = trans_system_rect_Type2 h1 hterm in hcut __
178
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 **)
183let trans_system_inv_rect_Type1 hterm h1 =
184  let hcut = trans_system_rect_Type1 h1 hterm in hcut __
185
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 **)
190let trans_system_inv_rect_Type0 hterm h1 =
191  let hcut = trans_system_rect_Type0 h1 hterm in hcut __
192
193(** val repeat :
194    Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2,
195    (Events.trace, __) Types.prod) IOMonad.iO **)
196let rec repeat n exec g s =
197  match n with
198  | Nat.O -> IOMonad.Value { Types.fst = Events.e0; Types.snd = s }
199  | Nat.S n' ->
200    Obj.magic
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);
206            Types.snd = sn }))))
207
208(** val trace_map :
209    ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
210    (Events.trace, 'a2 List.list) Types.prod Errors.res **)
211let rec trace_map f = function
212| List.Nil -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil }
213| List.Cons (h, t) ->
214  Obj.magic
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))
217        (fun tr' t' ->
218        Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); Types.snd =
219          (List.Cons (h', t')) }))))
220
221type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g : 
222                           __; avs_inv : (__ -> Bool.bool) }
223
224(** val await_value_stuff_rect_Type4 :
225    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
226    await_value_stuff -> 'a1 **)
227let 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
229  in
230  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
231
232(** val await_value_stuff_rect_Type5 :
233    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
234    await_value_stuff -> 'a1 **)
235let 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
237  in
238  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
239
240(** val await_value_stuff_rect_Type3 :
241    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
242    await_value_stuff -> 'a1 **)
243let 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
245  in
246  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
247
248(** val await_value_stuff_rect_Type2 :
249    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
250    await_value_stuff -> 'a1 **)
251let 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
253  in
254  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
255
256(** val await_value_stuff_rect_Type1 :
257    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
258    await_value_stuff -> 'a1 **)
259let 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
261  in
262  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
263
264(** val await_value_stuff_rect_Type0 :
265    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
266    await_value_stuff -> 'a1 **)
267let 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
269  in
270  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
271
272type avs_O = __
273
274type avs_I = __
275
276(** val avs_exec : await_value_stuff -> (__, __) trans_system **)
277let rec avs_exec xxx =
278  xxx.avs_exec
279
280(** val avs_g : await_value_stuff -> __ **)
281let rec avs_g xxx =
282  xxx.avs_g
283
284(** val avs_inv : await_value_stuff -> __ -> Bool.bool **)
285let rec avs_inv xxx =
286  xxx.avs_inv
287
288(** val await_value_stuff_inv_rect_Type4 :
289    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
290    Bool.bool) -> __ -> 'a1) -> 'a1 **)
291let await_value_stuff_inv_rect_Type4 hterm h1 =
292  let hcut = await_value_stuff_rect_Type4 h1 hterm in hcut __
293
294(** val await_value_stuff_inv_rect_Type3 :
295    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
296    Bool.bool) -> __ -> 'a1) -> 'a1 **)
297let await_value_stuff_inv_rect_Type3 hterm h1 =
298  let hcut = await_value_stuff_rect_Type3 h1 hterm in hcut __
299
300(** val await_value_stuff_inv_rect_Type2 :
301    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
302    Bool.bool) -> __ -> 'a1) -> 'a1 **)
303let await_value_stuff_inv_rect_Type2 hterm h1 =
304  let hcut = await_value_stuff_rect_Type2 h1 hterm in hcut __
305
306(** val await_value_stuff_inv_rect_Type1 :
307    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
308    Bool.bool) -> __ -> 'a1) -> 'a1 **)
309let await_value_stuff_inv_rect_Type1 hterm h1 =
310  let hcut = await_value_stuff_rect_Type1 h1 hterm in hcut __
311
312(** val await_value_stuff_inv_rect_Type0 :
313    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
314    Bool.bool) -> __ -> 'a1) -> 'a1 **)
315let await_value_stuff_inv_rect_Type0 hterm h1 =
316  let hcut = await_value_stuff_rect_Type0 h1 hterm in hcut __
317
318type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
319and ('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)
324
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 **)
330let execution_inv_rect_Type4 hterm h1 h2 h3 h4 =
331  let hcut =
332    match Lazy.force
333    hterm with
334    | E_stop (x, x0, x1) -> h1 x x0 x1
335    | E_step (x, x0, x1) -> h2 x x0 x1
336    | E_wrong x -> h3 x
337    | E_interact (x, x0) -> h4 x x0
338  in
339  hcut __
340
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 **)
346let execution_inv_rect_Type3 hterm h1 h2 h3 h4 =
347  let hcut =
348    match Lazy.force
349    hterm with
350    | E_stop (x, x0, x1) -> h1 x x0 x1
351    | E_step (x, x0, x1) -> h2 x x0 x1
352    | E_wrong x -> h3 x
353    | E_interact (x, x0) -> h4 x x0
354  in
355  hcut __
356
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 **)
362let execution_inv_rect_Type2 hterm h1 h2 h3 h4 =
363  let hcut =
364    match Lazy.force
365    hterm with
366    | E_stop (x, x0, x1) -> h1 x x0 x1
367    | E_step (x, x0, x1) -> h2 x x0 x1
368    | E_wrong x -> h3 x
369    | E_interact (x, x0) -> h4 x x0
370  in
371  hcut __
372
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 **)
378let execution_inv_rect_Type1 hterm h1 h2 h3 h4 =
379  let hcut =
380    match Lazy.force
381    hterm with
382    | E_stop (x, x0, x1) -> h1 x x0 x1
383    | E_step (x, x0, x1) -> h2 x x0 x1
384    | E_wrong x -> h3 x
385    | E_interact (x, x0) -> h4 x x0
386  in
387  hcut __
388
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 **)
394let execution_inv_rect_Type0 hterm h1 h2 h3 h4 =
395  let hcut =
396    match Lazy.force
397    hterm with
398    | E_stop (x, x0, x1) -> h1 x x0 x1
399    | E_step (x, x0, x1) -> h2 x x0 x1
400    | E_wrong x -> h3 x
401    | E_interact (x, x0) -> h4 x x0
402  in
403  hcut __
404
405(** val execution_discr :
406    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
407let execution_discr x y =
408  Logic.eq_rect_Type2 x
409    (match Lazy.force
410     x with
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
415
416(** val execution_jmdiscr :
417    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
418let execution_jmdiscr x y =
419  Logic.eq_rect_Type2 x
420    (match Lazy.force
421     x with
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
426
427(** val exec_inf_aux :
428    ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __)
429    Types.prod) IOMonad.iO -> (__, 'a1, 'a2) execution **)
430let 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))))
433| IOMonad.Value v ->
434  let { Types.fst = t; Types.snd = s' } = v in
435  (match exec.is_final g s' with
436   | Types.None ->
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)
440
441type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
442                                  make_global : (__ -> __);
443                                  make_initial_state : (__ -> __ Errors.res) }
444
445(** val fullexec_rect_Type4 :
446    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
447    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
448let 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
451  in
452  h_mk_fullexec __ es2 make_global0 make_initial_state0
453
454(** val fullexec_rect_Type5 :
455    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
456    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
457let 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
460  in
461  h_mk_fullexec __ es2 make_global0 make_initial_state0
462
463(** val fullexec_rect_Type3 :
464    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
465    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
466let 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
469  in
470  h_mk_fullexec __ es2 make_global0 make_initial_state0
471
472(** val fullexec_rect_Type2 :
473    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
474    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
475let 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
478  in
479  h_mk_fullexec __ es2 make_global0 make_initial_state0
480
481(** val fullexec_rect_Type1 :
482    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
483    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
484let 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
487  in
488  h_mk_fullexec __ es2 make_global0 make_initial_state0
489
490(** val fullexec_rect_Type0 :
491    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
492    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
493let 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
496  in
497  h_mk_fullexec __ es2 make_global0 make_initial_state0
498
499type ('x, 'x0) program = __
500
501(** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
502let rec es1 xxx =
503  xxx.es1
504
505(** val make_global : ('a1, 'a2) fullexec -> __ -> __ **)
506let rec make_global xxx =
507  xxx.make_global
508
509(** val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res **)
510let rec make_initial_state xxx =
511  xxx.make_initial_state
512
513(** val fullexec_inv_rect_Type4 :
514    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
515    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
516let fullexec_inv_rect_Type4 hterm h1 =
517  let hcut = fullexec_rect_Type4 h1 hterm in hcut __
518
519(** val fullexec_inv_rect_Type3 :
520    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
521    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
522let fullexec_inv_rect_Type3 hterm h1 =
523  let hcut = fullexec_rect_Type3 h1 hterm in hcut __
524
525(** val fullexec_inv_rect_Type2 :
526    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
527    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
528let fullexec_inv_rect_Type2 hterm h1 =
529  let hcut = fullexec_rect_Type2 h1 hterm in hcut __
530
531(** val fullexec_inv_rect_Type1 :
532    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
533    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
534let fullexec_inv_rect_Type1 hterm h1 =
535  let hcut = fullexec_rect_Type1 h1 hterm in hcut __
536
537(** val fullexec_inv_rect_Type0 :
538    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
539    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
540let fullexec_inv_rect_Type0 hterm h1 =
541  let hcut = fullexec_rect_Type0 h1 hterm in hcut __
542
543(** val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution **)
544let exec_inf fx p =
545  match fx.make_initial_state p with
546  | Errors.OK s ->
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)
550
551type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
552
553(** val split_trace :
554    ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
555    'a2) execution) Types.prod Types.option **)
556let rec split_trace x = function
557| Nat.O -> Types.Some { Types.fst = List.Nil; Types.snd = x }
558| Nat.S n' ->
559  (match Lazy.force
560   x with
561   | E_stop (tr, r, s) ->
562     (match n' with
563      | Nat.O ->
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') ->
568     Obj.magic
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)
575
576(** val exec_steps :
577    Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
578    Types.prod List.list, __) Types.prod Errors.res **)
579let rec exec_steps n fx g s =
580  match n with
581  | Nat.O ->
582    Obj.magic
583      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
584        Types.snd = s })
585  | Nat.S m ->
586    (match fx.es1.is_final g s with
587     | Types.None ->
588       (match fx.es1.step g s with
589        | IOMonad.Interact (x, x0) ->
590          Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
591        | IOMonad.Value trs ->
592          Obj.magic
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)
599     | Types.Some r ->
600       Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))
601
602(** val gather_trace :
603    ('a1, Events.trace) Types.prod List.list -> Events.trace **)
604let rec gather_trace = function
605| List.Nil -> Events.e0
606| List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)
607
608(** val switch_trace_aux :
609    Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
610    (Events.trace, 'a1) Types.prod List.list **)
611let rec switch_trace_aux tr l s' =
612  match l with
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'))
617
618(** val switch_trace :
619    ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
620    Types.prod List.list **)
621let switch_trace l s' =
622  match l with
623  | List.Nil -> List.Nil
624  | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'
625
Note: See TracBrowser for help on using the repository browser.