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

Module str.
  Module converts.
    (*
    pub const fn from_utf8(v: &[u8]) -> Result<&str, Utf8Error> {
        // FIXME(const-hack): This should use `?` again, once it's `const`
        match run_utf8_validation(v) {
            Ok(_) => {
                // SAFETY: validation succeeded.
                Ok(unsafe { from_utf8_unchecked(v) })
            }
            Err(err) => Err(err),
        }
    }
    *)
    Definition from_utf8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::str::validations::run_utf8_validation", [] |),
                  [ M.read (| v |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_function (| "core::str::converts::from_utf8_unchecked", [] |),
                            [ M.read (| v |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let err := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| err |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_utf8 : M.IsFunction "core::str::converts::from_utf8" from_utf8.
    
    (*
    pub const fn from_utf8_mut(v: &mut [u8]) -> Result<&mut str, Utf8Error> {
        // FIXME(const-hack): This should use `?` again, once it's `const`
        match run_utf8_validation(v) {
            Ok(_) => {
                // SAFETY: validation succeeded.
                Ok(unsafe { from_utf8_unchecked_mut(v) })
            }
            Err(err) => Err(err),
        }
    }
    *)
    Definition from_utf8_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::str::validations::run_utf8_validation", [] |),
                  [ M.read (| v |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_function (| "core::str::converts::from_utf8_unchecked_mut", [] |),
                            [ M.read (| v |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let err := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| err |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_utf8_mut : M.IsFunction "core::str::converts::from_utf8_mut" from_utf8_mut.
    
    (*
    pub const unsafe fn from_utf8_unchecked(v: &[u8]) -> &str {
        // SAFETY: the caller must guarantee that the bytes `v` are valid UTF-8.
        // Also relies on `&str` and `&[u8]` having the same layout.
        unsafe { mem::transmute(v) }
    }
    *)
    Definition from_utf8_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          M.call_closure (|
            M.get_function (|
              "core::intrinsics::transmute",
              [
                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                Ty.apply (Ty.path "&") [] [ Ty.path "str" ]
              ]
            |),
            [ M.read (| v |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_utf8_unchecked :
      M.IsFunction "core::str::converts::from_utf8_unchecked" from_utf8_unchecked.
    
    (*
    pub const unsafe fn from_utf8_unchecked_mut(v: &mut [u8]) -> &mut str {
        // SAFETY: the caller must guarantee that the bytes `v`
        // are valid UTF-8, thus the cast to `*mut str` is safe.
        // Also, the pointer dereference is safe because that pointer
        // comes from a reference which is guaranteed to be valid for writes.
        unsafe { &mut *(v as *mut [u8] as *mut str) }
    }
    *)
    Definition from_utf8_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          M.rust_cast (M.read (| M.use (M.alloc (| M.read (| v |) |)) |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_utf8_unchecked_mut :
      M.IsFunction "core::str::converts::from_utf8_unchecked_mut" from_utf8_unchecked_mut.
    
    (*
    pub const unsafe fn from_raw_parts<'a>(ptr: *const u8, len: usize) -> &'a str {
        // SAFETY: the caller must uphold the safety contract for `from_raw_parts`.
        unsafe { &*ptr::from_raw_parts(ptr, len) }
    }
    *)
    Definition from_raw_parts (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ptr; len ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (|
              "core::ptr::metadata::from_raw_parts",
              [ Ty.path "str"; Ty.path "u8" ]
            |),
            [ M.read (| ptr |); M.read (| len |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_raw_parts :
      M.IsFunction "core::str::converts::from_raw_parts" from_raw_parts.
    
    (*
    pub const unsafe fn from_raw_parts_mut<'a>(ptr: *mut u8, len: usize) -> &'a mut str {
        // SAFETY: the caller must uphold the safety contract for `from_raw_parts_mut`.
        unsafe { &mut *ptr::from_raw_parts_mut(ptr, len) }
    }
    *)
    Definition from_raw_parts_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ptr; len ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (|
              "core::ptr::metadata::from_raw_parts_mut",
              [ Ty.path "str"; Ty.path "u8" ]
            |),
            [ M.read (| ptr |); M.read (| len |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_raw_parts_mut :
      M.IsFunction "core::str::converts::from_raw_parts_mut" from_raw_parts_mut.
  End converts.
End str.
