source: extracted/smallstep.ml @ 2731

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

Exported again.

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