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

type registers_move =
| From_acc of I8051.register * Types.unit0
| To_acc of Types.unit0 * I8051.register
| Int_to_reg of I8051.register * BitVector.byte
| Int_to_acc of Types.unit0 * BitVector.byte

(** val registers_move_rect_Type4 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18638, x_18637) -> h_from_acc x_18638 x_18637
| To_acc (x_18640, x_18639) -> h_to_acc x_18640 x_18639
| Int_to_reg (x_18642, x_18641) -> h_int_to_reg x_18642 x_18641
| Int_to_acc (x_18644, x_18643) -> h_int_to_acc x_18644 x_18643

(** val registers_move_rect_Type5 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18651, x_18650) -> h_from_acc x_18651 x_18650
| To_acc (x_18653, x_18652) -> h_to_acc x_18653 x_18652
| Int_to_reg (x_18655, x_18654) -> h_int_to_reg x_18655 x_18654
| Int_to_acc (x_18657, x_18656) -> h_int_to_acc x_18657 x_18656

(** val registers_move_rect_Type3 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18664, x_18663) -> h_from_acc x_18664 x_18663
| To_acc (x_18666, x_18665) -> h_to_acc x_18666 x_18665
| Int_to_reg (x_18668, x_18667) -> h_int_to_reg x_18668 x_18667
| Int_to_acc (x_18670, x_18669) -> h_int_to_acc x_18670 x_18669

(** val registers_move_rect_Type2 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18677, x_18676) -> h_from_acc x_18677 x_18676
| To_acc (x_18679, x_18678) -> h_to_acc x_18679 x_18678
| Int_to_reg (x_18681, x_18680) -> h_int_to_reg x_18681 x_18680
| Int_to_acc (x_18683, x_18682) -> h_int_to_acc x_18683 x_18682

(** val registers_move_rect_Type1 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18690, x_18689) -> h_from_acc x_18690 x_18689
| To_acc (x_18692, x_18691) -> h_to_acc x_18692 x_18691
| Int_to_reg (x_18694, x_18693) -> h_int_to_reg x_18694 x_18693
| Int_to_acc (x_18696, x_18695) -> h_int_to_acc x_18696 x_18695

(** val registers_move_rect_Type0 :
    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
| From_acc (x_18703, x_18702) -> h_from_acc x_18703 x_18702
| To_acc (x_18705, x_18704) -> h_to_acc x_18705 x_18704
| Int_to_reg (x_18707, x_18706) -> h_int_to_reg x_18707 x_18706
| Int_to_acc (x_18709, x_18708) -> h_int_to_acc x_18709 x_18708

(** val registers_move_inv_rect_Type4 :
    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
    'a1) -> 'a1 **)
let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val registers_move_inv_rect_Type3 :
    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
    'a1) -> 'a1 **)
let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val registers_move_inv_rect_Type2 :
    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
    'a1) -> 'a1 **)
let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val registers_move_inv_rect_Type1 :
    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
    'a1) -> 'a1 **)
let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val registers_move_inv_rect_Type0 :
    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
    'a1) -> 'a1 **)
let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val registers_move_discr : registers_move -> registers_move -> __ **)
let registers_move_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
let registers_move_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

type ltl_lin_seq =
| SAVE_CARRY
| RESTORE_CARRY
| LOW_ADDRESS of Graphs.label
| HIGH_ADDRESS of Graphs.label

(** val ltl_lin_seq_rect_Type4 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18800 -> h_LOW_ADDRESS x_18800
| HIGH_ADDRESS x_18801 -> h_HIGH_ADDRESS x_18801

(** val ltl_lin_seq_rect_Type5 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18807 -> h_LOW_ADDRESS x_18807
| HIGH_ADDRESS x_18808 -> h_HIGH_ADDRESS x_18808

(** val ltl_lin_seq_rect_Type3 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18814 -> h_LOW_ADDRESS x_18814
| HIGH_ADDRESS x_18815 -> h_HIGH_ADDRESS x_18815

(** val ltl_lin_seq_rect_Type2 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18821 -> h_LOW_ADDRESS x_18821
| HIGH_ADDRESS x_18822 -> h_HIGH_ADDRESS x_18822

(** val ltl_lin_seq_rect_Type1 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18828 -> h_LOW_ADDRESS x_18828
| HIGH_ADDRESS x_18829 -> h_HIGH_ADDRESS x_18829

(** val ltl_lin_seq_rect_Type0 :
    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
    ltl_lin_seq -> 'a1 **)
let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
| SAVE_CARRY -> h_SAVE_CARRY
| RESTORE_CARRY -> h_RESTORE_CARRY
| LOW_ADDRESS x_18835 -> h_LOW_ADDRESS x_18835
| HIGH_ADDRESS x_18836 -> h_HIGH_ADDRESS x_18836

(** val ltl_lin_seq_inv_rect_Type4 :
    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val ltl_lin_seq_inv_rect_Type3 :
    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val ltl_lin_seq_inv_rect_Type2 :
    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val ltl_lin_seq_inv_rect_Type1 :
    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val ltl_lin_seq_inv_rect_Type0 :
    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
let ltl_lin_seq_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
let ltl_lin_seq_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
let ltl_lin_seq_labels = function
| SAVE_CARRY -> List.Nil
| RESTORE_CARRY -> List.Nil
| LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
| HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)

(** val lTL_LIN_uns : Joint.unserialized_params **)
let lTL_LIN_uns =
  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
    Joint.has_tailcalls = Bool.False }

(** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
let lTL_LIN_functs =
  { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
    List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
    (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
    Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
    List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
    (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
    Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
    List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
    (fun x -> List.Nil) }

(** val lTL_LIN : Joint.uns_params **)
let lTL_LIN =
  { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }