source: extracted/toRTLabs.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 54.5 KB
Line 
1open Preamble
2
3open Setoids
4
5open Monad
6
7open Option
8
9open Div_and_mod
10
11open Jmeq
12
13open Russell
14
15open Util
16
17open Bool
18
19open Relations
20
21open Nat
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Types
32
33open List
34
35open Lists
36
37open Extra_bool
38
39open Values
40
41open FrontEndVal
42
43open Hide
44
45open ByteValues
46
47open Division
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open GenMem
56
57open FrontEndMem
58
59open Proper
60
61open PositiveMap
62
63open Deqsets
64
65open Extralib
66
67open Identifiers
68
69open Coqlib
70
71open Floats
72
73open Arithmetic
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Extranat
82
83open Integers
84
85open AST
86
87open Positive
88
89open Char
90
91open String
92
93open PreIdentifiers
94
95open Errors
96
97open Globalenvs
98
99open CostLabel
100
101open FrontEndOps
102
103open Cminor_syntax
104
105open BitVectorTrie
106
107open Graphs
108
109open Order
110
111open Registers
112
113open RTLabs_syntax
114
115type env =
116  (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
117
118(** val populate_env :
119    env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list
120    -> (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
121    Identifiers.universe) Types.prod **)
122let populate_env en gen =
123  List.foldr (fun idt rsengen ->
124    let { Types.fst = id; Types.snd = ty } = idt in
125    let { Types.fst = eta2845; Types.snd = gen0 } = rsengen in
126    let { Types.fst = rs; Types.snd = en0 } = eta2845 in
127    let { Types.fst = r; Types.snd = gen' } =
128      Identifiers.fresh Registers.registerTag gen0
129    in
130    { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
131    ty }, rs)); Types.snd =
132    (Identifiers.add AST.symbolTag en0 id { Types.fst = r; Types.snd = ty }) };
133    Types.snd = gen' }) { Types.fst = { Types.fst = List.Nil; Types.snd =
134    en }; Types.snd = gen }
135
136(** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
137let lookup_reg e0 id ty =
138  (Identifiers.lookup_present AST.symbolTag e0 id).Types.fst
139
140type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
141               fx_rettyp : AST.typ Types.option }
142
143(** val fixed_rect_Type4 :
144    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
145    fixed -> 'a1 **)
146let rec fixed_rect_Type4 h_mk_fixed x_14420 =
147  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
148    x_14420
149  in
150  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
151
152(** val fixed_rect_Type5 :
153    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
154    fixed -> 'a1 **)
155let rec fixed_rect_Type5 h_mk_fixed x_14422 =
156  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
157    x_14422
158  in
159  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
160
161(** val fixed_rect_Type3 :
162    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
163    fixed -> 'a1 **)
164let rec fixed_rect_Type3 h_mk_fixed x_14424 =
165  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
166    x_14424
167  in
168  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
169
170(** val fixed_rect_Type2 :
171    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
172    fixed -> 'a1 **)
173let rec fixed_rect_Type2 h_mk_fixed x_14426 =
174  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
175    x_14426
176  in
177  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
178
179(** val fixed_rect_Type1 :
180    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
181    fixed -> 'a1 **)
182let rec fixed_rect_Type1 h_mk_fixed x_14428 =
183  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
184    x_14428
185  in
186  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
187
188(** val fixed_rect_Type0 :
189    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
190    fixed -> 'a1 **)
191let rec fixed_rect_Type0 h_mk_fixed x_14430 =
192  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
193    x_14430
194  in
195  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
196
197(** val fx_gotos : fixed -> Identifiers.identifier_set **)
198let rec fx_gotos xxx =
199  xxx.fx_gotos
200
201(** val fx_env : fixed -> env **)
202let rec fx_env xxx =
203  xxx.fx_env
204
205(** val fx_rettyp : fixed -> AST.typ Types.option **)
206let rec fx_rettyp xxx =
207  xxx.fx_rettyp
208
209(** val fixed_inv_rect_Type4 :
210    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
211    -> 'a1) -> 'a1 **)
212let fixed_inv_rect_Type4 hterm h1 =
213  let hcut = fixed_rect_Type4 h1 hterm in hcut __
214
215(** val fixed_inv_rect_Type3 :
216    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
217    -> 'a1) -> 'a1 **)
218let fixed_inv_rect_Type3 hterm h1 =
219  let hcut = fixed_rect_Type3 h1 hterm in hcut __
220
221(** val fixed_inv_rect_Type2 :
222    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
223    -> 'a1) -> 'a1 **)
224let fixed_inv_rect_Type2 hterm h1 =
225  let hcut = fixed_rect_Type2 h1 hterm in hcut __
226
227(** val fixed_inv_rect_Type1 :
228    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
229    -> 'a1) -> 'a1 **)
230let fixed_inv_rect_Type1 hterm h1 =
231  let hcut = fixed_rect_Type1 h1 hterm in hcut __
232
233(** val fixed_inv_rect_Type0 :
234    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
235    -> 'a1) -> 'a1 **)
236let fixed_inv_rect_Type0 hterm h1 =
237  let hcut = fixed_rect_Type0 h1 hterm in hcut __
238
239(** val fixed_discr : fixed -> fixed -> __ **)
240let fixed_discr x y =
241  Logic.eq_rect_Type2 x
242    (let { fx_gotos = a0; fx_env = a1; fx_rettyp = a2 } = x in
243    Obj.magic (fun _ dH -> dH __ __ __)) y
244
245(** val fixed_jmdiscr : fixed -> fixed -> __ **)
246let fixed_jmdiscr x y =
247  Logic.eq_rect_Type2 x
248    (let { fx_gotos = a0; fx_env = a1; fx_rettyp = a2 } = x in
249    Obj.magic (fun _ dH -> dH __ __ __)) y
250
251type resultok = __
252
253type goto_map =
254  PreIdentifiers.identifier Identifiers.identifier_map
255  (* singleton inductive, whose constructor was mk_goto_map *)
256
257(** val goto_map_rect_Type4 :
258    fixed -> RTLabs_syntax.statement Graphs.graph ->
259    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
260    -> goto_map -> 'a1 **)
261let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_14446 =
262  let gm_map = x_14446 in h_mk_goto_map gm_map __ __
263
264(** val goto_map_rect_Type5 :
265    fixed -> RTLabs_syntax.statement Graphs.graph ->
266    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
267    -> goto_map -> 'a1 **)
268let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_14448 =
269  let gm_map = x_14448 in h_mk_goto_map gm_map __ __
270
271(** val goto_map_rect_Type3 :
272    fixed -> RTLabs_syntax.statement Graphs.graph ->
273    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
274    -> goto_map -> 'a1 **)
275let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_14450 =
276  let gm_map = x_14450 in h_mk_goto_map gm_map __ __
277
278(** val goto_map_rect_Type2 :
279    fixed -> RTLabs_syntax.statement Graphs.graph ->
280    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
281    -> goto_map -> 'a1 **)
282let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_14452 =
283  let gm_map = x_14452 in h_mk_goto_map gm_map __ __
284
285(** val goto_map_rect_Type1 :
286    fixed -> RTLabs_syntax.statement Graphs.graph ->
287    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
288    -> goto_map -> 'a1 **)
289let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_14454 =
290  let gm_map = x_14454 in h_mk_goto_map gm_map __ __
291
292(** val goto_map_rect_Type0 :
293    fixed -> RTLabs_syntax.statement Graphs.graph ->
294    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
295    -> goto_map -> 'a1 **)
296let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_14456 =
297  let gm_map = x_14456 in h_mk_goto_map gm_map __ __
298
299(** val gm_map :
300    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
301    PreIdentifiers.identifier Identifiers.identifier_map **)
302let rec gm_map fx g0 xxx =
303  let yyy = xxx in yyy
304
305(** val goto_map_inv_rect_Type4 :
306    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
307    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
308    -> 'a1) -> 'a1 **)
309let goto_map_inv_rect_Type4 x1 x2 hterm h1 =
310  let hcut = goto_map_rect_Type4 x1 x2 h1 hterm in hcut __
311
312(** val goto_map_inv_rect_Type3 :
313    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
314    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
315    -> 'a1) -> 'a1 **)
316let goto_map_inv_rect_Type3 x1 x2 hterm h1 =
317  let hcut = goto_map_rect_Type3 x1 x2 h1 hterm in hcut __
318
319(** val goto_map_inv_rect_Type2 :
320    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
321    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
322    -> 'a1) -> 'a1 **)
323let goto_map_inv_rect_Type2 x1 x2 hterm h1 =
324  let hcut = goto_map_rect_Type2 x1 x2 h1 hterm in hcut __
325
326(** val goto_map_inv_rect_Type1 :
327    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
328    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
329    -> 'a1) -> 'a1 **)
330let goto_map_inv_rect_Type1 x1 x2 hterm h1 =
331  let hcut = goto_map_rect_Type1 x1 x2 h1 hterm in hcut __
332
333(** val goto_map_inv_rect_Type0 :
334    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
335    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
336    -> 'a1) -> 'a1 **)
337let goto_map_inv_rect_Type0 x1 x2 hterm h1 =
338  let hcut = goto_map_rect_Type0 x1 x2 h1 hterm in hcut __
339
340(** val goto_map_discr :
341    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
342    __ **)
343let goto_map_discr a1 a2 x y =
344  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
345
346(** val goto_map_jmdiscr :
347    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
348    __ **)
349let goto_map_jmdiscr a1 a2 x y =
350  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
351
352(** val dpi1__o__gm_map__o__inject :
353    fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
354    Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
355    Types.sig0 **)
356let dpi1__o__gm_map__o__inject x1 x2 x4 =
357  gm_map x1 x2 x4.Types.dpi1
358
359(** val eject__o__gm_map__o__inject :
360    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
361    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
362let eject__o__gm_map__o__inject x1 x2 x4 =
363  gm_map x1 x2 (Types.pi1 x4)
364
365(** val gm_map__o__inject :
366    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
367    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
368let gm_map__o__inject x1 x2 x3 =
369  gm_map x1 x2 x3
370
371(** val dpi1__o__gm_map :
372    fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
373    Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map **)
374let dpi1__o__gm_map x0 x1 x3 =
375  gm_map x0 x1 x3.Types.dpi1
376
377(** val eject__o__gm_map :
378    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
379    PreIdentifiers.identifier Identifiers.identifier_map **)
380let eject__o__gm_map x0 x1 x3 =
381  gm_map x0 x1 (Types.pi1 x3)
382
383type partial_fn = { pf_labgen : Identifiers.universe;
384                    pf_reggen : Identifiers.universe;
385                    pf_params : (Registers.register, AST.typ) Types.prod
386                                List.list;
387                    pf_locals : (Registers.register, AST.typ) Types.prod
388                                List.list; pf_result : resultok;
389                    pf_stacksize : Nat.nat;
390                    pf_graph : RTLabs_syntax.statement Graphs.graph;
391                    pf_gotos : goto_map;
392                    pf_labels : PreIdentifiers.identifier
393                                Identifiers.identifier_map Types.sig0;
394                    pf_entry : Graphs.label Types.sig0;
395                    pf_exit : Graphs.label Types.sig0 }
396
397(** val partial_fn_rect_Type4 :
398    fixed -> (Identifiers.universe -> Identifiers.universe ->
399    (Registers.register, AST.typ) Types.prod List.list ->
400    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
401    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
402    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
403    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
404    -> 'a1 **)
405let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_14474 =
406  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
407    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
408    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
409    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
410    x_14474
411  in
412  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
413    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
414
415(** val partial_fn_rect_Type5 :
416    fixed -> (Identifiers.universe -> Identifiers.universe ->
417    (Registers.register, AST.typ) Types.prod List.list ->
418    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
419    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
420    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
421    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
422    -> 'a1 **)
423let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_14476 =
424  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
425    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
426    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
427    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
428    x_14476
429  in
430  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
431    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
432
433(** val partial_fn_rect_Type3 :
434    fixed -> (Identifiers.universe -> Identifiers.universe ->
435    (Registers.register, AST.typ) Types.prod List.list ->
436    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
437    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
438    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
439    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
440    -> 'a1 **)
441let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_14478 =
442  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
443    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
444    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
445    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
446    x_14478
447  in
448  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
449    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
450
451(** val partial_fn_rect_Type2 :
452    fixed -> (Identifiers.universe -> Identifiers.universe ->
453    (Registers.register, AST.typ) Types.prod List.list ->
454    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
455    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
456    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
457    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
458    -> 'a1 **)
459let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_14480 =
460  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
461    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
462    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
463    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
464    x_14480
465  in
466  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
467    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
468
469(** val partial_fn_rect_Type1 :
470    fixed -> (Identifiers.universe -> Identifiers.universe ->
471    (Registers.register, AST.typ) Types.prod List.list ->
472    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
473    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
474    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
475    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
476    -> 'a1 **)
477let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_14482 =
478  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
479    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
480    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
481    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
482    x_14482
483  in
484  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
485    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
486
487(** val partial_fn_rect_Type0 :
488    fixed -> (Identifiers.universe -> Identifiers.universe ->
489    (Registers.register, AST.typ) Types.prod List.list ->
490    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
491    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
492    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
493    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
494    -> 'a1 **)
495let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_14484 =
496  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
497    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
498    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
499    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
500    x_14484
501  in
502  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
503    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
504
505(** val pf_labgen : fixed -> partial_fn -> Identifiers.universe **)
506let rec pf_labgen fx xxx =
507  xxx.pf_labgen
508
509(** val pf_reggen : fixed -> partial_fn -> Identifiers.universe **)
510let rec pf_reggen fx xxx =
511  xxx.pf_reggen
512
513(** val pf_params :
514    fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
515let rec pf_params fx xxx =
516  xxx.pf_params
517
518(** val pf_locals :
519    fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
520let rec pf_locals fx xxx =
521  xxx.pf_locals
522
523(** val pf_result : fixed -> partial_fn -> resultok **)
524let rec pf_result fx xxx =
525  xxx.pf_result
526
527(** val pf_stacksize : fixed -> partial_fn -> Nat.nat **)
528let rec pf_stacksize fx xxx =
529  xxx.pf_stacksize
530
531(** val pf_graph :
532    fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph **)
533let rec pf_graph fx xxx =
534  xxx.pf_graph
535
536(** val pf_gotos : fixed -> partial_fn -> goto_map **)
537let rec pf_gotos fx xxx =
538  xxx.pf_gotos
539
540(** val pf_labels :
541    fixed -> partial_fn -> PreIdentifiers.identifier
542    Identifiers.identifier_map Types.sig0 **)
543let rec pf_labels fx xxx =
544  xxx.pf_labels
545
546(** val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0 **)
547let rec pf_entry fx xxx =
548  xxx.pf_entry
549
550(** val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0 **)
551let rec pf_exit fx xxx =
552  xxx.pf_exit
553
554(** val partial_fn_inv_rect_Type4 :
555    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
556    (Registers.register, AST.typ) Types.prod List.list ->
557    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
558    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
559    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
560    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
561let partial_fn_inv_rect_Type4 x1 hterm h1 =
562  let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __
563
564(** val partial_fn_inv_rect_Type3 :
565    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
566    (Registers.register, AST.typ) Types.prod List.list ->
567    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
568    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
569    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
570    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
571let partial_fn_inv_rect_Type3 x1 hterm h1 =
572  let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __
573
574(** val partial_fn_inv_rect_Type2 :
575    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
576    (Registers.register, AST.typ) Types.prod List.list ->
577    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
578    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
579    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
580    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
581let partial_fn_inv_rect_Type2 x1 hterm h1 =
582  let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __
583
584(** val partial_fn_inv_rect_Type1 :
585    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
586    (Registers.register, AST.typ) Types.prod List.list ->
587    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
588    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
589    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
590    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
591let partial_fn_inv_rect_Type1 x1 hterm h1 =
592  let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __
593
594(** val partial_fn_inv_rect_Type0 :
595    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
596    (Registers.register, AST.typ) Types.prod List.list ->
597    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
598    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
599    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
600    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
601let partial_fn_inv_rect_Type0 x1 hterm h1 =
602  let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __
603
604(** val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
605let partial_fn_jmdiscr a1 x y =
606  Logic.eq_rect_Type2 x
607    (let { pf_labgen = a0; pf_reggen = a10; pf_params = a2; pf_locals = a3;
608       pf_result = a4; pf_stacksize = a6; pf_graph = a7; pf_gotos = a9;
609       pf_labels = a100; pf_entry = a12; pf_exit = a13 } = x
610     in
611    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
612
613(** val fn_contains_rect_Type4 :
614    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
615let rec fn_contains_rect_Type4 fx f1 f2 h_mk_fn_contains =
616  h_mk_fn_contains __ __ __
617
618(** val fn_contains_rect_Type5 :
619    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
620let rec fn_contains_rect_Type5 fx f1 f2 h_mk_fn_contains =
621  h_mk_fn_contains __ __ __
622
623(** val fn_contains_rect_Type3 :
624    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
625let rec fn_contains_rect_Type3 fx f1 f2 h_mk_fn_contains =
626  h_mk_fn_contains __ __ __
627
628(** val fn_contains_rect_Type2 :
629    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
630let rec fn_contains_rect_Type2 fx f1 f2 h_mk_fn_contains =
631  h_mk_fn_contains __ __ __
632
633(** val fn_contains_rect_Type1 :
634    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
635let rec fn_contains_rect_Type1 fx f1 f2 h_mk_fn_contains =
636  h_mk_fn_contains __ __ __
637
638(** val fn_contains_rect_Type0 :
639    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
640let rec fn_contains_rect_Type0 fx f1 f2 h_mk_fn_contains =
641  h_mk_fn_contains __ __ __
642
643(** val fn_contains_inv_rect_Type4 :
644    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
645let fn_contains_inv_rect_Type4 x1 x2 x3 h1 =
646  let hcut = fn_contains_rect_Type4 x1 x2 x3 h1 in hcut __
647
648(** val fn_contains_inv_rect_Type3 :
649    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
650let fn_contains_inv_rect_Type3 x1 x2 x3 h1 =
651  let hcut = fn_contains_rect_Type3 x1 x2 x3 h1 in hcut __
652
653(** val fn_contains_inv_rect_Type2 :
654    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
655let fn_contains_inv_rect_Type2 x1 x2 x3 h1 =
656  let hcut = fn_contains_rect_Type2 x1 x2 x3 h1 in hcut __
657
658(** val fn_contains_inv_rect_Type1 :
659    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
660let fn_contains_inv_rect_Type1 x1 x2 x3 h1 =
661  let hcut = fn_contains_rect_Type1 x1 x2 x3 h1 in hcut __
662
663(** val fn_contains_inv_rect_Type0 :
664    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
665let fn_contains_inv_rect_Type0 x1 x2 x3 h1 =
666  let hcut = fn_contains_rect_Type0 x1 x2 x3 h1 in hcut __
667
668(** val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __ **)
669let fn_contains_discr a1 a2 a3 =
670  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
671
672(** val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
673let fn_contains_jmdiscr a1 a2 a3 =
674  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
675
676(** val fill_in_statement :
677    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
678    partial_fn Types.sig0 **)
679let fill_in_statement fx l s f =
680  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
681    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
682    pf_stacksize = f.pf_stacksize; pf_graph =
683    (Identifiers.add Graphs.labelTag f.pf_graph l s); pf_gotos =
684    (gm_map fx f.pf_graph f.pf_gotos); pf_labels = (Types.pi1 f.pf_labels);
685    pf_entry = (Types.pi1 f.pf_entry); pf_exit = (Types.pi1 f.pf_exit) }
686
687(** val add_to_graph :
688    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
689    partial_fn Types.sig0 **)
690let add_to_graph fx l s f =
691  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
692    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
693    pf_stacksize = f.pf_stacksize; pf_graph =
694    (Identifiers.add Graphs.labelTag f.pf_graph l s); pf_gotos =
695    (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
696    pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) }
697
698(** val change_entry :
699    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
700let change_entry fx f l =
701  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
702    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
703    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
704    f.pf_gotos; pf_labels = f.pf_labels; pf_entry = l; pf_exit = f.pf_exit }
705
706(** val add_fresh_to_graph :
707    fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
708    partial_fn Types.sig0 **)
709let add_fresh_to_graph fx s f =
710  (let { Types.fst = l; Types.snd = g0 } =
711     Identifiers.fresh Graphs.labelTag f.pf_labgen
712   in
713  (fun _ ->
714  let s1 = s (Types.pi1 f.pf_entry) in
715  { pf_labgen = g0; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
716  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
717  f.pf_stacksize; pf_graph =
718  (Identifiers.add Graphs.labelTag f.pf_graph l s1); pf_gotos =
719  (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
720  pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __
721
722(** val fresh_reg :
723    fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
724    Registers.register Types.sig0) Types.dPair **)
725let fresh_reg fx f ty =
726  let { Types.fst = r; Types.snd = g0 } =
727    Identifiers.fresh Registers.registerTag f.pf_reggen
728  in
729  let f' = { pf_labgen = f.pf_labgen; pf_reggen = g0; pf_params =
730    f.pf_params; pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty },
731    f.pf_locals)); pf_result =
732    ((match fx.fx_rettyp with
733      | Types.None -> Obj.magic __
734      | Types.Some t ->
735        (fun clearme -> let r' = Obj.magic clearme in Obj.magic r'))
736      f.pf_result); pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph;
737    pf_gotos = f.pf_gotos; pf_labels = f.pf_labels; pf_entry = f.pf_entry;
738    pf_exit = f.pf_exit }
739  in
740  { Types.dpi1 = f'; Types.dpi2 = r }
741
742(** val choose_reg :
743    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
744    Types.sig0, Registers.register Types.sig0) Types.dPair **)
745let choose_reg fx ty e0 f =
746  (match e0 with
747   | Cminor_syntax.Id (t, i) ->
748     (fun _ -> { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) })
749   | Cminor_syntax.Cst (x, x0) -> (fun _ -> fresh_reg fx f x)
750   | Cminor_syntax.Op1 (x, x0, x1, x2) -> (fun _ -> fresh_reg fx f x0)
751   | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) ->
752     (fun _ -> fresh_reg fx f x1)
753   | Cminor_syntax.Mem (x, x0) -> (fun _ -> fresh_reg fx f x)
754   | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) ->
755     (fun _ -> fresh_reg fx f x1)
756   | Cminor_syntax.Ecost (x, x0, x1) -> (fun _ -> fresh_reg fx f x)) __
757
758(** val foldr_all :
759    ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
760let rec foldr_all f b l =
761  (match l with
762   | List.Nil -> (fun _ -> b)
763   | List.Cons (a, l0) -> (fun _ -> f a __ (foldr_all f b l0))) __
764
765(** val foldr_all' :
766    ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
767let rec foldr_all' f b l =
768  (match l with
769   | List.Nil -> (fun _ -> b)
770   | List.Cons (a, l0) -> (fun _ -> f a __ l0 (foldr_all' f b l0))) __
771
772(** val eject' : ('a1, 'a2) Types.dPair -> 'a1 **)
773let eject' x =
774  x.Types.dpi1
775
776(** val choose_regs :
777    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
778    partial_fn -> (partial_fn Types.sig0, Registers.register List.list
779    Types.sig0) Types.dPair **)
780let choose_regs fx es f =
781  foldr_all' (fun e0 _ tl acc ->
782    let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
783    (let { Types.dpi1 = t; Types.dpi2 = e1 } = e0 in
784    (fun _ ->
785    let { Types.dpi1 = f'; Types.dpi2 = r } =
786      choose_reg fx t e1 (Types.pi1 f1)
787    in
788    { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r),
789    (Types.pi1 rs))) })) __) { Types.dpi1 = f; Types.dpi2 = List.Nil } es
790
791(** val add_stmt_inv_rect_Type4 :
792    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
793    'a1) -> 'a1 **)
794let rec add_stmt_inv_rect_Type4 fx s f f' h_mk_add_stmt_inv =
795  h_mk_add_stmt_inv __ __
796
797(** val add_stmt_inv_rect_Type5 :
798    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
799    'a1) -> 'a1 **)
800let rec add_stmt_inv_rect_Type5 fx s f f' h_mk_add_stmt_inv =
801  h_mk_add_stmt_inv __ __
802
803(** val add_stmt_inv_rect_Type3 :
804    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
805    'a1) -> 'a1 **)
806let rec add_stmt_inv_rect_Type3 fx s f f' h_mk_add_stmt_inv =
807  h_mk_add_stmt_inv __ __
808
809(** val add_stmt_inv_rect_Type2 :
810    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
811    'a1) -> 'a1 **)
812let rec add_stmt_inv_rect_Type2 fx s f f' h_mk_add_stmt_inv =
813  h_mk_add_stmt_inv __ __
814
815(** val add_stmt_inv_rect_Type1 :
816    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
817    'a1) -> 'a1 **)
818let rec add_stmt_inv_rect_Type1 fx s f f' h_mk_add_stmt_inv =
819  h_mk_add_stmt_inv __ __
820
821(** val add_stmt_inv_rect_Type0 :
822    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
823    'a1) -> 'a1 **)
824let rec add_stmt_inv_rect_Type0 fx s f f' h_mk_add_stmt_inv =
825  h_mk_add_stmt_inv __ __
826
827(** val add_stmt_inv_inv_rect_Type4 :
828    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
829    __ -> 'a1) -> 'a1 **)
830let add_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
831  let hcut = add_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
832
833(** val add_stmt_inv_inv_rect_Type3 :
834    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
835    __ -> 'a1) -> 'a1 **)
836let add_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
837  let hcut = add_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
838
839(** val add_stmt_inv_inv_rect_Type2 :
840    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
841    __ -> 'a1) -> 'a1 **)
842let add_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
843  let hcut = add_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
844
845(** val add_stmt_inv_inv_rect_Type1 :
846    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
847    __ -> 'a1) -> 'a1 **)
848let add_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
849  let hcut = add_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
850
851(** val add_stmt_inv_inv_rect_Type0 :
852    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
853    __ -> 'a1) -> 'a1 **)
854let add_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
855  let hcut = add_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
856
857(** val add_stmt_inv_discr :
858    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
859let add_stmt_inv_discr a1 a2 a3 a4 =
860  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
861
862(** val add_stmt_inv_jmdiscr :
863    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
864let add_stmt_inv_jmdiscr a1 a2 a3 a4 =
865  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
866
867type fn_con_because =
868| Fn_con_eq of partial_fn
869| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
870| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
871   * partial_fn Types.sig0
872
873(** val fn_con_because_rect_Type4 :
874    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
875    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
876    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
877    fn_con_because -> 'a1 **)
878let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14560 = function
879| Fn_con_eq f -> h_fn_con_eq f
880| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
881| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
882
883(** val fn_con_because_rect_Type5 :
884    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
885    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
886    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
887    fn_con_because -> 'a1 **)
888let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14567 = function
889| Fn_con_eq f -> h_fn_con_eq f
890| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
891| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
892
893(** val fn_con_because_rect_Type3 :
894    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
895    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
896    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
897    fn_con_because -> 'a1 **)
898let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14574 = function
899| Fn_con_eq f -> h_fn_con_eq f
900| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
901| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
902
903(** val fn_con_because_rect_Type2 :
904    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
905    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
906    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
907    fn_con_because -> 'a1 **)
908let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14581 = function
909| Fn_con_eq f -> h_fn_con_eq f
910| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
911| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
912
913(** val fn_con_because_rect_Type1 :
914    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
915    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
916    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
917    fn_con_because -> 'a1 **)
918let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14588 = function
919| Fn_con_eq f -> h_fn_con_eq f
920| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
921| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
922
923(** val fn_con_because_rect_Type0 :
924    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
925    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
926    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
927    fn_con_because -> 'a1 **)
928let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14595 = function
929| Fn_con_eq f -> h_fn_con_eq f
930| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
931| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
932
933(** val fn_con_because_inv_rect_Type4 :
934    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
935    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
936    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
937    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
938let fn_con_because_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
939  let hcut = fn_con_because_rect_Type4 x1 h1 h2 h3 x2 hterm in hcut __ __
940
941(** val fn_con_because_inv_rect_Type3 :
942    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
943    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
944    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
945    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
946let fn_con_because_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
947  let hcut = fn_con_because_rect_Type3 x1 h1 h2 h3 x2 hterm in hcut __ __
948
949(** val fn_con_because_inv_rect_Type2 :
950    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
951    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
952    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
953    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
954let fn_con_because_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
955  let hcut = fn_con_because_rect_Type2 x1 h1 h2 h3 x2 hterm in hcut __ __
956
957(** val fn_con_because_inv_rect_Type1 :
958    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
959    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
960    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
961    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
962let fn_con_because_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
963  let hcut = fn_con_because_rect_Type1 x1 h1 h2 h3 x2 hterm in hcut __ __
964
965(** val fn_con_because_inv_rect_Type0 :
966    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
967    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
968    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
969    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
970let fn_con_because_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
971  let hcut = fn_con_because_rect_Type0 x1 h1 h2 h3 x2 hterm in hcut __ __
972
973(** val fn_con_because_discr :
974    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
975let fn_con_because_discr a1 a2 x y =
976  Logic.eq_rect_Type2 x
977    (match x with
978     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
979     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
980     | Fn_con_addinv (a0, a10, a3, a4) ->
981       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
982
983(** val fn_con_because_jmdiscr :
984    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
985let fn_con_because_jmdiscr a1 a2 x y =
986  Logic.eq_rect_Type2 x
987    (match x with
988     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
989     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
990     | Fn_con_addinv (a0, a10, a3, a4) ->
991       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
992
993(** val fn_con_because_left :
994    fixed -> partial_fn -> fn_con_because -> partial_fn **)
995let rec fn_con_because_left fx f0 = function
996| Fn_con_eq f -> f
997| Fn_con_sig (f, x, x1) -> f
998| Fn_con_addinv (f, x, x1, x2) -> f
999
1000(** val add_expr :
1001    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
1002    Registers.register Types.sig0 -> partial_fn Types.sig0 **)
1003let rec add_expr fx ty e0 f dst =
1004  (match e0 with
1005   | Cminor_syntax.Id (t, i) ->
1006     (fun _ dst0 ->
1007       let r = lookup_reg fx.fx_env i t in
1008       (match Registers.register_eq r (Types.pi1 dst0) with
1009        | Types.Inl _ -> f
1010        | Types.Inr _ ->
1011          Types.pi1
1012            (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t, t,
1013              (FrontEndOps.Oid t), (Types.pi1 dst0), r, x)) f)))
1014   | Cminor_syntax.Cst (x, c) ->
1015     (fun _ dst0 ->
1016       Types.pi1
1017         (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
1018           (Types.pi1 dst0), c, x0)) f))
1019   | Cminor_syntax.Op1 (t, t', op0, e') ->
1020     (fun _ dst0 ->
1021       let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
1022       let f1 =
1023         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op0,
1024           (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
1025       in
1026       let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
1027   | Cminor_syntax.Op2 (x, x0, x1, op0, e1, e2) ->
1028     (fun _ dst0 ->
1029       let { Types.dpi1 = f0; Types.dpi2 = r5 } = choose_reg fx x e1 f in
1030       let { Types.dpi1 = f1; Types.dpi2 = r6 } =
1031         choose_reg fx x0 e2 (Types.pi1 f0)
1032       in
1033       let f2 =
1034         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
1035           op0, (Types.pi1 dst0), (Types.pi1 r5), (Types.pi1 r6), x2))
1036           (Types.pi1 f1)
1037       in
1038       let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r6) in
1039       let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r5) in
1040       Types.pi1 f4)
1041   | Cminor_syntax.Mem (t, e') ->
1042     (fun _ dst0 ->
1043       let { Types.dpi1 = f0; Types.dpi2 = r } =
1044         choose_reg fx AST.ASTptr e' f
1045       in
1046       let f1 =
1047         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_load (t,
1048           (Types.pi1 r), (Types.pi1 dst0), x)) (Types.pi1 f0)
1049       in
1050       let f2 = add_expr fx AST.ASTptr e' (Types.pi1 f1) (Types.pi1 r) in
1051       Types.pi1 f2)
1052   | Cminor_syntax.Cond (x, x0, x1, e', e1, e2) ->
1053     (fun _ dst0 ->
1054       let resume_at = f.pf_entry in
1055       let f0 = add_expr fx x1 e2 f dst0 in
1056       let lfalse = (Types.pi1 f0).pf_entry in
1057       let f1 =
1058         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_skip
1059           (Types.pi1 resume_at)) (Types.pi1 f0)
1060       in
1061       let f2 = add_expr fx x1 e1 (Types.pi1 f1) (Types.pi1 dst0) in
1062       let { Types.dpi1 = f3; Types.dpi2 = r } =
1063         choose_reg fx (AST.ASTint (x, x0)) e' (Types.pi1 f2)
1064       in
1065       let f4 =
1066         add_fresh_to_graph fx (fun ltrue -> RTLabs_syntax.St_cond
1067           ((Types.pi1 r), ltrue, (Types.pi1 lfalse))) (Types.pi1 f3)
1068       in
1069       let f5 =
1070         add_expr fx (AST.ASTint (x, x0)) e' (Types.pi1 f4) (Types.pi1 r)
1071       in
1072       Types.pi1 f5)
1073   | Cminor_syntax.Ecost (x, l, e') ->
1074     (fun _ dst0 ->
1075       let f0 = add_expr fx x e' f dst0 in
1076       let f1 =
1077         add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_cost (l, x0))
1078           (Types.pi1 f0)
1079       in
1080       Types.pi1 f1)) __ dst
1081
1082(** val add_exprs :
1083    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
1084    Registers.register List.list -> partial_fn -> partial_fn Types.sig0 **)
1085let rec add_exprs fx es dsts f =
1086  (match es with
1087   | List.Nil ->
1088     (fun _ _ ->
1089       match dsts with
1090       | List.Nil -> (fun _ -> f)
1091       | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
1092   | List.Cons (e0, et) ->
1093     (fun _ ->
1094       match dsts with
1095       | List.Nil -> (fun _ _ -> assert false (* absurd case *))
1096       | List.Cons (r, rt) ->
1097         (fun _ _ ->
1098           let f' = add_exprs fx et rt f in
1099           (let { Types.dpi1 = ty; Types.dpi2 = e1 } = e0 in
1100           (fun _ _ ->
1101           let f'' = add_expr fx ty e1 (Types.pi1 f') r in Types.pi1 f'')) __
1102             __))) __ __ __
1103
1104(** val stmt_inv_rect_Type5 :
1105    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1106let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
1107  h_mk_stmt_inv __ __ __
1108
1109(** val stmt_inv_rect_Type6 :
1110    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1111let rec stmt_inv_rect_Type6 fx s h_mk_stmt_inv =
1112  h_mk_stmt_inv __ __ __
1113
1114(** val stmt_inv_rect_Type7 :
1115    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1116let rec stmt_inv_rect_Type7 fx s h_mk_stmt_inv =
1117  h_mk_stmt_inv __ __ __
1118
1119(** val stmt_inv_rect_Type8 :
1120    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1121let rec stmt_inv_rect_Type8 fx s h_mk_stmt_inv =
1122  h_mk_stmt_inv __ __ __
1123
1124(** val stmt_inv_rect_Type9 :
1125    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1126let rec stmt_inv_rect_Type9 fx s h_mk_stmt_inv =
1127  h_mk_stmt_inv __ __ __
1128
1129(** val stmt_inv_rect_Type10 :
1130    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1131let rec stmt_inv_rect_Type10 fx s h_mk_stmt_inv =
1132  h_mk_stmt_inv __ __ __
1133
1134(** val stmt_inv_inv_rect_Type4 :
1135    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1136let stmt_inv_inv_rect_Type4 x1 x2 h1 =
1137  let hcut = stmt_inv_rect_Type5 x1 x2 h1 in hcut __
1138
1139(** val stmt_inv_inv_rect_Type3 :
1140    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1141let stmt_inv_inv_rect_Type3 x1 x2 h1 =
1142  let hcut = stmt_inv_rect_Type7 x1 x2 h1 in hcut __
1143
1144(** val stmt_inv_inv_rect_Type2 :
1145    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1146let stmt_inv_inv_rect_Type2 x1 x2 h1 =
1147  let hcut = stmt_inv_rect_Type8 x1 x2 h1 in hcut __
1148
1149(** val stmt_inv_inv_rect_Type1 :
1150    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1151let stmt_inv_inv_rect_Type1 x1 x2 h1 =
1152  let hcut = stmt_inv_rect_Type9 x1 x2 h1 in hcut __
1153
1154(** val stmt_inv_inv_rect_Type0 :
1155    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1156let stmt_inv_inv_rect_Type0 x1 x2 h1 =
1157  let hcut = stmt_inv_rect_Type10 x1 x2 h1 in hcut __
1158
1159(** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
1160let stmt_inv_discr a1 a2 =
1161  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1162
1163(** val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __ **)
1164let stmt_inv_jmdiscr a1 a2 =
1165  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1166
1167(** val expr_is_Id :
1168    AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
1169let expr_is_Id t = function
1170| Cminor_syntax.Id (x, id) -> Types.Some id
1171| Cminor_syntax.Cst (x, x0) -> Types.None
1172| Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
1173| Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
1174| Cminor_syntax.Mem (x, x0) -> Types.None
1175| Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) -> Types.None
1176| Cminor_syntax.Ecost (x, x0, x1) -> Types.None
1177
1178(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1179let option_jmdiscr x y =
1180  Logic.eq_rect_Type2 x
1181    (match x with
1182     | Types.None -> Obj.magic (fun _ dH -> dH)
1183     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1184
1185(** val dPair_jmdiscr :
1186    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
1187let dPair_jmdiscr x y =
1188  Logic.eq_rect_Type2 x
1189    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
1190    Obj.magic (fun _ dH -> dH __ __)) y
1191
1192(** val add_return :
1193    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
1194    partial_fn -> partial_fn Types.sig0 **)
1195let add_return fx opt_e f =
1196  let f0 = f in
1197  let f1 = add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_return) f in
1198  (match opt_e with
1199   | Types.None -> (fun _ -> Types.pi1 f1)
1200   | Types.Some et ->
1201     let { Types.dpi1 = ty; Types.dpi2 = e0 } = et in
1202     (fun _ ->
1203     (match fx.fx_rettyp with
1204      | Types.None -> (fun _ -> assert false (* absurd case *))
1205      | Types.Some t ->
1206        (fun _ r ->
1207          let r5 = Obj.magic r in
1208          let f2 = add_expr fx ty e0 (Types.pi1 f1) r5 in Types.pi1 f2)) __
1209       (Types.pi1 f1).pf_result)) __
1210
1211(** val record_goto_label :
1212    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn **)
1213let record_goto_label fx f l =
1214  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
1215    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1216    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
1217    f.pf_gotos; pf_labels =
1218    (Identifiers.add Cminor_syntax.label (Types.pi1 f.pf_labels) l
1219      (Types.pi1 f.pf_entry)); pf_entry = f.pf_entry; pf_exit = f.pf_exit }
1220
1221(** val add_goto_dummy :
1222    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
1223let add_goto_dummy fx f dest =
1224  (let { Types.fst = l; Types.snd = g0 } =
1225     Identifiers.fresh Graphs.labelTag f.pf_labgen
1226   in
1227  (fun _ -> { pf_labgen = g0; pf_reggen = f.pf_reggen; pf_params =
1228  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1229  pf_stacksize = f.pf_stacksize; pf_graph =
1230  (Identifiers.add Graphs.labelTag f.pf_graph l RTLabs_syntax.St_return);
1231  pf_gotos =
1232  (Identifiers.add Graphs.labelTag (gm_map fx f.pf_graph f.pf_gotos) l dest);
1233  pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
1234  (Types.pi1 f.pf_exit) })) __
1235
1236(** val add_stmt :
1237    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0 **)
1238let rec add_stmt fx s f =
1239  (match s with
1240   | Cminor_syntax.St_skip -> (fun _ -> f)
1241   | Cminor_syntax.St_assign (t, x, e0) ->
1242     (fun _ ->
1243       let dst = lookup_reg fx.fx_env x t in
1244       Types.pi1 (add_expr fx t e0 f dst))
1245   | Cminor_syntax.St_store (t, e1, e2) ->
1246     (fun _ ->
1247       let { Types.dpi1 = f0; Types.dpi2 = val_reg } = choose_reg fx t e2 f
1248       in
1249       let { Types.dpi1 = f1; Types.dpi2 = addr_reg } =
1250         choose_reg fx AST.ASTptr e1 (Types.pi1 f0)
1251       in
1252       let f2 =
1253         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_store (t,
1254           (Types.pi1 addr_reg), (Types.pi1 val_reg), x)) (Types.pi1 f1)
1255       in
1256       let f3 = add_expr fx AST.ASTptr e1 (Types.pi1 f2) (Types.pi1 addr_reg)
1257       in
1258       Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
1259   | Cminor_syntax.St_call (return_opt_id, e0, args) ->
1260     (fun _ ->
1261       let return_opt_reg =
1262         (match return_opt_id with
1263          | Types.None -> (fun _ -> Types.None)
1264          | Types.Some idty ->
1265            (fun _ -> Types.Some
1266              (lookup_reg fx.fx_env idty.Types.fst idty.Types.snd))) __
1267       in
1268       let { Types.dpi1 = f0; Types.dpi2 = args_regs } =
1269         choose_regs fx args f
1270       in
1271       let f1 =
1272         match expr_is_Id AST.ASTptr e0 with
1273         | Types.None ->
1274           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
1275             choose_reg fx AST.ASTptr e0 (Types.pi1 f0)
1276           in
1277           let f2 =
1278             add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_ptr
1279               ((Types.pi1 fnr), (Types.pi1 args_regs), return_opt_reg, x))
1280               (Types.pi1 f1)
1281           in
1282           Types.pi1
1283             (add_expr fx AST.ASTptr e0 (Types.pi1 f2) (Types.pi1 fnr))
1284         | Types.Some id ->
1285           add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_id (id,
1286             (Types.pi1 args_regs), return_opt_reg, x)) (Types.pi1 f0)
1287       in
1288       Types.pi1 (add_exprs fx args (Types.pi1 args_regs) (Types.pi1 f1)))
1289   | Cminor_syntax.St_seq (s1, s2) ->
1290     (fun _ ->
1291       let f2 = add_stmt fx s2 f in
1292       let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
1293   | Cminor_syntax.St_ifthenelse (x, x0, e0, s1, s2) ->
1294     (fun _ ->
1295       let l_next = f.pf_entry in
1296       let f2 = add_stmt fx s2 f in
1297       let l2 = (Types.pi1 f2).pf_entry in
1298       let f0 = change_entry fx (Types.pi1 f2) (Types.pi1 l_next) in
1299       let f1 = add_stmt fx s1 (Types.pi1 f0) in
1300       let { Types.dpi1 = f3; Types.dpi2 = r } =
1301         choose_reg fx (AST.ASTint (x, x0)) e0 (Types.pi1 f1)
1302       in
1303       let f4 =
1304         add_fresh_to_graph fx (fun l1 -> RTLabs_syntax.St_cond
1305           ((Types.pi1 r), l1, (Types.pi1 l2))) (Types.pi1 f3)
1306       in
1307       Types.pi1
1308         (add_expr fx (AST.ASTint (x, x0)) e0 (Types.pi1 f4) (Types.pi1 r)))
1309   | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
1310   | Cminor_syntax.St_label (l, s') ->
1311     (fun _ ->
1312       let f0 = add_stmt fx s' f in record_goto_label fx (Types.pi1 f0) l)
1313   | Cminor_syntax.St_goto l -> (fun _ -> Types.pi1 (add_goto_dummy fx f l))
1314   | Cminor_syntax.St_cost (l, s') ->
1315     (fun _ ->
1316       let f0 = add_stmt fx s' f in
1317       Types.pi1
1318         (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_cost (l, x))
1319           (Types.pi1 f0)))) __
1320
1321(** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
1322let patch_gotos fx f =
1323  Identifiers.fold_inf Graphs.labelTag (gm_map fx f.pf_graph f.pf_gotos)
1324    (fun l l' _ f' ->
1325    Types.pi1
1326      (fill_in_statement fx l (RTLabs_syntax.St_skip
1327        (Identifiers.lookup_present Cminor_syntax.label
1328          (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f
1329
1330(** val c2ra_function :
1331    Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
1332let c2ra_function f =
1333  let labgen0 = Identifiers.new_universe Graphs.labelTag in
1334  let reggen0 = Identifiers.new_universe Registers.registerTag in
1335  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
1336  (let { Types.fst = eta3072; Types.snd = reggen1 } =
1337     populate_env (Identifiers.empty_map AST.symbolTag) reggen0
1338       f.Cminor_syntax.f_params
1339   in
1340  let { Types.fst = params; Types.snd = env1 } = eta3072 in
1341  (fun _ ->
1342  (let { Types.fst = eta3071; Types.snd = reggen2 } =
1343     populate_env env1 reggen1 f.Cminor_syntax.f_vars
1344   in
1345  let { Types.fst = locals0; Types.snd = env0 } = eta3071 in
1346  (fun _ ->
1347  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
1348     match f.Cminor_syntax.f_return with
1349     | Types.None ->
1350       { Types.dpi1 = { Types.fst = locals0; Types.snd = reggen2 };
1351         Types.dpi2 = (Obj.magic __) }
1352     | Types.Some ty ->
1353       let { Types.fst = r; Types.snd = gen } =
1354         Identifiers.fresh Registers.registerTag reggen2
1355       in
1356       { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
1357       ty }, locals0)); Types.snd = gen }; Types.dpi2 = r }
1358   in
1359  (fun _ ->
1360  let locals = locals_reggen.Types.fst in
1361  let reggen = locals_reggen.Types.snd in
1362  let { Types.fst = l; Types.snd = labgen } =
1363    Identifiers.fresh Graphs.labelTag labgen0
1364  in
1365  let fixed0 = { fx_gotos =
1366    (Identifiers.set_of_list Cminor_syntax.label
1367      (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
1368    fx_rettyp = f.Cminor_syntax.f_return }
1369  in
1370  let emptyfn = { pf_labgen = labgen; pf_reggen = reggen; pf_params = params;
1371    pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
1372    f.Cminor_syntax.f_stacksize; pf_graph =
1373    (Identifiers.add Graphs.labelTag (Identifiers.empty_map Graphs.labelTag)
1374      l RTLabs_syntax.St_return); pf_gotos =
1375    (Identifiers.empty_map Graphs.labelTag); pf_labels =
1376    (Identifiers.empty_map Cminor_syntax.label); pf_entry = l; pf_exit = l }
1377  in
1378  let f0 = add_stmt fixed0 f.Cminor_syntax.f_body emptyfn in
1379  let f1 = patch_gotos fixed0 (Types.pi1 f0) in
1380  { RTLabs_syntax.f_labgen = (Types.pi1 f1).pf_labgen;
1381  RTLabs_syntax.f_reggen = (Types.pi1 f1).pf_reggen; RTLabs_syntax.f_result =
1382  ((match fixed0.fx_rettyp with
1383    | Types.None -> Obj.magic (fun _ -> Types.None)
1384    | Types.Some t ->
1385      (fun r -> Types.Some { Types.fst = (Types.pi1 (Obj.magic r));
1386        Types.snd = t })) (Types.pi1 f1).pf_result); RTLabs_syntax.f_params =
1387  (Types.pi1 f1).pf_params; RTLabs_syntax.f_locals =
1388  (Types.pi1 f1).pf_locals; RTLabs_syntax.f_stacksize =
1389  (Types.pi1 f1).pf_stacksize; RTLabs_syntax.f_graph =
1390  (Types.pi1 f1).pf_graph; RTLabs_syntax.f_entry = (Types.pi1 f1).pf_entry;
1391  RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __
1392
1393(** val cminor_noinit_to_rtlabs :
1394    Cminor_syntax.cminor_noinit_program -> RTLabs_syntax.rTLabs_program **)
1395let cminor_noinit_to_rtlabs p =
1396  AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)
1397
1398open Initialisation
1399
1400(** val cminor_to_rtlabs :
1401    CostLabel.costlabel -> Cminor_syntax.cminor_program ->
1402    RTLabs_syntax.rTLabs_program **)
1403let cminor_to_rtlabs init_cost p =
1404  let p' = Initialisation.replace_init init_cost p in
1405  cminor_noinit_to_rtlabs p'
1406
Note: See TracBrowser for help on using the repository browser.