extracted/translateUtils.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 open State
 122
 123 open Bind_new
 124
 125 open BindLists
 126
 127 open Blocks
 128
 129 open Deqsets_extra
 130
 131 (** val fresh_label :
 132     Joint.params -> AST.ident List.list -> Graphs.label
 133     Monad.smax_def__o__monad **)
 134 let fresh_label g_pars globals =
 135   Obj.magic (fun def ->
 136     let { Types.fst = r; Types.snd = luniverse } =
 137       Identifiers.fresh PreIdentifiers.LabelTag def.Joint.joint_if_luniverse
 138     in
 139     { Types.fst = (Joint.set_luniverse g_pars globals def luniverse);
 140     Types.snd = r })
 141
 142 (** val fresh_register :
 143     Joint.params -> AST.ident List.list -> Registers.register
 144     Monad.smax_def__o__monad **)
 145 let fresh_register g_pars globals =
 146   Obj.magic (fun def ->
 147     let { Types.fst = r; Types.snd = runiverse } =
 148       Identifiers.fresh PreIdentifiers.RegisterTag
 149         def.Joint.joint_if_runiverse
 150     in
 151     { Types.fst = (Joint.set_runiverse g_pars globals def runiverse);
 152     Types.snd = r })
 153
 154 (** val adds_graph_pre :
 155     Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
 156     Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
 157     Monad.smax_def__o__monad **)
 158 let rec adds_graph_pre g_pars globals pre_process insts src =
 159   match insts with
 160   | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) src
 161   | List.Cons (i, rest) ->
 162     Monad.m_bind0 (Monad.smax_def State.state_monad)
 163       (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun mid ->
 164       Monad.m_bind0 (Monad.smax_def State.state_monad)
 165         (adds_graph_pre g_pars globals pre_process rest mid) (fun dst ->
 166         Monad.m_bind0 (Monad.smax_def State.state_monad)
 167           (State.state_update
 168             (Joint.add_graph g_pars globals src (Joint.Sequential
 169               ((Joint.Step_seq (pre_process dst i)), (Obj.magic mid)))))
 170           (fun x -> Monad.m_return0 (Monad.smax_def State.state_monad) dst)))
 171
 172 (** val adds_graph_post :
 173     Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
 174     Graphs.label -> Graphs.label Monad.smax_def__o__monad **)
 175 let rec adds_graph_post g_pars globals insts dst =
 176   match insts with
 177   | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) dst
 178   | List.Cons (i, rest) ->
 179     Monad.m_bind0 (Monad.smax_def State.state_monad)
 180       (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun src ->
 181       Monad.m_bind0 (Monad.smax_def State.state_monad)
 182         (adds_graph_post g_pars globals rest dst) (fun mid ->
 183         Monad.m_bind0 (Monad.smax_def State.state_monad)
 184           (State.state_update
 185             (Joint.add_graph g_pars globals src (Joint.Sequential
 186               ((Joint.Step_seq i), mid)))) (fun x ->
 187           Monad.m_return0 (Monad.smax_def State.state_monad) src)))
 188
 189 (** val adds_graph :
 190     Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
 191     Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
 192     Joint.joint_internal_function **)
 193 let adds_graph g_pars globals insts src dst def =
 194   let pref = insts.Types.fst.Types.fst in
 195   let op = insts.Types.fst.Types.snd in
 196   let post = insts.Types.snd in
 197   let { Types.fst = def0; Types.snd = mid } =
 198     Obj.magic adds_graph_pre g_pars globals (fun lbl inst -> inst lbl)
 199       (Obj.magic pref) src def
 200   in
 201   let { Types.fst = def1; Types.snd = mid' } =
 202     Obj.magic adds_graph_post g_pars globals post dst def0
 203   in
 204   Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
 205     mid')) def1
 206
 207 (** val fin_adds_graph :
 208     Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
 209     Graphs.label -> Joint.joint_internal_function ->
 210     Joint.joint_internal_function **)
 211 let fin_adds_graph g_pars globals insts src def =
 212   let pref = insts.Types.fst in
 213   let last = insts.Types.snd in
 214   let { Types.fst = def0; Types.snd = mid } =
 215     Obj.magic adds_graph_pre g_pars globals (fun x i -> i) pref src def
 216   in
 217   Joint.add_graph g_pars globals mid (Joint.Final last) def0
 218
 219 (** val b_adds_graph :
 220     Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
 221     Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
 222     Joint.joint_internal_function **)
 223 let b_adds_graph g_pars globals insts src dst def =
 224   let { Types.fst = def0; Types.snd = stmts } =
 225     Obj.magic Bind_new.bcompile
 226       (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
 227       def
 228   in
 229   adds_graph g_pars globals stmts src dst def0
 230
 231 (** val b_fin_adds_graph :
 232     Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
 233     Graphs.label -> Joint.joint_internal_function ->
 234     Joint.joint_internal_function **)
 235 let b_fin_adds_graph g_pars globals insts src def =
 236   let { Types.fst = def0; Types.snd = stmts } =
 237     Obj.magic Bind_new.bcompile
 238       (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
 239       def
 240   in
 241   fin_adds_graph g_pars globals stmts src def0
 242
 243 (** val step_registers :
 244     Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
 245     Registers.register List.list **)
 246 let step_registers p globals s =
 247   Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s
 248
 249 (** val fin_step_registers :
 250     Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
 251 let fin_step_registers p = function
 252 | Joint.GOTO x -> List.Nil
 253 | Joint.RETURN -> List.Nil
 254 | Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r
 255
 256 type b_graph_translate_data = { init_ret : __; init_params : __;
 257                                 init_stack_size : Nat.nat;
 258                                 added_prologue : Joint.joint_seq List.list;
 259                                 new_regs : Registers.register List.list;
 260                                 f_step : (Graphs.label -> Joint.joint_step ->
 261                                          Blocks.bind_step_block);
 262                                 f_fin : (Graphs.label -> Joint.joint_fin_step
 263                                         -> Blocks.bind_fin_block) }
 264
 265 (** val b_graph_translate_data_rect_Type4 :
 266     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 267     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 268     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 269     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 270     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 271 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18277 =
 272   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 273     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 274     f_step = f_step0; f_fin = f_fin0 } = x_18277
 275   in
 276   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 277     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 278
 279 (** val b_graph_translate_data_rect_Type5 :
 280     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 281     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 282     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 283     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 284     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 285 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18279 =
 286   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 287     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 288     f_step = f_step0; f_fin = f_fin0 } = x_18279
 289   in
 290   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 291     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 292
 293 (** val b_graph_translate_data_rect_Type3 :
 294     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 295     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 296     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 297     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 298     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 299 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18281 =
 300   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 301     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 302     f_step = f_step0; f_fin = f_fin0 } = x_18281
 303   in
 304   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 305     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 306
 307 (** val b_graph_translate_data_rect_Type2 :
 308     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 309     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 310     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 311     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 312     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 313 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18283 =
 314   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 315     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 316     f_step = f_step0; f_fin = f_fin0 } = x_18283
 317   in
 318   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 319     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 320
 321 (** val b_graph_translate_data_rect_Type1 :
 322     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 323     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 324     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 325     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 326     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 327 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18285 =
 328   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 329     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 330     f_step = f_step0; f_fin = f_fin0 } = x_18285
 331   in
 332   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 333     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 334
 335 (** val b_graph_translate_data_rect_Type0 :
 336     Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 337     __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
 338     List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
 339     -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
 340     -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
 341 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18287 =
 342   let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
 343     init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
 344     f_step = f_step0; f_fin = f_fin0 } = x_18287
 345   in
 346   h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
 347     added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
 348
 349 (** val init_ret :
 350     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 351     b_graph_translate_data -> __ **)
 352 let rec init_ret src dst globals xxx =
 353   xxx.init_ret
 354
 355 (** val init_params :
 356     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 357     b_graph_translate_data -> __ **)
 358 let rec init_params src dst globals xxx =
 359   xxx.init_params
 360
 361 (** val init_stack_size :
 362     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 363     b_graph_translate_data -> Nat.nat **)
 364 let rec init_stack_size src dst globals xxx =
 365   xxx.init_stack_size
 366
 367 (** val added_prologue :
 368     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 369     b_graph_translate_data -> Joint.joint_seq List.list **)
 370 let rec added_prologue src dst globals xxx =
 371   xxx.added_prologue
 372
 373 (** val new_regs :
 374     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 375     b_graph_translate_data -> Registers.register List.list **)
 376 let rec new_regs src dst globals xxx =
 377   xxx.new_regs
 378
 379 (** val f_step :
 380     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 381     b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
 382     Blocks.bind_step_block **)
 383 let rec f_step src dst globals xxx =
 384   xxx.f_step
 385
 386 (** val f_fin :
 387     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 388     b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
 389     Blocks.bind_fin_block **)
 390 let rec f_fin src dst globals xxx =
 391   xxx.f_fin
 392
 393 (** val b_graph_translate_data_inv_rect_Type4 :
 394     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 395     b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
 396     List.list -> Registers.register List.list -> (Graphs.label ->
 397     Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
 398     Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
 399     __ -> 'a1) -> 'a1 **)
 400 let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
 401   let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __
 402
 403 (** val b_graph_translate_data_inv_rect_Type3 :
 404     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 405     b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
 406     List.list -> Registers.register List.list -> (Graphs.label ->
 407     Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
 408     Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
 409     __ -> 'a1) -> 'a1 **)
 410 let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
 411   let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __
 412
 413 (** val b_graph_translate_data_inv_rect_Type2 :
 414     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 415     b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
 416     List.list -> Registers.register List.list -> (Graphs.label ->
 417     Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
 418     Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
 419     __ -> 'a1) -> 'a1 **)
 420 let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
 421   let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __
 422
 423 (** val b_graph_translate_data_inv_rect_Type1 :
 424     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 425     b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
 426     List.list -> Registers.register List.list -> (Graphs.label ->
 427     Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
 428     Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
 429     __ -> 'a1) -> 'a1 **)
 430 let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
 431   let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __
 432
 433 (** val b_graph_translate_data_inv_rect_Type0 :
 434     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 435     b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
 436     List.list -> Registers.register List.list -> (Graphs.label ->
 437     Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
 438     Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
 439     __ -> 'a1) -> 'a1 **)
 440 let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
 441   let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __
 442
 443 (** val b_graph_translate_data_jmdiscr :
 444     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 445     b_graph_translate_data -> b_graph_translate_data -> __ **)
 446 let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
 447   Logic.eq_rect_Type2 x
 448     (let { init_ret = a0; init_params = a10; init_stack_size = a20;
 449        added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
 450      in
 451     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
 452
 453 type bound_b_graph_translate_data =
 454   (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
 455
 456 (** val get_first_costlabel_next :
 457     Joint.params -> AST.ident List.list ->
 458     Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
 459     Types.prod **)
 460 let get_first_costlabel_next p g def =
 461   (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
 462            (Types.pi1 def).Joint.joint_if_entry with
 463    | Types.None -> (fun _ -> assert false (* absurd case *))
 464    | Types.Some s ->
 465      (match s with
 466       | Joint.Sequential (s', nxt) ->
 467         (match s' with
 468          | Joint.COST_LABEL c ->
 469            (fun _ -> { Types.fst = c; Types.snd = nxt })
 470          | Joint.CALL (x, x0, x1) ->
 471            (fun _ -> assert false (* absurd case *))
 472          | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
 473          | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
 474       | Joint.Final x -> (fun _ -> assert false (* absurd case *))
 475       | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
 476     __
 477
 478 (** val get_first_costlabel :
 479     Joint.params -> AST.ident List.list ->
 480     Joint.joint_closed_internal_function -> CostLabel.costlabel **)
 481 let get_first_costlabel p g f =
 482   (get_first_costlabel_next p g f).Types.fst
 483
 484 (** val not_emptyb : 'a1 List.list -> Bool.bool **)
 485 let not_emptyb = function
 486 | List.Nil -> Bool.False
 487 | List.Cons (x, x0) -> Bool.True
 488
 489 (** val b_graph_translate_props_rect_Type4 :
 490     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 491     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 492     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 493     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 494     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 495 let rec b_graph_translate_props_rect_Type4 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 496   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 497
 498 (** val b_graph_translate_props_rect_Type5 :
 499     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 500     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 501     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 502     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 503     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 504 let rec b_graph_translate_props_rect_Type5 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 505   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 506
 507 (** val b_graph_translate_props_rect_Type3 :
 508     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 509     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 510     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 511     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 512     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 513 let rec b_graph_translate_props_rect_Type3 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 514   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 515
 516 (** val b_graph_translate_props_rect_Type2 :
 517     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 518     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 519     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 520     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 521     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 522 let rec b_graph_translate_props_rect_Type2 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 523   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 524
 525 (** val b_graph_translate_props_rect_Type1 :
 526     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 527     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 528     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 529     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 530     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 531 let rec b_graph_translate_props_rect_Type1 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 532   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 533
 534 (** val b_graph_translate_props_rect_Type0 :
 535     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 536     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 537     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 538     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 539     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 540 let rec b_graph_translate_props_rect_Type0 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
 541   h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
 542
 543 (** val b_graph_translate_props_inv_rect_Type4 :
 544     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 545     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 546     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 547     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 548     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 549     'a1 **)
 550 let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
 551   let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
 552   hcut __
 553
 554 (** val b_graph_translate_props_inv_rect_Type3 :
 555     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 556     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 557     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 558     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 559     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 560     'a1 **)
 561 let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
 562   let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
 563   hcut __
 564
 565 (** val b_graph_translate_props_inv_rect_Type2 :
 566     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 567     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 568     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 569     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 570     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 571     'a1 **)
 572 let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
 573   let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
 574   hcut __
 575
 576 (** val b_graph_translate_props_inv_rect_Type1 :
 577     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 578     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 579     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 580     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 581     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 582     'a1 **)
 583 let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
 584   let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
 585   hcut __
 586
 587 (** val b_graph_translate_props_inv_rect_Type0 :
 588     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 589     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 590     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 591     List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 592     -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 593     'a1 **)
 594 let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
 595   let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
 596   hcut __
 597
 598 (** val b_graph_translate_props_jmdiscr :
 599     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 600     b_graph_translate_data -> Joint.joint_closed_internal_function ->
 601     Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 602     List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
 603 let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
 604   Logic.eq_rect_Type2 __
 605     (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
 606
 607 (** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
 608 let pair_swap pr =
 609   { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
 610
 611 (** val set_entry :
 612     AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
 613     __ -> Joint.joint_internal_function **)
 614 let set_entry globals pars int_fun entry =
 615   { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
 616     Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
 617     Joint.joint_if_result = int_fun.Joint.joint_if_result;
 618     Joint.joint_if_params = int_fun.Joint.joint_if_params;
 619     Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
 620     Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
 621     Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
 622     entry }
 623
 624 (** val b_graph_translate :
 625     Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 626     bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
 627     Joint.joint_closed_internal_function Types.sig0 **)
 628 let b_graph_translate src_g_pars dst_g_pars globals data def =
 629   let runiv_data =
 630     Obj.magic Bind_new.bcompile
 631       (Obj.magic
 632         (Relations.compose pair_swap
 633           (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
 634       (Types.pi1 def).Joint.joint_if_runiverse
 635   in
 636   let runiv = runiv_data.Types.fst in
 637   let data0 = runiv_data.Types.snd in
 638   let entry = (Types.pi1 def).Joint.joint_if_entry in
 639   let init = { Joint.joint_if_luniverse =
 640     (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
 641     runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
 642     data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
 643     Joint.joint_if_local_stacksize =
 644     (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
 645     (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
 646     Joint.joint_if_entry = entry }
 647   in
 648   let f = fun lbl stmt def0 ->
 649     match stmt with
 650     | Joint.Sequential (inst, next) ->
 651       b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
 652         (Obj.magic next) def0
 653     | Joint.Final inst ->
 654       b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
 655     | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
 656   in
 657   let def_out =
 658     Identifiers.foldi PreIdentifiers.LabelTag f
 659       (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
 660   in
 661   let prologue = data0.added_prologue in
 662   let def_out0 =
 663     match not_emptyb prologue with
 664     | Bool.True ->
 665       let { Types.fst = init_c; Types.snd = nxt } =
 666         get_first_costlabel_next (Joint.graph_params_to_params src_g_pars)
 667           globals def
 668       in
 669       let def_out0 =
 670         Joint.add_graph dst_g_pars globals (Obj.magic entry)
 671           (Joint.Sequential ((Joint.Step_seq
 672           (Joint.nOOP
 673             (Joint.uns_pars__o__u_pars
 674               (Joint.gp_to_p__o__stmt_pars dst_g_pars)) globals)), nxt))
 675           def_out
 676       in
 677       let { Types.fst = def_out1; Types.snd = entry' } =
 678         Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
 679           globals def_out0
 680       in
 681       let def_out2 =
 682         adds_graph dst_g_pars globals { Types.fst = { Types.fst = List.Nil;
 683           Types.snd = (fun x -> Joint.COST_LABEL init_c) }; Types.snd =
 684           prologue } entry' (Obj.magic entry) def_out1
 685       in
 686       set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out2
 687         (Obj.magic entry')
 688     | Bool.False -> def_out
 689   in
 690   def_out0
 691
 692 (** val b_graph_transform_program :
 693     Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
 694     Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
 695     Joint.joint_program -> Joint.joint_program **)
 696 let b_graph_transform_program src dst init =
 697   Joint.transform_joint_program (Joint.graph_params_to_params src)
 698     (Joint.graph_params_to_params dst) (fun varnames def_in ->
 699     Types.pi1
 700       (b_graph_translate src dst varnames (init varnames def_in) def_in))
 701
 702 (** val added_registers :
 703     Joint.graph_params -> AST.ident List.list ->
 704     Joint.joint_internal_function -> (Graphs.label -> Registers.register
 705     List.list) -> Registers.register List.list **)
 706 let added_registers p g def f_regs =
 707   let f = fun lbl x acc -> List.append (f_regs lbl) acc in
 708   Identifiers.foldi PreIdentifiers.LabelTag f
 709     (Obj.magic def.Joint.joint_if_code) List.Nil
 710