open Preamble

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Lists

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Identifiers

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open ErrorMessages

open Positive

open PreIdentifiers

open Errors

open Globalenvs

open CostLabel

open FrontEndOps

open Cminor_syntax

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

type env =
  (Registers.register, AST.typ) Types.prod Identifiers.identifier_map

(** val populate_env :
    env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list
    -> (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
    Identifiers.universe) Types.prod **)
let populate_env en gen =
  List.foldr (fun idt rsengen ->
    let { Types.fst = id; Types.snd = ty } = idt in
    let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in
    let { Types.fst = rs; Types.snd = en0 } = eta2881 in
    let { Types.fst = r; Types.snd = gen' } =
      Identifiers.fresh PreIdentifiers.RegisterTag gen0
    in
    { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
    ty }, rs)); Types.snd =
    (Identifiers.add PreIdentifiers.SymbolTag en0 id { Types.fst = r;
      Types.snd = ty }) }; Types.snd = gen' }) { Types.fst = { Types.fst =
    List.Nil; Types.snd = en }; Types.snd = gen }

(** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
let lookup_reg e id ty =
  (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst

type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
               fx_rettyp : AST.typ Types.option }

(** val fixed_rect_Type4 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type4 h_mk_fixed x_15483 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15483
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fixed_rect_Type5 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type5 h_mk_fixed x_15485 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15485
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fixed_rect_Type3 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type3 h_mk_fixed x_15487 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15487
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fixed_rect_Type2 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type2 h_mk_fixed x_15489 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15489
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fixed_rect_Type1 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type1 h_mk_fixed x_15491 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15491
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fixed_rect_Type0 :
    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    fixed -> 'a1 **)
let rec fixed_rect_Type0 h_mk_fixed x_15493 =
  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    x_15493
  in
  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0

(** val fx_gotos : fixed -> Identifiers.identifier_set **)
let rec fx_gotos xxx =
  xxx.fx_gotos

(** val fx_env : fixed -> env **)
let rec fx_env xxx =
  xxx.fx_env

(** val fx_rettyp : fixed -> AST.typ Types.option **)
let rec fx_rettyp xxx =
  xxx.fx_rettyp

(** val fixed_inv_rect_Type4 :
    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
    -> 'a1) -> 'a1 **)
let fixed_inv_rect_Type4 hterm h1 =
  let hcut = fixed_rect_Type4 h1 hterm in hcut __

(** val fixed_inv_rect_Type3 :
    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
    -> 'a1) -> 'a1 **)
let fixed_inv_rect_Type3 hterm h1 =
  let hcut = fixed_rect_Type3 h1 hterm in hcut __

(** val fixed_inv_rect_Type2 :
    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
    -> 'a1) -> 'a1 **)
let fixed_inv_rect_Type2 hterm h1 =
  let hcut = fixed_rect_Type2 h1 hterm in hcut __

(** val fixed_inv_rect_Type1 :
    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
    -> 'a1) -> 'a1 **)
let fixed_inv_rect_Type1 hterm h1 =
  let hcut = fixed_rect_Type1 h1 hterm in hcut __

(** val fixed_inv_rect_Type0 :
    fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
    -> 'a1) -> 'a1 **)
let fixed_inv_rect_Type0 hterm h1 =
  let hcut = fixed_rect_Type0 h1 hterm in hcut __

(** val fixed_discr : fixed -> fixed -> __ **)
let fixed_discr x y =
  Logic.eq_rect_Type2 x
    (let { fx_gotos = a0; fx_env = a1; fx_rettyp = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val fixed_jmdiscr : fixed -> fixed -> __ **)
let fixed_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { fx_gotos = a0; fx_env = a1; fx_rettyp = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

type resultok = __

type goto_map =
  PreIdentifiers.identifier Identifiers.identifier_map
  (* singleton inductive, whose constructor was mk_goto_map *)

(** val goto_map_rect_Type4 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15509 =
  let gm_map = x_15509 in h_mk_goto_map gm_map __ __

(** val goto_map_rect_Type5 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15511 =
  let gm_map = x_15511 in h_mk_goto_map gm_map __ __

(** val goto_map_rect_Type3 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15513 =
  let gm_map = x_15513 in h_mk_goto_map gm_map __ __

(** val goto_map_rect_Type2 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15515 =
  let gm_map = x_15515 in h_mk_goto_map gm_map __ __

(** val goto_map_rect_Type1 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15517 =
  let gm_map = x_15517 in h_mk_goto_map gm_map __ __

(** val goto_map_rect_Type0 :
    fixed -> RTLabs_syntax.statement Graphs.graph ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    -> goto_map -> 'a1 **)
let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15519 =
  let gm_map = x_15519 in h_mk_goto_map gm_map __ __

(** val gm_map :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map **)
let rec gm_map fx g xxx =
  let yyy = xxx in yyy

(** val goto_map_inv_rect_Type4 :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let goto_map_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = goto_map_rect_Type4 x1 x2 h1 hterm in hcut __

(** val goto_map_inv_rect_Type3 :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let goto_map_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = goto_map_rect_Type3 x1 x2 h1 hterm in hcut __

(** val goto_map_inv_rect_Type2 :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let goto_map_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = goto_map_rect_Type2 x1 x2 h1 hterm in hcut __

(** val goto_map_inv_rect_Type1 :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let goto_map_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = goto_map_rect_Type1 x1 x2 h1 hterm in hcut __

(** val goto_map_inv_rect_Type0 :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let goto_map_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = goto_map_rect_Type0 x1 x2 h1 hterm in hcut __

(** val goto_map_discr :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
    __ **)
let goto_map_discr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y

(** val goto_map_jmdiscr :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
    __ **)
let goto_map_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y

(** val dpi1__o__gm_map__o__inject :
    fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
    Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
    Types.sig0 **)
let dpi1__o__gm_map__o__inject x1 x2 x4 =
  gm_map x1 x2 x4.Types.dpi1

(** val eject__o__gm_map__o__inject :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
let eject__o__gm_map__o__inject x1 x2 x4 =
  gm_map x1 x2 (Types.pi1 x4)

(** val gm_map__o__inject :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
let gm_map__o__inject x1 x2 x3 =
  gm_map x1 x2 x3

(** val dpi1__o__gm_map :
    fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
    Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map **)
let dpi1__o__gm_map x0 x1 x3 =
  gm_map x0 x1 x3.Types.dpi1

(** val eject__o__gm_map :
    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
    PreIdentifiers.identifier Identifiers.identifier_map **)
let eject__o__gm_map x0 x1 x3 =
  gm_map x0 x1 (Types.pi1 x3)

type partial_fn = { pf_labgen : Identifiers.universe;
                    pf_reggen : Identifiers.universe;
                    pf_params : (Registers.register, AST.typ) Types.prod
                                List.list;
                    pf_locals : (Registers.register, AST.typ) Types.prod
                                List.list; pf_result : resultok;
                    pf_stacksize : Nat.nat;
                    pf_graph : RTLabs_syntax.statement Graphs.graph;
                    pf_gotos : goto_map;
                    pf_labels : PreIdentifiers.identifier
                                Identifiers.identifier_map Types.sig0;
                    pf_entry : Graphs.label Types.sig0;
                    pf_exit : Graphs.label Types.sig0 }

(** val partial_fn_rect_Type4 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15537 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15537
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val partial_fn_rect_Type5 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15539 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15539
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val partial_fn_rect_Type3 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15541 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15541
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val partial_fn_rect_Type2 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15543 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15543
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val partial_fn_rect_Type1 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15545 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15545
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val partial_fn_rect_Type0 :
    fixed -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    partial_fn -> 'a1 **)
let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15547 =
  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    x_15547
  in
  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __

(** val pf_labgen : fixed -> partial_fn -> Identifiers.universe **)
let rec pf_labgen fx xxx =
  xxx.pf_labgen

(** val pf_reggen : fixed -> partial_fn -> Identifiers.universe **)
let rec pf_reggen fx xxx =
  xxx.pf_reggen

(** val pf_params :
    fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
let rec pf_params fx xxx =
  xxx.pf_params

(** val pf_locals :
    fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
let rec pf_locals fx xxx =
  xxx.pf_locals

(** val pf_result : fixed -> partial_fn -> resultok **)
let rec pf_result fx xxx =
  xxx.pf_result

(** val pf_stacksize : fixed -> partial_fn -> Nat.nat **)
let rec pf_stacksize fx xxx =
  xxx.pf_stacksize

(** val pf_graph :
    fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph **)
let rec pf_graph fx xxx =
  xxx.pf_graph

(** val pf_gotos : fixed -> partial_fn -> goto_map **)
let rec pf_gotos fx xxx =
  xxx.pf_gotos

(** val pf_labels :
    fixed -> partial_fn -> PreIdentifiers.identifier
    Identifiers.identifier_map Types.sig0 **)
let rec pf_labels fx xxx =
  xxx.pf_labels

(** val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0 **)
let rec pf_entry fx xxx =
  xxx.pf_entry

(** val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0 **)
let rec pf_exit fx xxx =
  xxx.pf_exit

(** val partial_fn_inv_rect_Type4 :
    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
    'a1 **)
let partial_fn_inv_rect_Type4 x1 hterm h1 =
  let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __

(** val partial_fn_inv_rect_Type3 :
    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
    'a1 **)
let partial_fn_inv_rect_Type3 x1 hterm h1 =
  let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __

(** val partial_fn_inv_rect_Type2 :
    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
    'a1 **)
let partial_fn_inv_rect_Type2 x1 hterm h1 =
  let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __

(** val partial_fn_inv_rect_Type1 :
    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
    'a1 **)
let partial_fn_inv_rect_Type1 x1 hterm h1 =
  let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __

(** val partial_fn_inv_rect_Type0 :
    fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
    (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
    'a1 **)
let partial_fn_inv_rect_Type0 x1 hterm h1 =
  let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __

(** val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
let partial_fn_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let { pf_labgen = a0; pf_reggen = a10; pf_params = a2; pf_locals = a3;
       pf_result = a4; pf_stacksize = a6; pf_graph = a7; pf_gotos = a9;
       pf_labels = a100; pf_entry = a12; pf_exit = a13 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
    y

(** val fn_contains_rect_Type4 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type4 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_rect_Type5 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type5 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_rect_Type3 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type3 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_rect_Type2 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type2 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_rect_Type1 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type1 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_rect_Type0 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec fn_contains_rect_Type0 fx f1 f2 h_mk_fn_contains =
  h_mk_fn_contains __ __ __

(** val fn_contains_inv_rect_Type4 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let fn_contains_inv_rect_Type4 x1 x2 x3 h1 =
  let hcut = fn_contains_rect_Type4 x1 x2 x3 h1 in hcut __

(** val fn_contains_inv_rect_Type3 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let fn_contains_inv_rect_Type3 x1 x2 x3 h1 =
  let hcut = fn_contains_rect_Type3 x1 x2 x3 h1 in hcut __

(** val fn_contains_inv_rect_Type2 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let fn_contains_inv_rect_Type2 x1 x2 x3 h1 =
  let hcut = fn_contains_rect_Type2 x1 x2 x3 h1 in hcut __

(** val fn_contains_inv_rect_Type1 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let fn_contains_inv_rect_Type1 x1 x2 x3 h1 =
  let hcut = fn_contains_rect_Type1 x1 x2 x3 h1 in hcut __

(** val fn_contains_inv_rect_Type0 :
    fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let fn_contains_inv_rect_Type0 x1 x2 x3 h1 =
  let hcut = fn_contains_rect_Type0 x1 x2 x3 h1 in hcut __

(** val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __ **)
let fn_contains_discr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
let fn_contains_jmdiscr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val fill_in_statement :
    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
    partial_fn Types.sig0 **)
let fill_in_statement fx l s f =
  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    pf_stacksize = f.pf_stacksize; pf_graph =
    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
    (gm_map fx f.pf_graph f.pf_gotos); pf_labels = (Types.pi1 f.pf_labels);
    pf_entry = (Types.pi1 f.pf_entry); pf_exit = (Types.pi1 f.pf_exit) }

(** val add_to_graph :
    fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
    partial_fn Types.sig0 **)
let add_to_graph fx l s f =
  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    pf_stacksize = f.pf_stacksize; pf_graph =
    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
    (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
    pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) }

(** val change_entry :
    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
let change_entry fx f l =
  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
    f.pf_gotos; pf_labels = f.pf_labels; pf_entry = l; pf_exit = f.pf_exit }

(** val add_fresh_to_graph :
    fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
    partial_fn Types.sig0 **)
let add_fresh_to_graph fx s f =
  (let { Types.fst = l; Types.snd = g } =
     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
   in
  (fun _ ->
  let s1 = s (Types.pi1 f.pf_entry) in
  { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
  f.pf_stacksize; pf_graph =
  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
  (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
  pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __

(** val fresh_reg :
    fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
    Registers.register Types.sig0) Types.dPair **)
let fresh_reg fx f ty =
  let { Types.fst = r; Types.snd = g } =
    Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
  in
  let f' = { pf_labgen = f.pf_labgen; pf_reggen = g; pf_params = f.pf_params;
    pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty }, f.pf_locals));
    pf_result =
    ((match fx.fx_rettyp with
      | Types.None -> Obj.magic __
      | Types.Some t ->
        (fun clearme -> let r' = Obj.magic clearme in Obj.magic r'))
      f.pf_result); pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph;
    pf_gotos = f.pf_gotos; pf_labels = f.pf_labels; pf_entry = f.pf_entry;
    pf_exit = f.pf_exit }
  in
  { Types.dpi1 = f'; Types.dpi2 = r }

(** val choose_reg :
    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
    Types.sig0, Registers.register Types.sig0) Types.dPair **)
let choose_reg fx ty e f =
  (match e with
   | Cminor_syntax.Id (t, i) ->
     (fun _ -> { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) })
   | Cminor_syntax.Cst (x, x0) -> (fun _ -> fresh_reg fx f x)
   | Cminor_syntax.Op1 (x, x0, x1, x2) -> (fun _ -> fresh_reg fx f x0)
   | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) ->
     (fun _ -> fresh_reg fx f x1)
   | Cminor_syntax.Mem (x, x0) -> (fun _ -> fresh_reg fx f x)
   | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) ->
     (fun _ -> fresh_reg fx f x1)
   | Cminor_syntax.Ecost (x, x0, x1) -> (fun _ -> fresh_reg fx f x)) __

(** val foldr_all :
    ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
let rec foldr_all f b l =
  (match l with
   | List.Nil -> (fun _ -> b)
   | List.Cons (a, l0) -> (fun _ -> f a __ (foldr_all f b l0))) __

(** val foldr_all' :
    ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
let rec foldr_all' f b l =
  (match l with
   | List.Nil -> (fun _ -> b)
   | List.Cons (a, l0) -> (fun _ -> f a __ l0 (foldr_all' f b l0))) __

(** val eject' : ('a1, 'a2) Types.dPair -> 'a1 **)
let eject' x =
  x.Types.dpi1

(** val choose_regs :
    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
    partial_fn -> (partial_fn Types.sig0, Registers.register List.list
    Types.sig0) Types.dPair **)
let choose_regs fx es f =
  foldr_all' (fun e _ tl acc ->
    let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
    (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in
    (fun _ ->
    let { Types.dpi1 = f'; Types.dpi2 = r } =
      choose_reg fx t e0 (Types.pi1 f1)
    in
    { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r),
    (Types.pi1 rs))) })) __) { Types.dpi1 = f; Types.dpi2 = List.Nil } es

(** val add_stmt_inv_rect_Type4 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type4 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_rect_Type5 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type5 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_rect_Type3 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type3 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_rect_Type2 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type2 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_rect_Type1 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type1 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_rect_Type0 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    'a1) -> 'a1 **)
let rec add_stmt_inv_rect_Type0 fx s f f' h_mk_add_stmt_inv =
  h_mk_add_stmt_inv __ __

(** val add_stmt_inv_inv_rect_Type4 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    __ -> 'a1) -> 'a1 **)
let add_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
  let hcut = add_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __

(** val add_stmt_inv_inv_rect_Type3 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    __ -> 'a1) -> 'a1 **)
let add_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
  let hcut = add_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __

(** val add_stmt_inv_inv_rect_Type2 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    __ -> 'a1) -> 'a1 **)
let add_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
  let hcut = add_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __

(** val add_stmt_inv_inv_rect_Type1 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    __ -> 'a1) -> 'a1 **)
let add_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
  let hcut = add_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __

(** val add_stmt_inv_inv_rect_Type0 :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
    __ -> 'a1) -> 'a1 **)
let add_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
  let hcut = add_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __

(** val add_stmt_inv_discr :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
let add_stmt_inv_discr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __

(** val add_stmt_inv_jmdiscr :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __ **)
let add_stmt_inv_jmdiscr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __

type fn_con_because =
| Fn_con_eq of partial_fn
| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
   * partial_fn Types.sig0

(** val fn_con_because_rect_Type4 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15624 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_rect_Type5 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15631 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_rect_Type3 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15638 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_rect_Type2 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15645 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_rect_Type1 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15652 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_rect_Type0 :
    fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    fn_con_because -> 'a1 **)
let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15659 = function
| Fn_con_eq f -> h_fn_con_eq f
| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
| Fn_con_addinv (f1, f2, s, f3) -> h_fn_con_addinv f1 f2 __ s f3

(** val fn_con_because_inv_rect_Type4 :
    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
let fn_con_because_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
  let hcut = fn_con_because_rect_Type4 x1 h1 h2 h3 x2 hterm in hcut __ __

(** val fn_con_because_inv_rect_Type3 :
    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
let fn_con_because_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
  let hcut = fn_con_because_rect_Type3 x1 h1 h2 h3 x2 hterm in hcut __ __

(** val fn_con_because_inv_rect_Type2 :
    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
let fn_con_because_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
  let hcut = fn_con_because_rect_Type2 x1 h1 h2 h3 x2 hterm in hcut __ __

(** val fn_con_because_inv_rect_Type1 :
    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
let fn_con_because_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
  let hcut = fn_con_because_rect_Type1 x1 h1 h2 h3 x2 hterm in hcut __ __

(** val fn_con_because_inv_rect_Type0 :
    fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
    -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
    -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
    partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
let fn_con_because_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
  let hcut = fn_con_because_rect_Type0 x1 h1 h2 h3 x2 hterm in hcut __ __

(** val fn_con_because_discr :
    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
let fn_con_because_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Fn_con_addinv (a0, a10, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y

(** val fn_con_because_jmdiscr :
    fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
let fn_con_because_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
     | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Fn_con_addinv (a0, a10, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y

(** val fn_con_because_left :
    fixed -> partial_fn -> fn_con_because -> partial_fn **)
let rec fn_con_because_left fx f0 = function
| Fn_con_eq f -> f
| Fn_con_sig (f, x, x1) -> f
| Fn_con_addinv (f, x, x1, x2) -> f

(** val add_expr :
    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
    Registers.register Types.sig0 -> partial_fn Types.sig0 **)
let rec add_expr fx ty e f dst =
  (match e with
   | Cminor_syntax.Id (t, i) ->
     (fun _ dst0 ->
       let r = lookup_reg fx.fx_env i t in
       (match Registers.register_eq r (Types.pi1 dst0) with
        | Types.Inl _ -> f
        | Types.Inr _ ->
          Types.pi1
            (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t, t,
              (FrontEndOps.Oid t), (Types.pi1 dst0), r, x)) f)))
   | Cminor_syntax.Cst (x, c) ->
     (fun _ dst0 ->
       Types.pi1
         (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
           (Types.pi1 dst0), c, x0)) f))
   | Cminor_syntax.Op1 (t, t', op, e') ->
     (fun _ dst0 ->
       let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
       let f1 =
         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
           (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
       in
       let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
   | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
     (fun _ dst0 ->
       let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
       let { Types.dpi1 = f1; Types.dpi2 = r2 } =
         choose_reg fx x0 e2 (Types.pi1 f0)
       in
       let f2 =
         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
           op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
           (Types.pi1 f1)
       in
       let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r2) in
       let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r1) in
       Types.pi1 f4)
   | Cminor_syntax.Mem (t, e') ->
     (fun _ dst0 ->
       let { Types.dpi1 = f0; Types.dpi2 = r } =
         choose_reg fx AST.ASTptr e' f
       in
       let f1 =
         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_load (t,
           (Types.pi1 r), (Types.pi1 dst0), x)) (Types.pi1 f0)
       in
       let f2 = add_expr fx AST.ASTptr e' (Types.pi1 f1) (Types.pi1 r) in
       Types.pi1 f2)
   | Cminor_syntax.Cond (x, x0, x1, e', e1, e2) ->
     (fun _ dst0 ->
       let resume_at = f.pf_entry in
       let f0 = add_expr fx x1 e2 f dst0 in
       let lfalse = (Types.pi1 f0).pf_entry in
       let f1 =
         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_skip
           (Types.pi1 resume_at)) (Types.pi1 f0)
       in
       let f2 = add_expr fx x1 e1 (Types.pi1 f1) (Types.pi1 dst0) in
       let { Types.dpi1 = f3; Types.dpi2 = r } =
         choose_reg fx (AST.ASTint (x, x0)) e' (Types.pi1 f2)
       in
       let f4 =
         add_fresh_to_graph fx (fun ltrue -> RTLabs_syntax.St_cond
           ((Types.pi1 r), ltrue, (Types.pi1 lfalse))) (Types.pi1 f3)
       in
       let f5 =
         add_expr fx (AST.ASTint (x, x0)) e' (Types.pi1 f4) (Types.pi1 r)
       in
       Types.pi1 f5)
   | Cminor_syntax.Ecost (x, l, e') ->
     (fun _ dst0 ->
       let f0 = add_expr fx x e' f dst0 in
       let f1 =
         add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_cost (l, x0))
           (Types.pi1 f0)
       in
       Types.pi1 f1)) __ dst

(** val add_exprs :
    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
    Registers.register List.list -> partial_fn -> partial_fn Types.sig0 **)
let rec add_exprs fx es dsts f =
  (match es with
   | List.Nil ->
     (fun _ _ ->
       match dsts with
       | List.Nil -> (fun _ -> f)
       | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
   | List.Cons (e, et) ->
     (fun _ ->
       match dsts with
       | List.Nil -> (fun _ _ -> assert false (* absurd case *))
       | List.Cons (r, rt) ->
         (fun _ _ ->
           let f' = add_exprs fx et rt f in
           (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
           (fun _ _ ->
           let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
             __))) __ __ __

(** val stmt_inv_rect_Type4 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_rect_Type5 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_rect_Type3 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_rect_Type2 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_rect_Type1 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_rect_Type0 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
  h_mk_stmt_inv __ __ __

(** val stmt_inv_inv_rect_Type4 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let stmt_inv_inv_rect_Type4 x1 x2 h1 =
  let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __

(** val stmt_inv_inv_rect_Type3 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let stmt_inv_inv_rect_Type3 x1 x2 h1 =
  let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __

(** val stmt_inv_inv_rect_Type2 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let stmt_inv_inv_rect_Type2 x1 x2 h1 =
  let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __

(** val stmt_inv_inv_rect_Type1 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let stmt_inv_inv_rect_Type1 x1 x2 h1 =
  let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __

(** val stmt_inv_inv_rect_Type0 :
    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let stmt_inv_inv_rect_Type0 x1 x2 h1 =
  let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __

(** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
let stmt_inv_discr a1 a2 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __ **)
let stmt_inv_jmdiscr a1 a2 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val expr_is_cst_ident :
    AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
let expr_is_cst_ident t = function
| Cminor_syntax.Id (x, x0) -> Types.None
| Cminor_syntax.Cst (x, c) ->
  (match c with
   | FrontEndOps.Ointconst (x0, x1, x2) -> Types.None
   | FrontEndOps.Oaddrsymbol (id, n) ->
     (match n with
      | Nat.O -> Types.Some id
      | Nat.S x0 -> Types.None)
   | FrontEndOps.Oaddrstack x0 -> Types.None)
| Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
| Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
| Cminor_syntax.Mem (x, x0) -> Types.None
| Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) -> Types.None
| Cminor_syntax.Ecost (x, x0, x1) -> Types.None

(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
let option_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Types.None -> Obj.magic (fun _ dH -> dH)
     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val dPair_jmdiscr :
    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
let dPair_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val add_return :
    fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
    partial_fn -> partial_fn Types.sig0 **)
let add_return fx opt_e f =
  let f0 = f in
  let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
  (match opt_e with
   | Types.None -> (fun _ -> Types.pi1 f1)
   | Types.Some et ->
     let { Types.dpi1 = ty; Types.dpi2 = e } = et in
     (fun _ ->
     (match fx.fx_rettyp with
      | Types.None -> (fun _ -> assert false (* absurd case *))
      | Types.Some t ->
        (fun _ r ->
          let r0 = Obj.magic r in
          let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
       (Types.pi1 f1).pf_result)) __

(** val record_goto_label :
    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn **)
let record_goto_label fx f l =
  { pf_labgen = f.pf_labgen; pf_reggen = f.pf_reggen; pf_params =
    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
    f.pf_gotos; pf_labels =
    (Identifiers.add PreIdentifiers.Label (Types.pi1 f.pf_labels) l
      (Types.pi1 f.pf_entry)); pf_entry = f.pf_entry; pf_exit = f.pf_exit }

(** val add_goto_dummy :
    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
let add_goto_dummy fx f dest =
  (let { Types.fst = l; Types.snd = g } =
     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
   in
  (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
  pf_stacksize = f.pf_stacksize; pf_graph =
  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
    (RTLabs_syntax.St_skip l)); pf_gotos =
  (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
    l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
  (Types.pi1 f.pf_exit) })) __

(** val add_stmt :
    fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0 **)
let rec add_stmt fx s f =
  (match s with
   | Cminor_syntax.St_skip -> (fun _ -> f)
   | Cminor_syntax.St_assign (t, x, e) ->
     (fun _ ->
       let dst = lookup_reg fx.fx_env x t in
       Types.pi1 (add_expr fx t e f dst))
   | Cminor_syntax.St_store (t, e1, e2) ->
     (fun _ ->
       let { Types.dpi1 = f0; Types.dpi2 = val_reg } = choose_reg fx t e2 f
       in
       let { Types.dpi1 = f1; Types.dpi2 = addr_reg } =
         choose_reg fx AST.ASTptr e1 (Types.pi1 f0)
       in
       let f2 =
         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_store (t,
           (Types.pi1 addr_reg), (Types.pi1 val_reg), x)) (Types.pi1 f1)
       in
       let f3 = add_expr fx AST.ASTptr e1 (Types.pi1 f2) (Types.pi1 addr_reg)
       in
       Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
   | Cminor_syntax.St_call (return_opt_id, e, args) ->
     (fun _ ->
       let return_opt_reg =
         (match return_opt_id with
          | Types.None -> (fun _ -> Types.None)
          | Types.Some idty ->
            (fun _ -> Types.Some
              (lookup_reg fx.fx_env idty.Types.fst idty.Types.snd))) __
       in
       let { Types.dpi1 = f0; Types.dpi2 = args_regs } =
         choose_regs fx args f
       in
       let f1 =
         match expr_is_cst_ident AST.ASTptr e with
         | Types.None ->
           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
             choose_reg fx AST.ASTptr e (Types.pi1 f0)
           in
           let f2 =
             add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_ptr
               ((Types.pi1 fnr), (Types.pi1 args_regs), return_opt_reg, x))
               (Types.pi1 f1)
           in
           Types.pi1
             (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
         | Types.Some id ->
           add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_id (id,
             (Types.pi1 args_regs), return_opt_reg, x)) (Types.pi1 f0)
       in
       Types.pi1 (add_exprs fx args (Types.pi1 args_regs) (Types.pi1 f1)))
   | Cminor_syntax.St_seq (s1, s2) ->
     (fun _ ->
       let f2 = add_stmt fx s2 f in
       let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
   | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
     (fun _ ->
       let l_next = f.pf_entry in
       let f2 = add_stmt fx s2 f in
       let l2 = (Types.pi1 f2).pf_entry in
       let f0 = change_entry fx (Types.pi1 f2) (Types.pi1 l_next) in
       let f1 = add_stmt fx s1 (Types.pi1 f0) in
       let { Types.dpi1 = f3; Types.dpi2 = r } =
         choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
       in
       let f4 =
         add_fresh_to_graph fx (fun l1 -> RTLabs_syntax.St_cond
           ((Types.pi1 r), l1, (Types.pi1 l2))) (Types.pi1 f3)
       in
       Types.pi1
         (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
   | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
   | Cminor_syntax.St_label (l, s') ->
     (fun _ ->
       let f0 = add_stmt fx s' f in record_goto_label fx (Types.pi1 f0) l)
   | Cminor_syntax.St_goto l -> (fun _ -> Types.pi1 (add_goto_dummy fx f l))
   | Cminor_syntax.St_cost (l, s') ->
     (fun _ ->
       let f0 = add_stmt fx s' f in
       Types.pi1
         (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_cost (l, x))
           (Types.pi1 f0)))) __

(** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
let patch_gotos fx f =
  Identifiers.fold_inf PreIdentifiers.LabelTag
    (gm_map fx f.pf_graph f.pf_gotos) (fun l l' _ f' ->
    Types.pi1
      (fill_in_statement fx l (RTLabs_syntax.St_skip
        (Identifiers.lookup_present PreIdentifiers.Label
          (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f

(** val c2ra_function :
    Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
let c2ra_function f =
  let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
  (let { Types.fst = eta3108; Types.snd = reggen1 } =
     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
       f.Cminor_syntax.f_params
   in
  let { Types.fst = params; Types.snd = env1 } = eta3108 in
  (fun _ ->
  (let { Types.fst = eta3107; Types.snd = reggen2 } =
     populate_env env1 reggen1 f.Cminor_syntax.f_vars
   in
  let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
  (fun _ ->
  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
     match f.Cminor_syntax.f_return with
     | Types.None ->
       { Types.dpi1 = { Types.fst = locals0; Types.snd = reggen2 };
         Types.dpi2 = (Obj.magic __) }
     | Types.Some ty ->
       let { Types.fst = r; Types.snd = gen } =
         Identifiers.fresh PreIdentifiers.RegisterTag reggen2
       in
       { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
       ty }, locals0)); Types.snd = gen }; Types.dpi2 = r }
   in
  (fun _ ->
  let locals = locals_reggen.Types.fst in
  let reggen = locals_reggen.Types.snd in
  let { Types.fst = l; Types.snd = labgen } =
    Identifiers.fresh PreIdentifiers.LabelTag labgen0
  in
  let fixed0 = { fx_gotos =
    (Identifiers.set_of_list PreIdentifiers.Label
      (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
    fx_rettyp = f.Cminor_syntax.f_return }
  in
  let emptyfn = { pf_labgen = labgen; pf_reggen = reggen; pf_params = params;
    pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
    f.Cminor_syntax.f_stacksize; pf_graph =
    (Identifiers.add PreIdentifiers.LabelTag
      (Identifiers.empty_map PreIdentifiers.LabelTag) l
      RTLabs_syntax.St_return); pf_gotos =
    (Identifiers.empty_map PreIdentifiers.LabelTag); pf_labels =
    (Identifiers.empty_map PreIdentifiers.Label); pf_entry = l; pf_exit = l }
  in
  let f0 = add_stmt fixed0 f.Cminor_syntax.f_body emptyfn in
  let f1 = patch_gotos fixed0 (Types.pi1 f0) in
  { RTLabs_syntax.f_labgen = (Types.pi1 f1).pf_labgen;
  RTLabs_syntax.f_reggen = (Types.pi1 f1).pf_reggen; RTLabs_syntax.f_result =
  ((match fixed0.fx_rettyp with
    | Types.None -> Obj.magic (fun _ -> Types.None)
    | Types.Some t ->
      (fun r -> Types.Some { Types.fst = (Types.pi1 (Obj.magic r));
        Types.snd = t })) (Types.pi1 f1).pf_result); RTLabs_syntax.f_params =
  (Types.pi1 f1).pf_params; RTLabs_syntax.f_locals =
  (Types.pi1 f1).pf_locals; RTLabs_syntax.f_stacksize =
  (Types.pi1 f1).pf_stacksize; RTLabs_syntax.f_graph =
  (Types.pi1 f1).pf_graph; RTLabs_syntax.f_entry = (Types.pi1 f1).pf_entry;
  RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __

(** val cminor_to_rtlabs :
    Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
let cminor_to_rtlabs p =
  AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)