source: driver/extracted/toRTLabs.ml @ 3085

Last change on this file since 3085 was 3059, checked in by sacerdot, 7 years ago

New extraction

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 CostLabel
98
99open FrontEndOps
100
101open Cminor_syntax
102
103open BitVectorTrie
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 = eta2859; Types.snd = gen0 } = rsengen in
124    let { Types.fst = rs; Types.snd = en0 } = eta2859 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 e id ty =
136  (Identifiers.lookup_present PreIdentifiers.SymbolTag e 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_15483 =
145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
146    x_15483
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_15485 =
154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
155    x_15485
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_15487 =
163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
164    x_15487
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_15489 =
172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
173    x_15489
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_15491 =
181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
182    x_15491
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_15493 =
190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
191    x_15493
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 g h_mk_goto_map x_15509 =
260  let gm_map = x_15509 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 g h_mk_goto_map x_15511 =
267  let gm_map = x_15511 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 g h_mk_goto_map x_15513 =
274  let gm_map = x_15513 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 g h_mk_goto_map x_15515 =
281  let gm_map = x_15515 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 g h_mk_goto_map x_15517 =
288  let gm_map = x_15517 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 g h_mk_goto_map x_15519 =
295  let gm_map = x_15519 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 g 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) ->
402    partial_fn -> 'a1 **)
403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15537 =
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_15537
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) ->
420    partial_fn -> 'a1 **)
421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15539 =
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_15539
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) ->
438    partial_fn -> 'a1 **)
439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15541 =
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_15541
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) ->
456    partial_fn -> 'a1 **)
457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15543 =
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_15543
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) ->
474    partial_fn -> 'a1 **)
475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15545 =
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_15545
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) ->
492    partial_fn -> 'a1 **)
493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15547 =
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_15547
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) ->
559    'a1 **)
560let partial_fn_inv_rect_Type4 x1 hterm h1 =
561  let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __
562
563(** val partial_fn_inv_rect_Type3 :
564    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
565    (Registers.register, AST.typ) Types.prod List.list ->
566    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
567    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
568    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
569    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
570    '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) ->
581    'a1 **)
582let partial_fn_inv_rect_Type2 x1 hterm h1 =
583  let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __
584
585(** val partial_fn_inv_rect_Type1 :
586    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
587    (Registers.register, AST.typ) Types.prod List.list ->
588    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
589    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
590    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
591    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
592    'a1 **)
593let partial_fn_inv_rect_Type1 x1 hterm h1 =
594  let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __
595
596(** val partial_fn_inv_rect_Type0 :
597    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
598    (Registers.register, AST.typ) Types.prod List.list ->
599    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
600    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
601    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
602    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
603    'a1 **)
604let partial_fn_inv_rect_Type0 x1 hterm h1 =
605  let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __
606
607(** val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
608let partial_fn_jmdiscr a1 x y =
609  Logic.eq_rect_Type2 x
610    (let { pf_labgen = a0; pf_reggen = a10; pf_params = a2; pf_locals = a3;
611       pf_result = a4; pf_stacksize = a6; pf_graph = a7; pf_gotos = a9;
612       pf_labels = a100; pf_entry = a12; pf_exit = a13 } = x
613     in
614    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
615    y
616
617(** val fn_contains_rect_Type4 :
618    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
619let rec fn_contains_rect_Type4 fx f1 f2 h_mk_fn_contains =
620  h_mk_fn_contains __ __ __
621
622(** val fn_contains_rect_Type5 :
623    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
624let rec fn_contains_rect_Type5 fx f1 f2 h_mk_fn_contains =
625  h_mk_fn_contains __ __ __
626
627(** val fn_contains_rect_Type3 :
628    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
629let rec fn_contains_rect_Type3 fx f1 f2 h_mk_fn_contains =
630  h_mk_fn_contains __ __ __
631
632(** val fn_contains_rect_Type2 :
633    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
634let rec fn_contains_rect_Type2 fx f1 f2 h_mk_fn_contains =
635  h_mk_fn_contains __ __ __
636
637(** val fn_contains_rect_Type1 :
638    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
639let rec fn_contains_rect_Type1 fx f1 f2 h_mk_fn_contains =
640  h_mk_fn_contains __ __ __
641
642(** val fn_contains_rect_Type0 :
643    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
644let rec fn_contains_rect_Type0 fx f1 f2 h_mk_fn_contains =
645  h_mk_fn_contains __ __ __
646
647(** val fn_contains_inv_rect_Type4 :
648    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
649let fn_contains_inv_rect_Type4 x1 x2 x3 h1 =
650  let hcut = fn_contains_rect_Type4 x1 x2 x3 h1 in hcut __
651
652(** val fn_contains_inv_rect_Type3 :
653    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
654let fn_contains_inv_rect_Type3 x1 x2 x3 h1 =
655  let hcut = fn_contains_rect_Type3 x1 x2 x3 h1 in hcut __
656
657(** val fn_contains_inv_rect_Type2 :
658    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
659let fn_contains_inv_rect_Type2 x1 x2 x3 h1 =
660  let hcut = fn_contains_rect_Type2 x1 x2 x3 h1 in hcut __
661
662(** val fn_contains_inv_rect_Type1 :
663    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
664let fn_contains_inv_rect_Type1 x1 x2 x3 h1 =
665  let hcut = fn_contains_rect_Type1 x1 x2 x3 h1 in hcut __
666
667(** val fn_contains_inv_rect_Type0 :
668    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
669let fn_contains_inv_rect_Type0 x1 x2 x3 h1 =
670  let hcut = fn_contains_rect_Type0 x1 x2 x3 h1 in hcut __
671
672(** val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __ **)
673let fn_contains_discr a1 a2 a3 =
674  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
675
676(** val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
677let fn_contains_jmdiscr a1 a2 a3 =
678  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
679
680(** val fill_in_statement :
681    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
682    partial_fn Types.sig0 **)
683let fill_in_statement fx l s f =
684  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
685    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
686    pf_stacksize = f.pf_stacksize; pf_graph =
687    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
688    (gm_map fx f.pf_graph f.pf_gotos); pf_labels = (Types.pi1 f.pf_labels);
689    pf_entry = (Types.pi1 f.pf_entry); pf_exit = (Types.pi1 f.pf_exit) }
690
691(** val add_to_graph :
692    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
693    partial_fn Types.sig0 **)
694let add_to_graph fx l s f =
695  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
696    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
697    pf_stacksize = f.pf_stacksize; pf_graph =
698    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
699    (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
700    pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) }
701
702(** val change_entry :
703    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
704let change_entry fx f l =
705  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
706    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
707    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
708    f.pf_gotos; pf_labels = f.pf_labels; pf_entry = l; pf_exit = f.pf_exit }
709
710(** val add_fresh_to_graph :
711    fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
712    partial_fn Types.sig0 **)
713let add_fresh_to_graph fx s f =
714  (let { Types.fst = l; Types.snd = g } =
715     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
716   in
717  (fun _ ->
718  let s1 = s (Types.pi1 f.pf_entry) in
719  { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
720  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
721  f.pf_stacksize; pf_graph =
722  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
723  (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
724  pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __
725
726(** val fresh_reg :
727    fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
728    Registers.register Types.sig0) Types.dPair **)
729let fresh_reg fx f ty =
730  let { Types.fst = r; Types.snd = g } =
731    Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
732  in
733  let f' = { pf_labgen = f.pf_labgen; pf_reggen = g; pf_params = f.pf_params;
734    pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty }, f.pf_locals));
735    pf_result =
736    ((match fx.fx_rettyp with
737      | Types.None -> Obj.magic __
738      | Types.Some t ->
739        (fun clearme -> let r' = Obj.magic clearme in Obj.magic r'))
740      f.pf_result); pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph;
741    pf_gotos = f.pf_gotos; pf_labels = f.pf_labels; pf_entry = f.pf_entry;
742    pf_exit = f.pf_exit }
743  in
744  { Types.dpi1 = f'; Types.dpi2 = r }
745
746(** val choose_reg :
747    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
748    Types.sig0, Registers.register Types.sig0) Types.dPair **)
749let choose_reg fx ty e f =
750  (match e with
751   | Cminor_syntax.Id (t, i) ->
752     (fun _ -> { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) })
753   | Cminor_syntax.Cst (x, x0) -> (fun _ -> fresh_reg fx f x)
754   | Cminor_syntax.Op1 (x, x0, x1, x2) -> (fun _ -> fresh_reg fx f x0)
755   | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) ->
756     (fun _ -> fresh_reg fx f x1)
757   | Cminor_syntax.Mem (x, x0) -> (fun _ -> fresh_reg fx f x)
758   | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) ->
759     (fun _ -> fresh_reg fx f x1)
760   | Cminor_syntax.Ecost (x, x0, x1) -> (fun _ -> fresh_reg fx f x)) __
761
762(** val foldr_all :
763    ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
764let rec foldr_all f b l =
765  (match l with
766   | List.Nil -> (fun _ -> b)
767   | List.Cons (a, l0) -> (fun _ -> f a __ (foldr_all f b l0))) __
768
769(** val foldr_all' :
770    ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
771let rec foldr_all' f b l =
772  (match l with
773   | List.Nil -> (fun _ -> b)
774   | List.Cons (a, l0) -> (fun _ -> f a __ l0 (foldr_all' f b l0))) __
775
776(** val eject' : ('a1, 'a2) Types.dPair -> 'a1 **)
777let eject' x =
778  x.Types.dpi1
779
780(** val choose_regs :
781    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
782    partial_fn -> (partial_fn Types.sig0, Registers.register List.list
783    Types.sig0) Types.dPair **)
784let choose_regs fx es f =
785  foldr_all' (fun e _ tl acc ->
786    let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
787    (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in
788    (fun _ ->
789    let { Types.dpi1 = f'; Types.dpi2 = r } =
790      choose_reg fx t e0 (Types.pi1 f1)
791    in
792    { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r),
793    (Types.pi1 rs))) })) __) { Types.dpi1 = f; Types.dpi2 = List.Nil } es
794
795(** val add_stmt_inv_rect_Type4 :
796    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
797    'a1) -> 'a1 **)
798let rec add_stmt_inv_rect_Type4 fx s f f' h_mk_add_stmt_inv =
799  h_mk_add_stmt_inv __ __
800
801(** val add_stmt_inv_rect_Type5 :
802    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
803    'a1) -> 'a1 **)
804let rec add_stmt_inv_rect_Type5 fx s f f' h_mk_add_stmt_inv =
805  h_mk_add_stmt_inv __ __
806
807(** val add_stmt_inv_rect_Type3 :
808    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
809    'a1) -> 'a1 **)
810let rec add_stmt_inv_rect_Type3 fx s f f' h_mk_add_stmt_inv =
811  h_mk_add_stmt_inv __ __
812
813(** val add_stmt_inv_rect_Type2 :
814    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
815    'a1) -> 'a1 **)
816let rec add_stmt_inv_rect_Type2 fx s f f' h_mk_add_stmt_inv =
817  h_mk_add_stmt_inv __ __
818
819(** val add_stmt_inv_rect_Type1 :
820    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
821    'a1) -> 'a1 **)
822let rec add_stmt_inv_rect_Type1 fx s f f' h_mk_add_stmt_inv =
823  h_mk_add_stmt_inv __ __
824
825(** val add_stmt_inv_rect_Type0 :
826    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
827    'a1) -> 'a1 **)
828let rec add_stmt_inv_rect_Type0 fx s f f' h_mk_add_stmt_inv =
829  h_mk_add_stmt_inv __ __
830
831(** val add_stmt_inv_inv_rect_Type4 :
832    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
833    __ -> 'a1) -> 'a1 **)
834let add_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
835  let hcut = add_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
836
837(** val add_stmt_inv_inv_rect_Type3 :
838    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
839    __ -> 'a1) -> 'a1 **)
840let add_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
841  let hcut = add_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
842
843(** val add_stmt_inv_inv_rect_Type2 :
844    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
845    __ -> 'a1) -> 'a1 **)
846let add_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
847  let hcut = add_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
848
849(** val add_stmt_inv_inv_rect_Type1 :
850    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
851    __ -> 'a1) -> 'a1 **)
852let add_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
853  let hcut = add_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
854
855(** val add_stmt_inv_inv_rect_Type0 :
856    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
857    __ -> 'a1) -> 'a1 **)
858let add_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
859  let hcut = add_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
860
861(** val add_stmt_inv_discr :
862    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
863let add_stmt_inv_discr a1 a2 a3 a4 =
864  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
865
866(** val add_stmt_inv_jmdiscr :
867    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
868let add_stmt_inv_jmdiscr a1 a2 a3 a4 =
869  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
870
871type fn_con_because =
872| Fn_con_eq of partial_fn
873| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
874| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
875   * partial_fn Types.sig0
876
877(** val fn_con_because_rect_Type4 :
878    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
879    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
880    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
881    fn_con_because -> 'a1 **)
882let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15624 = function
883| Fn_con_eq f -> h_fn_con_eq f
884| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
885| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
886
887(** val fn_con_because_rect_Type5 :
888    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
889    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
890    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
891    fn_con_because -> 'a1 **)
892let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15631 = function
893| Fn_con_eq f -> h_fn_con_eq f
894| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
895| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
896
897(** val fn_con_because_rect_Type3 :
898    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
899    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
900    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
901    fn_con_because -> 'a1 **)
902let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15638 = function
903| Fn_con_eq f -> h_fn_con_eq f
904| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
905| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
906
907(** val fn_con_because_rect_Type2 :
908    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
909    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
910    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
911    fn_con_because -> 'a1 **)
912let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15645 = function
913| Fn_con_eq f -> h_fn_con_eq f
914| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
915| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
916
917(** val fn_con_because_rect_Type1 :
918    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
919    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
920    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
921    fn_con_because -> 'a1 **)
922let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15652 = function
923| Fn_con_eq f -> h_fn_con_eq f
924| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
925| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
926
927(** val fn_con_because_rect_Type0 :
928    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
929    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
930    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
931    fn_con_because -> 'a1 **)
932let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15659 = function
933| Fn_con_eq f -> h_fn_con_eq f
934| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
935| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
936
937(** val fn_con_because_inv_rect_Type4 :
938    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
939    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
940    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
941    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
942let fn_con_because_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
943  let hcut = fn_con_because_rect_Type4 x1 h1 h2 h3 x2 hterm in hcut __ __
944
945(** val fn_con_because_inv_rect_Type3 :
946    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
947    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
948    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
949    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
950let fn_con_because_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
951  let hcut = fn_con_because_rect_Type3 x1 h1 h2 h3 x2 hterm in hcut __ __
952
953(** val fn_con_because_inv_rect_Type2 :
954    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
955    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
956    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
957    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
958let fn_con_because_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
959  let hcut = fn_con_because_rect_Type2 x1 h1 h2 h3 x2 hterm in hcut __ __
960
961(** val fn_con_because_inv_rect_Type1 :
962    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
963    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
964    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
965    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
966let fn_con_because_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
967  let hcut = fn_con_because_rect_Type1 x1 h1 h2 h3 x2 hterm in hcut __ __
968
969(** val fn_con_because_inv_rect_Type0 :
970    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
971    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
972    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
973    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
974let fn_con_because_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
975  let hcut = fn_con_because_rect_Type0 x1 h1 h2 h3 x2 hterm in hcut __ __
976
977(** val fn_con_because_discr :
978    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
979let fn_con_because_discr a1 a2 x y =
980  Logic.eq_rect_Type2 x
981    (match x with
982     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
983     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
984     | Fn_con_addinv (a0, a10, a3, a4) ->
985       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
986
987(** val fn_con_because_jmdiscr :
988    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
989let fn_con_because_jmdiscr a1 a2 x y =
990  Logic.eq_rect_Type2 x
991    (match x with
992     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
993     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
994     | Fn_con_addinv (a0, a10, a3, a4) ->
995       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
996
997(** val fn_con_because_left :
998    fixed -> partial_fn -> fn_con_because -> partial_fn **)
999let rec fn_con_because_left fx f0 = function
1000| Fn_con_eq f -> f
1001| Fn_con_sig (f, x, x1) -> f
1002| Fn_con_addinv (f, x, x1, x2) -> f
1003
1004(** val add_expr :
1005    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
1006    Registers.register Types.sig0 -> partial_fn Types.sig0 **)
1007let rec add_expr fx ty e f dst =
1008  (match e with
1009   | Cminor_syntax.Id (t, i) ->
1010     (fun _ dst0 ->
1011       let r = lookup_reg fx.fx_env i t in
1012       (match Registers.register_eq r (Types.pi1 dst0) with
1013        | Types.Inl _ -> f
1014        | Types.Inr _ ->
1015          Types.pi1
1016            (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t, t,
1017              (FrontEndOps.Oid t), (Types.pi1 dst0), r, x)) f)))
1018   | Cminor_syntax.Cst (x, c) ->
1019     (fun _ dst0 ->
1020       Types.pi1
1021         (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
1022           (Types.pi1 dst0), c, x0)) f))
1023   | Cminor_syntax.Op1 (t, t', op, e') ->
1024     (fun _ dst0 ->
1025       let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
1026       let f1 =
1027         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
1028           (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
1029       in
1030       let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
1031   | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
1032     (fun _ dst0 ->
1033       let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
1034       let { Types.dpi1 = f1; Types.dpi2 = r2 } =
1035         choose_reg fx x0 e2 (Types.pi1 f0)
1036       in
1037       let f2 =
1038         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
1039           op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
1040           (Types.pi1 f1)
1041       in
1042       let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r2) in
1043       let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r1) in
1044       Types.pi1 f4)
1045   | Cminor_syntax.Mem (t, e') ->
1046     (fun _ dst0 ->
1047       let { Types.dpi1 = f0; Types.dpi2 = r } =
1048         choose_reg fx AST.ASTptr e' f
1049       in
1050       let f1 =
1051         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_load (t,
1052           (Types.pi1 r), (Types.pi1 dst0), x)) (Types.pi1 f0)
1053       in
1054       let f2 = add_expr fx AST.ASTptr e' (Types.pi1 f1) (Types.pi1 r) in
1055       Types.pi1 f2)
1056   | Cminor_syntax.Cond (x, x0, x1, e', e1, e2) ->
1057     (fun _ dst0 ->
1058       let resume_at = f.pf_entry in
1059       let f0 = add_expr fx x1 e2 f dst0 in
1060       let lfalse = (Types.pi1 f0).pf_entry in
1061       let f1 =
1062         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_skip
1063           (Types.pi1 resume_at)) (Types.pi1 f0)
1064       in
1065       let f2 = add_expr fx x1 e1 (Types.pi1 f1) (Types.pi1 dst0) in
1066       let { Types.dpi1 = f3; Types.dpi2 = r } =
1067         choose_reg fx (AST.ASTint (x, x0)) e' (Types.pi1 f2)
1068       in
1069       let f4 =
1070         add_fresh_to_graph fx (fun ltrue -> RTLabs_syntax.St_cond
1071           ((Types.pi1 r), ltrue, (Types.pi1 lfalse))) (Types.pi1 f3)
1072       in
1073       let f5 =
1074         add_expr fx (AST.ASTint (x, x0)) e' (Types.pi1 f4) (Types.pi1 r)
1075       in
1076       Types.pi1 f5)
1077   | Cminor_syntax.Ecost (x, l, e') ->
1078     (fun _ dst0 ->
1079       let f0 = add_expr fx x e' f dst0 in
1080       let f1 =
1081         add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_cost (l, x0))
1082           (Types.pi1 f0)
1083       in
1084       Types.pi1 f1)) __ dst
1085
1086(** val add_exprs :
1087    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
1088    Registers.register List.list -> partial_fn -> partial_fn Types.sig0 **)
1089let rec add_exprs fx es dsts f =
1090  (match es with
1091   | List.Nil ->
1092     (fun _ _ ->
1093       match dsts with
1094       | List.Nil -> (fun _ -> f)
1095       | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
1096   | List.Cons (e, et) ->
1097     (fun _ ->
1098       match dsts with
1099       | List.Nil -> (fun _ _ -> assert false (* absurd case *))
1100       | List.Cons (r, rt) ->
1101         (fun _ _ ->
1102           let f' = add_exprs fx et rt f in
1103           (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
1104           (fun _ _ ->
1105           let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
1106             __))) __ __ __
1107
1108(** val stmt_inv_rect_Type4 :
1109    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1110let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
1111  h_mk_stmt_inv __ __ __
1112
1113(** val stmt_inv_rect_Type5 :
1114    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1115let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
1116  h_mk_stmt_inv __ __ __
1117
1118(** val stmt_inv_rect_Type3 :
1119    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1120let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
1121  h_mk_stmt_inv __ __ __
1122
1123(** val stmt_inv_rect_Type2 :
1124    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1125let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
1126  h_mk_stmt_inv __ __ __
1127
1128(** val stmt_inv_rect_Type1 :
1129    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1130let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
1131  h_mk_stmt_inv __ __ __
1132
1133(** val stmt_inv_rect_Type0 :
1134    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1135let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
1136  h_mk_stmt_inv __ __ __
1137
1138(** val stmt_inv_inv_rect_Type4 :
1139    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1140let stmt_inv_inv_rect_Type4 x1 x2 h1 =
1141  let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __
1142
1143(** val stmt_inv_inv_rect_Type3 :
1144    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1145let stmt_inv_inv_rect_Type3 x1 x2 h1 =
1146  let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __
1147
1148(** val stmt_inv_inv_rect_Type2 :
1149    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1150let stmt_inv_inv_rect_Type2 x1 x2 h1 =
1151  let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __
1152
1153(** val stmt_inv_inv_rect_Type1 :
1154    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1155let stmt_inv_inv_rect_Type1 x1 x2 h1 =
1156  let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __
1157
1158(** val stmt_inv_inv_rect_Type0 :
1159    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1160let stmt_inv_inv_rect_Type0 x1 x2 h1 =
1161  let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __
1162
1163(** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
1164let stmt_inv_discr a1 a2 =
1165  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1166
1167(** val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __ **)
1168let stmt_inv_jmdiscr a1 a2 =
1169  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1170
1171(** val expr_is_cst_ident :
1172    AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
1173let expr_is_cst_ident t = function
1174| Cminor_syntax.Id (x, x0) -> Types.None
1175| Cminor_syntax.Cst (x, c) ->
1176  (match c with
1177   | FrontEndOps.Ointconst (x0, x1, x2) -> Types.None
1178   | FrontEndOps.Oaddrsymbol (id, n) ->
1179     (match n with
1180      | Nat.O -> Types.Some id
1181      | Nat.S x0 -> Types.None)
1182   | FrontEndOps.Oaddrstack x0 -> Types.None)
1183| Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
1184| Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
1185| Cminor_syntax.Mem (x, x0) -> Types.None
1186| Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) -> Types.None
1187| Cminor_syntax.Ecost (x, x0, x1) -> Types.None
1188
1189(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1190let option_jmdiscr x y =
1191  Logic.eq_rect_Type2 x
1192    (match x with
1193     | Types.None -> Obj.magic (fun _ dH -> dH)
1194     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1195
1196(** val dPair_jmdiscr :
1197    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
1198let dPair_jmdiscr x y =
1199  Logic.eq_rect_Type2 x
1200    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
1201    Obj.magic (fun _ dH -> dH __ __)) y
1202
1203(** val add_return :
1204    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
1205    partial_fn -> partial_fn Types.sig0 **)
1206let add_return fx opt_e f =
1207  let f0 = f in
1208  let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
1209  (match opt_e with
1210   | Types.None -> (fun _ -> Types.pi1 f1)
1211   | Types.Some et ->
1212     let { Types.dpi1 = ty; Types.dpi2 = e } = et in
1213     (fun _ ->
1214     (match fx.fx_rettyp with
1215      | Types.None -> (fun _ -> assert false (* absurd case *))
1216      | Types.Some t ->
1217        (fun _ r ->
1218          let r0 = Obj.magic r in
1219          let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
1220       (Types.pi1 f1).pf_result)) __
1221
1222(** val record_goto_label :
1223    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn **)
1224let record_goto_label fx f l =
1225  { pf_labgen = f.pf_labgen; 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 = f.pf_graph; pf_gotos =
1228    f.pf_gotos; pf_labels =
1229    (Identifiers.add PreIdentifiers.Label (Types.pi1 f.pf_labels) l
1230      (Types.pi1 f.pf_entry)); pf_entry = f.pf_entry; pf_exit = f.pf_exit }
1231
1232(** val add_goto_dummy :
1233    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
1234let add_goto_dummy fx f dest =
1235  (let { Types.fst = l; Types.snd = g } =
1236     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
1237   in
1238  (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
1239  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1240  pf_stacksize = f.pf_stacksize; pf_graph =
1241  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
1242    (RTLabs_syntax.St_skip l)); pf_gotos =
1243  (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
1244    l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
1245  (Types.pi1 f.pf_exit) })) __
1246
1247(** val add_stmt :
1248    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0 **)
1249let rec add_stmt fx s f =
1250  (match s with
1251   | Cminor_syntax.St_skip -> (fun _ -> f)
1252   | Cminor_syntax.St_assign (t, x, e) ->
1253     (fun _ ->
1254       let dst = lookup_reg fx.fx_env x t in
1255       Types.pi1 (add_expr fx t e f dst))
1256   | Cminor_syntax.St_store (t, e1, e2) ->
1257     (fun _ ->
1258       let { Types.dpi1 = f0; Types.dpi2 = val_reg } = choose_reg fx t e2 f
1259       in
1260       let { Types.dpi1 = f1; Types.dpi2 = addr_reg } =
1261         choose_reg fx AST.ASTptr e1 (Types.pi1 f0)
1262       in
1263       let f2 =
1264         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_store (t,
1265           (Types.pi1 addr_reg), (Types.pi1 val_reg), x)) (Types.pi1 f1)
1266       in
1267       let f3 = add_expr fx AST.ASTptr e1 (Types.pi1 f2) (Types.pi1 addr_reg)
1268       in
1269       Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
1270   | Cminor_syntax.St_call (return_opt_id, e, args) ->
1271     (fun _ ->
1272       let return_opt_reg =
1273         (match return_opt_id with
1274          | Types.None -> (fun _ -> Types.None)
1275          | Types.Some idty ->
1276            (fun _ -> Types.Some
1277              (lookup_reg fx.fx_env idty.Types.fst idty.Types.snd))) __
1278       in
1279       let { Types.dpi1 = f0; Types.dpi2 = args_regs } =
1280         choose_regs fx args f
1281       in
1282       let f1 =
1283         match expr_is_cst_ident AST.ASTptr e with
1284         | Types.None ->
1285           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
1286             choose_reg fx AST.ASTptr e (Types.pi1 f0)
1287           in
1288           let f2 =
1289             add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_ptr
1290               ((Types.pi1 fnr), (Types.pi1 args_regs), return_opt_reg, x))
1291               (Types.pi1 f1)
1292           in
1293           Types.pi1
1294             (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
1295         | Types.Some id ->
1296           add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_id (id,
1297             (Types.pi1 args_regs), return_opt_reg, x)) (Types.pi1 f0)
1298       in
1299       Types.pi1 (add_exprs fx args (Types.pi1 args_regs) (Types.pi1 f1)))
1300   | Cminor_syntax.St_seq (s1, s2) ->
1301     (fun _ ->
1302       let f2 = add_stmt fx s2 f in
1303       let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
1304   | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
1305     (fun _ ->
1306       let l_next = f.pf_entry in
1307       let f2 = add_stmt fx s2 f in
1308       let l2 = (Types.pi1 f2).pf_entry in
1309       let f0 = change_entry fx (Types.pi1 f2) (Types.pi1 l_next) in
1310       let f1 = add_stmt fx s1 (Types.pi1 f0) in
1311       let { Types.dpi1 = f3; Types.dpi2 = r } =
1312         choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
1313       in
1314       let f4 =
1315         add_fresh_to_graph fx (fun l1 -> RTLabs_syntax.St_cond
1316           ((Types.pi1 r), l1, (Types.pi1 l2))) (Types.pi1 f3)
1317       in
1318       Types.pi1
1319         (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
1320   | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
1321   | Cminor_syntax.St_label (l, s') ->
1322     (fun _ ->
1323       let f0 = add_stmt fx s' f in record_goto_label fx (Types.pi1 f0) l)
1324   | Cminor_syntax.St_goto l -> (fun _ -> Types.pi1 (add_goto_dummy fx f l))
1325   | Cminor_syntax.St_cost (l, s') ->
1326     (fun _ ->
1327       let f0 = add_stmt fx s' f in
1328       Types.pi1
1329         (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_cost (l, x))
1330           (Types.pi1 f0)))) __
1331
1332(** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
1333let patch_gotos fx f =
1334  Identifiers.fold_inf PreIdentifiers.LabelTag
1335    (gm_map fx f.pf_graph f.pf_gotos) (fun l l' _ f' ->
1336    Types.pi1
1337      (fill_in_statement fx l (RTLabs_syntax.St_skip
1338        (Identifiers.lookup_present PreIdentifiers.Label
1339          (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f
1340
1341(** val c2ra_function :
1342    Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
1343let c2ra_function f =
1344  let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
1345  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
1346  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
1347  (let { Types.fst = eta3086; Types.snd = reggen1 } =
1348     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
1349       f.Cminor_syntax.f_params
1350   in
1351  let { Types.fst = params; Types.snd = env1 } = eta3086 in
1352  (fun _ ->
1353  (let { Types.fst = eta3085; Types.snd = reggen2 } =
1354     populate_env env1 reggen1 f.Cminor_syntax.f_vars
1355   in
1356  let { Types.fst = locals0; Types.snd = env0 } = eta3085 in
1357  (fun _ ->
1358  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
1359     match f.Cminor_syntax.f_return with
1360     | Types.None ->
1361       { Types.dpi1 = { Types.fst = locals0; Types.snd = reggen2 };
1362         Types.dpi2 = (Obj.magic __) }
1363     | Types.Some ty ->
1364       let { Types.fst = r; Types.snd = gen } =
1365         Identifiers.fresh PreIdentifiers.RegisterTag reggen2
1366       in
1367       { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
1368       ty }, locals0)); Types.snd = gen }; Types.dpi2 = r }
1369   in
1370  (fun _ ->
1371  let locals = locals_reggen.Types.fst in
1372  let reggen = locals_reggen.Types.snd in
1373  let { Types.fst = l; Types.snd = labgen } =
1374    Identifiers.fresh PreIdentifiers.LabelTag labgen0
1375  in
1376  let fixed0 = { fx_gotos =
1377    (Identifiers.set_of_list PreIdentifiers.Label
1378      (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
1379    fx_rettyp = f.Cminor_syntax.f_return }
1380  in
1381  let emptyfn = { pf_labgen = labgen; pf_reggen = reggen; pf_params = params;
1382    pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
1383    f.Cminor_syntax.f_stacksize; pf_graph =
1384    (Identifiers.add PreIdentifiers.LabelTag
1385      (Identifiers.empty_map PreIdentifiers.LabelTag) l
1386      RTLabs_syntax.St_return); pf_gotos =
1387    (Identifiers.empty_map PreIdentifiers.LabelTag); pf_labels =
1388    (Identifiers.empty_map PreIdentifiers.Label); pf_entry = l; pf_exit = l }
1389  in
1390  let f0 = add_stmt fixed0 f.Cminor_syntax.f_body emptyfn in
1391  let f1 = patch_gotos fixed0 (Types.pi1 f0) in
1392  { RTLabs_syntax.f_labgen = (Types.pi1 f1).pf_labgen;
1393  RTLabs_syntax.f_reggen = (Types.pi1 f1).pf_reggen; RTLabs_syntax.f_result =
1394  ((match fixed0.fx_rettyp with
1395    | Types.None -> Obj.magic (fun _ -> Types.None)
1396    | Types.Some t ->
1397      (fun r -> Types.Some { Types.fst = (Types.pi1 (Obj.magic r));
1398        Types.snd = t })) (Types.pi1 f1).pf_result); RTLabs_syntax.f_params =
1399  (Types.pi1 f1).pf_params; RTLabs_syntax.f_locals =
1400  (Types.pi1 f1).pf_locals; RTLabs_syntax.f_stacksize =
1401  (Types.pi1 f1).pf_stacksize; RTLabs_syntax.f_graph =
1402  (Types.pi1 f1).pf_graph; RTLabs_syntax.f_entry = (Types.pi1 f1).pf_entry;
1403  RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __
1404
1405(** val cminor_to_rtlabs :
1406    Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
1407let cminor_to_rtlabs p =
1408  AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)
1409
Note: See TracBrowser for help on using the repository browser.