source: extracted/toRTLabs.ml @ 2649

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

...

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