Module `Jasmin.Arch_decl`

type __ = Obj.t

type 't coq_ToString = {

category : string;
_finC : 't Utils0.finTypeC;
to_string : 't -> string;

}

val category : Type.ltype -> 'a1 coq_ToString -> string

val _finC : Type.ltype -> 'a1 coq_ToString -> 'a1 Utils0.finTypeC

val to_string : Type.ltype -> 'a1 coq_ToString -> 'a1 -> string

val rtype : Type.ltype -> 'a1 coq_ToString -> Type.ltype

type ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_decl = {

reg_size : Wsize.wsize;
xreg_size : Wsize.wsize;
cond_eqC : 'cond Utils0.eqTypeC;
toS_r : 'reg coq_ToString;
toS_rx : 'regx coq_ToString;
toS_x : 'xreg coq_ToString;
toS_f : 'rflag coq_ToString;
ad_rsp : 'reg;
ad_fcp : Flag_combination.coq_FlagCombinationParams;
caimm_cond_eqC : __ Utils0.eqTypeC;
caimm_cond_pp : __ -> string;
check_CAimm : __ -> Wsize.wsize -> Word0.word -> bool;

}

val reg_size : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.wsize

val xreg_size : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.wsize

val cond_eqC : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a5 Utils0.eqTypeC

val toS_r : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a1 coq_ToString

val toS_rx : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a2 coq_ToString

val toS_x : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a3 coq_ToString

val toS_f : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a4 coq_ToString

val ad_rsp : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a1

val ad_fcp : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Flag_combination.coq_FlagCombinationParams

