open Preamble

open Deqsets

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 Bool

open Relations

open Nat

open BitVector

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open BitVectorTrie

open BitVectorTrieSet

open State

open String

open Exp

open Arithmetic

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open CostLabel

open ASM

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open Sets

open Listb

open Graphs

open I8051

open Order

open Registers

open Hide

open Division

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open Joint_LTL_LIN

open LIN

type aSM_universe = { id_univ : Identifiers.universe;
                      current_funct : AST.ident;
                      ident_map : ASM.identifier Identifiers.identifier_map;
                      label_map : ASM.identifier Identifiers.identifier_map
                                  Identifiers.identifier_map;
                      fresh_cost_label : Positive.pos }

val aSM_universe_rect_Type4 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val aSM_universe_rect_Type5 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val aSM_universe_rect_Type3 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val aSM_universe_rect_Type2 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val aSM_universe_rect_Type1 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val aSM_universe_rect_Type0 :
  (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1

val id_univ : aSM_universe -> Identifiers.universe

val current_funct : aSM_universe -> AST.ident

val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map

val label_map :
  aSM_universe -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map

val fresh_cost_label : aSM_universe -> Positive.pos

val aSM_universe_inv_rect_Type4 :
  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1

val aSM_universe_inv_rect_Type3 :
  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1

val aSM_universe_inv_rect_Type2 :
  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1

val aSM_universe_inv_rect_Type1 :
  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1

val aSM_universe_inv_rect_Type0 :
  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1

val aSM_universe_discr : aSM_universe -> aSM_universe -> __

val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __

val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad

val identifier_of_label :
  Graphs.label -> ASM.identifier Monad.smax_def__o__monad

val identifier_of_ident :
  AST.ident -> ASM.identifier Monad.smax_def__o__monad

val new_ASM_universe : Joint.joint_program -> aSM_universe

val start_funct_translation :
  AST.ident List.list -> AST.ident List.list -> (AST.ident,
  Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad

val aSM_fresh : ASM.identifier Monad.smax_def__o__monad

val register_address : I8051.register -> ASM.subaddressing_mode

val vector_cast :
  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector

val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode

type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj

val data_of_int : BitVector.byte -> ASM.addressing_mode

val data16_of_int : Nat.nat -> ASM.addressing_mode

val accumulator_address : ASM.addressing_mode

val asm_other_bit : ASM.addressing_mode

val one_word : BitVector.word

val translate_statements :
  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
  Monad.smax_def__o__monad

val build_translated_statement : AST.ident List.list -> lin_statement -> __

val translate_code : AST.ident List.list -> lin_statement List.list -> __

val translate_fun_def :
  AST.ident List.list -> AST.ident List.list -> (AST.ident,
  Joint.joint_function) Types.prod -> __

type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
                      actual_dptr : (ASM.identifier, Z.z) Types.prod;
                      built_code : ASM.labelled_instruction List.list
                                   List.list;
                      built_preamble : (ASM.identifier, BitVector.word)
                                       Types.prod List.list }

val init_mutable_rect_Type4 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val init_mutable_rect_Type5 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val init_mutable_rect_Type3 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val init_mutable_rect_Type2 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val init_mutable_rect_Type1 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val init_mutable_rect_Type0 :
  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1

val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod

val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod

val built_code : init_mutable -> ASM.labelled_instruction List.list List.list

val built_preamble :
  init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list

val init_mutable_inv_rect_Type4 :
  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
  Types.prod -> ASM.labelled_instruction List.list List.list ->
  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1

val init_mutable_inv_rect_Type3 :
  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
  Types.prod -> ASM.labelled_instruction List.list List.list ->
  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1

val init_mutable_inv_rect_Type2 :
  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
  Types.prod -> ASM.labelled_instruction List.list List.list ->
  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1

val init_mutable_inv_rect_Type1 :
  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
  Types.prod -> ASM.labelled_instruction List.list List.list ->
  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1

val init_mutable_inv_rect_Type0 :
  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
  Types.prod -> ASM.labelled_instruction List.list List.list ->
  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1

val init_mutable_discr : init_mutable -> init_mutable -> __

val init_mutable_jmdiscr : init_mutable -> init_mutable -> __

val store_byte_or_Identifier :
  (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
  init_mutable -> init_mutable

val do_store_init_data :
  init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
  Monad.smax_def__o__monad

val do_store_global :
  init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
  Types.prod, AST.init_data List.list) Types.prod -> init_mutable
  Monad.smax_def__o__monad

val reversed_flatten_aux :
  'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list

val translate_premain :
  LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
  (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
  Monad.smax_def__o__monad

val get_symboltable :
  (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad

val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option