23 open Hints_declaration
114 (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
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 **)
120 let populate_env en gen =
121 List.foldr (fun idt rsengen ->
122 let { Types.fst = id; Types.snd = ty } = idt in
123 let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in
124 let { Types.fst = rs; Types.snd = en0 } = eta2881 in
125 let { Types.fst = r; Types.snd = gen' } =
126 Identifiers.fresh PreIdentifiers.RegisterTag gen0
128 { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
129 ty }, rs)); Types.snd =
130 (Identifiers.add PreIdentifiers.SymbolTag en0 id { Types.fst = r;
131 Types.snd = ty }) }; Types.snd = gen' }) { Types.fst = { Types.fst =
132 List.Nil; Types.snd = en }; Types.snd = gen }
134 (** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
135 let lookup_reg e id ty =
136 (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst
138 type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
139 fx_rettyp : AST.typ Types.option }
141 (** val fixed_rect_Type4 :
142 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
144 let rec fixed_rect_Type4 h_mk_fixed x_15483 =
145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
148 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
150 (** val fixed_rect_Type5 :
151 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
153 let rec fixed_rect_Type5 h_mk_fixed x_15485 =
154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
157 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
159 (** val fixed_rect_Type3 :
160 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
162 let rec fixed_rect_Type3 h_mk_fixed x_15487 =
163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
166 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
168 (** val fixed_rect_Type2 :
169 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
171 let rec fixed_rect_Type2 h_mk_fixed x_15489 =
172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
175 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
177 (** val fixed_rect_Type1 :
178 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
180 let rec fixed_rect_Type1 h_mk_fixed x_15491 =
181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
184 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
186 (** val fixed_rect_Type0 :
187 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
189 let rec fixed_rect_Type0 h_mk_fixed x_15493 =
190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
193 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
195 (** val fx_gotos : fixed -> Identifiers.identifier_set **)
196 let rec fx_gotos xxx =
199 (** val fx_env : fixed -> env **)
203 (** val fx_rettyp : fixed -> AST.typ Types.option **)
204 let rec fx_rettyp xxx =
207 (** val fixed_inv_rect_Type4 :
208 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
210 let fixed_inv_rect_Type4 hterm h1 =
211 let hcut = fixed_rect_Type4 h1 hterm in hcut __
213 (** val fixed_inv_rect_Type3 :
214 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
216 let fixed_inv_rect_Type3 hterm h1 =
217 let hcut = fixed_rect_Type3 h1 hterm in hcut __
219 (** val fixed_inv_rect_Type2 :
220 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
222 let fixed_inv_rect_Type2 hterm h1 =
223 let hcut = fixed_rect_Type2 h1 hterm in hcut __
225 (** val fixed_inv_rect_Type1 :
226 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
228 let fixed_inv_rect_Type1 hterm h1 =
229 let hcut = fixed_rect_Type1 h1 hterm in hcut __
231 (** val fixed_inv_rect_Type0 :
232 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
234 let fixed_inv_rect_Type0 hterm h1 =
235 let hcut = fixed_rect_Type0 h1 hterm in hcut __
237 (** val fixed_discr : fixed -> fixed -> __ **)
238 let 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
243 (** val fixed_jmdiscr : fixed -> fixed -> __ **)
244 let 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
252 PreIdentifiers.identifier Identifiers.identifier_map
253 (* singleton inductive, whose constructor was mk_goto_map *)
255 (** val goto_map_rect_Type4 :
256 fixed -> RTLabs_syntax.statement Graphs.graph ->
257 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
258 -> goto_map -> 'a1 **)
259 let 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 __ __
262 (** val goto_map_rect_Type5 :
263 fixed -> RTLabs_syntax.statement Graphs.graph ->
264 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
265 -> goto_map -> 'a1 **)
266 let 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 __ __
269 (** val goto_map_rect_Type3 :
270 fixed -> RTLabs_syntax.statement Graphs.graph ->
271 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
272 -> goto_map -> 'a1 **)
273 let 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 __ __
276 (** val goto_map_rect_Type2 :
277 fixed -> RTLabs_syntax.statement Graphs.graph ->
278 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
279 -> goto_map -> 'a1 **)
280 let 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 __ __
283 (** val goto_map_rect_Type1 :
284 fixed -> RTLabs_syntax.statement Graphs.graph ->
285 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
286 -> goto_map -> 'a1 **)
287 let 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 __ __
290 (** val goto_map_rect_Type0 :
291 fixed -> RTLabs_syntax.statement Graphs.graph ->
292 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
293 -> goto_map -> 'a1 **)
294 let 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 __ __
298 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
299 PreIdentifiers.identifier Identifiers.identifier_map **)
300 let rec gm_map fx g xxx =
303 (** val goto_map_inv_rect_Type4 :
304 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
305 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
307 let goto_map_inv_rect_Type4 x1 x2 hterm h1 =
308 let hcut = goto_map_rect_Type4 x1 x2 h1 hterm in hcut __
310 (** val goto_map_inv_rect_Type3 :
311 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
312 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
314 let goto_map_inv_rect_Type3 x1 x2 hterm h1 =
315 let hcut = goto_map_rect_Type3 x1 x2 h1 hterm in hcut __
317 (** val goto_map_inv_rect_Type2 :
318 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
319 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
321 let goto_map_inv_rect_Type2 x1 x2 hterm h1 =
322 let hcut = goto_map_rect_Type2 x1 x2 h1 hterm in hcut __
324 (** val goto_map_inv_rect_Type1 :
325 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
326 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
328 let goto_map_inv_rect_Type1 x1 x2 hterm h1 =
329 let hcut = goto_map_rect_Type1 x1 x2 h1 hterm in hcut __
331 (** val goto_map_inv_rect_Type0 :
332 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
333 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
335 let goto_map_inv_rect_Type0 x1 x2 hterm h1 =
336 let hcut = goto_map_rect_Type0 x1 x2 h1 hterm in hcut __
338 (** val goto_map_discr :
339 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
341 let goto_map_discr a1 a2 x y =
342 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
344 (** val goto_map_jmdiscr :
345 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
347 let goto_map_jmdiscr a1 a2 x y =
348 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
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
354 let dpi1__o__gm_map__o__inject x1 x2 x4 =
355 gm_map x1 x2 x4.Types.dpi1
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 **)
360 let eject__o__gm_map__o__inject x1 x2 x4 =
361 gm_map x1 x2 (Types.pi1 x4)
363 (** val gm_map__o__inject :
364 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
365 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
366 let gm_map__o__inject x1 x2 x3 =
369 (** val dpi1__o__gm_map :
370 fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
371 Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map **)
372 let dpi1__o__gm_map x0 x1 x3 =
373 gm_map x0 x1 x3.Types.dpi1
375 (** val eject__o__gm_map :
376 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
377 PreIdentifiers.identifier Identifiers.identifier_map **)
378 let eject__o__gm_map x0 x1 x3 =
379 gm_map x0 x1 (Types.pi1 x3)
381 type partial_fn = { pf_labgen : Identifiers.universe;
382 pf_reggen : Identifiers.universe;
383 pf_params : (Registers.register, AST.typ) Types.prod
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;
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 }
395 (** val partial_fn_rect_Type4 :
396 fixed -> (Identifiers.universe -> Identifiers.universe ->
397 (Registers.register, AST.typ) Types.prod List.list ->
398 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
399 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
400 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
401 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
402 partial_fn -> 'a1 **)
403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15537 =
404 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
405 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
406 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
407 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
410 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
411 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
413 (** val partial_fn_rect_Type5 :
414 fixed -> (Identifiers.universe -> Identifiers.universe ->
415 (Registers.register, AST.typ) Types.prod List.list ->
416 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
417 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
418 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
419 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
420 partial_fn -> 'a1 **)
421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15539 =
422 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
423 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
424 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
425 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
428 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
429 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
431 (** val partial_fn_rect_Type3 :
432 fixed -> (Identifiers.universe -> Identifiers.universe ->
433 (Registers.register, AST.typ) Types.prod List.list ->
434 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
435 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
436 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
437 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
438 partial_fn -> 'a1 **)
439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15541 =
440 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
441 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
442 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
443 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
446 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
447 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
449 (** val partial_fn_rect_Type2 :
450 fixed -> (Identifiers.universe -> Identifiers.universe ->
451 (Registers.register, AST.typ) Types.prod List.list ->
452 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
453 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
454 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
455 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
456 partial_fn -> 'a1 **)
457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15543 =
458 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
459 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
460 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
461 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
464 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
465 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
467 (** val partial_fn_rect_Type1 :
468 fixed -> (Identifiers.universe -> Identifiers.universe ->
469 (Registers.register, AST.typ) Types.prod List.list ->
470 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
471 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
472 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
473 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
474 partial_fn -> 'a1 **)
475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15545 =
476 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
477 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
478 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
479 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
482 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
483 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
485 (** val partial_fn_rect_Type0 :
486 fixed -> (Identifiers.universe -> Identifiers.universe ->
487 (Registers.register, AST.typ) Types.prod List.list ->
488 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
489 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
490 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
491 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
492 partial_fn -> 'a1 **)
493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15547 =
494 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
495 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
496 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
497 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
501 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
503 (** val pf_labgen : fixed -> partial_fn -> Identifiers.universe **)
504 let rec pf_labgen fx xxx =
507 (** val pf_reggen : fixed -> partial_fn -> Identifiers.universe **)
508 let rec pf_reggen fx xxx =
512 fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
513 let rec pf_params fx xxx =
517 fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
518 let rec pf_locals fx xxx =
521 (** val pf_result : fixed -> partial_fn -> resultok **)
522 let rec pf_result fx xxx =
525 (** val pf_stacksize : fixed -> partial_fn -> Nat.nat **)
526 let rec pf_stacksize fx xxx =
530 fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph **)
531 let rec pf_graph fx xxx =
534 (** val pf_gotos : fixed -> partial_fn -> goto_map **)
535 let rec pf_gotos fx xxx =
539 fixed -> partial_fn -> PreIdentifiers.identifier
540 Identifiers.identifier_map Types.sig0 **)
541 let rec pf_labels fx xxx =
544 (** val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0 **)
545 let rec pf_entry fx xxx =
548 (** val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0 **)
549 let rec pf_exit fx xxx =
552 (** val partial_fn_inv_rect_Type4 :
553 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
554 (Registers.register, AST.typ) Types.prod List.list ->
555 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
556 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
557 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
558 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
560 let partial_fn_inv_rect_Type4 x1 hterm h1 =
561 let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __
563 (** val partial_fn_inv_rect_Type3 :
564 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
565 (Registers.register, AST.typ) Types.prod List.list ->
566 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
567 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
568 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
569 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
571 let partial_fn_inv_rect_Type3 x1 hterm h1 =
572 let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __
574 (** val partial_fn_inv_rect_Type2 :
575 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
576 (Registers.register, AST.typ) Types.prod List.list ->
577 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
578 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
579 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
580 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
582 let partial_fn_inv_rect_Type2 x1 hterm h1 =
583 let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __
585 (** val partial_fn_inv_rect_Type1 :
586 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
587 (Registers.register, AST.typ) Types.prod List.list ->
588 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
589 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
590 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
591 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
593 let partial_fn_inv_rect_Type1 x1 hterm h1 =
594 let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __
596 (** val partial_fn_inv_rect_Type0 :
597 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
598 (Registers.register, AST.typ) Types.prod List.list ->
599 (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
600 Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
601 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
602 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
604 let partial_fn_inv_rect_Type0 x1 hterm h1 =
605 let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __
607 (** val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
608 let 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
614 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
617 (** val fn_contains_rect_Type4 :
618 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
619 let rec fn_contains_rect_Type4 fx f1 f2 h_mk_fn_contains =
620 h_mk_fn_contains __ __ __
622 (** val fn_contains_rect_Type5 :
623 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
624 let rec fn_contains_rect_Type5 fx f1 f2 h_mk_fn_contains =
625 h_mk_fn_contains __ __ __
627 (** val fn_contains_rect_Type3 :
628 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
629 let rec fn_contains_rect_Type3 fx f1 f2 h_mk_fn_contains =
630 h_mk_fn_contains __ __ __
632 (** val fn_contains_rect_Type2 :
633 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
634 let rec fn_contains_rect_Type2 fx f1 f2 h_mk_fn_contains =
635 h_mk_fn_contains __ __ __
637 (** val fn_contains_rect_Type1 :
638 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
639 let rec fn_contains_rect_Type1 fx f1 f2 h_mk_fn_contains =
640 h_mk_fn_contains __ __ __
642 (** val fn_contains_rect_Type0 :
643 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
644 let rec fn_contains_rect_Type0 fx f1 f2 h_mk_fn_contains =
645 h_mk_fn_contains __ __ __
647 (** val fn_contains_inv_rect_Type4 :
648 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
649 let fn_contains_inv_rect_Type4 x1 x2 x3 h1 =
650 let hcut = fn_contains_rect_Type4 x1 x2 x3 h1 in hcut __
652 (** val fn_contains_inv_rect_Type3 :
653 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
654 let fn_contains_inv_rect_Type3 x1 x2 x3 h1 =
655 let hcut = fn_contains_rect_Type3 x1 x2 x3 h1 in hcut __
657 (** val fn_contains_inv_rect_Type2 :
658 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
659 let fn_contains_inv_rect_Type2 x1 x2 x3 h1 =
660 let hcut = fn_contains_rect_Type2 x1 x2 x3 h1 in hcut __
662 (** val fn_contains_inv_rect_Type1 :
663 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
664 let fn_contains_inv_rect_Type1 x1 x2 x3 h1 =
665 let hcut = fn_contains_rect_Type1 x1 x2 x3 h1 in hcut __
667 (** val fn_contains_inv_rect_Type0 :
668 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
669 let fn_contains_inv_rect_Type0 x1 x2 x3 h1 =
670 let hcut = fn_contains_rect_Type0 x1 x2 x3 h1 in hcut __
672 (** val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __ **)
673 let fn_contains_discr a1 a2 a3 =
674 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
676 (** val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
677 let fn_contains_jmdiscr a1 a2 a3 =
678 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
680 (** val fill_in_statement :
681 fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
682 partial_fn Types.sig0 **)
683 let fill_in_statement fx l s f =
684 { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
685 f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
686 pf_stacksize = f.pf_stacksize; pf_graph =
687 (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
688 (gm_map fx f.pf_graph f.pf_gotos); pf_labels = (Types.pi1 f.pf_labels);
689 pf_entry = (Types.pi1 f.pf_entry); pf_exit = (Types.pi1 f.pf_exit) }
691 (** val add_to_graph :
692 fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
693 partial_fn Types.sig0 **)
694 let add_to_graph fx l s f =
695 { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
696 f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
697 pf_stacksize = f.pf_stacksize; pf_graph =
698 (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
699 (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
700 pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) }
702 (** val change_entry :
703 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
704 let 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 }
710 (** val add_fresh_to_graph :
711 fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
712 partial_fn Types.sig0 **)
713 let add_fresh_to_graph fx s f =
714 (let { Types.fst = l; Types.snd = g } =
715 Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
718 let s1 = s (Types.pi1 f.pf_entry) in
719 { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
720 pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
721 f.pf_stacksize; pf_graph =
722 (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
723 (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
724 pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __
727 fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
728 Registers.register Types.sig0) Types.dPair **)
729 let fresh_reg fx f ty =
730 let { Types.fst = r; Types.snd = g } =
731 Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
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));
736 ((match fx.fx_rettyp with
737 | Types.None -> Obj.magic __
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 }
744 { Types.dpi1 = f'; Types.dpi2 = r }
747 fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
748 Types.sig0, Registers.register Types.sig0) Types.dPair **)
749 let choose_reg fx ty e f =
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)) __
763 ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
764 let rec foldr_all f b l =
766 | List.Nil -> (fun _ -> b)
767 | List.Cons (a, l0) -> (fun _ -> f a __ (foldr_all f b l0))) __
770 ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
771 let rec foldr_all' f b l =
773 | List.Nil -> (fun _ -> b)
774 | List.Cons (a, l0) -> (fun _ -> f a __ l0 (foldr_all' f b l0))) __
776 (** val eject' : ('a1, 'a2) Types.dPair -> 'a1 **)
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 **)
784 let choose_regs fx es f =
785 foldr_all' (fun e _ tl acc ->
786 let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
787 (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in
789 let { Types.dpi1 = f'; Types.dpi2 = r } =
790 choose_reg fx t e0 (Types.pi1 f1)
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
795 (** val add_stmt_inv_rect_Type4 :
796 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
798 let rec add_stmt_inv_rect_Type4 fx s f f' h_mk_add_stmt_inv =
799 h_mk_add_stmt_inv __ __
801 (** val add_stmt_inv_rect_Type5 :
802 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
804 let rec add_stmt_inv_rect_Type5 fx s f f' h_mk_add_stmt_inv =
805 h_mk_add_stmt_inv __ __
807 (** val add_stmt_inv_rect_Type3 :
808 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
810 let rec add_stmt_inv_rect_Type3 fx s f f' h_mk_add_stmt_inv =
811 h_mk_add_stmt_inv __ __
813 (** val add_stmt_inv_rect_Type2 :
814 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
816 let rec add_stmt_inv_rect_Type2 fx s f f' h_mk_add_stmt_inv =
817 h_mk_add_stmt_inv __ __
819 (** val add_stmt_inv_rect_Type1 :
820 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
822 let rec add_stmt_inv_rect_Type1 fx s f f' h_mk_add_stmt_inv =
823 h_mk_add_stmt_inv __ __
825 (** val add_stmt_inv_rect_Type0 :
826 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
828 let rec add_stmt_inv_rect_Type0 fx s f f' h_mk_add_stmt_inv =
829 h_mk_add_stmt_inv __ __
831 (** val add_stmt_inv_inv_rect_Type4 :
832 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
833 __ -> 'a1) -> 'a1 **)
834 let 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 __
837 (** val add_stmt_inv_inv_rect_Type3 :
838 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
839 __ -> 'a1) -> 'a1 **)
840 let 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 __
843 (** val add_stmt_inv_inv_rect_Type2 :
844 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
845 __ -> 'a1) -> 'a1 **)
846 let 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 __
849 (** val add_stmt_inv_inv_rect_Type1 :
850 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
851 __ -> 'a1) -> 'a1 **)
852 let 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 __
855 (** val add_stmt_inv_inv_rect_Type0 :
856 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
857 __ -> 'a1) -> 'a1 **)
858 let 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 __
861 (** val add_stmt_inv_discr :
862 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
863 let add_stmt_inv_discr a1 a2 a3 a4 =
864 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
866 (** val add_stmt_inv_jmdiscr :
867 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
868 let add_stmt_inv_jmdiscr a1 a2 a3 a4 =
869 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
871 type 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
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 **)
882 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15624 = function
883 | Fn_con_eq f -> h_fn_con_eq f
884 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
885 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
892 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15631 = function
893 | Fn_con_eq f -> h_fn_con_eq f
894 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
895 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
902 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15638 = function
903 | Fn_con_eq f -> h_fn_con_eq f
904 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
905 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
912 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15645 = function
913 | Fn_con_eq f -> h_fn_con_eq f
914 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
915 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
922 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15652 = function
923 | Fn_con_eq f -> h_fn_con_eq f
924 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
925 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
932 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15659 = function
933 | Fn_con_eq f -> h_fn_con_eq f
934 | Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
935 | Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3
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 **)
942 let 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 __ __
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 **)
950 let 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 __ __
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 **)
958 let 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 __ __
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 **)
966 let 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 __ __
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 **)
974 let 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 __ __
977 (** val fn_con_because_discr :
978 fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
979 let fn_con_because_discr a1 a2 x y =
980 Logic.eq_rect_Type2 x
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
987 (** val fn_con_because_jmdiscr :
988 fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
989 let fn_con_because_jmdiscr a1 a2 x y =
990 Logic.eq_rect_Type2 x
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
997 (** val fn_con_because_left :
998 fixed -> partial_fn -> fn_con_because -> partial_fn **)
999 let rec fn_con_because_left fx f0 = function
1001 | Fn_con_sig (f, x, x1) -> f
1002 | Fn_con_addinv (f, x, x1, x2) -> f
1005 fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
1006 Registers.register Types.sig0 -> partial_fn Types.sig0 **)
1007 let rec add_expr fx ty e f dst =
1009 | Cminor_syntax.Id (t, i) ->
1011 let r = lookup_reg fx.fx_env i t in
1012 (match Registers.register_eq r (Types.pi1 dst0) with
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) ->
1021 (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
1022 (Types.pi1 dst0), c, x0)) f))
1023 | Cminor_syntax.Op1 (t, t', op, e') ->
1025 let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
1027 add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
1028 (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
1030 let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
1031 | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
1033 let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
1034 let { Types.dpi1 = f1; Types.dpi2 = r2 } =
1035 choose_reg fx x0 e2 (Types.pi1 f0)
1038 add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
1039 op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
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
1045 | Cminor_syntax.Mem (t, e') ->
1047 let { Types.dpi1 = f0; Types.dpi2 = r } =
1048 choose_reg fx AST.ASTptr e' f
1051 add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_load (t,
1052 (Types.pi1 r), (Types.pi1 dst0), x)) (Types.pi1 f0)
1054 let f2 = add_expr fx AST.ASTptr e' (Types.pi1 f1) (Types.pi1 r) in
1056 | Cminor_syntax.Cond (x, x0, x1, e', e1, e2) ->
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
1062 add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_skip
1063 (Types.pi1 resume_at)) (Types.pi1 f0)
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)
1070 add_fresh_to_graph fx (fun ltrue -> RTLabs_syntax.St_cond
1071 ((Types.pi1 r), ltrue, (Types.pi1 lfalse))) (Types.pi1 f3)
1074 add_expr fx (AST.ASTint (x, x0)) e' (Types.pi1 f4) (Types.pi1 r)
1077 | Cminor_syntax.Ecost (x, l, e') ->
1079 let f0 = add_expr fx x e' f dst0 in
1081 add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_cost (l, x0))
1084 Types.pi1 f1)) __ dst
1087 fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
1088 Registers.register List.list -> partial_fn -> partial_fn Types.sig0 **)
1089 let rec add_exprs fx es dsts f =
1094 | List.Nil -> (fun _ -> f)
1095 | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
1096 | List.Cons (e, et) ->
1099 | List.Nil -> (fun _ _ -> assert false (* absurd case *))
1100 | List.Cons (r, rt) ->
1102 let f' = add_exprs fx et rt f in
1103 (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
1105 let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
1108 (** val stmt_inv_rect_Type4 :
1109 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1110 let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
1111 h_mk_stmt_inv __ __ __
1113 (** val stmt_inv_rect_Type5 :
1114 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1115 let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
1116 h_mk_stmt_inv __ __ __
1118 (** val stmt_inv_rect_Type3 :
1119 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1120 let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
1121 h_mk_stmt_inv __ __ __
1123 (** val stmt_inv_rect_Type2 :
1124 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1125 let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
1126 h_mk_stmt_inv __ __ __
1128 (** val stmt_inv_rect_Type1 :
1129 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1130 let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
1131 h_mk_stmt_inv __ __ __
1133 (** val stmt_inv_rect_Type0 :
1134 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1135 let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
1136 h_mk_stmt_inv __ __ __
1138 (** val stmt_inv_inv_rect_Type4 :
1139 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1140 let stmt_inv_inv_rect_Type4 x1 x2 h1 =
1141 let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __
1143 (** val stmt_inv_inv_rect_Type3 :
1144 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1145 let stmt_inv_inv_rect_Type3 x1 x2 h1 =
1146 let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __
1148 (** val stmt_inv_inv_rect_Type2 :
1149 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1150 let stmt_inv_inv_rect_Type2 x1 x2 h1 =
1151 let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __
1153 (** val stmt_inv_inv_rect_Type1 :
1154 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1155 let stmt_inv_inv_rect_Type1 x1 x2 h1 =
1156 let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __
1158 (** val stmt_inv_inv_rect_Type0 :
1159 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1160 let stmt_inv_inv_rect_Type0 x1 x2 h1 =
1161 let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __
1163 (** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
1164 let stmt_inv_discr a1 a2 =
1165 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1167 (** val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __ **)
1168 let stmt_inv_jmdiscr a1 a2 =
1169 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1171 (** val expr_is_cst_ident :
1172 AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
1173 let expr_is_cst_ident t = function
1174 | Cminor_syntax.Id (x, x0) -> Types.None
1175 | Cminor_syntax.Cst (x, c) ->
1177 | FrontEndOps.Ointconst (x0, x1, x2) -> Types.None
1178 | FrontEndOps.Oaddrsymbol (id, n) ->
1180 | Nat.O -> Types.Some id
1181 | Nat.S x0 -> Types.None)
1182 | FrontEndOps.Oaddrstack x0 -> Types.None)
1183 | Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
1184 | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
1185 | Cminor_syntax.Mem (x, x0) -> Types.None
1186 | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) -> Types.None
1187 | Cminor_syntax.Ecost (x, x0, x1) -> Types.None
1189 (** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1190 let option_jmdiscr x y =
1191 Logic.eq_rect_Type2 x
1193 | Types.None -> Obj.magic (fun _ dH -> dH)
1194 | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1196 (** val dPair_jmdiscr :
1197 ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
1198 let 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
1203 (** val add_return :
1204 fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
1205 partial_fn -> partial_fn Types.sig0 **)
1206 let add_return fx opt_e f =
1208 let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
1210 | Types.None -> (fun _ -> Types.pi1 f1)
1212 let { Types.dpi1 = ty; Types.dpi2 = e } = et in
1214 (match fx.fx_rettyp with
1215 | Types.None -> (fun _ -> assert false (* absurd case *))
1218 let r0 = Obj.magic r in
1219 let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
1220 (Types.pi1 f1).pf_result)) __
1222 (** val record_goto_label :
1223 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn **)
1224 let record_goto_label fx f l =
1225 { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
1226 f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1227 pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
1228 f.pf_gotos; pf_labels =
1229 (Identifiers.add PreIdentifiers.Label (Types.pi1 f.pf_labels) l
1230 (Types.pi1 f.pf_entry)); pf_entry = f.pf_entry; pf_exit = f.pf_exit }
1232 (** val add_goto_dummy :
1233 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
1234 let add_goto_dummy fx f dest =
1235 (let { Types.fst = l; Types.snd = g } =
1236 Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
1238 (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
1239 f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1240 pf_stacksize = f.pf_stacksize; pf_graph =
1241 (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
1242 (RTLabs_syntax.St_skip l)); pf_gotos =
1243 (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
1244 l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
1245 (Types.pi1 f.pf_exit) })) __
1248 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0 **)
1249 let rec add_stmt fx s f =
1251 | Cminor_syntax.St_skip -> (fun _ -> f)
1252 | Cminor_syntax.St_assign (t, x, e) ->
1254 let dst = lookup_reg fx.fx_env x t in
1255 Types.pi1 (add_expr fx t e f dst))
1256 | Cminor_syntax.St_store (t, e1, e2) ->
1258 let { Types.dpi1 = f0; Types.dpi2 = val_reg } = choose_reg fx t e2 f
1260 let { Types.dpi1 = f1; Types.dpi2 = addr_reg } =
1261 choose_reg fx AST.ASTptr e1 (Types.pi1 f0)
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)
1267 let f3 = add_expr fx AST.ASTptr e1 (Types.pi1 f2) (Types.pi1 addr_reg)
1269 Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
1270 | Cminor_syntax.St_call (return_opt_id, e, args) ->
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))) __
1279 let { Types.dpi1 = f0; Types.dpi2 = args_regs } =
1280 choose_regs fx args f
1283 match expr_is_cst_ident AST.ASTptr e with
1285 let { Types.dpi1 = f1; Types.dpi2 = fnr } =
1286 choose_reg fx AST.ASTptr e (Types.pi1 f0)
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))
1294 (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
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)
1299 Types.pi1 (add_exprs fx args (Types.pi1 args_regs) (Types.pi1 f1)))
1300 | Cminor_syntax.St_seq (s1, s2) ->
1302 let f2 = add_stmt fx s2 f in
1303 let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
1304 | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
1306 let l_next = f.pf_entry in
1307 let f2 = add_stmt fx s2 f in
1308 let l2 = (Types.pi1 f2).pf_entry in
1309 let f0 = change_entry fx (Types.pi1 f2) (Types.pi1 l_next) in
1310 let f1 = add_stmt fx s1 (Types.pi1 f0) in
1311 let { Types.dpi1 = f3; Types.dpi2 = r } =
1312 choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
1315 add_fresh_to_graph fx (fun l1 -> RTLabs_syntax.St_cond
1316 ((Types.pi1 r), l1, (Types.pi1 l2))) (Types.pi1 f3)
1319 (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
1320 | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
1321 | Cminor_syntax.St_label (l, s') ->
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') ->
1327 let f0 = add_stmt fx s' f in
1329 (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_cost (l, x))
1330 (Types.pi1 f0)))) __
1332 (** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
1333 let patch_gotos fx f =
1334 Identifiers.fold_inf PreIdentifiers.LabelTag
1335 (gm_map fx f.pf_graph f.pf_gotos) (fun l l' _ f' ->
1337 (fill_in_statement fx l (RTLabs_syntax.St_skip
1338 (Identifiers.lookup_present PreIdentifiers.Label
1339 (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f
1341 (** val c2ra_function :
1342 Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
1343 let c2ra_function f =
1344 let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
1345 let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
1346 let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
1347 (let { Types.fst = eta3108; Types.snd = reggen1 } =
1348 populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
1349 f.Cminor_syntax.f_params
1351 let { Types.fst = params; Types.snd = env1 } = eta3108 in
1353 (let { Types.fst = eta3107; Types.snd = reggen2 } =
1354 populate_env env1 reggen1 f.Cminor_syntax.f_vars
1356 let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
1358 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
1359 match f.Cminor_syntax.f_return with
1361 { Types.dpi1 = { Types.fst = locals0; Types.snd = reggen2 };
1362 Types.dpi2 = (Obj.magic __) }
1364 let { Types.fst = r; Types.snd = gen } =
1365 Identifiers.fresh PreIdentifiers.RegisterTag reggen2
1367 { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
1368 ty }, locals0)); Types.snd = gen }; Types.dpi2 = r }
1371 let locals = locals_reggen.Types.fst in
1372 let reggen = locals_reggen.Types.snd in
1373 let { Types.fst = l; Types.snd = labgen } =
1374 Identifiers.fresh PreIdentifiers.LabelTag labgen0
1376 let fixed0 = { fx_gotos =
1377 (Identifiers.set_of_list PreIdentifiers.Label
1378 (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
1379 fx_rettyp = f.Cminor_syntax.f_return }
1381 let emptyfn = { pf_labgen = labgen; pf_reggen = reggen; pf_params = params;
1382 pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
1383 f.Cminor_syntax.f_stacksize; pf_graph =
1384 (Identifiers.add PreIdentifiers.LabelTag
1385 (Identifiers.empty_map PreIdentifiers.LabelTag) l
1386 RTLabs_syntax.St_return); pf_gotos =
1387 (Identifiers.empty_map PreIdentifiers.LabelTag); pf_labels =
1388 (Identifiers.empty_map PreIdentifiers.Label); pf_entry = l; pf_exit = l }
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)
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 })) __)) __)) __
1405 (** val cminor_to_rtlabs :
1406 Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
1407 let cminor_to_rtlabs p =
1408 AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)