source: extracted/smallstepExec.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).
File size: 21.6 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 BitVectorTrie
64
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 **)
101let rec trans_system_rect_Type4 h_mk_trans_system x_5873 =
102  let { is_final = is_final0; step = step0 } = x_5873 in
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 **)
109let rec trans_system_rect_Type5 h_mk_trans_system x_5875 =
110  let { is_final = is_final0; step = step0 } = x_5875 in
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 **)
117let rec trans_system_rect_Type3 h_mk_trans_system x_5877 =
118  let { is_final = is_final0; step = step0 } = x_5877 in
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 **)
125let rec trans_system_rect_Type2 h_mk_trans_system x_5879 =
126  let { is_final = is_final0; step = step0 } = x_5879 in
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 **)
133let rec trans_system_rect_Type1 h_mk_trans_system x_5881 =
134  let { is_final = is_final0; step = step0 } = x_5881 in
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 **)
141let rec trans_system_rect_Type0 h_mk_trans_system x_5883 =
142  let { is_final = is_final0; step = step0 } = x_5883 in
143  h_mk_trans_system __ __ is_final0 step0
144
145type ('x, 'x0) global = __
146
147type ('x, 'x0) 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 **)
229let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6045 =
230  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6045
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 **)
237let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6047 =
238  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6047
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 **)
245let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6049 =
246  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6049
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 **)
253let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6051 =
254  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6051
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 **)
261let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6053 =
262  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6053
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 **)
269let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6055 =
270  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6055
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
324type assert_nz = __
325
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 **)
458let rec fullexec_rect_Type4 h_mk_fullexec x_6073 =
459  let { es1 = es2; make_global = make_global0; make_initial_state =
460    make_initial_state0 } = x_6073
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 **)
467let rec fullexec_rect_Type5 h_mk_fullexec x_6075 =
468  let { es1 = es2; make_global = make_global0; make_initial_state =
469    make_initial_state0 } = x_6075
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 **)
476let rec fullexec_rect_Type3 h_mk_fullexec x_6077 =
477  let { es1 = es2; make_global = make_global0; make_initial_state =
478    make_initial_state0 } = x_6077
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 **)
485let rec fullexec_rect_Type2 h_mk_fullexec x_6079 =
486  let { es1 = es2; make_global = make_global0; make_initial_state =
487    make_initial_state0 } = x_6079
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 **)
494let rec fullexec_rect_Type1 h_mk_fullexec x_6081 =
495  let { es1 = es2; make_global = make_global0; make_initial_state =
496    make_initial_state0 } = x_6081
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 **)
503let rec fullexec_rect_Type0 h_mk_fullexec x_6083 =
504  let { es1 = es2; make_global = make_global0; make_initial_state =
505    make_initial_state0 } = x_6083
506  in
507  h_mk_fullexec __ es2 make_global0 make_initial_state0
508
509type ('x, 'x0) 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
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
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.