(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(* fn used_function() {} *)
Definition used_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_used_function : M.IsFunction "dead_code::used_function" used_function.

(* fn unused_function() {} *)
Definition unused_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_unused_function : M.IsFunction "dead_code::unused_function" unused_function.

(* fn noisy_unused_function() {} *)
Definition noisy_unused_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_noisy_unused_function :
  M.IsFunction "dead_code::noisy_unused_function" noisy_unused_function.

(*
fn main() {
    used_function();
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _ :=
          M.alloc (|
            M.call_closure (| M.get_function (| "dead_code::used_function", [] |), [] |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "dead_code::main" main.
