source: extracted/smallstep.ml @ 2716

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

...

File size: 16.8 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Integers
18
19open AST
20
21open Division
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open Events
84
85type transrel =
86| Mk_transrel
87
88(** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
89let rec transrel_rect_Type4 h_mk_transrel = function
90| Mk_transrel -> h_mk_transrel __ __ __
91
92(** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
93let rec transrel_rect_Type5 h_mk_transrel = function
94| Mk_transrel -> h_mk_transrel __ __ __
95
96(** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
97let rec transrel_rect_Type3 h_mk_transrel = function
98| Mk_transrel -> h_mk_transrel __ __ __
99
100(** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
101let rec transrel_rect_Type2 h_mk_transrel = function
102| Mk_transrel -> h_mk_transrel __ __ __
103
104(** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
105let rec transrel_rect_Type1 h_mk_transrel = function
106| Mk_transrel -> h_mk_transrel __ __ __
107
108(** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
109let rec transrel_rect_Type0 h_mk_transrel = function
110| Mk_transrel -> h_mk_transrel __ __ __
111
112type genv = __
113
114type state = __
115
116type step = __
117
118(** val transrel_inv_rect_Type4 :
119    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
120let transrel_inv_rect_Type4 hterm h1 =
121  let hcut = transrel_rect_Type4 h1 hterm in hcut __
122
123(** val transrel_inv_rect_Type3 :
124    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
125let transrel_inv_rect_Type3 hterm h1 =
126  let hcut = transrel_rect_Type3 h1 hterm in hcut __
127
128(** val transrel_inv_rect_Type2 :
129    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
130let transrel_inv_rect_Type2 hterm h1 =
131  let hcut = transrel_rect_Type2 h1 hterm in hcut __
132
133(** val transrel_inv_rect_Type1 :
134    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
135let transrel_inv_rect_Type1 hterm h1 =
136  let hcut = transrel_rect_Type1 h1 hterm in hcut __
137
138(** val transrel_inv_rect_Type0 :
139    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
140let transrel_inv_rect_Type0 hterm h1 =
141  let hcut = transrel_rect_Type0 h1 hterm in hcut __
142
143(** val transrel_jmdiscr : transrel -> transrel -> __ **)
144let transrel_jmdiscr x y =
145  Logic.eq_rect_Type2 x
146    (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y
147
148type program_behavior =
149| Terminates of Events.trace * Integers.int
150| Diverges of Events.trace
151| Reacts of Events.traceinf
152| Goes_wrong of Events.trace
153
154(** val program_behavior_rect_Type4 :
155    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
156    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
157    'a1 **)
158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
159| Terminates (x_4040, x_4039) -> h_Terminates x_4040 x_4039
160| Diverges x_4041 -> h_Diverges x_4041
161| Reacts x_4042 -> h_Reacts x_4042
162| Goes_wrong x_4043 -> h_Goes_wrong x_4043
163
164(** val program_behavior_rect_Type5 :
165    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
166    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
167    'a1 **)
168let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
169| Terminates (x_4050, x_4049) -> h_Terminates x_4050 x_4049
170| Diverges x_4051 -> h_Diverges x_4051
171| Reacts x_4052 -> h_Reacts x_4052
172| Goes_wrong x_4053 -> h_Goes_wrong x_4053
173
174(** val program_behavior_rect_Type3 :
175    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
176    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
177    'a1 **)
178let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
179| Terminates (x_4060, x_4059) -> h_Terminates x_4060 x_4059
180| Diverges x_4061 -> h_Diverges x_4061
181| Reacts x_4062 -> h_Reacts x_4062
182| Goes_wrong x_4063 -> h_Goes_wrong x_4063
183
184(** val program_behavior_rect_Type2 :
185    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
186    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
187    'a1 **)
188let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
189| Terminates (x_4070, x_4069) -> h_Terminates x_4070 x_4069
190| Diverges x_4071 -> h_Diverges x_4071
191| Reacts x_4072 -> h_Reacts x_4072
192| Goes_wrong x_4073 -> h_Goes_wrong x_4073
193
194(** val program_behavior_rect_Type1 :
195    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
196    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
197    'a1 **)
198let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
199| Terminates (x_4080, x_4079) -> h_Terminates x_4080 x_4079
200| Diverges x_4081 -> h_Diverges x_4081
201| Reacts x_4082 -> h_Reacts x_4082
202| Goes_wrong x_4083 -> h_Goes_wrong x_4083
203
204(** val program_behavior_rect_Type0 :
205    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
206    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
207    'a1 **)
208let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
209| Terminates (x_4090, x_4089) -> h_Terminates x_4090 x_4089
210| Diverges x_4091 -> h_Diverges x_4091
211| Reacts x_4092 -> h_Reacts x_4092
212| Goes_wrong x_4093 -> h_Goes_wrong x_4093
213
214(** val program_behavior_inv_rect_Type4 :
215    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
216    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
217    (Events.trace -> __ -> 'a1) -> 'a1 **)
218let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
219  let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __
220
221(** val program_behavior_inv_rect_Type3 :
222    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
223    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
224    (Events.trace -> __ -> 'a1) -> 'a1 **)
225let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
226  let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __
227
228(** val program_behavior_inv_rect_Type2 :
229    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
230    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
231    (Events.trace -> __ -> 'a1) -> 'a1 **)
232let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
233  let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __
234
235(** val program_behavior_inv_rect_Type1 :
236    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
237    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
238    (Events.trace -> __ -> 'a1) -> 'a1 **)
239let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
240  let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __
241
242(** val program_behavior_inv_rect_Type0 :
243    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
244    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
245    (Events.trace -> __ -> 'a1) -> 'a1 **)
246let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
247  let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __
248
249(** val program_behavior_discr :
250    program_behavior -> program_behavior -> __ **)
251let program_behavior_discr x y =
252  Logic.eq_rect_Type2 x
253    (match x with
254     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
255     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
256     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
257     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
258
259(** val program_behavior_jmdiscr :
260    program_behavior -> program_behavior -> __ **)
261let program_behavior_jmdiscr x y =
262  Logic.eq_rect_Type2 x
263    (match x with
264     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
265     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
266     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
267     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
268
269type semantics = { trans : transrel; ge : __ }
270
271(** val semantics_rect_Type4 :
272    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
273let rec semantics_rect_Type4 h_mk_semantics x_4420 =
274  let { trans = trans0; ge = ge0 } = x_4420 in
275  h_mk_semantics trans0 __ __ ge0
276
277(** val semantics_rect_Type5 :
278    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
279let rec semantics_rect_Type5 h_mk_semantics x_4422 =
280  let { trans = trans0; ge = ge0 } = x_4422 in
281  h_mk_semantics trans0 __ __ ge0
282
283(** val semantics_rect_Type3 :
284    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
285let rec semantics_rect_Type3 h_mk_semantics x_4424 =
286  let { trans = trans0; ge = ge0 } = x_4424 in
287  h_mk_semantics trans0 __ __ ge0
288
289(** val semantics_rect_Type2 :
290    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
291let rec semantics_rect_Type2 h_mk_semantics x_4426 =
292  let { trans = trans0; ge = ge0 } = x_4426 in
293  h_mk_semantics trans0 __ __ ge0
294
295(** val semantics_rect_Type1 :
296    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
297let rec semantics_rect_Type1 h_mk_semantics x_4428 =
298  let { trans = trans0; ge = ge0 } = x_4428 in
299  h_mk_semantics trans0 __ __ ge0
300
301(** val semantics_rect_Type0 :
302    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
303let rec semantics_rect_Type0 h_mk_semantics x_4430 =
304  let { trans = trans0; ge = ge0 } = x_4430 in
305  h_mk_semantics trans0 __ __ ge0
306
307(** val trans : semantics -> transrel **)
308let rec trans xxx =
309  xxx.trans
310
311type initial = __
312
313type final = __
314
315(** val ge : semantics -> __ **)
316let rec ge xxx =
317  xxx.ge
318
319(** val semantics_inv_rect_Type4 :
320    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
321let semantics_inv_rect_Type4 hterm h1 =
322  let hcut = semantics_rect_Type4 h1 hterm in hcut __
323
324(** val semantics_inv_rect_Type3 :
325    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
326let semantics_inv_rect_Type3 hterm h1 =
327  let hcut = semantics_rect_Type3 h1 hterm in hcut __
328
329(** val semantics_inv_rect_Type2 :
330    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
331let semantics_inv_rect_Type2 hterm h1 =
332  let hcut = semantics_rect_Type2 h1 hterm in hcut __
333
334(** val semantics_inv_rect_Type1 :
335    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
336let semantics_inv_rect_Type1 hterm h1 =
337  let hcut = semantics_rect_Type1 h1 hterm in hcut __
338
339(** val semantics_inv_rect_Type0 :
340    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
341let semantics_inv_rect_Type0 hterm h1 =
342  let hcut = semantics_rect_Type0 h1 hterm in hcut __
343
344(** val semantics_jmdiscr : semantics -> semantics -> __ **)
345let semantics_jmdiscr x y =
346  Logic.eq_rect_Type2 x
347    (let { trans = a0; ge = a3 } = x in
348    Obj.magic (fun _ dH -> dH __ __ __ __)) y
349
350type related_semantics = { sem1 : semantics; sem2 : semantics }
351
352(** val related_semantics_rect_Type4 :
353    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
354    'a1 **)
355let rec related_semantics_rect_Type4 h_mk_related_semantics x_4449 =
356  let { sem1 = sem3; sem2 = sem4 } = x_4449 in
357  h_mk_related_semantics sem3 sem4 __ __ __
358
359(** val related_semantics_rect_Type5 :
360    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
361    'a1 **)
362let rec related_semantics_rect_Type5 h_mk_related_semantics x_4451 =
363  let { sem1 = sem3; sem2 = sem4 } = x_4451 in
364  h_mk_related_semantics sem3 sem4 __ __ __
365
366(** val related_semantics_rect_Type3 :
367    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
368    'a1 **)
369let rec related_semantics_rect_Type3 h_mk_related_semantics x_4453 =
370  let { sem1 = sem3; sem2 = sem4 } = x_4453 in
371  h_mk_related_semantics sem3 sem4 __ __ __
372
373(** val related_semantics_rect_Type2 :
374    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
375    'a1 **)
376let rec related_semantics_rect_Type2 h_mk_related_semantics x_4455 =
377  let { sem1 = sem3; sem2 = sem4 } = x_4455 in
378  h_mk_related_semantics sem3 sem4 __ __ __
379
380(** val related_semantics_rect_Type1 :
381    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
382    'a1 **)
383let rec related_semantics_rect_Type1 h_mk_related_semantics x_4457 =
384  let { sem1 = sem3; sem2 = sem4 } = x_4457 in
385  h_mk_related_semantics sem3 sem4 __ __ __
386
387(** val related_semantics_rect_Type0 :
388    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
389    'a1 **)
390let rec related_semantics_rect_Type0 h_mk_related_semantics x_4459 =
391  let { sem1 = sem3; sem2 = sem4 } = x_4459 in
392  h_mk_related_semantics sem3 sem4 __ __ __
393
394(** val sem1 : related_semantics -> semantics **)
395let rec sem1 xxx =
396  xxx.sem1
397
398(** val sem2 : related_semantics -> semantics **)
399let rec sem2 xxx =
400  xxx.sem2
401
402type match_states = __
403
404(** val related_semantics_inv_rect_Type4 :
405    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
406    'a1) -> 'a1 **)
407let related_semantics_inv_rect_Type4 hterm h1 =
408  let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
409
410(** val related_semantics_inv_rect_Type3 :
411    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
412    'a1) -> 'a1 **)
413let related_semantics_inv_rect_Type3 hterm h1 =
414  let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
415
416(** val related_semantics_inv_rect_Type2 :
417    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
418    'a1) -> 'a1 **)
419let related_semantics_inv_rect_Type2 hterm h1 =
420  let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
421
422(** val related_semantics_inv_rect_Type1 :
423    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
424    'a1) -> 'a1 **)
425let related_semantics_inv_rect_Type1 hterm h1 =
426  let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
427
428(** val related_semantics_inv_rect_Type0 :
429    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
430    'a1) -> 'a1 **)
431let related_semantics_inv_rect_Type0 hterm h1 =
432  let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
433
434(** val related_semantics_jmdiscr :
435    related_semantics -> related_semantics -> __ **)
436let related_semantics_jmdiscr x y =
437  Logic.eq_rect_Type2 x
438    (let { sem1 = a0; sem2 = a1 } = x in
439    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
440
441type order_sim =
442  related_semantics
443  (* singleton inductive, whose constructor was mk_order_sim *)
444
445(** val order_sim_rect_Type4 :
446    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
447let rec order_sim_rect_Type4 h_mk_order_sim x_4480 =
448  let sem = x_4480 in h_mk_order_sim sem __ __
449
450(** val order_sim_rect_Type5 :
451    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
452let rec order_sim_rect_Type5 h_mk_order_sim x_4482 =
453  let sem = x_4482 in h_mk_order_sim sem __ __
454
455(** val order_sim_rect_Type3 :
456    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
457let rec order_sim_rect_Type3 h_mk_order_sim x_4484 =
458  let sem = x_4484 in h_mk_order_sim sem __ __
459
460(** val order_sim_rect_Type2 :
461    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
462let rec order_sim_rect_Type2 h_mk_order_sim x_4486 =
463  let sem = x_4486 in h_mk_order_sim sem __ __
464
465(** val order_sim_rect_Type1 :
466    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
467let rec order_sim_rect_Type1 h_mk_order_sim x_4488 =
468  let sem = x_4488 in h_mk_order_sim sem __ __
469
470(** val order_sim_rect_Type0 :
471    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
472let rec order_sim_rect_Type0 h_mk_order_sim x_4490 =
473  let sem = x_4490 in h_mk_order_sim sem __ __
474
475(** val sem : order_sim -> related_semantics **)
476let rec sem xxx =
477  let yyy = xxx in yyy
478
479type order = __
480
481(** val order_sim_inv_rect_Type4 :
482    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
483let order_sim_inv_rect_Type4 hterm h1 =
484  let hcut = order_sim_rect_Type4 h1 hterm in hcut __
485
486(** val order_sim_inv_rect_Type3 :
487    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
488let order_sim_inv_rect_Type3 hterm h1 =
489  let hcut = order_sim_rect_Type3 h1 hterm in hcut __
490
491(** val order_sim_inv_rect_Type2 :
492    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
493let order_sim_inv_rect_Type2 hterm h1 =
494  let hcut = order_sim_rect_Type2 h1 hterm in hcut __
495
496(** val order_sim_inv_rect_Type1 :
497    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
498let order_sim_inv_rect_Type1 hterm h1 =
499  let hcut = order_sim_rect_Type1 h1 hterm in hcut __
500
501(** val order_sim_inv_rect_Type0 :
502    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
503let order_sim_inv_rect_Type0 hterm h1 =
504  let hcut = order_sim_rect_Type0 h1 hterm in hcut __
505
506(** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
507let order_sim_jmdiscr x y =
508  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
509
Note: See TracBrowser for help on using the repository browser.