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

Module fmt.
  (*
  pub fn format(args: Arguments<'_>) -> string::String {
      fn format_inner(args: Arguments<'_>) -> string::String {
          let capacity = args.estimated_capacity();
          let mut output = string::String::with_capacity(capacity);
          output
              .write_fmt(args)
              .expect("a formatting trait implementation returned an error when the underlying stream did not");
          output
      }
  
      args.as_str().map_or_else(|| format_inner(args), crate::borrow::ToOwned::to_owned)
  }
  *)
  Definition format (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ args ] =>
      ltac:(M.monadic
        (let args := M.alloc (| args |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
            "map_or_else",
            [
              Ty.path "alloc::string::String";
              Ty.function [ Ty.tuple [] ] (Ty.path "alloc::string::String");
              Ty.function [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ] Ty.associated
            ]
          |),
          [
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Arguments", "as_str", [] |),
              [ args ]
            |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.call_closure (|
                                M.get_function (| "alloc::fmt::format.format_inner", [] |),
                                [ M.read (| args |) ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end));
            M.get_trait_method (| "alloc::borrow::ToOwned", Ty.path "str", [], "to_owned", [] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_format : M.IsFunction "alloc::fmt::format" format.
  
  Module format.
    (*
        fn format_inner(args: Arguments<'_>) -> string::String {
            let capacity = args.estimated_capacity();
            let mut output = string::String::with_capacity(capacity);
            output
                .write_fmt(args)
                .expect("a formatting trait implementation returned an error when the underlying stream did not");
            output
        }
    *)
    Definition format_inner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ args ] =>
        ltac:(M.monadic
          (let args := M.alloc (| args |) in
          M.read (|
            let~ capacity :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Arguments",
                    "estimated_capacity",
                    []
                  |),
                  [ args ]
                |)
              |) in
            let~ output :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "alloc::string::String",
                    "with_capacity",
                    []
                  |),
                  [ M.read (| capacity |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                    "expect",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::fmt::Write",
                        Ty.path "alloc::string::String",
                        [],
                        "write_fmt",
                        []
                      |),
                      [ output; M.read (| args |) ]
                    |);
                    M.read (|
                      Value.String
                        "a formatting trait implementation returned an error when the underlying stream did not"
                    |)
                  ]
                |)
              |) in
            output
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_format_inner : M.IsFunction "alloc::fmt::format::format_inner" format_inner.
  End format.
End fmt.
