open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open Joint_LTL_LIN

open LTL

open Fixpoints

open Set_adt

open ERTL

open Liveness

open Interference

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

(** val dpi1__o__Reg_to_dec__o__inject :
    (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
let dpi1__o__Reg_to_dec__o__inject x2 =
  Interference.Decision_colour x2.Types.dpi1

(** val eject__o__Reg_to_dec__o__inject :
    I8051.register Types.sig0 -> Interference.decision Types.sig0 **)
let eject__o__Reg_to_dec__o__inject x2 =
  Interference.Decision_colour (Types.pi1 x2)

(** val reg_to_dec__o__inject :
    I8051.register -> Interference.decision Types.sig0 **)
let reg_to_dec__o__inject x1 =
  Interference.Decision_colour x1

(** val dpi1__o__Reg_to_dec :
    (I8051.register, 'a1) Types.dPair -> Interference.decision **)
let dpi1__o__Reg_to_dec x1 =
  Interference.Decision_colour x1.Types.dpi1

(** val eject__o__Reg_to_dec :
    I8051.register Types.sig0 -> Interference.decision **)
let eject__o__Reg_to_dec x1 =
  Interference.Decision_colour (Types.pi1 x1)

type arg_decision =
| Arg_decision_colour of I8051.register
| Arg_decision_spill of Nat.nat
| Arg_decision_imm of BitVector.byte

(** val arg_decision_rect_Type4 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19045 -> h_arg_decision_colour x_19045
| Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
| Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047

(** val arg_decision_rect_Type5 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19052 -> h_arg_decision_colour x_19052
| Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
| Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054

(** val arg_decision_rect_Type3 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19059 -> h_arg_decision_colour x_19059
| Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
| Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061

(** val arg_decision_rect_Type2 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19066 -> h_arg_decision_colour x_19066
| Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
| Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068

(** val arg_decision_rect_Type1 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19073 -> h_arg_decision_colour x_19073
| Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
| Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075

(** val arg_decision_rect_Type0 :
    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
    arg_decision -> 'a1 **)
let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
| Arg_decision_colour x_19080 -> h_arg_decision_colour x_19080
| Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
| Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082

(** val arg_decision_inv_rect_Type4 :
    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
let arg_decision_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = arg_decision_rect_Type4 h1 h2 h3 hterm in hcut __

(** val arg_decision_inv_rect_Type3 :
    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
let arg_decision_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = arg_decision_rect_Type3 h1 h2 h3 hterm in hcut __

(** val arg_decision_inv_rect_Type2 :
    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
let arg_decision_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = arg_decision_rect_Type2 h1 h2 h3 hterm in hcut __

(** val arg_decision_inv_rect_Type1 :
    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
let arg_decision_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = arg_decision_rect_Type1 h1 h2 h3 hterm in hcut __

(** val arg_decision_inv_rect_Type0 :
    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
let arg_decision_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = arg_decision_rect_Type0 h1 h2 h3 hterm in hcut __

(** val arg_decision_discr : arg_decision -> arg_decision -> __ **)
let arg_decision_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
     | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
     | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val arg_decision_jmdiscr : arg_decision -> arg_decision -> __ **)
let arg_decision_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
     | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
     | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val dpi1__o__Reg_to_arg_dec__o__inject :
    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
let dpi1__o__Reg_to_arg_dec__o__inject x2 =
  Arg_decision_colour x2.Types.dpi1

(** val eject__o__Reg_to_arg_dec__o__inject :
    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
let eject__o__Reg_to_arg_dec__o__inject x2 =
  Arg_decision_colour (Types.pi1 x2)

(** val reg_to_arg_dec__o__inject :
    I8051.register -> arg_decision Types.sig0 **)
let reg_to_arg_dec__o__inject x1 =
  Arg_decision_colour x1

(** val dpi1__o__Reg_to_arg_dec :
    (I8051.register, 'a1) Types.dPair -> arg_decision **)
let dpi1__o__Reg_to_arg_dec x1 =
  Arg_decision_colour x1.Types.dpi1

(** val eject__o__Reg_to_arg_dec :
    I8051.register Types.sig0 -> arg_decision **)
let eject__o__Reg_to_arg_dec x1 =
  Arg_decision_colour (Types.pi1 x1)

(** val preserve_carry_bit :
    AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
    Joint.joint_seq List.list **)
let preserve_carry_bit globals do_it steps =
  match do_it with
  | Bool.True ->
    List.Cons ((Joint.Extension_seq (Obj.magic Joint_LTL_LIN.SAVE_CARRY)),
      (List.append steps (List.Cons ((Joint.Extension_seq
        (Obj.magic Joint_LTL_LIN.RESTORE_CARRY)), List.Nil))))
  | Bool.False -> steps

(** val a : Types.unit0 **)
let a =
  Types.It

(** val dpi1__o__beval_of_byte__o__inject :
    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
let dpi1__o__beval_of_byte__o__inject x2 =
  ByteValues.BVByte x2.Types.dpi1

(** val eject__o__beval_of_byte__o__inject :
    BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **)
let eject__o__beval_of_byte__o__inject x2 =
  ByteValues.BVByte (Types.pi1 x2)

(** val beval_of_byte__o__inject :
    BitVector.byte -> ByteValues.beval Types.sig0 **)
let beval_of_byte__o__inject x1 =
  ByteValues.BVByte x1

(** val dpi1__o__beval_of_byte :
    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **)
let dpi1__o__beval_of_byte x1 =
  ByteValues.BVByte x1.Types.dpi1

(** val eject__o__beval_of_byte :
    BitVector.byte Types.sig0 -> ByteValues.beval **)
let eject__o__beval_of_byte x1 =
  ByteValues.BVByte (Types.pi1 x1)

(** val set_dp_by_offset :
    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
let set_dp_by_offset globals off =
  List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, (Joint.byte_of_nat off))))),
    (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPL)))), (List.Cons
    ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPL, a)))), (List.Cons
    ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))), (List.Cons
    ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPH)))), (List.Cons
    ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPH, a)))),
    List.Nil)))))))))))

