source: extracted/toRTLabs.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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