source: extracted/smallstep.ml @ 2890

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

Everything extracted again.

File size: 16.7 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 Exp
24
25open Arithmetic
26
27open Extranat
28
29open Vector
30
31open FoldStuff
32
33open BitVector
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open ErrorMessages
42
43open Option
44
45open Setoids
46
47open Monad
48
49open Positive
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Events
86
87type transrel =
88| Mk_transrel
89
90(** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
91let rec transrel_rect_Type4 h_mk_transrel = function
92| Mk_transrel -> h_mk_transrel __ __ __
93
94(** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
95let rec transrel_rect_Type5 h_mk_transrel = function
96| Mk_transrel -> h_mk_transrel __ __ __
97
98(** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
99let rec transrel_rect_Type3 h_mk_transrel = function
100| Mk_transrel -> h_mk_transrel __ __ __
101
102(** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
103let rec transrel_rect_Type2 h_mk_transrel = function
104| Mk_transrel -> h_mk_transrel __ __ __
105
106(** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
107let rec transrel_rect_Type1 h_mk_transrel = function
108| Mk_transrel -> h_mk_transrel __ __ __
109
110(** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
111let rec transrel_rect_Type0 h_mk_transrel = function
112| Mk_transrel -> h_mk_transrel __ __ __
113
114type genv = __
115
116type state = __
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_6913, x_6912) -> h_Terminates x_6913 x_6912
160| Diverges x_6914 -> h_Diverges x_6914
161| Reacts x_6915 -> h_Reacts x_6915
162| Goes_wrong x_6916 -> h_Goes_wrong x_6916
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_6923, x_6922) -> h_Terminates x_6923 x_6922
170| Diverges x_6924 -> h_Diverges x_6924
171| Reacts x_6925 -> h_Reacts x_6925
172| Goes_wrong x_6926 -> h_Goes_wrong x_6926
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_6933, x_6932) -> h_Terminates x_6933 x_6932
180| Diverges x_6934 -> h_Diverges x_6934
181| Reacts x_6935 -> h_Reacts x_6935
182| Goes_wrong x_6936 -> h_Goes_wrong x_6936
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_6943, x_6942) -> h_Terminates x_6943 x_6942
190| Diverges x_6944 -> h_Diverges x_6944
191| Reacts x_6945 -> h_Reacts x_6945
192| Goes_wrong x_6946 -> h_Goes_wrong x_6946
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_6953, x_6952) -> h_Terminates x_6953 x_6952
200| Diverges x_6954 -> h_Diverges x_6954
201| Reacts x_6955 -> h_Reacts x_6955
202| Goes_wrong x_6956 -> h_Goes_wrong x_6956
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_6963, x_6962) -> h_Terminates x_6963 x_6962
210| Diverges x_6964 -> h_Diverges x_6964
211| Reacts x_6965 -> h_Reacts x_6965
212| Goes_wrong x_6966 -> h_Goes_wrong x_6966
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_7293 =
274  let { trans = trans0; ge = ge0 } = x_7293 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_7295 =
280  let { trans = trans0; ge = ge0 } = x_7295 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_7297 =
286  let { trans = trans0; ge = ge0 } = x_7297 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_7299 =
292  let { trans = trans0; ge = ge0 } = x_7299 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_7301 =
298  let { trans = trans0; ge = ge0 } = x_7301 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_7303 =
304  let { trans = trans0; ge = ge0 } = x_7303 in
305  h_mk_semantics trans0 __ __ ge0
306
307(** val trans : semantics -> transrel **)
308let rec trans xxx =
309  xxx.trans
310
311(** val ge : semantics -> __ **)
312let rec ge xxx =
313  xxx.ge
314
315(** val semantics_inv_rect_Type4 :
316    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
317let semantics_inv_rect_Type4 hterm h1 =
318  let hcut = semantics_rect_Type4 h1 hterm in hcut __
319
320(** val semantics_inv_rect_Type3 :
321    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
322let semantics_inv_rect_Type3 hterm h1 =
323  let hcut = semantics_rect_Type3 h1 hterm in hcut __
324
325(** val semantics_inv_rect_Type2 :
326    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
327let semantics_inv_rect_Type2 hterm h1 =
328  let hcut = semantics_rect_Type2 h1 hterm in hcut __
329
330(** val semantics_inv_rect_Type1 :
331    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
332let semantics_inv_rect_Type1 hterm h1 =
333  let hcut = semantics_rect_Type1 h1 hterm in hcut __
334
335(** val semantics_inv_rect_Type0 :
336    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
337let semantics_inv_rect_Type0 hterm h1 =
338  let hcut = semantics_rect_Type0 h1 hterm in hcut __
339
340(** val semantics_jmdiscr : semantics -> semantics -> __ **)
341let semantics_jmdiscr x y =
342  Logic.eq_rect_Type2 x
343    (let { trans = a0; ge = a3 } = x in
344    Obj.magic (fun _ dH -> dH __ __ __ __)) y
345
346type related_semantics = { sem1 : semantics; sem2 : semantics }
347
348(** val related_semantics_rect_Type4 :
349    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
350    'a1 **)
351let rec related_semantics_rect_Type4 h_mk_related_semantics x_7322 =
352  let { sem1 = sem3; sem2 = sem4 } = x_7322 in
353  h_mk_related_semantics sem3 sem4 __ __ __
354
355(** val related_semantics_rect_Type5 :
356    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
357    'a1 **)
358let rec related_semantics_rect_Type5 h_mk_related_semantics x_7324 =
359  let { sem1 = sem3; sem2 = sem4 } = x_7324 in
360  h_mk_related_semantics sem3 sem4 __ __ __
361
362(** val related_semantics_rect_Type3 :
363    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
364    'a1 **)
365let rec related_semantics_rect_Type3 h_mk_related_semantics x_7326 =
366  let { sem1 = sem3; sem2 = sem4 } = x_7326 in
367  h_mk_related_semantics sem3 sem4 __ __ __
368
369(** val related_semantics_rect_Type2 :
370    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
371    'a1 **)
372let rec related_semantics_rect_Type2 h_mk_related_semantics x_7328 =
373  let { sem1 = sem3; sem2 = sem4 } = x_7328 in
374  h_mk_related_semantics sem3 sem4 __ __ __
375
376(** val related_semantics_rect_Type1 :
377    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
378    'a1 **)
379let rec related_semantics_rect_Type1 h_mk_related_semantics x_7330 =
380  let { sem1 = sem3; sem2 = sem4 } = x_7330 in
381  h_mk_related_semantics sem3 sem4 __ __ __
382
383(** val related_semantics_rect_Type0 :
384    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
385    'a1 **)
386let rec related_semantics_rect_Type0 h_mk_related_semantics x_7332 =
387  let { sem1 = sem3; sem2 = sem4 } = x_7332 in
388  h_mk_related_semantics sem3 sem4 __ __ __
389
390(** val sem1 : related_semantics -> semantics **)
391let rec sem1 xxx =
392  xxx.sem1
393
394(** val sem2 : related_semantics -> semantics **)
395let rec sem2 xxx =
396  xxx.sem2
397
398(** val related_semantics_inv_rect_Type4 :
399    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
400    'a1) -> 'a1 **)
401let related_semantics_inv_rect_Type4 hterm h1 =
402  let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
403
404(** val related_semantics_inv_rect_Type3 :
405    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
406    'a1) -> 'a1 **)
407let related_semantics_inv_rect_Type3 hterm h1 =
408  let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
409
410(** val related_semantics_inv_rect_Type2 :
411    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
412    'a1) -> 'a1 **)
413let related_semantics_inv_rect_Type2 hterm h1 =
414  let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
415
416(** val related_semantics_inv_rect_Type1 :
417    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
418    'a1) -> 'a1 **)
419let related_semantics_inv_rect_Type1 hterm h1 =
420  let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
421
422(** val related_semantics_inv_rect_Type0 :
423    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
424    'a1) -> 'a1 **)
425let related_semantics_inv_rect_Type0 hterm h1 =
426  let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
427
428(** val related_semantics_jmdiscr :
429    related_semantics -> related_semantics -> __ **)
430let related_semantics_jmdiscr x y =
431  Logic.eq_rect_Type2 x
432    (let { sem1 = a0; sem2 = a1 } = x in
433    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
434
435type order_sim =
436  related_semantics
437  (* singleton inductive, whose constructor was mk_order_sim *)
438
439(** val order_sim_rect_Type4 :
440    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
441let rec order_sim_rect_Type4 h_mk_order_sim x_7353 =
442  let sem = x_7353 in h_mk_order_sim sem __ __
443
444(** val order_sim_rect_Type5 :
445    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
446let rec order_sim_rect_Type5 h_mk_order_sim x_7355 =
447  let sem = x_7355 in h_mk_order_sim sem __ __
448
449(** val order_sim_rect_Type3 :
450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
451let rec order_sim_rect_Type3 h_mk_order_sim x_7357 =
452  let sem = x_7357 in h_mk_order_sim sem __ __
453
454(** val order_sim_rect_Type2 :
455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
456let rec order_sim_rect_Type2 h_mk_order_sim x_7359 =
457  let sem = x_7359 in h_mk_order_sim sem __ __
458
459(** val order_sim_rect_Type1 :
460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
461let rec order_sim_rect_Type1 h_mk_order_sim x_7361 =
462  let sem = x_7361 in h_mk_order_sim sem __ __
463
464(** val order_sim_rect_Type0 :
465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
466let rec order_sim_rect_Type0 h_mk_order_sim x_7363 =
467  let sem = x_7363 in h_mk_order_sim sem __ __
468
469(** val sem : order_sim -> related_semantics **)
470let rec sem xxx =
471  let yyy = xxx in yyy
472
473(** val order_sim_inv_rect_Type4 :
474    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
475let order_sim_inv_rect_Type4 hterm h1 =
476  let hcut = order_sim_rect_Type4 h1 hterm in hcut __
477
478(** val order_sim_inv_rect_Type3 :
479    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
480let order_sim_inv_rect_Type3 hterm h1 =
481  let hcut = order_sim_rect_Type3 h1 hterm in hcut __
482
483(** val order_sim_inv_rect_Type2 :
484    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
485let order_sim_inv_rect_Type2 hterm h1 =
486  let hcut = order_sim_rect_Type2 h1 hterm in hcut __
487
488(** val order_sim_inv_rect_Type1 :
489    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
490let order_sim_inv_rect_Type1 hterm h1 =
491  let hcut = order_sim_rect_Type1 h1 hterm in hcut __
492
493(** val order_sim_inv_rect_Type0 :
494    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
495let order_sim_inv_rect_Type0 hterm h1 =
496  let hcut = order_sim_rect_Type0 h1 hterm in hcut __
497
498(** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
499let order_sim_jmdiscr x y =
500  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
501
Note: See TracBrowser for help on using the repository browser.