(** val get_stack :
    AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
    Joint.joint_seq List.list **)
let get_stack globals localss r off =
  let off0 = Nat.plus localss off in
  List.append (set_dp_by_offset globals off0)
    (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
      (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
      (match I8051.eq_Register r I8051.RegisterA with
       | Bool.True -> List.Nil
       | Bool.False ->
         List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))),
           List.Nil)))

(** val set_stack_not_a :
    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
    Joint.joint_seq List.list **)
let set_stack_not_a globals localss off r =
  let off0 = Nat.plus localss off in
  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
    ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
    List.Nil))))

(** val set_stack_a :
    AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list **)
let set_stack_a globals localss off =
  List.append (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
    (set_stack_not_a globals localss off I8051.registerST1)

(** val set_stack :
    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
    Joint.joint_seq List.list **)
let set_stack globals localss off r =
  match I8051.eq_Register r I8051.RegisterA with
  | Bool.True -> set_stack_a globals localss off
  | Bool.False -> set_stack_not_a globals localss off r

(** val set_stack_int :
    AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
    Joint.joint_seq List.list **)
let set_stack_int globals localss off int =
  let off0 = Nat.plus localss off in
  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
    ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
    (Obj.magic a))), List.Nil))))

(** val move :
    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
    arg_decision -> Joint.joint_seq List.list **)
let move globals localss carry_lives_after dst src =
  match dst with
  | Interference.Decision_spill dsto ->
    (match src with
     | Arg_decision_colour srcr ->
       preserve_carry_bit globals carry_lives_after
         (set_stack globals localss dsto srcr)
     | Arg_decision_spill srco ->
       (match Nat.eqb srco dsto with
        | Bool.True -> List.Nil
        | Bool.False ->
          preserve_carry_bit globals carry_lives_after
            (List.append (get_stack globals localss I8051.RegisterA srco)
              (set_stack globals localss dsto I8051.RegisterA)))
     | Arg_decision_imm int ->
       preserve_carry_bit globals carry_lives_after
         (set_stack_int globals localss dsto int))
  | Interference.Decision_colour dstr ->
    (match src with
     | Arg_decision_colour srcr ->
       (match I8051.eq_Register dstr srcr with
        | Bool.True -> List.Nil
        | Bool.False ->
          (match I8051.eq_Register dstr I8051.RegisterA with
           | Bool.True ->
             List.Cons ((Joint.MOVE
               (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil)
           | Bool.False ->
             (match I8051.eq_Register srcr I8051.RegisterA with
              | Bool.True ->
                List.Cons ((Joint.MOVE
                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)
              | Bool.False ->
                List.Cons ((Joint.MOVE
                  (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons
                  ((Joint.MOVE
                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))),
                  List.Nil))))))
     | Arg_decision_spill srco ->
       preserve_carry_bit globals carry_lives_after
         (get_stack globals localss dstr srco)
     | Arg_decision_imm int ->
       List.append (List.Cons ((Joint.MOVE
         (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
         (match I8051.eq_Register dstr I8051.RegisterA with
          | Bool.True -> List.Nil
          | Bool.False ->
            List.Cons ((Joint.MOVE
              (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)))

(** val arg_is_spilled : arg_decision -> Bool.bool **)
let arg_is_spilled = function
| Arg_decision_colour x0 -> Bool.False
| Arg_decision_spill x0 -> Bool.True
| Arg_decision_imm x0 -> Bool.False

(** val is_spilled : Interference.decision -> Bool.bool **)
let is_spilled = function
| Interference.Decision_spill x0 -> Bool.True
| Interference.Decision_colour x0 -> Bool.False

(** val newframe :
    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
let newframe globals stack_sz =
  List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
    (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
    (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
    ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
    List.Nil)))))))))))))

