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

Module slice.
  Module specialize.
    (* Trait *)
    (* Empty module 'SpecFill' *)
    
    Module Impl_core_slice_specialize_SpecFill_where_core_clone_Clone_T_T_for_slice_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          default fn spec_fill(&mut self, value: T) {
              if let Some((last, elems)) = self.split_last_mut() {
                  for el in elems {
                      el.clone_from(&value);
                  }
      
                  *last = value
              }
          }
      *)
      Definition spec_fill (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.read (|
              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") [] [ T ],
                              "split_last_mut",
                              []
                            |),
                            [ M.read (| self |) ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                      let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                      let last := M.copy (| γ1_0 |) in
                      let elems := M.copy (| γ1_1 |) in
                      let~ _ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::collect::IntoIterator",
                                  Ty.apply
                                    (Ty.path "&mut")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                  [],
                                  "into_iter",
                                  []
                                |),
                                [ M.read (| elems |) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let iter := M.copy (| γ |) in
                                  M.loop (|
                                    ltac:(M.monadic
                                      (let~ _ :=
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path "core::slice::iter::IterMut")
                                                  []
                                                  [ T ],
                                                [],
                                                "next",
                                                []
                                              |),
                                              [ iter ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let _ :=
                                                  M.is_struct_tuple (|
                                                    γ,
                                                    "core::option::Option::None"
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (| M.read (| M.break (||) |) |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::option::Option::Some",
                                                    0
                                                  |) in
                                                let el := M.copy (| γ0_0 |) in
                                                let~ _ :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::clone::Clone",
                                                        T,
                                                        [],
                                                        "clone_from",
                                                        []
                                                      |),
                                                      [ M.read (| el |); value ]
                                                    |)
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                  |)))
                            ]
                          |)) in
                      M.write (| M.read (| last |), M.read (| value |) |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::specialize::SpecFill"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("spec_fill", InstanceField.Method (spec_fill T)) ].
    End Impl_core_slice_specialize_SpecFill_where_core_clone_Clone_T_T_for_slice_T.
    
    Module Impl_core_slice_specialize_SpecFill_where_core_marker_Copy_T_T_for_slice_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn spec_fill(&mut self, value: T) {
              for item in self.iter_mut() {
                  *item = value;
              }
          }
      *)
      Definition spec_fill (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.read (|
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "iter_mut",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let item := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.write (| M.read (| item |), M.read (| value |) |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::specialize::SpecFill"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("spec_fill", InstanceField.Method (spec_fill T)) ].
    End Impl_core_slice_specialize_SpecFill_where_core_marker_Copy_T_T_for_slice_T.
  End specialize.
End slice.
