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

Module vec.
  Module spec_from_elem.
    (* Trait *)
    (* Empty module 'SpecFromElem' *)
    
    Module Impl_alloc_vec_spec_from_elem_SpecFromElem_where_core_clone_Clone_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*
          default fn from_elem<A: Allocator>(elem: Self, n: usize, alloc: A) -> Vec<Self, A> {
              let mut v = Vec::with_capacity_in(n, alloc);
              v.extend_with(n, elem);
              v
          }
      *)
      Definition from_elem (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ A ], [ elem; n; alloc ] =>
          ltac:(M.monadic
            (let elem := M.alloc (| elem |) in
            let n := M.alloc (| n |) in
            let alloc := M.alloc (| alloc |) in
            M.read (|
              let~ v :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                      "with_capacity_in",
                      []
                    |),
                    [ M.read (| n |); M.read (| alloc |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                      "extend_with",
                      []
                    |),
                    [ v; M.read (| n |); M.read (| elem |) ]
                  |)
                |) in
              v
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::spec_from_elem::SpecFromElem"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_elem", InstanceField.Method (from_elem T)) ].
    End Impl_alloc_vec_spec_from_elem_SpecFromElem_where_core_clone_Clone_T_for_T.
    
    Module Impl_alloc_vec_spec_from_elem_SpecFromElem_where_core_clone_Clone_T_where_alloc_vec_is_zero_IsZero_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*
          default fn from_elem<A: Allocator>(elem: T, n: usize, alloc: A) -> Vec<T, A> {
              if elem.is_zero() {
                  return Vec { buf: RawVec::with_capacity_zeroed_in(n, alloc), len: n };
              }
              let mut v = Vec::with_capacity_in(n, alloc);
              v.extend_with(n, elem);
              v
          }
      *)
      Definition from_elem (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ A ], [ elem; n; alloc ] =>
          ltac:(M.monadic
            (let elem := M.alloc (| elem |) in
            let n := M.alloc (| n |) in
            let alloc := M.alloc (| alloc |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "alloc::vec::is_zero::IsZero",
                                      T,
                                      [],
                                      "is_zero",
                                      []
                                    |),
                                    [ elem ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructRecord
                                      "alloc::vec::Vec"
                                      [
                                        ("buf",
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::raw_vec::RawVec")
                                                []
                                                [ T; A ],
                                              "with_capacity_zeroed_in",
                                              []
                                            |),
                                            [ M.read (| n |); M.read (| alloc |) ]
                                          |));
                                        ("len", M.read (| n |))
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ v :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                          "with_capacity_in",
                          []
                        |),
                        [ M.read (| n |); M.read (| alloc |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                          "extend_with",
                          []
                        |),
                        [ v; M.read (| n |); M.read (| elem |) ]
                      |)
                    |) in
                  v
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::spec_from_elem::SpecFromElem"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_elem", InstanceField.Method (from_elem T)) ].
    End Impl_alloc_vec_spec_from_elem_SpecFromElem_where_core_clone_Clone_T_where_alloc_vec_is_zero_IsZero_T_for_T.
    
    Module Impl_alloc_vec_spec_from_elem_SpecFromElem_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*
          fn from_elem<A: Allocator>(elem: i8, n: usize, alloc: A) -> Vec<i8, A> {
              if elem == 0 {
                  return Vec { buf: RawVec::with_capacity_zeroed_in(n, alloc), len: n };
              }
              let mut v = Vec::with_capacity_in(n, alloc);
              unsafe {
                  ptr::write_bytes(v.as_mut_ptr(), elem as u8, n);
                  v.set_len(n);
              }
              v
          }
      *)
      Definition from_elem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A ], [ elem; n; alloc ] =>
          ltac:(M.monadic
            (let elem := M.alloc (| elem |) in
            let n := M.alloc (| n |) in
            let alloc := M.alloc (| alloc |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (| M.read (| elem |), Value.Integer IntegerKind.I8 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructRecord
                                      "alloc::vec::Vec"
                                      [
                                        ("buf",
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::raw_vec::RawVec")
                                                []
                                                [ Ty.path "i8"; A ],
                                              "with_capacity_zeroed_in",
                                              []
                                            |),
                                            [ M.read (| n |); M.read (| alloc |) ]
                                          |));
                                        ("len", M.read (| n |))
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ v :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "i8"; A ],
                          "with_capacity_in",
                          []
                        |),
                        [ M.read (| n |); M.read (| alloc |) ]
                      |)
                    |) in
                  let~ _ :=
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::intrinsics::write_bytes", [ Ty.path "i8" ] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "i8"; A ],
                                "as_mut_ptr",
                                []
                              |),
                              [ v ]
                            |);
                            M.rust_cast (M.read (| elem |));
                            M.read (| n |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "i8"; A ],
                            "set_len",
                            []
                          |),
                          [ v; M.read (| n |) ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |) in
                  v
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "alloc::vec::spec_from_elem::SpecFromElem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_elem", InstanceField.Method from_elem) ].
    End Impl_alloc_vec_spec_from_elem_SpecFromElem_for_i8.
    
    Module Impl_alloc_vec_spec_from_elem_SpecFromElem_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
          fn from_elem<A: Allocator>(elem: u8, n: usize, alloc: A) -> Vec<u8, A> {
              if elem == 0 {
                  return Vec { buf: RawVec::with_capacity_zeroed_in(n, alloc), len: n };
              }
              let mut v = Vec::with_capacity_in(n, alloc);
              unsafe {
                  ptr::write_bytes(v.as_mut_ptr(), elem, n);
                  v.set_len(n);
              }
              v
          }
      *)
      Definition from_elem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A ], [ elem; n; alloc ] =>
          ltac:(M.monadic
            (let elem := M.alloc (| elem |) in
            let n := M.alloc (| n |) in
            let alloc := M.alloc (| alloc |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (| M.read (| elem |), Value.Integer IntegerKind.U8 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructRecord
                                      "alloc::vec::Vec"
                                      [
                                        ("buf",
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::raw_vec::RawVec")
                                                []
                                                [ Ty.path "u8"; A ],
                                              "with_capacity_zeroed_in",
                                              []
                                            |),
                                            [ M.read (| n |); M.read (| alloc |) ]
                                          |));
                                        ("len", M.read (| n |))
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ v :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; A ],
                          "with_capacity_in",
                          []
                        |),
                        [ M.read (| n |); M.read (| alloc |) ]
                      |)
                    |) in
                  let~ _ :=
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::intrinsics::write_bytes", [ Ty.path "u8" ] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; A ],
                                "as_mut_ptr",
                                []
                              |),
                              [ v ]
                            |);
                            M.read (| elem |);
                            M.read (| n |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; A ],
                            "set_len",
                            []
                          |),
                          [ v; M.read (| n |) ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |) in
                  v
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "alloc::vec::spec_from_elem::SpecFromElem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_elem", InstanceField.Method from_elem) ].
    End Impl_alloc_vec_spec_from_elem_SpecFromElem_for_u8.
    
    Module Impl_alloc_vec_spec_from_elem_SpecFromElem_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      (*
          fn from_elem<A: Allocator>(_elem: (), n: usize, alloc: A) -> Vec<(), A> {
              let mut v = Vec::with_capacity_in(n, alloc);
              // SAFETY: the capacity has just been set to `n`
              // and `()` is a ZST with trivial `Clone` implementation
              unsafe {
                  v.set_len(n);
              }
              v
          }
      *)
      Definition from_elem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A ], [ _elem; n; alloc ] =>
          ltac:(M.monadic
            (let _elem := M.alloc (| _elem |) in
            let n := M.alloc (| n |) in
            let alloc := M.alloc (| alloc |) in
            M.read (|
              let~ v :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.tuple []; A ],
                      "with_capacity_in",
                      []
                    |),
                    [ M.read (| n |); M.read (| alloc |) ]
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.tuple []; A ],
                        "set_len",
                        []
                      |),
                      [ v; M.read (| n |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              v
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "alloc::vec::spec_from_elem::SpecFromElem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_elem", InstanceField.Method from_elem) ].
    End Impl_alloc_vec_spec_from_elem_SpecFromElem_for_Tuple_.
  End spec_from_elem.
End vec.