(** val delframe :
    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
let delframe globals stack_sz =
  List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
    ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
    (List.Cons ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
    ((Joint.MOVE
    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
    List.Nil)))))))))))

(** val commutative : BackEndOps.op2 -> Bool.bool **)
let commutative = function
| BackEndOps.Add -> Bool.True
| BackEndOps.Addc -> Bool.True
| BackEndOps.Sub -> Bool.False
| BackEndOps.And -> Bool.True
| BackEndOps.Or -> Bool.True
| BackEndOps.Xor -> Bool.True

(** val uses_carry : BackEndOps.op2 -> Bool.bool **)
let uses_carry = function
| BackEndOps.Add -> Bool.False
| BackEndOps.Addc -> Bool.True
| BackEndOps.Sub -> Bool.True
| BackEndOps.And -> Bool.False
| BackEndOps.Or -> Bool.False
| BackEndOps.Xor -> Bool.False

(** val sets_carry : BackEndOps.op2 -> Bool.bool **)
let sets_carry = function
| BackEndOps.Add -> Bool.True
| BackEndOps.Addc -> Bool.True
| BackEndOps.Sub -> Bool.True
| BackEndOps.And -> Bool.False
| BackEndOps.Or -> Bool.False
| BackEndOps.Xor -> Bool.False

(** val translate_op2 :
    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    List.list **)
let translate_op2 globals localss carry_lives_after op dst arg1 arg2 =
  List.append
    (preserve_carry_bit globals
      (Bool.andb (uses_carry op)
        (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
      (List.append
        (move globals localss Bool.False (Interference.Decision_colour
          I8051.RegisterB) arg2)
        (move globals localss Bool.False (Interference.Decision_colour
          I8051.RegisterA) arg1)))
    (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
      (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst
        (Arg_decision_colour I8051.RegisterA)))

(** val translate_op2_smart :
    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    List.list **)
let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 =
  preserve_carry_bit globals
    (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
      (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
        (is_spilled dst)))
    (match arg2 with
     | Arg_decision_colour arg2r ->
       List.append
         (move globals localss (uses_carry op) (Interference.Decision_colour
           I8051.RegisterA) arg1)
         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
           List.Nil))
           (move globals localss
             (Bool.andb (sets_carry op) carry_lives_after) dst
             (Arg_decision_colour I8051.RegisterA)))
     | Arg_decision_spill x ->
       (match commutative op with
        | Bool.True ->
          (match arg1 with
           | Arg_decision_colour arg1r ->
             List.append
               (move globals localss (uses_carry op)
                 (Interference.Decision_colour I8051.RegisterA) arg2)
               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
                 (Obj.magic a),
                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
                 List.Nil))
                 (move globals localss
                   (Bool.andb (sets_carry op) carry_lives_after) dst
                   (Arg_decision_colour I8051.RegisterA)))
           | Arg_decision_spill x0 ->
             translate_op2 globals localss carry_lives_after op dst arg1 arg2
           | Arg_decision_imm arg1i ->
             List.append
               (move globals localss (uses_carry op)
                 (Interference.Decision_colour I8051.RegisterA) arg2)
               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
                 (Obj.magic a),
                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
                 List.Nil))
                 (move globals localss
                   (Bool.andb (sets_carry op) carry_lives_after) dst
                   (Arg_decision_colour I8051.RegisterA))))
        | Bool.False ->
          translate_op2 globals localss carry_lives_after op dst arg1 arg2)
     | Arg_decision_imm arg2i ->
       List.append
         (move globals localss (uses_carry op) (Interference.Decision_colour
           I8051.RegisterA) arg1)
         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
           List.Nil))
           (move globals localss
             (Bool.andb (sets_carry op) carry_lives_after) dst
             (Arg_decision_colour I8051.RegisterA))))

