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

Module net.
  Module display_buffer.
    (* StructRecord
      {
        name := "DisplayBuffer";
        const_params := [ "SIZE" ];
        ty_params := [];
        fields :=
          [
            ("buf",
              Ty.apply
                (Ty.path "array")
                [ SIZE ]
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ]);
            ("len", Ty.path "usize")
          ];
      } *)
    
    Module Impl_core_net_display_buffer_DisplayBuffer_SIZE.
      Definition Self (SIZE : Value.t) : Ty.t :=
        Ty.apply (Ty.path "core::net::display_buffer::DisplayBuffer") [ SIZE ] [].
      
      (*
          pub const fn new() -> Self {
              Self { buf: [MaybeUninit::uninit(); SIZE], len: 0 }
          }
      *)
      Definition new (SIZE : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self SIZE in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "core::net::display_buffer::DisplayBuffer"
              [
                ("buf",
                  repeat (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                          []
                          [ Ty.path "u8" ],
                        "uninit",
                        []
                      |),
                      []
                    |),
                    SIZE
                  |));
                ("len", Value.Integer IntegerKind.Usize 0)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (SIZE : Value.t),
        M.IsAssociatedFunction (Self SIZE) "new" (new SIZE).
      
      (*
          pub fn as_str(&self) -> &str {
              // SAFETY: `buf` is only written to by the `fmt::Write::write_str` implementation
              // which writes a valid UTF-8 string to `buf` and correctly sets `len`.
              unsafe {
                  let s = MaybeUninit::slice_assume_init_ref(&self.buf[..self.len]);
                  str::from_utf8_unchecked(s)
              }
          }
      *)
      Definition as_str
          (SIZE : Value.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self SIZE in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ s :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                      "slice_assume_init_ref",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply
                            (Ty.path "array")
                            [ SIZE ]
                            [
                              Ty.apply
                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                []
                                [ Ty.path "u8" ]
                            ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::net::display_buffer::DisplayBuffer",
                            "buf"
                          |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [
                              ("end_",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::net::display_buffer::DisplayBuffer",
                                    "len"
                                  |)
                                |))
                            ]
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::str::converts::from_utf8_unchecked", [] |),
                  [ M.read (| s |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_str :
        forall (SIZE : Value.t),
        M.IsAssociatedFunction (Self SIZE) "as_str" (as_str SIZE).
    End Impl_core_net_display_buffer_DisplayBuffer_SIZE.
    
    Module Impl_core_fmt_Write_for_core_net_display_buffer_DisplayBuffer_SIZE.
      Definition Self (SIZE : Value.t) : Ty.t :=
        Ty.apply (Ty.path "core::net::display_buffer::DisplayBuffer") [ SIZE ] [].
      
      (*
          fn write_str(&mut self, s: &str) -> fmt::Result {
              let bytes = s.as_bytes();
      
              if let Some(buf) = self.buf.get_mut(self.len..(self.len + bytes.len())) {
                  MaybeUninit::copy_from_slice(buf, bytes);
                  self.len += bytes.len();
                  Ok(())
              } else {
                  Err(fmt::Error)
              }
          }
      *)
      Definition write_str
          (SIZE : Value.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self SIZE in
        match ε, τ, α with
        | [], [], [ self; s ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let s := M.alloc (| s |) in
            M.read (|
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| s |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ],
                              "get_mut",
                              [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ]
                              ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::net::display_buffer::DisplayBuffer",
                                "buf"
                              |);
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start",
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::net::display_buffer::DisplayBuffer",
                                        "len"
                                      |)
                                    |));
                                  ("end_",
                                    BinOp.Wrap.add (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::net::display_buffer::DisplayBuffer",
                                          "len"
                                        |)
                                      |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| bytes |) ]
                                      |)
                                    |))
                                ]
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let buf := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                []
                                [ Ty.path "u8" ],
                              "copy_from_slice",
                              []
                            |),
                            [ M.read (| buf |); M.read (| bytes |) ]
                          |)
                        |) in
                      let~ _ :=
                        let β :=
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::net::display_buffer::DisplayBuffer",
                            "len"
                          |) in
                        M.write (|
                          β,
                          BinOp.Wrap.add (|
                            M.read (| β |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "len",
                                []
                              |),
                              [ M.read (| bytes |) ]
                            |)
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::fmt::Error" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (SIZE : Value.t),
        M.IsTraitInstance
          "core::fmt::Write"
          (Self SIZE)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("write_str", InstanceField.Method (write_str SIZE)) ].
    End Impl_core_fmt_Write_for_core_net_display_buffer_DisplayBuffer_SIZE.
  End display_buffer.
End net.
