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

Module foo.
  Module gre.
    (*
            pub fn f_foo_gre() {
                println!("foo::gre::bar");
            }
    *)
    Definition f_foo_gre (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.read (|
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_const",
                          []
                        |),
                        [ M.alloc (| Value.Array [ M.read (| Value.String "foo::gre::bar
" |) ] |) ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_f_foo_gre : M.IsFunction "module_duplicate::foo::gre::f_foo_gre" f_foo_gre.
  End gre.
  
  (*
      pub fn f_foo() {
          println!("foo::bar");
          gre::f_foo_gre();
      }
  *)
  Definition f_foo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "std::io::stdio::_print", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Arguments",
                        "new_const",
                        []
                      |),
                      [ M.alloc (| Value.Array [ M.read (| Value.String "foo::bar
" |) ] |) ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "module_duplicate::foo::gre::f_foo_gre", [] |),
                []
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_f_foo : M.IsFunction "module_duplicate::foo::f_foo" f_foo.
End foo.

(*
fn f() {
    foo::f_foo();
}
*)
Definition f (ε : 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 (| "module_duplicate::foo::f_foo", [] |), [] |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_f : M.IsFunction "module_duplicate::f" f.
