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

Module array.
  Module ascii.
    Module Impl_array_N_u8.
      Definition Self (N : Value.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ Ty.path "u8" ].
      
      (*
          pub const fn as_ascii(&self) -> Option<&[ascii::Char; N]> {
              if self.is_ascii() {
                  // SAFETY: Just checked that it's ASCII
                  Some(unsafe { self.as_ascii_unchecked() })
              } else {
                  None
              }
          }
      *)
      Definition as_ascii (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self N in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "is_ascii",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "array") [ N ] [ Ty.path "u8" ],
                                "as_ascii_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ascii :
        forall (N : Value.t),
        M.IsAssociatedFunction (Self N) "as_ascii" (as_ascii N).
      
      (*
          pub const unsafe fn as_ascii_unchecked(&self) -> &[ascii::Char; N] {
              let byte_ptr: *const [u8; N] = self;
              let ascii_ptr = byte_ptr as *const [ascii::Char; N];
              // SAFETY: The caller promised all the bytes are ASCII
              unsafe { &*ascii_ptr }
          }
      *)
      Definition as_ascii_unchecked
          (N : Value.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ byte_ptr := M.alloc (| M.read (| self |) |) in
              let~ ascii_ptr := M.alloc (| M.rust_cast (M.read (| byte_ptr |)) |) in
              M.alloc (| M.read (| ascii_ptr |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ascii_unchecked :
        forall (N : Value.t),
        M.IsAssociatedFunction (Self N) "as_ascii_unchecked" (as_ascii_unchecked N).
    End Impl_array_N_u8.
  End ascii.
End array.
