source: driver/extracted/toRTLabs.ml @ 3106

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

New extraction.

File size: 54.6 KB
RevLine 
[2601]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
[2649]39open Coqlib
40
[2601]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
[2717]71open Exp
72
[2601]73open Arithmetic
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Extranat
82
83open Integers
84
85open AST
86
[2649]87open ErrorMessages
88
[2601]89open Positive
90
91open PreIdentifiers
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open FrontEndOps
100
101open Cminor_syntax
102
[2773]103open BitVectorTrie
104
[2601]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
[3106]123    let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in
124    let { Types.fst = rs; Types.snd = en0 } = eta2881 in
[2601]125    let { Types.fst = r; Types.snd = gen' } =
[2649]126      Identifiers.fresh PreIdentifiers.RegisterTag gen0
[2601]127    in
128    { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
129    ty }, rs)); Types.snd =
[2649]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 }
[2601]133
134(** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
[2773]135let lookup_reg e id ty =
136  (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst
[2601]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 **)
[3059]144let rec fixed_rect_Type4 h_mk_fixed x_15483 =
[2601]145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]146    x_15483
[2601]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 **)
[3059]153let rec fixed_rect_Type5 h_mk_fixed x_15485 =
[2601]154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]155    x_15485
[2601]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 **)
[3059]162let rec fixed_rect_Type3 h_mk_fixed x_15487 =
[2601]163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]164    x_15487
[2601]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 **)
[3059]171let rec fixed_rect_Type2 h_mk_fixed x_15489 =
[2601]172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]173    x_15489
[2601]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 **)
[3059]180let rec fixed_rect_Type1 h_mk_fixed x_15491 =
[2601]181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]182    x_15491
[2601]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 **)
[3059]189let rec fixed_rect_Type0 h_mk_fixed x_15493 =
[2601]190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
[3059]191    x_15493
[2601]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 **)
[3059]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 __ __
[2601]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 **)
[3059]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 __ __
[2601]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 **)
[3059]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 __ __
[2601]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 **)
[3059]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 __ __
[2601]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 **)
[3059]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 __ __
[2601]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 **)
[3059]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 __ __
[2601]296
297(** val gm_map :
298    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
299    PreIdentifiers.identifier Identifiers.identifier_map **)
[2773]300let rec gm_map fx g xxx =
[2601]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 -> __ ->
[2997]401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
402    partial_fn -> 'a1 **)
[3059]403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15537 =
[2601]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 } =
[3059]408    x_15537
[2601]409  in
410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]411    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
420    partial_fn -> 'a1 **)
[3059]421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15539 =
[2601]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 } =
[3059]426    x_15539
[2601]427  in
428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]429    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
438    partial_fn -> 'a1 **)
[3059]439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15541 =
[2601]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 } =
[3059]444    x_15541
[2601]445  in
446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]447    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
456    partial_fn -> 'a1 **)
[3059]457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15543 =
[2601]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 } =
[3059]462    x_15543
[2601]463  in
464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]465    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
474    partial_fn -> 'a1 **)
[3059]475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15545 =
[2601]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 } =
[3059]480    x_15545
[2601]481  in
482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]483    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
492    partial_fn -> 'a1 **)
[3059]493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15547 =
[2601]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 } =
[3059]498    x_15547
[2601]499  in
500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
[2997]501    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
[2601]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 -> __ ->
[2997]558    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
559    'a1 **)
[2601]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 -> __ ->
[2997]569    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
570    'a1 **)
[2601]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 -> __ ->
[2997]580    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
581    'a1 **)
[2601]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 -> __ ->
[2997]591    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
592    'a1 **)
[2601]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 -> __ ->
[2997]602    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
603    'a1 **)
[2601]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
[2997]614    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
615    y
[2601]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 =
[2649]687    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
[2601]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 =
[2649]698    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
[2601]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 =
[2773]714  (let { Types.fst = l; Types.snd = g } =
[2649]715     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
[2601]716   in
717  (fun _ ->
718  let s1 = s (Types.pi1 f.pf_entry) in
[2773]719  { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
[2601]720  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
721  f.pf_stacksize; pf_graph =
[2649]722  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
[2601]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 =
[2773]730  let { Types.fst = r; Types.snd = g } =
[2649]731    Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
[2601]732  in
[2773]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 =
[2601]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 **)
[2773]749let choose_reg fx ty e f =
750  (match e with
[2601]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 =
[2773]785  foldr_all' (fun e _ tl acc ->
[2601]786    let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
[2773]787    (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in
[2601]788    (fun _ ->
789    let { Types.dpi1 = f'; Types.dpi2 = r } =
[2773]790      choose_reg fx t e0 (Types.pi1 f1)
[2601]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 **)
[3059]882let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15624 = function
[2601]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 **)
[3059]892let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15631 = function
[2601]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 **)
[3059]902let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15638 = function
[2601]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 **)
[3059]912let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15645 = function
[2601]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 **)
[3059]922let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15652 = function
[2601]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 **)
[3059]932let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15659 = function
[2601]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 **)
[2773]1007let rec add_expr fx ty e f dst =
1008  (match e with
[2601]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))
[2773]1023   | Cminor_syntax.Op1 (t, t', op, e') ->
[2601]1024     (fun _ dst0 ->
1025       let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
1026       let f1 =
[2773]1027         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
[2601]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)
[2773]1031   | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
[2601]1032     (fun _ dst0 ->
[2773]1033       let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
1034       let { Types.dpi1 = f1; Types.dpi2 = r2 } =
[2601]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,
[2773]1039           op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
[2601]1040           (Types.pi1 f1)
1041       in
[2773]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
[2601]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 *)))
[2773]1096   | List.Cons (e, et) ->
[2601]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
[2773]1103           (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
[2601]1104           (fun _ _ ->
[2773]1105           let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
[2601]1106             __))) __ __ __
1107
[2773]1108(** val stmt_inv_rect_Type4 :
[2601]1109    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1110let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
[2601]1111  h_mk_stmt_inv __ __ __
1112
[2773]1113(** val stmt_inv_rect_Type5 :
[2601]1114    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1115let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
[2601]1116  h_mk_stmt_inv __ __ __
1117
[2773]1118(** val stmt_inv_rect_Type3 :
[2601]1119    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1120let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
[2601]1121  h_mk_stmt_inv __ __ __
1122
[2773]1123(** val stmt_inv_rect_Type2 :
[2601]1124    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1125let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
[2601]1126  h_mk_stmt_inv __ __ __
1127
[2773]1128(** val stmt_inv_rect_Type1 :
[2601]1129    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1130let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
[2601]1131  h_mk_stmt_inv __ __ __
1132
[2773]1133(** val stmt_inv_rect_Type0 :
[2601]1134    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2773]1135let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
[2601]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 =
[2773]1141  let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __
[2601]1142
1143(** val stmt_inv_inv_rect_Type3 :
1144    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1145let stmt_inv_inv_rect_Type3 x1 x2 h1 =
[2773]1146  let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __
[2601]1147
1148(** val stmt_inv_inv_rect_Type2 :
1149    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1150let stmt_inv_inv_rect_Type2 x1 x2 h1 =
[2773]1151  let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __
[2601]1152
1153(** val stmt_inv_inv_rect_Type1 :
1154    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1155let stmt_inv_inv_rect_Type1 x1 x2 h1 =
[2773]1156  let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __
[2601]1157
1158(** val stmt_inv_inv_rect_Type0 :
1159    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1160let stmt_inv_inv_rect_Type0 x1 x2 h1 =
[2773]1161  let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __
[2601]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
[2951]1171(** val expr_is_cst_ident :
[2601]1172    AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
[2951]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)
[2601]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
[2974]1208  let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
[2601]1209  (match opt_e with
1210   | Types.None -> (fun _ -> Types.pi1 f1)
1211   | Types.Some et ->
[2773]1212     let { Types.dpi1 = ty; Types.dpi2 = e } = et in
[2601]1213     (fun _ ->
1214     (match fx.fx_rettyp with
1215      | Types.None -> (fun _ -> assert false (* absurd case *))
1216      | Types.Some t ->
1217        (fun _ r ->
[2773]1218          let r0 = Obj.magic r in
1219          let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
[2601]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 =
[2649]1229    (Identifiers.add PreIdentifiers.Label (Types.pi1 f.pf_labels) l
[2601]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 =
[2773]1235  (let { Types.fst = l; Types.snd = g } =
[2649]1236     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
[2601]1237   in
[2773]1238  (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
[2601]1239  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1240  pf_stacksize = f.pf_stacksize; pf_graph =
[2649]1241  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
[2997]1242    (RTLabs_syntax.St_skip l)); pf_gotos =
[2649]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 =
[2601]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)
[2773]1252   | Cminor_syntax.St_assign (t, x, e) ->
[2601]1253     (fun _ ->
1254       let dst = lookup_reg fx.fx_env x t in
[2773]1255       Types.pi1 (add_expr fx t e f dst))
[2601]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)))
[2773]1270   | Cminor_syntax.St_call (return_opt_id, e, args) ->
[2601]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 =
[2951]1283         match expr_is_cst_ident AST.ASTptr e with
[2601]1284         | Types.None ->
1285           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
[2773]1286             choose_reg fx AST.ASTptr e (Types.pi1 f0)
[2601]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
[2773]1294             (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
[2601]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)
[2773]1304   | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
[2601]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 } =
[2773]1312         choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
[2601]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
[2773]1319         (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
[2601]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 =
[2649]1334  Identifiers.fold_inf PreIdentifiers.LabelTag
1335    (gm_map fx f.pf_graph f.pf_gotos) (fun l l' _ f' ->
[2601]1336    Types.pi1
1337      (fill_in_statement fx l (RTLabs_syntax.St_skip
[2649]1338        (Identifiers.lookup_present PreIdentifiers.Label
[2601]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 =
[2649]1344  let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
1345  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
[2601]1346  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
[3106]1347  (let { Types.fst = eta3108; Types.snd = reggen1 } =
[2649]1348     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
[2601]1349       f.Cminor_syntax.f_params
1350   in
[3106]1351  let { Types.fst = params; Types.snd = env1 } = eta3108 in
[2601]1352  (fun _ ->
[3106]1353  (let { Types.fst = eta3107; Types.snd = reggen2 } =
[2601]1354     populate_env env1 reggen1 f.Cminor_syntax.f_vars
1355   in
[3106]1356  let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
[2601]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 } =
[2649]1365         Identifiers.fresh PreIdentifiers.RegisterTag reggen2
[2601]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 } =
[2649]1374    Identifiers.fresh PreIdentifiers.LabelTag labgen0
[2601]1375  in
1376  let fixed0 = { fx_gotos =
[2649]1377    (Identifiers.set_of_list PreIdentifiers.Label
[2601]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 =
[2649]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 }
[2601]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
[2951]1405(** val cminor_to_rtlabs :
1406    Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
1407let cminor_to_rtlabs p =
[2601]1408  AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)
1409
Note: See TracBrowser for help on using the repository browser.