extracted/eRTL.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 type move_dst =
 122 | PSD of Registers.register
 123 | HDW of I8051.register
 124
 125 (** val move_dst_rect_Type4 :
 126     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 127 let rec move_dst_rect_Type4 h_PSD h_HDW = function
 128 | PSD x_18499 -> h_PSD x_18499
 129 | HDW x_18500 -> h_HDW x_18500
 130
 131 (** val move_dst_rect_Type5 :
 132     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 133 let rec move_dst_rect_Type5 h_PSD h_HDW = function
 134 | PSD x_18504 -> h_PSD x_18504
 135 | HDW x_18505 -> h_HDW x_18505
 136
 137 (** val move_dst_rect_Type3 :
 138     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 139 let rec move_dst_rect_Type3 h_PSD h_HDW = function
 140 | PSD x_18509 -> h_PSD x_18509
 141 | HDW x_18510 -> h_HDW x_18510
 142
 143 (** val move_dst_rect_Type2 :
 144     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 145 let rec move_dst_rect_Type2 h_PSD h_HDW = function
 146 | PSD x_18514 -> h_PSD x_18514
 147 | HDW x_18515 -> h_HDW x_18515
 148
 149 (** val move_dst_rect_Type1 :
 150     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 151 let rec move_dst_rect_Type1 h_PSD h_HDW = function
 152 | PSD x_18519 -> h_PSD x_18519
 153 | HDW x_18520 -> h_HDW x_18520
 154
 155 (** val move_dst_rect_Type0 :
 156     (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
 157 let rec move_dst_rect_Type0 h_PSD h_HDW = function
 158 | PSD x_18524 -> h_PSD x_18524
 159 | HDW x_18525 -> h_HDW x_18525
 160
 161 (** val move_dst_inv_rect_Type4 :
 162     move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 163     'a1) -> 'a1 **)
 164 let move_dst_inv_rect_Type4 hterm h1 h2 =
 165   let hcut = move_dst_rect_Type4 h1 h2 hterm in hcut __
 166
 167 (** val move_dst_inv_rect_Type3 :
 168     move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 169     'a1) -> 'a1 **)
 170 let move_dst_inv_rect_Type3 hterm h1 h2 =
 171   let hcut = move_dst_rect_Type3 h1 h2 hterm in hcut __
 172
 173 (** val move_dst_inv_rect_Type2 :
 174     move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 175     'a1) -> 'a1 **)
 176 let move_dst_inv_rect_Type2 hterm h1 h2 =
 177   let hcut = move_dst_rect_Type2 h1 h2 hterm in hcut __
 178
 179 (** val move_dst_inv_rect_Type1 :
 180     move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 181     'a1) -> 'a1 **)
 182 let move_dst_inv_rect_Type1 hterm h1 h2 =
 183   let hcut = move_dst_rect_Type1 h1 h2 hterm in hcut __
 184
 185 (** val move_dst_inv_rect_Type0 :
 186     move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 187     'a1) -> 'a1 **)
 188 let move_dst_inv_rect_Type0 hterm h1 h2 =
 189   let hcut = move_dst_rect_Type0 h1 h2 hterm in hcut __
 190
 191 (** val move_dst_discr : move_dst -> move_dst -> __ **)
 192 let move_dst_discr x y =
 193   Logic.eq_rect_Type2 x
 194     (match x with
 195      | PSD a0 -> Obj.magic (fun _ dH -> dH __)
 196      | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
 197
 198 (** val move_dst_jmdiscr : move_dst -> move_dst -> __ **)
 199 let move_dst_jmdiscr x y =
 200   Logic.eq_rect_Type2 x
 201     (match x with
 202      | PSD a0 -> Obj.magic (fun _ dH -> dH __)
 203      | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
 204
 205 type move_src = move_dst Joint.argument
 206
 207 (** val move_src_from_dst : move_dst -> move_src **)
 208 let move_src_from_dst x =
 209   Joint.Reg x
 210
 211 (** val dpi1__o__move_dst_to_src__o__inject :
 212     (move_dst, 'a1) Types.dPair -> move_src Types.sig0 **)
 213 let dpi1__o__move_dst_to_src__o__inject x2 =
 214   move_src_from_dst x2.Types.dpi1
 215
 216 (** val eject__o__move_dst_to_src__o__inject :
 217     move_dst Types.sig0 -> move_src Types.sig0 **)
 218 let eject__o__move_dst_to_src__o__inject x2 =
 219   move_src_from_dst (Types.pi1 x2)
 220
 221 (** val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0 **)
 222 let move_dst_to_src__o__inject x1 =
 223   move_src_from_dst x1
 224
 225 (** val dpi1__o__move_dst_to_src :
 226     (move_dst, 'a1) Types.dPair -> move_src **)
 227 let dpi1__o__move_dst_to_src x1 =
 228   move_src_from_dst x1.Types.dpi1
 229
 230 (** val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src **)
 231 let eject__o__move_dst_to_src x1 =
 232   move_src_from_dst (Types.pi1 x1)
 233
 234 (** val psd_argument_move_src : Joint.psd_argument -> move_src **)
 235 let psd_argument_move_src = function
 236 | Joint.Reg r -> Joint.Reg (PSD r)
 237 | Joint.Imm b -> Joint.Imm b
 238
 239 (** val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 240     BitVector.byte -> move_src Types.sig0 **)
 241 let byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
 242   psd_argument_move_src (Joint.psd_argument_from_byte x0)
 243
 244 (** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
 245     (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
 246 let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
 247   psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x2)
 248
 249 (** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 250     (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
 251 let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
 252   psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x2)
 253
 254 (** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 255     (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
 256 let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
 257   psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x2)
 258
 259 (** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
 260     BitVector.byte Types.sig0 -> move_src Types.sig0 **)
 261 let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
 262   psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x2)
 263
 264 (** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 265     BitVector.byte Types.sig0 -> move_src Types.sig0 **)
 266 let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
 267   psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x2)
 268
 269 (** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 270     Registers.register Types.sig0 -> move_src Types.sig0 **)
 271 let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
 272   psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x2)
 273
 274 (** val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 275     Registers.register -> move_src Types.sig0 **)
 276 let reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
 277   psd_argument_move_src (Joint.psd_argument_from_reg x0)
 278
 279 (** val dpi1__o__psd_argument_to_move_src__o__inject :
 280     (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0 **)
 281 let dpi1__o__psd_argument_to_move_src__o__inject x2 =
 282   psd_argument_move_src x2.Types.dpi1
 283
 284 (** val eject__o__psd_argument_to_move_src__o__inject :
 285     Joint.psd_argument Types.sig0 -> move_src Types.sig0 **)
 286 let eject__o__psd_argument_to_move_src__o__inject x2 =
 287   psd_argument_move_src (Types.pi1 x2)
 288
 289 (** val psd_argument_to_move_src__o__inject :
 290     Joint.psd_argument -> move_src Types.sig0 **)
 291 let psd_argument_to_move_src__o__inject x1 =
 292   psd_argument_move_src x1
 293
 294 (** val byte_to_psd_argument__o__psd_argument_to_move_src :
 295     BitVector.byte -> move_src **)
 296 let byte_to_psd_argument__o__psd_argument_to_move_src x0 =
 297   psd_argument_move_src (Joint.psd_argument_from_byte x0)
 298
 299 (** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
 300     (BitVector.byte, 'a1) Types.dPair -> move_src **)
 301 let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
 302   psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x1)
 303
 304 (** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
 305     (BitVector.byte, 'a1) Types.dPair -> move_src **)
 306 let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
 307   psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x1)
 308
 309 (** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
 310     (Registers.register, 'a1) Types.dPair -> move_src **)
 311 let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
 312   psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x1)
 313
 314 (** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
 315     BitVector.byte Types.sig0 -> move_src **)
 316 let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
 317   psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x1)
 318
 319 (** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
 320     BitVector.byte Types.sig0 -> move_src **)
 321 let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
 322   psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x1)
 323
 324 (** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
 325     Registers.register Types.sig0 -> move_src **)
 326 let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
 327   psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x1)
 328
 329 (** val reg_to_psd_argument__o__psd_argument_to_move_src :
 330     Registers.register -> move_src **)
 331 let reg_to_psd_argument__o__psd_argument_to_move_src x0 =
 332   psd_argument_move_src (Joint.psd_argument_from_reg x0)
 333
 334 (** val dpi1__o__psd_argument_to_move_src :
 335     (Joint.psd_argument, 'a1) Types.dPair -> move_src **)
 336 let dpi1__o__psd_argument_to_move_src x1 =
 337   psd_argument_move_src x1.Types.dpi1
 338
 339 (** val eject__o__psd_argument_to_move_src :
 340     Joint.psd_argument Types.sig0 -> move_src **)
 341 let eject__o__psd_argument_to_move_src x1 =
 342   psd_argument_move_src (Types.pi1 x1)
 343
 344 type ertl_seq =
 345 | Ertl_new_frame
 346 | Ertl_del_frame
 347 | Ertl_frame_size of Registers.register
 348
 349 (** val ertl_seq_rect_Type4 :
 350     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 351 let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 352 | Ertl_new_frame -> h_ertl_new_frame
 353 | Ertl_del_frame -> h_ertl_del_frame
 354 | Ertl_frame_size x_18564 -> h_ertl_frame_size x_18564
 355
 356 (** val ertl_seq_rect_Type5 :
 357     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 358 let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 359 | Ertl_new_frame -> h_ertl_new_frame
 360 | Ertl_del_frame -> h_ertl_del_frame
 361 | Ertl_frame_size x_18569 -> h_ertl_frame_size x_18569
 362
 363 (** val ertl_seq_rect_Type3 :
 364     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 365 let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 366 | Ertl_new_frame -> h_ertl_new_frame
 367 | Ertl_del_frame -> h_ertl_del_frame
 368 | Ertl_frame_size x_18574 -> h_ertl_frame_size x_18574
 369
 370 (** val ertl_seq_rect_Type2 :
 371     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 372 let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 373 | Ertl_new_frame -> h_ertl_new_frame
 374 | Ertl_del_frame -> h_ertl_del_frame
 375 | Ertl_frame_size x_18579 -> h_ertl_frame_size x_18579
 376
 377 (** val ertl_seq_rect_Type1 :
 378     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 379 let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 380 | Ertl_new_frame -> h_ertl_new_frame
 381 | Ertl_del_frame -> h_ertl_del_frame
 382 | Ertl_frame_size x_18584 -> h_ertl_frame_size x_18584
 383
 384 (** val ertl_seq_rect_Type0 :
 385     'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
 386 let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
 387 | Ertl_new_frame -> h_ertl_new_frame
 388 | Ertl_del_frame -> h_ertl_del_frame
 389 | Ertl_frame_size x_18589 -> h_ertl_frame_size x_18589
 390
 391 (** val ertl_seq_inv_rect_Type4 :
 392     ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
 393     'a1) -> 'a1 **)
 394 let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
 395   let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __
 396
 397 (** val ertl_seq_inv_rect_Type3 :
 398     ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
 399     'a1) -> 'a1 **)
 400 let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
 401   let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __
 402
 403 (** val ertl_seq_inv_rect_Type2 :
 404     ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
 405     'a1) -> 'a1 **)
 406 let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
 407   let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __
 408
 409 (** val ertl_seq_inv_rect_Type1 :
 410     ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
 411     'a1) -> 'a1 **)
 412 let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
 413   let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __
 414
 415 (** val ertl_seq_inv_rect_Type0 :
 416     ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
 417     'a1) -> 'a1 **)
 418 let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
 419   let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __
 420
 421 (** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
 422 let ertl_seq_discr x y =
 423   Logic.eq_rect_Type2 x
 424     (match x with
 425      | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
 426      | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
 427      | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
 428
 429 (** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
 430 let ertl_seq_jmdiscr x y =
 431   Logic.eq_rect_Type2 x
 432     (match x with
 433      | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
 434      | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
 435      | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
 436
 437 (** val eRTL_uns : Joint.unserialized_params **)
 438 let eRTL_uns =
 439   { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
 440     Bool.False }
 441
 442 (** val regs_from_move_dst : move_dst -> Registers.register List.list **)
 443 let regs_from_move_dst = function
 444 | PSD r -> List.Cons (r, List.Nil)
 445 | HDW x -> List.Nil
 446
 447 (** val regs_from_move_src : move_src -> Registers.register List.list **)
 448 let regs_from_move_src = function
 449 | Joint.Reg r ->
 450   (match r with
 451    | PSD r1 -> List.Cons (r1, List.Nil)
 452    | HDW x -> List.Nil)
 453 | Joint.Imm x -> List.Nil
 454
 455 (** val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list **)
 456 let ertl_ext_seq_regs = function
 457 | Ertl_new_frame -> List.Nil
 458 | Ertl_del_frame -> List.Nil
 459 | Ertl_frame_size r -> List.Cons (r, List.Nil)
 460
 461 (** val eRTL_functs : Joint.get_pseudo_reg_functs **)
 462 let eRTL_functs =
 463   { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
 464     Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
 465     Joint.acc_a_args = (fun arg ->
 466     match Obj.magic arg with
 467     | Joint.Reg r -> List.Cons (r, List.Nil)
 468     | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
 469     match Obj.magic arg with
 470     | Joint.Reg r -> List.Cons (r, List.Nil)
 471     | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
 472     ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
 473     ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
 474     match Obj.magic arg with
 475     | Joint.Reg r -> List.Cons (r, List.Nil)
 476     | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
 477     match Obj.magic arg with
 478     | Joint.Reg r -> List.Cons (r, List.Nil)
 479     | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
 480     match Obj.magic arg with
 481     | Joint.Reg r -> List.Cons (r, List.Nil)
 482     | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
 483     List.append (regs_from_move_dst (Obj.magic x).Types.fst)
 484       (regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
 485     (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
 486     Joint.ext_seq_regs = (Obj.magic ertl_ext_seq_regs); Joint.params_regs =
 487     (fun x -> List.Nil) }
 488
 489 (** val eRTL : Joint.graph_params **)
 490 let eRTL =
 491   { Joint.u_pars = eRTL_uns; Joint.functs = eRTL_functs }
 492
 493 type ertl_program = Joint.joint_program
 494
 495 (** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
 496     (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
 497 let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
 498   Joint.psd_argument_from_reg x2.Types.dpi1
 499
 500 (** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 501     (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
 502 let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
 503   psd_argument_to_move_src__o__inject
 504     (Joint.psd_argument_from_reg x2.Types.dpi1)
 505
 506 (** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 507     (Registers.register, 'a1) Types.dPair -> move_src **)
 508 let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
 509   psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)
 510
 511 (** val eject__o__reg_to_ertl_snd_argument__o__inject :
 512     Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
 513 let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
 514   Joint.psd_argument_from_reg (Types.pi1 x2)
 515
 516 (** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 517     Registers.register Types.sig0 -> move_src Types.sig0 **)
 518 let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
 519   psd_argument_to_move_src__o__inject
 520     (Joint.psd_argument_from_reg (Types.pi1 x2))
 521
 522 (** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 523     Registers.register Types.sig0 -> move_src **)
 524 let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
 525   psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))
 526
 527 (** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 528     Registers.register -> move_src **)
 529 let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
 530   psd_argument_move_src (Joint.psd_argument_from_reg x0)
 531
 532 (** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 533     Registers.register -> move_src Types.sig0 **)
 534 let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
 535   psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)
 536
 537 (** val reg_to_ertl_snd_argument__o__inject :
 538     Registers.register -> Joint.psd_argument Types.sig0 **)
 539 let reg_to_ertl_snd_argument__o__inject x1 =
 540   Joint.psd_argument_from_reg x1
 541
 542 (** val dpi1__o__reg_to_ertl_snd_argument :
 543     (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
 544 let dpi1__o__reg_to_ertl_snd_argument x1 =
 545   Joint.psd_argument_from_reg x1.Types.dpi1
 546
 547 (** val eject__o__reg_to_ertl_snd_argument :
 548     Registers.register Types.sig0 -> Joint.psd_argument **)
 549 let eject__o__reg_to_ertl_snd_argument x1 =
 550   Joint.psd_argument_from_reg (Types.pi1 x1)
 551
 552 (** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
 553     (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
 554 let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
 555   Joint.psd_argument_from_byte x2.Types.dpi1
 556
 557 (** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 558     (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
 559 let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
 560   psd_argument_to_move_src__o__inject
 561     (Joint.psd_argument_from_byte x2.Types.dpi1)
 562
 563 (** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 564     (BitVector.byte, 'a1) Types.dPair -> move_src **)
 565 let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
 566   psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)
 567
 568 (** val eject__o__byte_to_ertl_snd_argument__o__inject :
 569     BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
 570 let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
 571   Joint.psd_argument_from_byte (Types.pi1 x2)
 572
 573 (** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 574     BitVector.byte Types.sig0 -> move_src Types.sig0 **)
 575 let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
 576   psd_argument_to_move_src__o__inject
 577     (Joint.psd_argument_from_byte (Types.pi1 x2))
 578
 579 (** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 580     BitVector.byte Types.sig0 -> move_src **)
 581 let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
 582   psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))
 583
 584 (** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 585     BitVector.byte -> move_src **)
 586 let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
 587   psd_argument_move_src (Joint.psd_argument_from_byte x0)
 588
 589 (** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 590     BitVector.byte -> move_src Types.sig0 **)
 591 let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
 592   psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)
 593
 594 (** val byte_to_ertl_snd_argument__o__inject :
 595     BitVector.byte -> Joint.psd_argument Types.sig0 **)
 596 let byte_to_ertl_snd_argument__o__inject x1 =
 597   Joint.psd_argument_from_byte x1
 598
 599 (** val dpi1__o__byte_to_ertl_snd_argument :
 600     (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
 601 let dpi1__o__byte_to_ertl_snd_argument x1 =
 602   Joint.psd_argument_from_byte x1.Types.dpi1
 603
 604 (** val eject__o__byte_to_ertl_snd_argument :
 605     BitVector.byte Types.sig0 -> Joint.psd_argument **)
 606 let eject__o__byte_to_ertl_snd_argument x1 =
 607   Joint.psd_argument_from_byte (Types.pi1 x1)
 608
 609 (** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
 610 let ertl_seq_joint =
 611   Obj.magic (fun _ x -> Joint.Extension_seq x)
 612
 613 (** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
 614     AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
 615     Types.sig0 **)
 616 let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
 617   ertl_seq_joint x1 x2.Types.dpi1
 618
 619 (** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 620     AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
 621     Types.sig0 **)
 622 let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
 623   Joint.seq_to_step__o__inject
 624     (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
 625     (ertl_seq_joint x1 x2.Types.dpi1)
 626
 627 (** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
 628     AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
 629 let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
 630   Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)
 631
 632 (** val eject__o__ertl_seq_to_joint_seq__o__inject :
 633     AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
 634 let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
 635   ertl_seq_joint x1 (Types.pi1 x2)
 636
 637 (** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 638     AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
 639 let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
 640   Joint.seq_to_step__o__inject
 641     (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
 642     (ertl_seq_joint x1 (Types.pi1 x2))
 643
 644 (** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
 645     AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
 646 let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
 647   Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))
 648
 649 (** val ertl_seq_to_joint_seq__o__seq_to_step :
 650     AST.ident List.list -> __ -> Joint.joint_step **)
 651 let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
 652   Joint.Step_seq (ertl_seq_joint x0 x1)
 653
 654 (** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 655     AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
 656 let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
 657   Joint.seq_to_step__o__inject
 658     (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x0
 659     (ertl_seq_joint x0 x1)
 660
 661 (** val ertl_seq_to_joint_seq__o__inject :
 662     AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
 663 let ertl_seq_to_joint_seq__o__inject x0 x1 =
 664   ertl_seq_joint x0 x1
 665
 666 (** val dpi1__o__ertl_seq_to_joint_seq :
 667     AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
 668 let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
 669   ertl_seq_joint x1 x2.Types.dpi1
 670
 671 (** val eject__o__ertl_seq_to_joint_seq :
 672     AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
 673 let eject__o__ertl_seq_to_joint_seq x1 x2 =
 674   ertl_seq_joint x1 (Types.pi1 x2)
 675
 676 (** val eRTL_premain :
 677     ertl_program -> Joint.joint_closed_internal_function **)
 678 let eRTL_premain p =
 679   let l1 = Positive.One in
 680   let l2 = Positive.P0 Positive.One in
 681   let l3 = Positive.P1 Positive.One in
 682   let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
 683     Positive.One)); Joint.joint_if_runiverse = Positive.One;
 684     Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
 685     (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
 686     Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
 687     Joint.joint_if_code =
 688     (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
 689     Joint.joint_if_entry = (Obj.magic l1) }
 690   in
 691   let res0 =
 692     Joint.add_graph eRTL
 693       (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l1
 694       (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
 695       (Obj.magic l2))) res
 696   in
 697   let res1 =
 698     Joint.add_graph eRTL
 699       (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l2
 700       (Joint.Sequential ((Joint.CALL ((Types.Inl
 701       p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
 702       (Obj.magic Types.It))), (Obj.magic l3))) res0
 703   in
 704   let res2 =
 705     Joint.add_graph eRTL
 706       (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l3
 707       (Joint.Final (Joint.GOTO l3)) res1
 708   in
 709   res2
 710