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

(*
fn main() {
    // `F` must be generic.
    fn apply<F>(f: F)
    where
        F: FnOnce(),
    {
        f();
    }
}
*)
Definition main (ε : 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_main : M.IsFunction "functions_closures_type_anonymity_define::main" main.

Module main.
  (*
      fn apply<F>(f: F)
      where
          F: FnOnce(),
      {
          f();
      }
  *)
  Definition apply (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ F ], [ f ] =>
      ltac:(M.monadic
        (let f := M.alloc (| f |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [] ],
                  "call_once",
                  []
                |),
                [ M.read (| f |); Value.Tuple [] ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_apply : M.IsFunction "functions_closures_type_anonymity_define::main::apply" apply.
End main.