type ('reg, 'regx, 'xreg, 'rflag, 'cond) caimm_cond = __

val caimm_cond_eqC : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond Utils0.eqTypeC

val caimm_cond_pp : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond ->
  string

val check_CAimm : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond ->
  Wsize.wsize ->
  Word0.word ->
  bool

val arch_pd : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.coq_PointerData

val arch_msfsz : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.coq_MSFsize

val mk_ptr : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Ident.Ident.ident ->
  Var0.Var.var

type ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t = 'reg

type ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t = 'regx

type ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t = 'xreg

type ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t = 'rflag

type ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t = 'cond

val lreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.ltype

type ('reg, 'regx, 'xreg, 'rflag, 'cond) wreg = Sem_type.sem_t

val lxreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.ltype

type ('reg, 'regx, 'xreg, 'rflag, 'cond) wxreg = Sem_type.sem_t

type ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_address = {

ad_disp : Word0.word;
ad_base : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t option;
ad_scale : Datatypes.nat;
ad_offset : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t option;

}

val ad_disp : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  Word0.word

val ad_base : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option

val ad_scale : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  Datatypes.nat

val ad_offset : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option

type ('reg, 'regx, 'xreg, 'rflag, 'cond) address =

| Areg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_address
| Arip of Word0.word

val oeq_reg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option ->
  bool

val reg_address_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address ->
  bool

val reg_address_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address Eqtype.eq_axiom

val coq_HB_unnamed_factory_1 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_address Eqtype.Coq_hasDecEq.axioms_

val arch_decl_reg_address__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

val address_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) address ->
  ('a1, 'a2, 'a3, 'a4, 'a5) address ->
  bool

val address_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) address Eqtype.eq_axiom

val coq_HB_unnamed_factory_3 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) address Eqtype.Coq_hasDecEq.axioms_

val arch_decl_address__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg =

| Condt of ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t
| Imm of Wsize.wsize * Word0.word
| Reg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
| Regx of ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t
| Addr of ('reg, 'regx, 'xreg, 'rflag, 'cond) address
| XReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t

type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args =
  ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg list

val is_Condt : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) cond_t option

val asm_arg_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  bool

val asm_arg_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg Eqtype.eq_axiom

val coq_HB_unnamed_factory_5 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg Eqtype.Coq_hasDecEq.axioms_

val arch_decl_asm_arg__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

type msb_flag =

| MSB_CLEAR
| MSB_MERGE

val msb_flag_rect : 'a1 -> 'a1 -> msb_flag -> 'a1

val msb_flag_rec : 'a1 -> 'a1 -> msb_flag -> 'a1

type is_msb_flag =

| Coq_is_MSB_CLEAR
| Coq_is_MSB_MERGE

val is_msb_flag_rect : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1

val is_msb_flag_rec : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1

val msb_flag_tag : msb_flag -> BinNums.positive

val is_msb_flag_inhab : msb_flag -> is_msb_flag

val is_msb_flag_functor : msb_flag -> is_msb_flag -> is_msb_flag

type box_msb_flag_MSB_CLEAR =

| Box_msb_flag_MSB_CLEAR

type msb_flag_fields_t = __

val msb_flag_fields : msb_flag -> msb_flag_fields_t

val msb_flag_construct : 
  BinNums.positive ->
  msb_flag_fields_t ->
  msb_flag option

val msb_flag_induction : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1

val msb_flag_eqb_fields : 
  (msb_flag -> msb_flag -> bool) ->
  BinNums.positive ->
  msb_flag_fields_t ->
  msb_flag_fields_t ->
  bool

val msb_flag_eqb : msb_flag -> msb_flag -> bool

val msb_flag_eqb_OK : msb_flag -> msb_flag -> Datatypes.reflect

val msb_flag_eqb_OK_sumbool : msb_flag -> msb_flag -> bool

val coq_HB_unnamed_factory_7 : msb_flag Eqtype.Coq_hasDecEq.axioms_

val arch_decl_msb_flag__canonical__eqtype_Equality : Eqtype.Equality.coq_type

type ('reg, 'regx, 'xreg, 'rflag, 'cond) implicit_arg =

| IArflag of ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t
| IAreg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t

val implicit_arg_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg ->
  bool

val implicit_arg_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg Eqtype.eq_axiom

val coq_HB_unnamed_factory_9 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg Eqtype.Coq_hasDecEq.axioms_

val arch_decl_implicit_arg__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

type addr_kind =

| AK_compute
| AK_mem of Memory_model.aligned

type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_constrained_register =

| ACR_any
| ACR_exact of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
| ACR_vector of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t
| ACR_subset of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list

type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc =

| ADImplicit of ('reg, 'regx, 'xreg, 'rflag, 'cond) implicit_arg
| ADExplicit of addr_kind * Datatypes.nat * ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_constrained_register

val coq_F : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val coq_R : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val coq_Ea : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Datatypes.nat ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val coq_Eu : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Datatypes.nat ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val coq_Ec : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Datatypes.nat ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val coq_Ef : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Datatypes.nat ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc

val check_oreg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_constrained_register ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  bool

type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kind =

| CAcond
| CAreg
| CAregx
| CAxmm
| CAmem of bool
| CAimm of ('reg, 'regx, 'xreg, 'rflag, 'cond) caimm_cond option * Wsize.wsize

val arg_kind_eqb : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  bool

val arg_kind_eqb_OK : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  Datatypes.reflect

val coq_HB_unnamed_factory_11 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind Eqtype.Coq_hasDecEq.axioms_

val arch_decl_arg_kind__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kinds =
  ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kind list

type ('reg, 'regx, 'xreg, 'rflag, 'cond) args_kinds =
  ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kinds list

type ('reg, 'regx, 'xreg, 'rflag, 'cond) i_args_kinds =
  ('reg, 'regx, 'xreg, 'rflag, 'cond) args_kinds list

val check_arg_kind : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  bool

val check_arg_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kinds ->
  bool

val check_args_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_args ->
  ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds ->
  bool

val check_i_args_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_args ->
  bool

val check_arg_dest : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc ->
  Type.ltype ->
  bool

type ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op_ext =

| PP_error
| PP_name
| PP_iname of Wsize.wsize
| PP_iname2 of string * Wsize.wsize * Wsize.wsize
| PP_viname of Wsize.velem * bool
| PP_viname2 of Wsize.velem * Wsize.velem
| PP_ct of ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg

type ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op = {

pp_aop_name : string;
pp_aop_ext : ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op_ext;
pp_aop_args : (Wsize.wsize * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg) list;

}

val pp_aop_name : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op ->
  string

val pp_aop_ext : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op ->
  ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op_ext

val pp_aop_args : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op ->
  (Wsize.wsize * ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg) list

type ('reg, 'regx, 'xreg, 'rflag, 'cond) instr_desc_t = {

id_valid : bool;
id_msb_flag : msb_flag;
id_tin : Type.ltype list;
id_in : ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc list;
id_tout : Type.ltype list;
id_out : ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc list;
id_semi : Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod;
id_args_kinds : ('reg, 'regx, 'xreg, 'rflag, 'cond) i_args_kinds;
id_nargs : Datatypes.nat;
id_str_jas : unit -> string;
id_safe : Wsize.safe_cond list;
id_doit : Sopn.doit_t;
id_pp_asm : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args -> ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op;

}

val id_valid : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  bool

val id_msb_flag : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  msb_flag

val id_tin : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Type.ltype list

val id_in : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list

val id_tout : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Type.ltype list

val id_out : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list

val id_semi : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod

val id_args_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds

val id_nargs : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Datatypes.nat

val id_str_jas : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  unit ->
  string

val id_safe : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Wsize.safe_cond list

val id_doit : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  Sopn.doit_t

val id_pp_asm : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_args ->
  ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_decl = {

_eqT : 'asm_op Utils0.eqTypeC;
instr_desc_op : 'asm_op -> ('reg, 'regx, 'xreg, 'rflag, 'cond) instr_desc_t;
prim_string : (string * 'asm_op Sopn.prim_constructor) list;

}

val _eqT : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  'a6 Utils0.eqTypeC

val instr_desc_op : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  'a6 ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t

val prim_string : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  (string * 'a6 Sopn.prim_constructor) list

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_t' = 'asm_op

type 'asm_op asm_op_msb_t_gen = Wsize.wsize option * 'asm_op

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_msb_t =
  'asm_op asm_op_msb_t_gen

val extend_size : Wsize.wsize -> Type.ltype -> Type.ltype

val wextend_size : 
  Wsize.wsize ->
  Type.ltype ->
  Sem_type.sem_ot ->
  Sem_type.sem_ot

val extend_tuple : 
  Wsize.wsize ->
  Type.ltype list ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val apply_lprod : 
  ('a1 -> 'a2) ->
  __ list ->
  'a1 Utils0.lprod ->
  'a2 Utils0.lprod

val is_not_CAmem : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind ->
  bool

val exclude_mem_args_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc ->
  ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds ->
  ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds

val exclude_mem_i_args_kinds : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds

val exclude_mem_aux : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds

val is_nil : 'a1 list -> bool

val exclude_mem : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list ->
  ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds

val extend_sem : 
  Type.ltype list ->
  Type.ltype list ->
  Wsize.wsize ->
  Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod ->
  Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod

val can_zeroextend : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t ->
  bool

val instr_desc : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_msb_t ->
  ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i_r =

| ALIGN
| LABEL of Label.label_kind * Label.label
| STORELABEL of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t * Label.label
| JMP of Label.remote_label
| JMPI of ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg
| Jcc of Label.label * ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t
| JAL of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t * Label.remote_label
| CALL of Label.remote_label
| POPPC
| AsmOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_t' * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args
| SysCall of (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t
| Declassify_val of Type.ltype * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg
| Declassify_mem of BinNums.coq_Z * ('reg, 'regx, 'xreg, 'rflag, 'cond) address

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i = {

asmi_ii : Expr.instr_info;
asmi_i : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i_r;

}

val asmi_ii : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i ->
  Expr.instr_info

val asmi_i : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i_r

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_code =
  ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i list

type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg =

| ARReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
| ARegX of ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t
| AXReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t
| ABReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t

val asm_typed_reg_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  bool

val asm_typed_reg_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg Eqtype.eq_axiom

val coq_HB_unnamed_factory_13 : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg Eqtype.Coq_hasDecEq.axioms_

val arch_decl_asm_typed_reg__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  Eqtype.Equality.coq_type

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_fundef = {

asm_fd_align : Wsize.wsize;
asm_fd_arg : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
asm_fd_body : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_code;
asm_fd_res : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
asm_fd_export : bool;
asm_fd_total_stack : BinNums.coq_Z;
asm_fd_align_args : Wsize.wsize list;

}

val asm_fd_align : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  Wsize.wsize

val asm_fd_arg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list

val asm_fd_body : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_code

val asm_fd_res : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list

val asm_fd_export : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  bool

val asm_fd_total_stack : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  BinNums.coq_Z

val asm_fd_align_args : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  Wsize.wsize list

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_prog = {

asm_globs : Word0.word list;
asm_glob_names : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
asm_funcs : (Var0.funname * ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_fundef) list;

}

val asm_globs : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog ->
  Word0.word list

val asm_glob_names : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog ->
  ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list

val asm_funcs : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog ->
  (Var0.funname * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef) list

val is_ABReg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  bool

type ('reg, 'regx, 'xreg, 'rflag, 'cond) calling_convention = {

callee_saved : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
call_reg_args : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
call_xreg_args : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;
call_reg_ret : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
call_xreg_ret : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;

}

val callee_saved : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list

val call_reg_args : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list

val call_xreg_args : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list

val call_reg_ret : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list

val call_xreg_ret : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list

val get_ARReg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option

val get_ARegX : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) regx_t option

val get_AXReg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg ->
  ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t option

val check_list : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  'a6 Utils0.eqTypeC ->
  (('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> 'a6 option) ->
  ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list ->
  'a6 list ->
  bool

val check_call_conv : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef ->
  bool

type ('reg, 'regx, 'xreg, 'rflag, 'cond) internal_calling_convention = {

icall_reg : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
icall_regx : ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t list;
icall_xreg : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;
icall_rflag : ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t list;

}

val icall_reg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list

val icall_regx : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) regx_t list

val icall_xreg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list

val icall_rflag : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention ->
  ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t list

val registers : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list

val registerxs : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) regx_t list

val xregisters : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list

val rflags : 
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t list

type rflagv =

| Def of bool
| Undef

val rflagv_rect : (bool -> 'a1) -> 'a1 -> rflagv -> 'a1

val rflagv_rec : (bool -> 'a1) -> 'a1 -> rflagv -> 'a1

type is_rflagv =

| Coq_is_Def of bool * Param1.Coq_exports.is_bool
| Coq_is_Undef

val is_rflagv_rect : 
  (bool -> Param1.Coq_exports.is_bool -> 'a1) ->
  'a1 ->
  rflagv ->
  is_rflagv ->
  'a1

val is_rflagv_rec : 
  (bool -> Param1.Coq_exports.is_bool -> 'a1) ->
  'a1 ->
  rflagv ->
  is_rflagv ->
  'a1

val rflagv_tag : rflagv -> BinNums.positive

val is_rflagv_inhab : rflagv -> is_rflagv

val is_rflagv_functor : rflagv -> is_rflagv -> is_rflagv

type box_rflagv_Def = bool

val coq_Box_rflagv_Def_0 : box_rflagv_Def -> bool

type box_rflagv_Undef =

| Box_rflagv_Undef

type rflagv_fields_t = __

val rflagv_fields : rflagv -> rflagv_fields_t

val rflagv_construct : BinNums.positive -> rflagv_fields_t -> rflagv option

val rflagv_induction : 
  (bool -> Param1.Coq_exports.is_bool -> 'a1) ->
  'a1 ->
  rflagv ->
  is_rflagv ->
  'a1

val rflagv_eqb_fields : 
  (rflagv -> rflagv -> bool) ->
  BinNums.positive ->
  rflagv_fields_t ->
  rflagv_fields_t ->
  bool

val rflagv_eqb : rflagv -> rflagv -> bool

val rflagv_eqb_OK : rflagv -> rflagv -> Datatypes.reflect

val rflagv_eqb_OK_sumbool : rflagv -> rflagv -> bool

val coq_HB_unnamed_factory_15 : rflagv Eqtype.Coq_hasDecEq.axioms_

val arch_decl_rflagv__canonical__eqtype_Equality : Eqtype.Equality.coq_type

type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm = {

_arch_decl : ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_decl;
_asm_op_decl : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_decl;
eval_cond : (('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t -> Word0.word) -> (('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t -> bool Utils0.exec) -> ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t -> bool Utils0.exec;

}

val _arch_decl : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl

val _asm_op_decl : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl

val eval_cond : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm ->
  (('a1, 'a2, 'a3, 'a4, 'a5) reg_t -> Word0.word) ->
  (('a1, 'a2, 'a3, 'a4, 'a5) rflag_t -> bool Utils0.exec) ->
  ('a1, 'a2, 'a3, 'a4, 'a5) cond_t ->
  bool Utils0.exec

package jasmin

Module Jasmin.Arch_decl

Module `Jasmin.Arch_decl`