extracted/toRTLabs.ml

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Div_and_mod
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Util
  16
  17 open Bool
  18
  19 open Relations
  20
  21 open Nat
  22
  23 open Hints_declaration
  24
  25 open Core_notation
  26
  27 open Pts
  28
  29 open Logic
  30
  31 open Types
  32
  33 open List
  34
  35 open Lists
  36
  37 open Extra_bool
  38
  39 open Coqlib
  40
  41 open Values
  42
  43 open FrontEndVal
  44
  45 open Hide
  46
  47 open ByteValues
  48
  49 open Division
  50
  51 open Z
  52
  53 open BitVectorZ
  54
  55 open Pointers
  56
  57 open GenMem
  58
  59 open FrontEndMem
  60
  61 open Proper
  62
  63 open PositiveMap
  64
  65 open Deqsets
  66
  67 open Extralib
  68
  69 open Identifiers
  70
  71 open Exp
  72
  73 open Arithmetic
  74
  75 open Vector
  76
  77 open FoldStuff
  78
  79 open BitVector
  80
  81 open Extranat
  82
  83 open Integers
  84
  85 open AST
  86
  87 open ErrorMessages
  88
  89 open Positive
  90
  91 open PreIdentifiers
  92
  93 open Errors
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open FrontEndOps
 100
 101 open Cminor_syntax
 102
 103 open BitVectorTrie
 104
 105 open Graphs
 106
 107 open Order
 108
 109 open Registers
 110
 111 open RTLabs_syntax
 112
 113 type env =
 114   (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
 115
 116 (** val populate_env :
 117     env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list
 118     -> (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
 119     Identifiers.universe) Types.prod **)
 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
 127     in
 128     { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
 129     ty }, rs)); Types.snd =
 130     (Identifiers.add PreIdentifiers.SymbolTag en0 id { Types.fst = r;
 131       Types.snd = ty }) }; Types.snd = gen' }) { Types.fst = { Types.fst =
 132     List.Nil; Types.snd = en }; Types.snd = gen }
 133
 134 (** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
 135 let lookup_reg e id ty =
 136   (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst
 137
 138 type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
 139                fx_rettyp : AST.typ Types.option }
 140
 141 (** val fixed_rect_Type4 :
 142     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 143     fixed -> 'a1 **)
 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 } =
 146     x_15483
 147   in
 148   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 149
 150 (** val fixed_rect_Type5 :
 151     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 152     fixed -> 'a1 **)
 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 } =
 155     x_15485
 156   in
 157   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 158
 159 (** val fixed_rect_Type3 :
 160     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 161     fixed -> 'a1 **)
 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 } =
 164     x_15487
 165   in
 166   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 167
 168 (** val fixed_rect_Type2 :
 169     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 170     fixed -> 'a1 **)
 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 } =
 173     x_15489
 174   in
 175   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 176
 177 (** val fixed_rect_Type1 :
 178     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 179     fixed -> 'a1 **)
 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 } =
 182     x_15491
 183   in
 184   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 185
 186 (** val fixed_rect_Type0 :
 187     (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
 188     fixed -> 'a1 **)
 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 } =
 191     x_15493
 192   in
 193   h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
 194
 195 (** val fx_gotos : fixed -> Identifiers.identifier_set **)
 196 let rec fx_gotos xxx =
 197   xxx.fx_gotos
 198
 199 (** val fx_env : fixed -> env **)
 200 let rec fx_env xxx =
 201   xxx.fx_env
 202
 203 (** val fx_rettyp : fixed -> AST.typ Types.option **)
 204 let rec fx_rettyp xxx =
 205   xxx.fx_rettyp
 206
 207 (** val fixed_inv_rect_Type4 :
 208     fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 209     -> 'a1) -> 'a1 **)
 210 let fixed_inv_rect_Type4 hterm h1 =
 211   let hcut = fixed_rect_Type4 h1 hterm in hcut __
 212
 213 (** val fixed_inv_rect_Type3 :
 214     fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 215     -> 'a1) -> 'a1 **)
 216 let fixed_inv_rect_Type3 hterm h1 =
 217   let hcut = fixed_rect_Type3 h1 hterm in hcut __
 218
 219 (** val fixed_inv_rect_Type2 :
 220     fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 221     -> 'a1) -> 'a1 **)
 222 let fixed_inv_rect_Type2 hterm h1 =
 223   let hcut = fixed_rect_Type2 h1 hterm in hcut __
 224
 225 (** val fixed_inv_rect_Type1 :
 226     fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 227     -> 'a1) -> 'a1 **)
 228 let fixed_inv_rect_Type1 hterm h1 =
 229   let hcut = fixed_rect_Type1 h1 hterm in hcut __
 230
 231 (** val fixed_inv_rect_Type0 :
 232     fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 233     -> 'a1) -> 'a1 **)
 234 let fixed_inv_rect_Type0 hterm h1 =
 235   let hcut = fixed_rect_Type0 h1 hterm in hcut __
 236
 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
 242
 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
 248
 249 type resultok = __
 250
 251 type goto_map =
 252   PreIdentifiers.identifier Identifiers.identifier_map
 253   (* singleton inductive, whose constructor was mk_goto_map *)
 254
 255 (** val goto_map_rect_Type4 :
 256     fixed -> RTLabs_syntax.statement Graphs.graph ->
 257     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 258     -> goto_map -> 'a1 **)
 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 __ __
 261
 262 (** val goto_map_rect_Type5 :
 263     fixed -> RTLabs_syntax.statement Graphs.graph ->
 264     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 265     -> goto_map -> 'a1 **)
 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 __ __
 268
 269 (** val goto_map_rect_Type3 :
 270     fixed -> RTLabs_syntax.statement Graphs.graph ->
 271     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 272     -> goto_map -> 'a1 **)
 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 __ __
 275
 276 (** val goto_map_rect_Type2 :
 277     fixed -> RTLabs_syntax.statement Graphs.graph ->
 278     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 279     -> goto_map -> 'a1 **)
 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 __ __
 282
 283 (** val goto_map_rect_Type1 :
 284     fixed -> RTLabs_syntax.statement Graphs.graph ->
 285     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 286     -> goto_map -> 'a1 **)
 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 __ __
 289
 290 (** val goto_map_rect_Type0 :
 291     fixed -> RTLabs_syntax.statement Graphs.graph ->
 292     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
 293     -> goto_map -> 'a1 **)
 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 __ __
 296
 297 (** val 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 =
 301   let yyy = xxx in yyy
 302
 303 (** val goto_map_inv_rect_Type4 :
 304     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 305     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
 306     -> 'a1) -> 'a1 **)
 307 let goto_map_inv_rect_Type4 x1 x2 hterm h1 =
 308   let hcut = goto_map_rect_Type4 x1 x2 h1 hterm in hcut __
 309
 310 (** val goto_map_inv_rect_Type3 :
 311     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 312     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
 313     -> 'a1) -> 'a1 **)
 314 let goto_map_inv_rect_Type3 x1 x2 hterm h1 =
 315   let hcut = goto_map_rect_Type3 x1 x2 h1 hterm in hcut __
 316
 317 (** val goto_map_inv_rect_Type2 :
 318     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 319     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
 320     -> 'a1) -> 'a1 **)
 321 let goto_map_inv_rect_Type2 x1 x2 hterm h1 =
 322   let hcut = goto_map_rect_Type2 x1 x2 h1 hterm in hcut __
 323
 324 (** val goto_map_inv_rect_Type1 :
 325     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 326     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
 327     -> 'a1) -> 'a1 **)
 328 let goto_map_inv_rect_Type1 x1 x2 hterm h1 =
 329   let hcut = goto_map_rect_Type1 x1 x2 h1 hterm in hcut __
 330
 331 (** val goto_map_inv_rect_Type0 :
 332     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 333     (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __
 334     -> 'a1) -> 'a1 **)
 335 let goto_map_inv_rect_Type0 x1 x2 hterm h1 =
 336   let hcut = goto_map_rect_Type0 x1 x2 h1 hterm in hcut __
 337
 338 (** val goto_map_discr :
 339     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
 340     __ **)
 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
 343
 344 (** val goto_map_jmdiscr :
 345     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map ->
 346     __ **)
 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
 349
 350 (** val dpi1__o__gm_map__o__inject :
 351     fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
 352     Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
 353     Types.sig0 **)
 354 let dpi1__o__gm_map__o__inject x1 x2 x4 =
 355   gm_map x1 x2 x4.Types.dpi1
 356
 357 (** val eject__o__gm_map__o__inject :
 358     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
 359     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
 360 let eject__o__gm_map__o__inject x1 x2 x4 =
 361   gm_map x1 x2 (Types.pi1 x4)
 362
 363 (** val gm_map__o__inject :
 364     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 365     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 **)
 366 let gm_map__o__inject x1 x2 x3 =
 367   gm_map x1 x2 x3
 368
 369 (** val dpi1__o__gm_map :
 370     fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
 371     Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map **)
 372 let dpi1__o__gm_map x0 x1 x3 =
 373   gm_map x0 x1 x3.Types.dpi1
 374
 375 (** val eject__o__gm_map :
 376     fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
 377     PreIdentifiers.identifier Identifiers.identifier_map **)
 378 let eject__o__gm_map x0 x1 x3 =
 379   gm_map x0 x1 (Types.pi1 x3)
 380
 381 type partial_fn = { pf_labgen : Identifiers.universe;
 382                     pf_reggen : Identifiers.universe;
 383                     pf_params : (Registers.register, AST.typ) Types.prod
 384                                 List.list;
 385                     pf_locals : (Registers.register, AST.typ) Types.prod
 386                                 List.list; pf_result : resultok;
 387                     pf_stacksize : Nat.nat;
 388                     pf_graph : RTLabs_syntax.statement Graphs.graph;
 389                     pf_gotos : goto_map;
 390                     pf_labels : PreIdentifiers.identifier
 391                                 Identifiers.identifier_map Types.sig0;
 392                     pf_entry : Graphs.label Types.sig0;
 393                     pf_exit : Graphs.label Types.sig0 }
 394
 395 (** val partial_fn_rect_Type4 :
 396     fixed -> (Identifiers.universe -> Identifiers.universe ->
 397     (Registers.register, AST.typ) Types.prod List.list ->
 398     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 399     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 400     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 401     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 402     partial_fn -> 'a1 **)
 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 } =
 408     x_15537
 409   in
 410   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 411     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 412
 413 (** val partial_fn_rect_Type5 :
 414     fixed -> (Identifiers.universe -> Identifiers.universe ->
 415     (Registers.register, AST.typ) Types.prod List.list ->
 416     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 417     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 418     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 419     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 420     partial_fn -> 'a1 **)
 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 } =
 426     x_15539
 427   in
 428   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 429     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 430
 431 (** val partial_fn_rect_Type3 :
 432     fixed -> (Identifiers.universe -> Identifiers.universe ->
 433     (Registers.register, AST.typ) Types.prod List.list ->
 434     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 435     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 436     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 437     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 438     partial_fn -> 'a1 **)
 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 } =
 444     x_15541
 445   in
 446   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 447     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 448
 449 (** val partial_fn_rect_Type2 :
 450     fixed -> (Identifiers.universe -> Identifiers.universe ->
 451     (Registers.register, AST.typ) Types.prod List.list ->
 452     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 453     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 454     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 455     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 456     partial_fn -> 'a1 **)
 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 } =
 462     x_15543
 463   in
 464   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 465     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 466
 467 (** val partial_fn_rect_Type1 :
 468     fixed -> (Identifiers.universe -> Identifiers.universe ->
 469     (Registers.register, AST.typ) Types.prod List.list ->
 470     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 471     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 472     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 473     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 474     partial_fn -> 'a1 **)
 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 } =
 480     x_15545
 481   in
 482   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 483     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 484
 485 (** val partial_fn_rect_Type0 :
 486     fixed -> (Identifiers.universe -> Identifiers.universe ->
 487     (Registers.register, AST.typ) Types.prod List.list ->
 488     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 489     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 490     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 491     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 492     partial_fn -> 'a1 **)
 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 } =
 498     x_15547
 499   in
 500   h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
 501     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
 502
 503 (** val pf_labgen : fixed -> partial_fn -> Identifiers.universe **)
 504 let rec pf_labgen fx xxx =
 505   xxx.pf_labgen
 506
 507 (** val pf_reggen : fixed -> partial_fn -> Identifiers.universe **)
 508 let rec pf_reggen fx xxx =
 509   xxx.pf_reggen
 510
 511 (** val pf_params :
 512     fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
 513 let rec pf_params fx xxx =
 514   xxx.pf_params
 515
 516 (** val pf_locals :
 517     fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list **)
 518 let rec pf_locals fx xxx =
 519   xxx.pf_locals
 520
 521 (** val pf_result : fixed -> partial_fn -> resultok **)
 522 let rec pf_result fx xxx =
 523   xxx.pf_result
 524
 525 (** val pf_stacksize : fixed -> partial_fn -> Nat.nat **)
 526 let rec pf_stacksize fx xxx =
 527   xxx.pf_stacksize
 528
 529 (** val pf_graph :
 530     fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph **)
 531 let rec pf_graph fx xxx =
 532   xxx.pf_graph
 533
 534 (** val pf_gotos : fixed -> partial_fn -> goto_map **)
 535 let rec pf_gotos fx xxx =
 536   xxx.pf_gotos
 537
 538 (** val pf_labels :
 539     fixed -> partial_fn -> PreIdentifiers.identifier
 540     Identifiers.identifier_map Types.sig0 **)
 541 let rec pf_labels fx xxx =
 542   xxx.pf_labels
 543
 544 (** val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0 **)
 545 let rec pf_entry fx xxx =
 546   xxx.pf_entry
 547
 548 (** val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0 **)
 549 let rec pf_exit fx xxx =
 550   xxx.pf_exit
 551
 552 (** val partial_fn_inv_rect_Type4 :
 553     fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 554     (Registers.register, AST.typ) Types.prod List.list ->
 555     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 556     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 557     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 558     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 559     'a1 **)
 560 let partial_fn_inv_rect_Type4 x1 hterm h1 =
 561   let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __
 562
 563 (** val partial_fn_inv_rect_Type3 :
 564     fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 565     (Registers.register, AST.typ) Types.prod List.list ->
 566     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 567     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 568     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 569     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 570     'a1 **)
 571 let partial_fn_inv_rect_Type3 x1 hterm h1 =
 572   let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __
 573
 574 (** val partial_fn_inv_rect_Type2 :
 575     fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 576     (Registers.register, AST.typ) Types.prod List.list ->
 577     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 578     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 579     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 580     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 581     'a1 **)
 582 let partial_fn_inv_rect_Type2 x1 hterm h1 =
 583   let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __
 584
 585 (** val partial_fn_inv_rect_Type1 :
 586     fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 587     (Registers.register, AST.typ) Types.prod List.list ->
 588     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 589     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 590     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 591     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 592     'a1 **)
 593 let partial_fn_inv_rect_Type1 x1 hterm h1 =
 594   let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __
 595
 596 (** val partial_fn_inv_rect_Type0 :
 597     fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 598     (Registers.register, AST.typ) Types.prod List.list ->
 599     (Registers.register, AST.typ) Types.prod List.list -> resultok -> __ ->
 600     Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 601     PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 602     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 603     'a1 **)
 604 let partial_fn_inv_rect_Type0 x1 hterm h1 =
 605   let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __
 606
 607 (** val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
 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
 613      in
 614     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
 615     y
 616
 617 (** val fn_contains_rect_Type4 :
 618     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 619 let rec fn_contains_rect_Type4 fx f1 f2 h_mk_fn_contains =
 620   h_mk_fn_contains __ __ __
 621
 622 (** val fn_contains_rect_Type5 :
 623     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 624 let rec fn_contains_rect_Type5 fx f1 f2 h_mk_fn_contains =
 625   h_mk_fn_contains __ __ __
 626
 627 (** val fn_contains_rect_Type3 :
 628     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 629 let rec fn_contains_rect_Type3 fx f1 f2 h_mk_fn_contains =
 630   h_mk_fn_contains __ __ __
 631
 632 (** val fn_contains_rect_Type2 :
 633     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 634 let rec fn_contains_rect_Type2 fx f1 f2 h_mk_fn_contains =
 635   h_mk_fn_contains __ __ __
 636
 637 (** val fn_contains_rect_Type1 :
 638     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 639 let rec fn_contains_rect_Type1 fx f1 f2 h_mk_fn_contains =
 640   h_mk_fn_contains __ __ __
 641
 642 (** val fn_contains_rect_Type0 :
 643     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 644 let rec fn_contains_rect_Type0 fx f1 f2 h_mk_fn_contains =
 645   h_mk_fn_contains __ __ __
 646
 647 (** val fn_contains_inv_rect_Type4 :
 648     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 649 let fn_contains_inv_rect_Type4 x1 x2 x3 h1 =
 650   let hcut = fn_contains_rect_Type4 x1 x2 x3 h1 in hcut __
 651
 652 (** val fn_contains_inv_rect_Type3 :
 653     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 654 let fn_contains_inv_rect_Type3 x1 x2 x3 h1 =
 655   let hcut = fn_contains_rect_Type3 x1 x2 x3 h1 in hcut __
 656
 657 (** val fn_contains_inv_rect_Type2 :
 658     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 659 let fn_contains_inv_rect_Type2 x1 x2 x3 h1 =
 660   let hcut = fn_contains_rect_Type2 x1 x2 x3 h1 in hcut __
 661
 662 (** val fn_contains_inv_rect_Type1 :
 663     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 664 let fn_contains_inv_rect_Type1 x1 x2 x3 h1 =
 665   let hcut = fn_contains_rect_Type1 x1 x2 x3 h1 in hcut __
 666
 667 (** val fn_contains_inv_rect_Type0 :
 668     fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 669 let fn_contains_inv_rect_Type0 x1 x2 x3 h1 =
 670   let hcut = fn_contains_rect_Type0 x1 x2 x3 h1 in hcut __
 671
 672 (** val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __ **)
 673 let fn_contains_discr a1 a2 a3 =
 674   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 675
 676 (** val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __ **)
 677 let fn_contains_jmdiscr a1 a2 a3 =
 678   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 679
 680 (** val fill_in_statement :
 681     fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
 682     partial_fn Types.sig0 **)
 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) }
 690
 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) }
 701
 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 }
 709
 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
 716    in
 717   (fun _ ->
 718   let s1 = s (Types.pi1 f.pf_entry) in
 719   { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
 720   pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
 721   f.pf_stacksize; pf_graph =
 722   (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
 723   (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
 724   pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __
 725
 726 (** val fresh_reg :
 727     fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
 728     Registers.register Types.sig0) Types.dPair **)
 729 let fresh_reg fx f ty =
 730   let { Types.fst = r; Types.snd = g } =
 731     Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
 732   in
 733   let f' = { pf_labgen = f.pf_labgen; pf_reggen = g; pf_params = f.pf_params;
 734     pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty }, f.pf_locals));
 735     pf_result =
 736     ((match fx.fx_rettyp with
 737       | Types.None -> Obj.magic __
 738       | Types.Some t ->
 739         (fun clearme -> let r' = Obj.magic clearme in Obj.magic r'))
 740       f.pf_result); pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph;
 741     pf_gotos = f.pf_gotos; pf_labels = f.pf_labels; pf_entry = f.pf_entry;
 742     pf_exit = f.pf_exit }
 743   in
 744   { Types.dpi1 = f'; Types.dpi2 = r }
 745
 746 (** val choose_reg :
 747     fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
 748     Types.sig0, Registers.register Types.sig0) Types.dPair **)
 749 let choose_reg fx ty e f =
 750   (match e with
 751    | Cminor_syntax.Id (t, i) ->
 752      (fun _ -> { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) })
 753    | Cminor_syntax.Cst (x, x0) -> (fun _ -> fresh_reg fx f x)
 754    | Cminor_syntax.Op1 (x, x0, x1, x2) -> (fun _ -> fresh_reg fx f x0)
 755    | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) ->
 756      (fun _ -> fresh_reg fx f x1)
 757    | Cminor_syntax.Mem (x, x0) -> (fun _ -> fresh_reg fx f x)
 758    | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) ->
 759      (fun _ -> fresh_reg fx f x1)
 760    | Cminor_syntax.Ecost (x, x0, x1) -> (fun _ -> fresh_reg fx f x)) __
 761
 762 (** val foldr_all :
 763     ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
 764 let rec foldr_all f b l =
 765   (match l with
 766    | List.Nil -> (fun _ -> b)
 767    | List.Cons (a, l0) -> (fun _ -> f a __ (foldr_all f b l0))) __
 768
 769 (** val foldr_all' :
 770     ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2 **)
 771 let rec foldr_all' f b l =
 772   (match l with
 773    | List.Nil -> (fun _ -> b)
 774    | List.Cons (a, l0) -> (fun _ -> f a __ l0 (foldr_all' f b l0))) __
 775
 776 (** val eject' : ('a1, 'a2) Types.dPair -> 'a1 **)
 777 let eject' x =
 778   x.Types.dpi1
 779
 780 (** val choose_regs :
 781     fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
 782     partial_fn -> (partial_fn Types.sig0, Registers.register List.list
 783     Types.sig0) Types.dPair **)
 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
 788     (fun _ ->
 789     let { Types.dpi1 = f'; Types.dpi2 = r } =
 790       choose_reg fx t e0 (Types.pi1 f1)
 791     in
 792     { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r),
 793     (Types.pi1 rs))) })) __) { Types.dpi1 = f; Types.dpi2 = List.Nil } es
 794
 795 (** val add_stmt_inv_rect_Type4 :
 796     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 797     'a1) -> 'a1 **)
 798 let rec add_stmt_inv_rect_Type4 fx s f f' h_mk_add_stmt_inv =
 799   h_mk_add_stmt_inv __ __
 800
 801 (** val add_stmt_inv_rect_Type5 :
 802     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 803     'a1) -> 'a1 **)
 804 let rec add_stmt_inv_rect_Type5 fx s f f' h_mk_add_stmt_inv =
 805   h_mk_add_stmt_inv __ __
 806
 807 (** val add_stmt_inv_rect_Type3 :
 808     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 809     'a1) -> 'a1 **)
 810 let rec add_stmt_inv_rect_Type3 fx s f f' h_mk_add_stmt_inv =
 811   h_mk_add_stmt_inv __ __
 812
 813 (** val add_stmt_inv_rect_Type2 :
 814     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 815     'a1) -> 'a1 **)
 816 let rec add_stmt_inv_rect_Type2 fx s f f' h_mk_add_stmt_inv =
 817   h_mk_add_stmt_inv __ __
 818
 819 (** val add_stmt_inv_rect_Type1 :
 820     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 821     'a1) -> 'a1 **)
 822 let rec add_stmt_inv_rect_Type1 fx s f f' h_mk_add_stmt_inv =
 823   h_mk_add_stmt_inv __ __
 824
 825 (** val add_stmt_inv_rect_Type0 :
 826     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 827     'a1) -> 'a1 **)
 828 let rec add_stmt_inv_rect_Type0 fx s f f' h_mk_add_stmt_inv =
 829   h_mk_add_stmt_inv __ __
 830
 831 (** val add_stmt_inv_inv_rect_Type4 :
 832     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 833     __ -> 'a1) -> 'a1 **)
 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 __
 836
 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 __
 842
 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 __
 848
 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 __
 854
 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 __
 860
 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 __ __)) __
 865
 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 __ __)) __
 870
 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
 876
 877 (** val fn_con_because_rect_Type4 :
 878     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 879     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 880     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 881     fn_con_because -> 'a1 **)
 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
 886
 887 (** val fn_con_because_rect_Type5 :
 888     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 889     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 890     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 891     fn_con_because -> 'a1 **)
 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
 896
 897 (** val fn_con_because_rect_Type3 :
 898     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 899     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 900     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 901     fn_con_because -> 'a1 **)
 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
 906
 907 (** val fn_con_because_rect_Type2 :
 908     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 909     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 910     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 911     fn_con_because -> 'a1 **)
 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
 916
 917 (** val fn_con_because_rect_Type1 :
 918     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 919     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 920     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 921     fn_con_because -> 'a1 **)
 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
 926
 927 (** val fn_con_because_rect_Type0 :
 928     fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 929     partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 930     Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 931     fn_con_because -> 'a1 **)
 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
 936
 937 (** val fn_con_because_inv_rect_Type4 :
 938     fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
 939     -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
 940     -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
 941     partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 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 __ __
 944
 945 (** val fn_con_because_inv_rect_Type3 :
 946     fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
 947     -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
 948     -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
 949     partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 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 __ __
 952
 953 (** val fn_con_because_inv_rect_Type2 :
 954     fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
 955     -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
 956     -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
 957     partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 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 __ __
 960
 961 (** val fn_con_because_inv_rect_Type1 :
 962     fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
 963     -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
 964     -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
 965     partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 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 __ __
 968
 969 (** val fn_con_because_inv_rect_Type0 :
 970     fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1)
 971     -> (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __
 972     -> 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt ->
 973     partial_fn Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 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 __ __
 976
 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
 981     (match x with
 982      | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
 983      | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 984      | Fn_con_addinv (a0, a10, a3, a4) ->
 985        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 986
 987 (** val fn_con_because_jmdiscr :
 988     fixed -> partial_fn -> fn_con_because -> fn_con_because -> __ **)
 989 let fn_con_because_jmdiscr a1 a2 x y =
 990   Logic.eq_rect_Type2 x
 991     (match x with
 992      | Fn_con_eq a0 -> Obj.magic (fun _ dH -> dH __)
 993      | Fn_con_sig (a0, a10, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 994      | Fn_con_addinv (a0, a10, a3, a4) ->
 995        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 996
 997 (** val fn_con_because_left :
 998     fixed -> partial_fn -> fn_con_because -> partial_fn **)
 999 let rec fn_con_because_left fx f0 = function
1000 | Fn_con_eq f -> f
1001 | Fn_con_sig (f, x, x1) -> f
1002 | Fn_con_addinv (f, x, x1, x2) -> f
1003
1004 (** val add_expr :
1005     fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
1006     Registers.register Types.sig0 -> partial_fn Types.sig0 **)
1007 let rec add_expr fx ty e f dst =
1008   (match e with
1009    | Cminor_syntax.Id (t, i) ->
1010      (fun _ dst0 ->
1011        let r = lookup_reg fx.fx_env i t in
1012        (match Registers.register_eq r (Types.pi1 dst0) with
1013         | Types.Inl _ -> f
1014         | Types.Inr _ ->
1015           Types.pi1
1016             (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t, t,
1017               (FrontEndOps.Oid t), (Types.pi1 dst0), r, x)) f)))
1018    | Cminor_syntax.Cst (x, c) ->
1019      (fun _ dst0 ->
1020        Types.pi1
1021          (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
1022            (Types.pi1 dst0), c, x0)) f))
1023    | Cminor_syntax.Op1 (t, t', op, e') ->
1024      (fun _ dst0 ->
1025        let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
1026        let f1 =
1027          add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
1028            (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
1029        in
1030        let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
1031    | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
1032      (fun _ dst0 ->
1033        let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
1034        let { Types.dpi1 = f1; Types.dpi2 = r2 } =
1035          choose_reg fx x0 e2 (Types.pi1 f0)
1036        in
1037        let f2 =
1038          add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
1039            op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
1040            (Types.pi1 f1)
1041        in
1042        let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r2) in
1043        let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r1) in
1044        Types.pi1 f4)
1045    | Cminor_syntax.Mem (t, e') ->
1046      (fun _ dst0 ->
1047        let { Types.dpi1 = f0; Types.dpi2 = r } =
1048          choose_reg fx AST.ASTptr e' f
1049        in
1050        let f1 =
1051          add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_load (t,
1052            (Types.pi1 r), (Types.pi1 dst0), x)) (Types.pi1 f0)
1053        in
1054        let f2 = add_expr fx AST.ASTptr e' (Types.pi1 f1) (Types.pi1 r) in
1055        Types.pi1 f2)
1056    | Cminor_syntax.Cond (x, x0, x1, e', e1, e2) ->
1057      (fun _ dst0 ->
1058        let resume_at = f.pf_entry in
1059        let f0 = add_expr fx x1 e2 f dst0 in
1060        let lfalse = (Types.pi1 f0).pf_entry in
1061        let f1 =
1062          add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_skip
1063            (Types.pi1 resume_at)) (Types.pi1 f0)
1064        in
1065        let f2 = add_expr fx x1 e1 (Types.pi1 f1) (Types.pi1 dst0) in
1066        let { Types.dpi1 = f3; Types.dpi2 = r } =
1067          choose_reg fx (AST.ASTint (x, x0)) e' (Types.pi1 f2)
1068        in
1069        let f4 =
1070          add_fresh_to_graph fx (fun ltrue -> RTLabs_syntax.St_cond
1071            ((Types.pi1 r), ltrue, (Types.pi1 lfalse))) (Types.pi1 f3)
1072        in
1073        let f5 =
1074          add_expr fx (AST.ASTint (x, x0)) e' (Types.pi1 f4) (Types.pi1 r)
1075        in
1076        Types.pi1 f5)
1077    | Cminor_syntax.Ecost (x, l, e') ->
1078      (fun _ dst0 ->
1079        let f0 = add_expr fx x e' f dst0 in
1080        let f1 =
1081          add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_cost (l, x0))
1082            (Types.pi1 f0)
1083        in
1084        Types.pi1 f1)) __ dst
1085
1086 (** val add_exprs :
1087     fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
1088     Registers.register List.list -> partial_fn -> partial_fn Types.sig0 **)
1089 let rec add_exprs fx es dsts f =
1090   (match es with
1091    | List.Nil ->
1092      (fun _ _ ->
1093        match dsts with
1094        | List.Nil -> (fun _ -> f)
1095        | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
1096    | List.Cons (e, et) ->
1097      (fun _ ->
1098        match dsts with
1099        | List.Nil -> (fun _ _ -> assert false (* absurd case *))
1100        | List.Cons (r, rt) ->
1101          (fun _ _ ->
1102            let f' = add_exprs fx et rt f in
1103            (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
1104            (fun _ _ ->
1105            let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
1106              __))) __ __ __
1107
1108 (** val stmt_inv_rect_Type4 :
1109     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1110 let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
1111   h_mk_stmt_inv __ __ __
1112
1113 (** val stmt_inv_rect_Type5 :
1114     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1115 let rec stmt_inv_rect_Type5 fx s h_mk_stmt_inv =
1116   h_mk_stmt_inv __ __ __
1117
1118 (** val stmt_inv_rect_Type3 :
1119     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1120 let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
1121   h_mk_stmt_inv __ __ __
1122
1123 (** val stmt_inv_rect_Type2 :
1124     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1125 let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
1126   h_mk_stmt_inv __ __ __
1127
1128 (** val stmt_inv_rect_Type1 :
1129     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1130 let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
1131   h_mk_stmt_inv __ __ __
1132
1133 (** val stmt_inv_rect_Type0 :
1134     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
1135 let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
1136   h_mk_stmt_inv __ __ __
1137
1138 (** val stmt_inv_inv_rect_Type4 :
1139     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1140 let stmt_inv_inv_rect_Type4 x1 x2 h1 =
1141   let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __
1142
1143 (** val stmt_inv_inv_rect_Type3 :
1144     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1145 let stmt_inv_inv_rect_Type3 x1 x2 h1 =
1146   let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __
1147
1148 (** val stmt_inv_inv_rect_Type2 :
1149     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1150 let stmt_inv_inv_rect_Type2 x1 x2 h1 =
1151   let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __
1152
1153 (** val stmt_inv_inv_rect_Type1 :
1154     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1155 let stmt_inv_inv_rect_Type1 x1 x2 h1 =
1156   let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __
1157
1158 (** val stmt_inv_inv_rect_Type0 :
1159     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1160 let stmt_inv_inv_rect_Type0 x1 x2 h1 =
1161   let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __
1162
1163 (** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
1164 let stmt_inv_discr a1 a2 =
1165   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1166
1167 (** val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __ **)
1168 let stmt_inv_jmdiscr a1 a2 =
1169   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1170
1171 (** val expr_is_cst_ident :
1172     AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
1173 let expr_is_cst_ident t = function
1174 | Cminor_syntax.Id (x, x0) -> Types.None
1175 | Cminor_syntax.Cst (x, c) ->
1176   (match c with
1177    | FrontEndOps.Ointconst (x0, x1, x2) -> Types.None
1178    | FrontEndOps.Oaddrsymbol (id, n) ->
1179      (match n with
1180       | Nat.O -> Types.Some id
1181       | Nat.S x0 -> Types.None)
1182    | FrontEndOps.Oaddrstack x0 -> Types.None)
1183 | Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
1184 | Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
1185 | Cminor_syntax.Mem (x, x0) -> Types.None
1186 | Cminor_syntax.Cond (x, x0, x1, x2, x3, x4) -> Types.None
1187 | Cminor_syntax.Ecost (x, x0, x1) -> Types.None
1188
1189 (** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1190 let option_jmdiscr x y =
1191   Logic.eq_rect_Type2 x
1192     (match x with
1193      | Types.None -> Obj.magic (fun _ dH -> dH)
1194      | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1195
1196 (** val dPair_jmdiscr :
1197     ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
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
1202
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 =
1207   let f0 = f in
1208   let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
1209   (match opt_e with
1210    | Types.None -> (fun _ -> Types.pi1 f1)
1211    | Types.Some et ->
1212      let { Types.dpi1 = ty; Types.dpi2 = e } = et in
1213      (fun _ ->
1214      (match fx.fx_rettyp with
1215       | Types.None -> (fun _ -> assert false (* absurd case *))
1216       | Types.Some t ->
1217         (fun _ r ->
1218           let r0 = Obj.magic r in
1219           let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
1220        (Types.pi1 f1).pf_result)) __
1221
1222 (** val record_goto_label :
1223     fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn **)
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 }
1231
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
1237    in
1238   (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
1239   f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
1240   pf_stacksize = f.pf_stacksize; pf_graph =
1241   (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
1242     (RTLabs_syntax.St_skip l)); pf_gotos =
1243   (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
1244     l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
1245   (Types.pi1 f.pf_exit) })) __
1246
1247 (** val add_stmt :
1248     fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0 **)
1249 let rec add_stmt fx s f =
1250   (match s with
1251    | Cminor_syntax.St_skip -> (fun _ -> f)
1252    | Cminor_syntax.St_assign (t, x, e) ->
1253      (fun _ ->
1254        let dst = lookup_reg fx.fx_env x t in
1255        Types.pi1 (add_expr fx t e f dst))
1256    | Cminor_syntax.St_store (t, e1, e2) ->
1257      (fun _ ->
1258        let { Types.dpi1 = f0; Types.dpi2 = val_reg } = choose_reg fx t e2 f
1259        in
1260        let { Types.dpi1 = f1; Types.dpi2 = addr_reg } =
1261          choose_reg fx AST.ASTptr e1 (Types.pi1 f0)
1262        in
1263        let f2 =
1264          add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_store (t,
1265            (Types.pi1 addr_reg), (Types.pi1 val_reg), x)) (Types.pi1 f1)
1266        in
1267        let f3 = add_expr fx AST.ASTptr e1 (Types.pi1 f2) (Types.pi1 addr_reg)
1268        in
1269        Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
1270    | Cminor_syntax.St_call (return_opt_id, e, args) ->
1271      (fun _ ->
1272        let return_opt_reg =
1273          (match return_opt_id with
1274           | Types.None -> (fun _ -> Types.None)
1275           | Types.Some idty ->
1276             (fun _ -> Types.Some
1277               (lookup_reg fx.fx_env idty.Types.fst idty.Types.snd))) __
1278        in
1279        let { Types.dpi1 = f0; Types.dpi2 = args_regs } =
1280          choose_regs fx args f
1281        in
1282        let f1 =
1283          match expr_is_cst_ident AST.ASTptr e with
1284          | Types.None ->
1285            let { Types.dpi1 = f1; Types.dpi2 = fnr } =
1286              choose_reg fx AST.ASTptr e (Types.pi1 f0)
1287            in
1288            let f2 =
1289              add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_ptr
1290                ((Types.pi1 fnr), (Types.pi1 args_regs), return_opt_reg, x))
1291                (Types.pi1 f1)
1292            in
1293            Types.pi1
1294              (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
1295          | Types.Some id ->
1296            add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_id (id,
1297              (Types.pi1 args_regs), return_opt_reg, x)) (Types.pi1 f0)
1298        in
1299        Types.pi1 (add_exprs fx args (Types.pi1 args_regs) (Types.pi1 f1)))
1300    | Cminor_syntax.St_seq (s1, s2) ->
1301      (fun _ ->
1302        let f2 = add_stmt fx s2 f in
1303        let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
1304    | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
1305      (fun _ ->
1306        let l_next = f.pf_entry in
1307        let f2 = add_stmt fx s2 f in
1308        let l2 = (Types.pi1 f2).pf_entry in
1309        let f0 = change_entry fx (Types.pi1 f2) (Types.pi1 l_next) in
1310        let f1 = add_stmt fx s1 (Types.pi1 f0) in
1311        let { Types.dpi1 = f3; Types.dpi2 = r } =
1312          choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
1313        in
1314        let f4 =
1315          add_fresh_to_graph fx (fun l1 -> RTLabs_syntax.St_cond
1316            ((Types.pi1 r), l1, (Types.pi1 l2))) (Types.pi1 f3)
1317        in
1318        Types.pi1
1319          (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
1320    | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
1321    | Cminor_syntax.St_label (l, s') ->
1322      (fun _ ->
1323        let f0 = add_stmt fx s' f in record_goto_label fx (Types.pi1 f0) l)
1324    | Cminor_syntax.St_goto l -> (fun _ -> Types.pi1 (add_goto_dummy fx f l))
1325    | Cminor_syntax.St_cost (l, s') ->
1326      (fun _ ->
1327        let f0 = add_stmt fx s' f in
1328        Types.pi1
1329          (add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_cost (l, x))
1330            (Types.pi1 f0)))) __
1331
1332 (** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
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' ->
1336     Types.pi1
1337       (fill_in_statement fx l (RTLabs_syntax.St_skip
1338         (Identifiers.lookup_present PreIdentifiers.Label
1339           (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f
1340
1341 (** val c2ra_function :
1342     Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
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
1350    in
1351   let { Types.fst = params; Types.snd = env1 } = eta3108 in
1352   (fun _ ->
1353   (let { Types.fst = eta3107; Types.snd = reggen2 } =
1354      populate_env env1 reggen1 f.Cminor_syntax.f_vars
1355    in
1356   let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
1357   (fun _ ->
1358   (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
1359      match f.Cminor_syntax.f_return with
1360      | Types.None ->
1361        { Types.dpi1 = { Types.fst = locals0; Types.snd = reggen2 };
1362          Types.dpi2 = (Obj.magic __) }
1363      | Types.Some ty ->
1364        let { Types.fst = r; Types.snd = gen } =
1365          Identifiers.fresh PreIdentifiers.RegisterTag reggen2
1366        in
1367        { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
1368        ty }, locals0)); Types.snd = gen }; Types.dpi2 = r }
1369    in
1370   (fun _ ->
1371   let locals = locals_reggen.Types.fst in
1372   let reggen = locals_reggen.Types.snd in
1373   let { Types.fst = l; Types.snd = labgen } =
1374     Identifiers.fresh PreIdentifiers.LabelTag labgen0
1375   in
1376   let fixed0 = { fx_gotos =
1377     (Identifiers.set_of_list PreIdentifiers.Label
1378       (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
1379     fx_rettyp = f.Cminor_syntax.f_return }
1380   in
1381   let emptyfn = { pf_labgen = labgen; pf_reggen = reggen; pf_params = params;
1382     pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
1383     f.Cminor_syntax.f_stacksize; pf_graph =
1384     (Identifiers.add PreIdentifiers.LabelTag
1385       (Identifiers.empty_map PreIdentifiers.LabelTag) l
1386       RTLabs_syntax.St_return); pf_gotos =
1387     (Identifiers.empty_map PreIdentifiers.LabelTag); pf_labels =
1388     (Identifiers.empty_map PreIdentifiers.Label); pf_entry = l; pf_exit = l }
1389   in
1390   let f0 = add_stmt fixed0 f.Cminor_syntax.f_body emptyfn in
1391   let f1 = patch_gotos fixed0 (Types.pi1 f0) in
1392   { RTLabs_syntax.f_labgen = (Types.pi1 f1).pf_labgen;
1393   RTLabs_syntax.f_reggen = (Types.pi1 f1).pf_reggen; RTLabs_syntax.f_result =
1394   ((match fixed0.fx_rettyp with
1395     | Types.None -> Obj.magic (fun _ -> Types.None)
1396     | Types.Some t ->
1397       (fun r -> Types.Some { Types.fst = (Types.pi1 (Obj.magic r));
1398         Types.snd = t })) (Types.pi1 f1).pf_result); RTLabs_syntax.f_params =
1399   (Types.pi1 f1).pf_params; RTLabs_syntax.f_locals =
1400   (Types.pi1 f1).pf_locals; RTLabs_syntax.f_stacksize =
1401   (Types.pi1 f1).pf_stacksize; RTLabs_syntax.f_graph =
1402   (Types.pi1 f1).pf_graph; RTLabs_syntax.f_entry = (Types.pi1 f1).pf_entry;
1403   RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __
1404
1405 (** val cminor_to_rtlabs :
1406     Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
1407 let cminor_to_rtlabs p =
1408   AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)
1409