source: extracted/eRTL.ml @ 2717

open Preamble

open String

open Sets

open Listb

open LabelledObjects

open Graphs

open I8051

open Order

open Registers

open BitVectorTrie

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

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 move_dst =
| PSD of Registers.register
| HDW of I8051.register

(** val move_dst_rect_Type4 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type4 h_PSD h_HDW = function
| PSD x_17821 -> h_PSD x_17821
| HDW x_17822 -> h_HDW x_17822

(** val move_dst_rect_Type5 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type5 h_PSD h_HDW = function
| PSD x_17826 -> h_PSD x_17826
| HDW x_17827 -> h_HDW x_17827

(** val move_dst_rect_Type3 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type3 h_PSD h_HDW = function
| PSD x_17831 -> h_PSD x_17831
| HDW x_17832 -> h_HDW x_17832

(** val move_dst_rect_Type2 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type2 h_PSD h_HDW = function
| PSD x_17836 -> h_PSD x_17836
| HDW x_17837 -> h_HDW x_17837

(** val move_dst_rect_Type1 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type1 h_PSD h_HDW = function
| PSD x_17841 -> h_PSD x_17841
| HDW x_17842 -> h_HDW x_17842

(** val move_dst_rect_Type0 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type0 h_PSD h_HDW = function
| PSD x_17846 -> h_PSD x_17846
| HDW x_17847 -> h_HDW x_17847

(** val move_dst_inv_rect_Type4 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type4 hterm h1 h2 =
  let hcut = move_dst_rect_Type4 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type3 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type3 hterm h1 h2 =
  let hcut = move_dst_rect_Type3 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type2 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type2 hterm h1 h2 =
  let hcut = move_dst_rect_Type2 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type1 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type1 hterm h1 h2 =
  let hcut = move_dst_rect_Type1 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type0 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type0 hterm h1 h2 =
  let hcut = move_dst_rect_Type0 h1 h2 hterm in hcut __

(** val move_dst_discr : move_dst -> move_dst -> __ **)
let move_dst_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val move_dst_jmdiscr : move_dst -> move_dst -> __ **)
let move_dst_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y

type move_src = move_dst Joint.argument

(** val move_src_from_dst : move_dst -> move_src **)
let move_src_from_dst x =
  Joint.Reg x

(** val psd_argument_move_src : Joint.psd_argument -> move_src **)
let psd_argument_move_src = function
| Joint.Reg r -> Joint.Reg (PSD r)
| Joint.Imm b -> Joint.Imm b

type ertl_seq =
| Ertl_new_frame
| Ertl_del_frame
| Ertl_frame_size of Registers.register

(** val ertl_seq_rect_Type4 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17886 -> h_ertl_frame_size x_17886

(** val ertl_seq_rect_Type5 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17891 -> h_ertl_frame_size x_17891

(** val ertl_seq_rect_Type3 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17896 -> h_ertl_frame_size x_17896

(** val ertl_seq_rect_Type2 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17901 -> h_ertl_frame_size x_17901

(** val ertl_seq_rect_Type1 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17906 -> h_ertl_frame_size x_17906

(** val ertl_seq_rect_Type0 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_17911 -> h_ertl_frame_size x_17911

(** val ertl_seq_inv_rect_Type4 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type3 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type2 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type1 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type0 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __

(** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
let ertl_seq_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
let ertl_seq_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val eRTL_uns : Joint.unserialized_params **)
let eRTL_uns =
  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
    Bool.False }

(** val eRTL : Joint.graph_params **)
let eRTL =
  eRTL_uns

type ertl_program = Joint.joint_program

(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
let ertl_seq_joint =
  Obj.magic (fun _ x -> Joint.Extension_seq x)

let byte_to_ertl_snd_argument__o__psd_argument_to_move_src _ = assert false