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

val eject__o__Reg_to_dec__o__inject :
  I8051.register Types.sig0 -> Interference.decision Types.sig0

val reg_to_dec__o__inject :
  I8051.register -> Interference.decision Types.sig0

val dpi1__o__Reg_to_dec :
  (I8051.register, 'a1) Types.dPair -> Interference.decision

val eject__o__Reg_to_dec : I8051.register Types.sig0 -> Interference.decision

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

val arg_decision_rect_Type5 :
  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
  arg_decision -> 'a1

val arg_decision_rect_Type3 :
  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
  arg_decision -> 'a1

val arg_decision_rect_Type2 :
  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
  arg_decision -> 'a1

val arg_decision_rect_Type1 :
  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
  arg_decision -> 'a1

val arg_decision_rect_Type0 :
  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
  arg_decision -> 'a1

val arg_decision_inv_rect_Type4 :
  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> 'a1

val arg_decision_inv_rect_Type3 :
  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> 'a1

val arg_decision_inv_rect_Type2 :
  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> 'a1

val arg_decision_inv_rect_Type1 :
  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> 'a1

val arg_decision_inv_rect_Type0 :
  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
  (BitVector.byte -> __ -> 'a1) -> 'a1

val arg_decision_discr : arg_decision -> arg_decision -> __

val arg_decision_jmdiscr : arg_decision -> arg_decision -> __

val dpi1__o__Reg_to_arg_dec__o__inject :
  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0

val eject__o__Reg_to_arg_dec__o__inject :
  I8051.register Types.sig0 -> arg_decision Types.sig0

val reg_to_arg_dec__o__inject : I8051.register -> arg_decision Types.sig0

val dpi1__o__Reg_to_arg_dec :
  (I8051.register, 'a1) Types.dPair -> arg_decision

val eject__o__Reg_to_arg_dec : I8051.register Types.sig0 -> arg_decision

val preserve_carry_bit :
  AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
  Joint.joint_seq List.list

val a : Types.unit0

val dpi1__o__beval_of_byte__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0

val eject__o__beval_of_byte__o__inject :
  BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0

val beval_of_byte__o__inject : BitVector.byte -> ByteValues.beval Types.sig0

val dpi1__o__beval_of_byte :
  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval

val eject__o__beval_of_byte : BitVector.byte Types.sig0 -> ByteValues.beval

val set_dp_by_offset :
  AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list

val get_stack :
  AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
  Joint.joint_seq List.list

val set_stack_not_a :
  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
  Joint.joint_seq List.list

val set_stack_a :
  AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list

val set_stack :
  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
  Joint.joint_seq List.list

val set_stack_int :
  AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
  Joint.joint_seq List.list

val move :
  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
  arg_decision -> Joint.joint_seq List.list

val arg_is_spilled : arg_decision -> Bool.bool

val is_spilled : Interference.decision -> Bool.bool

val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list

val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list

val commutative : BackEndOps.op2 -> Bool.bool

val uses_carry : BackEndOps.op2 -> Bool.bool

val sets_carry : BackEndOps.op2 -> Bool.bool

val translate_op2 :
  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
  List.list

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

val dec_to_arg_dec : Interference.decision -> arg_decision

val reg_to_dec__o__dec_arg_dec__o__inject :
  I8051.register -> arg_decision Types.sig0

val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0

val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
  I8051.register Types.sig0 -> arg_decision Types.sig0

val dpi1__o__dec_arg_dec__o__inject :
  (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0

val eject__o__dec_arg_dec__o__inject :
  Interference.decision Types.sig0 -> arg_decision Types.sig0

val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0

val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision

val dpi1__o__Reg_to_dec__o__dec_arg_dec :
  (I8051.register, 'a1) Types.dPair -> arg_decision

val eject__o__Reg_to_dec__o__dec_arg_dec :
  I8051.register Types.sig0 -> arg_decision

val dpi1__o__dec_arg_dec :
  (Interference.decision, 'a1) Types.dPair -> arg_decision

val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision

val translate_op1 :
  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
  Interference.decision -> Interference.decision -> Joint.joint_seq List.list

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

val move_to_dp :
  AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
  Joint.joint_seq List.list

val translate_store :
  AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision -> arg_decision
  -> arg_decision -> Joint.joint_seq List.list

val translate_load :
  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
  arg_decision -> arg_decision -> Joint.joint_seq List.list

val translate_address :
  __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
  Interference.decision -> Interference.decision -> Joint.joint_seq List.list

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

val translate_fin_step :
  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block

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

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