Remove_globals (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Remove

module E : sig ... end

val check_data : 
  Global.glob_value ->
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  bool

val find_glob : 
  Expr.instr_info ->
  Expr.var_i ->
  Global.glob_decl list ->
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  (Compiler_util.pp_error_loc, Var0.Var.var) Utils0.result

val add_glob : 
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  Expr.instr_info ->
  Var0.Var.var ->
  Global.glob_decl list ->
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val extend_glob_i : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  'a1 Expr.instr ->
  Global.glob_decl list ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val extend_glob_prog : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  'a1 Expr.uprog ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val get_var_ : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.gvar ->
  (Compiler_util.pp_error_loc, Expr.gvar) Utils0.result

val remove_glob_e : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, Expr.pexpr) Utils0.result

val remove_glob_lv : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.lval ->
  (Compiler_util.pp_error_loc, Expr.lval) Utils0.result

val remove_glob : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t ->
    'a1 Expr.instr ->
    (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
  Var0.Var.var Var0.Mvar.t ->
  'a1 Expr.instr list ->
  (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec

val merge_glob : 
  Var0.Var.var ->
  Var0.Var.var option ->
  Var0.Var.var option ->
  Var0.Var.var option

val coq_Mincl : Var0.Var.var Var0.Mvar.t -> Var0.Var.var Var0.Mvar.t -> bool

val merge_env : 
  Var0.Var.var Var0.Mvar.t ->
  Var0.Var.var Var0.Mvar.t ->
  Var0.Var.var Var0.Mvar.t

val loop : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t ->
    (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
  Datatypes.nat ->
  Var0.Var.var Var0.Mvar.t ->
  (Compiler_util.pp_error_loc, Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list)
    Utils0.result

type 'asm_op check2_r =

| Check2_r of Expr.pexpr * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list

type 'asm_op loop2_r =

| Loop2_r of Expr.pexpr * 'asm_op Expr.instr list * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t

val loop2 : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t -> 'a1 check2_r Compiler_util.cexec) ->
  Datatypes.nat ->
  Var0.Var.var Var0.Mvar.t ->
  (Compiler_util.pp_error_loc, 'a1 loop2_r) Utils0.result

val remove_glob_i : 
  'a1 Sopn.asmOp ->
  Global.glob_decl list ->
  Var0.Var.var Var0.Mvar.t ->
  'a1 Expr.instr ->
  (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec

val remove_glob_fundef : 
  'a1 Sopn.asmOp ->
  Global.glob_decl list ->
  'a1 Expr.ufundef ->
  (Compiler_util.pp_error_loc, ('a1, Expr.extra_fun_t) Expr._fundef)
    Utils0.result

val remove_glob_prog : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  'a1 Expr.uprog ->
  (Compiler_util.pp_error_loc,
    ('a1, Expr.extra_fun_t, Expr.extra_prog_t) Expr._prog)
    Utils0.result