(** val dec_to_arg_dec : Interference.decision -> arg_decision **)
let dec_to_arg_dec = function
| Interference.Decision_spill n -> Arg_decision_spill n
| Interference.Decision_colour r -> Arg_decision_colour r

(** val reg_to_dec__o__dec_arg_dec__o__inject :
    I8051.register -> arg_decision Types.sig0 **)
let reg_to_dec__o__dec_arg_dec__o__inject x0 =
  dec_to_arg_dec (Interference.Decision_colour x0)

(** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
  dec_to_arg_dec (dpi1__o__Reg_to_dec x2)

(** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
  dec_to_arg_dec (eject__o__Reg_to_dec x2)

(** val dpi1__o__dec_arg_dec__o__inject :
    (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
let dpi1__o__dec_arg_dec__o__inject x2 =
  dec_to_arg_dec x2.Types.dpi1

(** val eject__o__dec_arg_dec__o__inject :
    Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
let eject__o__dec_arg_dec__o__inject x2 =
  dec_to_arg_dec (Types.pi1 x2)

(** val dec_arg_dec__o__inject :
    Interference.decision -> arg_decision Types.sig0 **)
let dec_arg_dec__o__inject x1 =
  dec_to_arg_dec x1

(** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
let reg_to_dec__o__dec_arg_dec x0 =
  dec_to_arg_dec (Interference.Decision_colour x0)

(** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
    (I8051.register, 'a1) Types.dPair -> arg_decision **)
let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
  dec_to_arg_dec (dpi1__o__Reg_to_dec x1)

(** val eject__o__Reg_to_dec__o__dec_arg_dec :
    I8051.register Types.sig0 -> arg_decision **)
let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
  dec_to_arg_dec (eject__o__Reg_to_dec x1)

(** val dpi1__o__dec_arg_dec :
    (Interference.decision, 'a1) Types.dPair -> arg_decision **)
let dpi1__o__dec_arg_dec x1 =
  dec_to_arg_dec x1.Types.dpi1

(** val eject__o__dec_arg_dec :
    Interference.decision Types.sig0 -> arg_decision **)
let eject__o__dec_arg_dec x1 =
  dec_to_arg_dec (Types.pi1 x1)

(** val translate_op1 :
    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
    Interference.decision -> Interference.decision -> Joint.joint_seq
    List.list **)
let translate_op1 globals localss carry_lives_after op dst arg =
  let preserve_carry =
    Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
  in
  preserve_carry_bit globals preserve_carry
    (List.append
      (move globals localss Bool.False (Interference.Decision_colour
        I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
      (Obj.magic Types.It), (Obj.magic Types.It))),
      (move globals localss Bool.False dst (Arg_decision_colour
        I8051.RegisterA)))))

(** val translate_opaccs :
    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
    Interference.decision -> Interference.decision -> arg_decision ->
    arg_decision -> Joint.joint_seq List.list **)
let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 =
  List.append
    (move globals localss Bool.False (Interference.Decision_colour
      I8051.RegisterB) arg2)
    (List.append
      (move globals localss Bool.False (Interference.Decision_colour
        I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op,
      (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It),
      (Obj.magic Types.It))),
      (List.append
        (move globals localss Bool.False dst1 (Arg_decision_colour
          I8051.RegisterA))
        (List.append
          (move globals localss Bool.False dst2 (Arg_decision_colour
            I8051.RegisterB))
          (match Bool.andb carry_lives_after
                   (Bool.orb (is_spilled dst1) (is_spilled dst2)) with
           | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
           | Bool.False -> List.Nil))))))

(** val move_to_dp :
    AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
    Joint.joint_seq List.list **)
let move_to_dp globals localss arg1 arg2 =
  match Bool.notb (arg_is_spilled arg1) with
  | Bool.True ->
    List.append
      (move globals localss Bool.False (Interference.Decision_colour
        I8051.RegisterDPH) arg2)
      (move globals localss Bool.False (Interference.Decision_colour
        I8051.RegisterDPL) arg1)
  | Bool.False ->
    (match Bool.notb (arg_is_spilled arg2) with
     | Bool.True ->
       List.append
         (move globals localss Bool.False (Interference.Decision_colour
           I8051.RegisterDPL) arg1)
         (move globals localss Bool.False (Interference.Decision_colour
           I8051.RegisterDPH) arg2)
     | Bool.False ->
       List.append
         (move globals localss Bool.False (Interference.Decision_colour
           I8051.RegisterB) arg1)
         (List.append
           (move globals localss Bool.False (Interference.Decision_colour
             I8051.RegisterDPH) arg2)
           (move globals localss Bool.False (Interference.Decision_colour
             I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))

(** val translate_store :
    AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision ->
    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
let translate_store globals localss carry_lives_after addr1 addr2 src =
  preserve_carry_bit globals
    (Bool.andb carry_lives_after
      (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
        (arg_is_spilled src)))
    (let move_to_dptr = move_to_dp globals localss addr1 addr2 in
    List.append
      (match arg_is_spilled src with
       | Bool.True ->
         List.append
           (move globals localss Bool.False (Interference.Decision_colour
             I8051.registerST0) src)
           (List.append move_to_dptr (List.Cons ((Joint.MOVE
             (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
             List.Nil)))
       | Bool.False ->
         List.append move_to_dptr
           (move globals localss Bool.False (Interference.Decision_colour
             I8051.RegisterA) src)) (List.Cons ((Joint.STORE
      ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
      List.Nil)))

(** val translate_load :
    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
let translate_load globals localss carry_lives_after dst addr1 addr2 =
  preserve_carry_bit globals
    (Bool.andb carry_lives_after
      (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
        (arg_is_spilled addr1)))
    (List.append (move_to_dp globals localss addr1 addr2)
      (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
        (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
        (move globals localss Bool.False dst (Arg_decision_colour
          I8051.RegisterA))))

(** val translate_address :
    __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
    Interference.decision -> Interference.decision -> Joint.joint_seq
    List.list **)
let translate_address globals localss carry_lives_after id off addr1 addr2 =
  preserve_carry_bit (Obj.magic globals)
    (Bool.andb carry_lives_after
      (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
    ((Joint.ADDRESS ((Obj.magic id), off, (Obj.magic Types.It),
    (Obj.magic Types.It))),
    (List.append
      (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
        I8051.RegisterDPL))
      (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
        I8051.RegisterDPH)))))

(** val translate_step :
    AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
    Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
    Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
let translate_step globals fn localss after grph stack_sz lbl s =
  Bind_new.Bret
    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
    let lookup_arg = fun a0 ->
      match a0 with
      | Joint.Reg r -> dec_to_arg_dec (lookup r)
      | Joint.Imm b -> Arg_decision_imm b
    in
    let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
    in
    let move0 = move globals localss carry_lives_after in
    (match Liveness.eliminable_step globals (after lbl) s with
     | Bool.True ->
       let x =
         Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
           globals List.Nil
       in
       x
     | Bool.False ->
       (match s with
        | Joint.COST_LABEL cost_lbl ->
          { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
            Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
        | Joint.CALL (f, n_args, x) ->
          (match f with
           | Types.Inl f0 ->
             { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
               Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
               Types.snd = List.Nil }
           | Types.Inr dp ->
             let { Types.fst = dpl; Types.snd = dph } = dp in
             { Types.fst = { Types.fst =
             (List.append
               (Blocks.add_dummy_variance
                 (move_to_dp globals localss (Obj.magic lookup_arg dpl)
                   (Obj.magic lookup_arg dph))) (List.Cons ((fun l ->
               let x0 = Joint.Extension_seq
                 (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (Obj.magic l)))
               in
               x0), (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
               (List.Cons ((fun l -> Joint.Extension_seq
               (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (Obj.magic l)))),
               (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
               (List.Cons ((fun x0 -> Joint.MOVE
               (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))),
               List.Nil))))))))))); Types.snd = (fun x0 -> Joint.CALL
             ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
             (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
             Types.snd = List.Nil })
        | Joint.COND (r, ltrue) ->
          { Types.fst = { Types.fst =
            (Blocks.add_dummy_variance
              (move0 (Interference.Decision_colour I8051.RegisterA)
                (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd =
            (fun x -> Joint.COND ((Obj.magic Types.It), ltrue)) };
            Types.snd = List.Nil }
        | Joint.Step_seq s' ->
          (match s' with
           | Joint.COMMENT c ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals (List.Cons ((Joint.COMMENT c), List.Nil))
           | Joint.MOVE pair_regs ->
             let lookup_move_dst = fun x ->
               match x with
               | ERTL.PSD r -> lookup r
               | ERTL.HDW r -> Interference.Decision_colour r
             in
             let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
             let src =
               match (Obj.magic pair_regs).Types.snd with
               | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
               | Joint.Imm b -> Arg_decision_imm b
             in
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals (move0 dst src)
           | Joint.POP r ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals (List.Cons ((Joint.POP (Obj.magic a)),
               (move0 (Obj.magic lookup r) (Arg_decision_colour
                 I8051.RegisterA))))
           | Joint.PUSH a0 ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (List.append
                 (move0 (Interference.Decision_colour I8051.RegisterA)
                   (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
                 (Obj.magic a)), List.Nil)))
           | Joint.ADDRESS (lbl0, off, dpl, dph) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_address (Obj.magic globals) localss
                 carry_lives_after (Obj.magic lbl0) off
                 (Obj.magic lookup dpl) (Obj.magic lookup dph))
           | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_opaccs globals localss carry_lives_after op
                 (Obj.magic lookup dst1) (Obj.magic lookup dst2)
                 (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
           | Joint.OP1 (op, dst, arg) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_op1 globals localss carry_lives_after op
                 (Obj.magic lookup dst) (Obj.magic lookup arg))
           | Joint.OP2 (op, dst, arg1, arg2) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_op2_smart globals localss carry_lives_after op
                 (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
                 (Obj.magic lookup_arg arg2))
           | Joint.CLEAR_CARRY ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
           | Joint.SET_CARRY ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals (List.Cons (Joint.SET_CARRY, List.Nil))
           | Joint.LOAD (dstr, addr1, addr2) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_load globals localss carry_lives_after
                 (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
                 (Obj.magic lookup_arg addr2))
           | Joint.STORE (addr1, addr2, srcr) ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (translate_store globals localss carry_lives_after
                 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
                 (Obj.magic lookup_arg srcr))
           | Joint.Extension_seq ext ->
             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
               globals
               (match Obj.magic ext with
                | ERTL.Ertl_new_frame -> newframe globals stack_sz
                | ERTL.Ertl_del_frame -> delframe globals stack_sz
                | ERTL.Ertl_frame_size r ->
                  move0 (lookup r) (Arg_decision_imm
                    (Joint.byte_of_nat stack_sz)))))))

(** val translate_fin_step :
    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
    Blocks.bind_fin_block **)
let translate_fin_step globals lbl s =
  Bind_new.Bret { Types.fst = List.Nil; Types.snd =
    (match s with
     | Joint.GOTO l -> Joint.GOTO l
     | Joint.RETURN -> Joint.RETURN
     | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }

(** val translate_data :
    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
    AST.ident List.list -> Joint.joint_closed_internal_function ->
    (Registers.register, TranslateUtils.b_graph_translate_data)
    Bind_new.bind_new **)
let translate_data the_fixpoint build globals int_fun =
  let after =
    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
  in
  let coloured_graph =
    build globals (Types.pi1 int_fun)
      (Fixpoints.fix_lfp Liveness.register_lattice
        (Liveness.liveafter globals (Types.pi1 int_fun)) after)
  in
  let stack_sz =
    Nat.plus coloured_graph.Interference.spilled_no
      (Types.pi1 int_fun).Joint.joint_if_stacksize
  in
  Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
  TranslateUtils.init_params = (Obj.magic Types.It);
  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
  List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
  (translate_step globals (Types.pi1 int_fun)
    (Types.pi1 int_fun).Joint.joint_if_local_stacksize
    (Fixpoints.fix_lfp Liveness.register_lattice
      (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph
    stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) }

(** val ertl_to_ltl :
    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
    ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model)
    Types.prod, Nat.nat) Types.prod **)
let ertl_to_ltl the_fixpoint build pr =
  let ltlprog =
    TranslateUtils.b_graph_transform_program ERTL.eRTL LTL.lTL
      (fun globals h -> translate_data the_fixpoint build globals h) pr
  in
  { Types.fst = { Types.fst = ltlprog; Types.snd =
  (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
  Types.snd =
  (Nat.minus
    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))))))))))
    (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }