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

Module clone.
  Module uninit.
    (* Trait *)
    (* Empty module 'CopySpec' *)
    
    Module Impl_core_clone_uninit_CopySpec_where_core_clone_Clone_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*
          default unsafe fn clone_one(src: &Self, dst: *mut Self) {
              // SAFETY: The safety conditions of clone_to_uninit() are a superset of those of
              // ptr::write().
              unsafe {
                  // We hope the optimizer will figure out to create the cloned value in-place,
                  // skipping ever storing it on the stack and the copy to the destination.
                  ptr::write(dst, src.clone());
              }
          }
      *)
      Definition clone_one (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ src; dst ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            let dst := M.alloc (| dst |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ptr::write", [ T ] |),
                    [
                      M.read (| dst |);
                      M.call_closure (|
                        M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                        [ M.read (| src |) ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          default unsafe fn clone_slice(src: &[Self], dst: *mut [Self]) {
              let len = src.len();
              // This is the most likely mistake to make, so check it as a debug assertion.
              debug_assert_eq!(
                  len,
                  dst.len(),
                  "clone_to_uninit() source and destination must have equal lengths",
              );
      
              // SAFETY: The produced `&mut` is valid because:
              // * The caller is obligated to provide a pointer which is valid for writes.
              // * All bytes pointed to are in MaybeUninit, so we don't care about the memory's
              //   initialization status.
              let uninit_ref = unsafe { &mut *(dst as *mut [MaybeUninit<T>]) };
      
              // Copy the elements
              let mut initializing = InitializingSlice::from_fully_uninit(uninit_ref);
              for element_ref in src {
                  // If the clone() panics, `initializing` will take care of the cleanup.
                  initializing.push(element_ref.clone());
              }
              // If we reach here, then the entire slice is initialized, and we've satisfied our
              // responsibilities to the caller. Disarm the cleanup guard by forgetting it.
              mem::forget(initializing);
          }
      *)
      Definition clone_slice (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ src; dst ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            let dst := M.alloc (| dst |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| src |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              Value.Tuple
                                [
                                  len;
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*mut")
                                          []
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| dst |) ]
                                    |)
                                  |)
                                ]
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let left_val := M.copy (| γ0_0 |) in
                                  let right_val := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  BinOp.eq (|
                                                    M.read (| M.read (| left_val |) |),
                                                    M.read (| M.read (| right_val |) |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ kind :=
                                                  M.alloc (|
                                                    Value.StructTuple
                                                      "core::panicking::AssertKind::Eq"
                                                      []
                                                  |) in
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::panicking::assert_failed",
                                                      [ Ty.path "usize"; Ty.path "usize" ]
                                                    |),
                                                    [
                                                      M.read (| kind |);
                                                      M.read (| left_val |);
                                                      M.read (| right_val |);
                                                      Value.StructTuple
                                                        "core::option::Option::Some"
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Arguments",
                                                              "new_const",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.read (|
                                                                      Value.String
                                                                        "clone_to_uninit() source and destination must have equal lengths"
                                                                    |)
                                                                  ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                    ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ uninit_ref := M.alloc (| M.rust_cast (M.read (| dst |)) |) in
              let~ initializing :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::clone::uninit::InitializingSlice") [] [ T ],
                      "from_fully_uninit",
                      []
                    |),
                    [ M.read (| uninit_ref |) ]
                  |)
                |) 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 "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          [],
                          "into_iter",
                          []
                        |),
                        [ M.read (| src |) ]
                      |)
                    |),
                    [
                      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::Iter") [] [ 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 element_ref := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::clone::uninit::InitializingSlice")
                                                  []
                                                  [ T ],
                                                "push",
                                                []
                                              |),
                                              [
                                                initializing;
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::clone::Clone",
                                                    T,
                                                    [],
                                                    "clone",
                                                    []
                                                  |),
                                                  [ M.read (| element_ref |) ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::clone::uninit::InitializingSlice") [] [ T ] ]
                    |),
                    [ M.read (| initializing |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::clone::uninit::CopySpec"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("clone_one", InstanceField.Method (clone_one T));
            ("clone_slice", InstanceField.Method (clone_slice T))
          ].
    End Impl_core_clone_uninit_CopySpec_where_core_clone_Clone_T_for_T.
    
    Module Impl_core_clone_uninit_CopySpec_where_core_marker_Copy_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*
          unsafe fn clone_one(src: &Self, dst: *mut Self) {
              // SAFETY: The safety conditions of clone_to_uninit() are a superset of those of
              // ptr::copy_nonoverlapping().
              unsafe {
                  ptr::copy_nonoverlapping(src, dst, 1);
              }
          }
      *)
      Definition clone_one (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ src; dst ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            let dst := M.alloc (| dst |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                    [ M.read (| src |); M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn clone_slice(src: &[Self], dst: *mut [Self]) {
              let len = src.len();
              // This is the most likely mistake to make, so check it as a debug assertion.
              debug_assert_eq!(
                  len,
                  dst.len(),
                  "clone_to_uninit() source and destination must have equal lengths",
              );
      
              // SAFETY: The safety conditions of clone_to_uninit() are a superset of those of
              // ptr::copy_nonoverlapping().
              unsafe {
                  ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), len);
              }
          }
      *)
      Definition clone_slice (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ src; dst ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            let dst := M.alloc (| dst |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| src |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              Value.Tuple
                                [
                                  len;
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*mut")
                                          []
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| dst |) ]
                                    |)
                                  |)
                                ]
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let left_val := M.copy (| γ0_0 |) in
                                  let right_val := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  BinOp.eq (|
                                                    M.read (| M.read (| left_val |) |),
                                                    M.read (| M.read (| right_val |) |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ kind :=
                                                  M.alloc (|
                                                    Value.StructTuple
                                                      "core::panicking::AssertKind::Eq"
                                                      []
                                                  |) in
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::panicking::assert_failed",
                                                      [ Ty.path "usize"; Ty.path "usize" ]
                                                    |),
                                                    [
                                                      M.read (| kind |);
                                                      M.read (| left_val |);
                                                      M.read (| right_val |);
                                                      Value.StructTuple
                                                        "core::option::Option::Some"
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Arguments",
                                                              "new_const",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.read (|
                                                                      Value.String
                                                                        "clone_to_uninit() source and destination must have equal lengths"
                                                                    |)
                                                                  ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                    ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| src |) ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          "as_mut_ptr",
                          []
                        |),
                        [ M.read (| dst |) ]
                      |);
                      M.read (| len |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::clone::uninit::CopySpec"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("clone_one", InstanceField.Method (clone_one T));
            ("clone_slice", InstanceField.Method (clone_slice T))
          ].
    End Impl_core_clone_uninit_CopySpec_where_core_marker_Copy_T_for_T.
    
    (* StructRecord
      {
        name := "InitializingSlice";
        const_params := [];
        ty_params := [ "T" ];
        fields :=
          [
            ("data",
              Ty.apply
                (Ty.path "&mut")
                []
                [
                  Ty.apply
                    (Ty.path "slice")
                    []
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                ]);
            ("initialized_len", Ty.path "usize")
          ];
      } *)
    
    Module Impl_core_clone_uninit_InitializingSlice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::clone::uninit::InitializingSlice") [] [ T ].
      
      (*
          fn from_fully_uninit(data: &'a mut [MaybeUninit<T>]) -> Self {
              Self { data, initialized_len: 0 }
          }
      *)
      Definition from_fully_uninit
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ data ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            Value.StructRecord
              "core::clone::uninit::InitializingSlice"
              [ ("data", M.read (| data |)); ("initialized_len", Value.Integer IntegerKind.Usize 0)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_fully_uninit :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "from_fully_uninit" (from_fully_uninit T).
      
      (*
          fn push(&mut self, value: T) {
              MaybeUninit::write(&mut self.data[self.initialized_len], value);
              self.initialized_len += 1;
          }
      *)
      Definition push (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 (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "write",
                      []
                    |),
                    [
                      M.SubPointer.get_array_field (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::clone::uninit::InitializingSlice",
                            "data"
                          |)
                        |),
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::clone::uninit::InitializingSlice",
                          "initialized_len"
                        |)
                      |);
                      M.read (| value |)
                    ]
                  |)
                |) in
              let~ _ :=
                let β :=
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::clone::uninit::InitializingSlice",
                    "initialized_len"
                  |) in
                M.write (|
                  β,
                  BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_push :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "push" (push T).
    End Impl_core_clone_uninit_InitializingSlice_T.
    
    Module Impl_core_ops_drop_Drop_for_core_clone_uninit_InitializingSlice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::clone::uninit::InitializingSlice") [] [ T ].
      
      (*
          fn drop(&mut self) {
              let initialized_slice = ptr::slice_from_raw_parts_mut(
                  MaybeUninit::slice_as_mut_ptr(self.data),
                  self.initialized_len,
              );
              // SAFETY:
              // * the pointer is valid because it was made from a mutable reference
              // * `initialized_len` counts the initialized elements as an invariant of this type,
              //   so each of the pointed-to elements is initialized and may be dropped.
              unsafe {
                  ptr::drop_in_place::<[T]>(initialized_slice);
              }
          }
      *)
      Definition drop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ initialized_slice :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                          "slice_as_mut_ptr",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::clone::uninit::InitializingSlice",
                              "data"
                            |)
                          |)
                        ]
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::clone::uninit::InitializingSlice",
                          "initialized_len"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::ptr::drop_in_place",
                      [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    |),
                    [ M.read (| initialized_slice |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::drop::Drop"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method (drop T)) ].
    End Impl_core_ops_drop_Drop_for_core_clone_uninit_InitializingSlice_T.
  End uninit.
End clone.
