Arch_extra (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Arch

type 't coq_ToIdent = {

to_ident : 't -> Ident.Ident.ident;
of_ident : Ident.Ident.ident -> 't option;

}

val to_ident : 
  Type.stype ->
  'a1 Arch_decl.coq_ToString ->
  'a1 coq_ToIdent ->
  'a1 ->
  Ident.Ident.ident

val of_ident : 
  Type.stype ->
  'a1 Arch_decl.coq_ToString ->
  'a1 coq_ToIdent ->
  Ident.Ident.ident ->
  'a1 option

val to_var : 
  Type.stype ->
  'a1 Arch_decl.coq_ToString ->
  'a1 coq_ToIdent ->
  'a1 ->
  Var0.Var.var

val of_var : 
  Type.stype ->
  'a1 Arch_decl.coq_ToString ->
  'a1 coq_ToIdent ->
  Var0.Var.var ->
  'a1 option

module type MkToIdent_T = sig ... end

module MkToIdent : MkToIdent_T

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

toI_r : 'reg coq_ToIdent;
toI_rx : 'regx coq_ToIdent;
toI_x : 'xreg coq_ToIdent;
toI_f : 'rflag coq_ToIdent;

}

val toI_r : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  'a1 coq_ToIdent

val toI_rx : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  'a2 coq_ToIdent

val toI_x : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  'a3 coq_ToIdent

val toI_f : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  'a4 coq_ToIdent

module type AToIdent_T = sig ... end

module MkAToIdent : AToIdent_T

val var_of_implicit_arg : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.implicit_arg ->
  Var0.Var.var

val sopn_constrained_register : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arg_constrained_register ->
  Sopn.arg_constrained_register

val sopn_arg_desc : 
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent ->
  ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arg_desc ->
  Sopn.arg_desc

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

_asm : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm;
_atoI : ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_toIdent;
_extra : 'extra_op Sopn.asmOp;
to_asm : Expr.instr_info -> 'extra_op -> Fexpr.lexpr list -> Fexpr.rexpr list -> ((('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm_op_msb_t * Fexpr.lexpr list) * Fexpr.rexpr list) list Compiler_util.cexec;

}

val _asm : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm

val _atoI : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent

val _extra : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> 'a7 Sopn.asmOp

val to_asm : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  Expr.instr_info ->
  'a7 ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  ((('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm_op_msb_t * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

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

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

| BaseOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm_op_msb_t
| ExtOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) extra_op_t

val extended_op_beq : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op ->
  bool

val extended_op_eq_axiom : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Eqtype.eq_axiom

val coq_HB_unnamed_factory_1 : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Eqtype.Coq_hasDecEq.axioms_

val arch_extra_extended_op__canonical__eqtype_Equality : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  Eqtype.Equality.coq_type

val get_instr_desc : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op ->
  Sopn.instruction_desc

val sopn_prim_string_base : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  (string * 'a6 Sopn.prim_constructor) list ->
  (string
   * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor)
    list

val sopn_prim_string_extra : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  (string * 'a7 Sopn.prim_constructor) list ->
  (string
   * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor)
    list

val get_prime_op : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  (string
   * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor)
    list

val eqTC_extended_op : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Utils0.eqTypeC

val asm_opI : 
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra ->
  ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.asmOp