source: extracted/smallstep.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: 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_6848, x_6847) -> h_Terminates x_6848 x_6847
164| Diverges x_6849 -> h_Diverges x_6849
165| Reacts x_6850 -> h_Reacts x_6850
166| Goes_wrong x_6851 -> h_Goes_wrong x_6851
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_6858, x_6857) -> h_Terminates x_6858 x_6857
174| Diverges x_6859 -> h_Diverges x_6859
175| Reacts x_6860 -> h_Reacts x_6860
176| Goes_wrong x_6861 -> h_Goes_wrong x_6861
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_6868, x_6867) -> h_Terminates x_6868 x_6867
184| Diverges x_6869 -> h_Diverges x_6869
185| Reacts x_6870 -> h_Reacts x_6870
186| Goes_wrong x_6871 -> h_Goes_wrong x_6871
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_6878, x_6877) -> h_Terminates x_6878 x_6877
194| Diverges x_6879 -> h_Diverges x_6879
195| Reacts x_6880 -> h_Reacts x_6880
196| Goes_wrong x_6881 -> h_Goes_wrong x_6881
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_6888, x_6887) -> h_Terminates x_6888 x_6887
204| Diverges x_6889 -> h_Diverges x_6889
205| Reacts x_6890 -> h_Reacts x_6890
206| Goes_wrong x_6891 -> h_Goes_wrong x_6891
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_6898, x_6897) -> h_Terminates x_6898 x_6897
214| Diverges x_6899 -> h_Diverges x_6899
215| Reacts x_6900 -> h_Reacts x_6900
216| Goes_wrong x_6901 -> h_Goes_wrong x_6901
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_7228 =
278  let { trans = trans0; ge = ge0 } = x_7228 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_7230 =
284  let { trans = trans0; ge = ge0 } = x_7230 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_7232 =
290  let { trans = trans0; ge = ge0 } = x_7232 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_7234 =
296  let { trans = trans0; ge = ge0 } = x_7234 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_7236 =
302  let { trans = trans0; ge = ge0 } = x_7236 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_7238 =
308  let { trans = trans0; ge = ge0 } = x_7238 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_7257 =
360  let { sem1 = sem3; sem2 = sem4 } = x_7257 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_7259 =
367  let { sem1 = sem3; sem2 = sem4 } = x_7259 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_7261 =
374  let { sem1 = sem3; sem2 = sem4 } = x_7261 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_7263 =
381  let { sem1 = sem3; sem2 = sem4 } = x_7263 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_7265 =
388  let { sem1 = sem3; sem2 = sem4 } = x_7265 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_7267 =
395  let { sem1 = sem3; sem2 = sem4 } = x_7267 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_7288 =
452  let sem = x_7288 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_7290 =
457  let sem = x_7290 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_7292 =
462  let sem = x_7292 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_7294 =
467  let sem = x_7294 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_7296 =
472  let sem = x_7296 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_7298 =
477  let sem = x_7298 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.