source: extracted/smallstepExec.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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_5847 =
102  let { is_final = is_final0; step = step0 } = x_5847 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_5849 =
110  let { is_final = is_final0; step = step0 } = x_5849 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_5851 =
118  let { is_final = is_final0; step = step0 } = x_5851 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_5853 =
126  let { is_final = is_final0; step = step0 } = x_5853 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_5855 =
134  let { is_final = is_final0; step = step0 } = x_5855 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_5857 =
142  let { is_final = is_final0; step = step0 } = x_5857 in
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 **)
229let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6019 =
230  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6019
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_6021 =
238  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6021
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_6023 =
246  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6023
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_6025 =
254  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6025
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_6027 =
262  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6027
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_6029 =
270  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6029
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_6047 =
459  let { es1 = es2; make_global = make_global0; make_initial_state =
460    make_initial_state0 } = x_6047
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_6049 =
468  let { es1 = es2; make_global = make_global0; make_initial_state =
469    make_initial_state0 } = x_6049
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_6051 =
477  let { es1 = es2; make_global = make_global0; make_initial_state =
478    make_initial_state0 } = x_6051
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_6053 =
486  let { es1 = es2; make_global = make_global0; make_initial_state =
487    make_initial_state0 } = x_6053
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_6055 =
495  let { es1 = es2; make_global = make_global0; make_initial_state =
496    make_initial_state0 } = x_6055
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_6057 =
504  let { es1 = es2; make_global = make_global0; make_initial_state =
505    make_initial_state0 } = x_6057
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
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.