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

(* StructRecord
  {
    name := "CustomAllocator";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("value",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ])
      ];
  } *)

Module Impl_custom_allocator_CustomAllocator.
  Definition Self : Ty.t := Ty.path "custom_allocator::CustomAllocator".
  
  (*
      pub fn new(init_value: bool) -> Self {
          Self {
              value: vec![init_value],
          }
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ init_value ] =>
      ltac:(M.monadic
        (let init_value := M.alloc (| init_value |) in
        Value.StructRecord
          "custom_allocator::CustomAllocator"
          [
            ("value",
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "bool" ],
                  "into_vec",
                  [ Ty.path "alloc::alloc::Global" ]
                |),
                [
                  M.read (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.apply
                              (Ty.path "array")
                              [ Value.Integer IntegerKind.Usize 1 ]
                              [ Ty.path "bool" ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [ M.alloc (| Value.Array [ M.read (| init_value |) ] |) ]
                    |)
                  |)
                ]
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub fn default() -> Self {
          Self::new(Default::default())
      }
  *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (| Ty.path "custom_allocator::CustomAllocator", "new", [] |),
          [
            M.call_closure (|
              M.get_trait_method (| "core::default::Default", Ty.path "bool", [], "default", [] |),
              []
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_default : M.IsAssociatedFunction Self "default" default.
  
  (*
      pub fn flip(&mut self) {
          self.value[0] = !self.value[0];
      }
  *)
  Definition flip (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          let~ _ :=
            M.write (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::IndexMut",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ],
                  [ Ty.path "usize" ],
                  "index_mut",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "custom_allocator::CustomAllocator",
                    "value"
                  |);
                  Value.Integer IntegerKind.Usize 0
                ]
              |),
              UnOp.not (|
                M.read (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ],
                      [ Ty.path "usize" ],
                      "index",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "custom_allocator::CustomAllocator",
                        "value"
                      |);
                      Value.Integer IntegerKind.Usize 0
                    ]
                  |)
                |)
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_flip : M.IsAssociatedFunction Self "flip" flip.
  
  (*
      pub fn get(&self) -> bool {
          self.value[0]
      }
  *)
  Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::Index",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ],
              [ Ty.path "usize" ],
              "index",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "custom_allocator::CustomAllocator",
                "value"
              |);
              Value.Integer IntegerKind.Usize 0
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get : M.IsAssociatedFunction Self "get" get.
End Impl_custom_allocator_CustomAllocator.
