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

Module str.
  Module Impl_alloc_slice_Concat_where_core_borrow_Borrow_S_str_str_for_slice_S.
    Definition Self (S : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ S ].
    
    (*     type Output = String; *)
    Definition _Output (S : Ty.t) : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn concat(slice: &Self) -> String {
            Join::join(slice, "")
        }
    *)
    Definition concat (S : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self S in
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (let slice := M.alloc (| slice |) in
          M.call_closure (|
            M.get_trait_method (|
              "alloc::slice::Join",
              Ty.apply (Ty.path "slice") [] [ S ],
              [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
              "join",
              []
            |),
            [ M.read (| slice |); M.read (| Value.String "" |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (S : Ty.t),
      M.IsTraitInstance
        "alloc::slice::Concat"
        (Self S)
        (* Trait polymorphic types *) [ (* Item *) Ty.path "str" ]
        (* Instance *)
        [ ("Output", InstanceField.Ty (_Output S)); ("concat", InstanceField.Method (concat S)) ].
  End Impl_alloc_slice_Concat_where_core_borrow_Borrow_S_str_str_for_slice_S.
  
  Module Impl_alloc_slice_Join_where_core_borrow_Borrow_S_str_ref__str_for_slice_S.
    Definition Self (S : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ S ].
    
    (*     type Output = String; *)
    Definition _Output (S : Ty.t) : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn join(slice: &Self, sep: &str) -> String {
            unsafe { String::from_utf8_unchecked(join_generic_copy(slice, sep.as_bytes())) }
        }
    *)
    Definition join (S : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self S in
      match ε, τ, α with
      | [], [], [ slice; sep ] =>
        ltac:(M.monadic
          (let slice := M.alloc (| slice |) in
          let sep := M.alloc (| sep |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "alloc::string::String",
              "from_utf8_unchecked",
              []
            |),
            [
              M.call_closure (|
                M.get_function (|
                  "alloc::str::join_generic_copy",
                  [ Ty.path "str"; Ty.path "u8"; S ]
                |),
                [
                  M.read (| slice |);
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| sep |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (S : Ty.t),
      M.IsTraitInstance
        "alloc::slice::Join"
        (Self S)
        (* Trait polymorphic types *)
        [ (* Separator *) Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
        (* Instance *)
        [ ("Output", InstanceField.Ty (_Output S)); ("join", InstanceField.Method (join S)) ].
  End Impl_alloc_slice_Join_where_core_borrow_Borrow_S_str_ref__str_for_slice_S.
  
  (*
  fn join_generic_copy<B, T, S>(slice: &[S], sep: &[T]) -> Vec<T>
  where
      T: Copy,
      B: AsRef<[T]> + ?Sized,
      S: Borrow<B>,
  {
      let sep_len = sep.len();
      let mut iter = slice.iter();
  
      // the first slice is the only one without a separator preceding it
      let first = match iter.next() {
          Some(first) => first,
          None => return vec![],
      };
  
      // compute the exact total length of the joined Vec
      // if the `len` calculation overflows, we'll panic
      // we would have run out of memory anyway and the rest of the function requires
      // the entire Vec pre-allocated for safety
      let reserved_len = sep_len
          .checked_mul(iter.len())
          .and_then(|n| {
              slice.iter().map(|s| s.borrow().as_ref().len()).try_fold(n, usize::checked_add)
          })
          .expect("attempt to join into collection with len > usize::MAX");
  
      // prepare an uninitialized buffer
      let mut result = Vec::with_capacity(reserved_len);
      debug_assert!(result.capacity() >= reserved_len);
  
      result.extend_from_slice(first.borrow().as_ref());
  
      unsafe {
          let pos = result.len();
          let target = result.spare_capacity_mut().get_unchecked_mut(..reserved_len - pos);
  
          // Convert the separator and slices to slices of MaybeUninit
          // to simplify implementation in specialize_for_lengths
          let sep_uninit = core::slice::from_raw_parts(sep.as_ptr().cast(), sep.len());
          let iter_uninit = iter.map(|it| {
              let it = it.borrow().as_ref();
              core::slice::from_raw_parts(it.as_ptr().cast(), it.len())
          });
  
          // copy separator and slices over without bounds checks
          // generate loops with hardcoded offsets for small separators
          // massive improvements possible (~ x2)
          let remain = specialize_for_lengths!(sep_uninit, target, iter_uninit; 0, 1, 2, 3, 4);
  
          // A weird borrow implementation may return different
          // slices for the length calculation and the actual copy.
          // Make sure we don't expose uninitialized bytes to the caller.
          let result_len = reserved_len - remain.len();
          result.set_len(result_len);
      }
      result
  }
  *)
  Definition join_generic_copy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ B; T; _ as S ], [ slice; sep ] =>
      ltac:(M.monadic
        (let slice := M.alloc (| slice |) in
        let sep := M.alloc (| sep |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ sep_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| sep |) ]
                  |)
                |) in
              let~ iter :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ S ], "iter", [] |),
                    [ M.read (| slice |) ]
                  |)
                |) in
              let~ first :=
                M.copy (|
                  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") [] [ S ],
                          [],
                          "next",
                          []
                        |),
                        [ iter ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let first := M.copy (| γ0_0 |) in
                          first));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ T; Ty.path "alloc::alloc::Global" ],
                                      "new",
                                      []
                                    |),
                                    []
                                  |)
                                |)
                              |)
                            |)
                          |)))
                    ]
                  |)
                |) in
              let~ reserved_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                      "expect",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                          "and_then",
                          [
                            Ty.path "usize";
                            Ty.function
                              [ Ty.tuple [ Ty.path "usize" ] ]
                              (Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ])
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "usize", "checked_mul", [] |),
                            [
                              M.read (| sep_len |);
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::exact_size::ExactSizeIterator",
                                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ],
                                  [],
                                  "len",
                                  []
                                |),
                                [ iter ]
                              |)
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let n := M.copy (| γ |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path "core::iter::adapters::map::Map")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ S ];
                                                    Ty.function
                                                      [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ]
                                                      ]
                                                      (Ty.path "usize")
                                                  ],
                                                [],
                                                "try_fold",
                                                [
                                                  Ty.path "usize";
                                                  Ty.function
                                                    [ Ty.path "usize"; Ty.path "usize" ]
                                                    (Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ Ty.path "usize" ]);
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.path "usize" ]
                                                ]
                                              |),
                                              [
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::iterator::Iterator",
                                                      Ty.apply
                                                        (Ty.path "core::slice::iter::Iter")
                                                        []
                                                        [ S ],
                                                      [],
                                                      "map",
                                                      [
                                                        Ty.path "usize";
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [ Ty.apply (Ty.path "&") [] [ S ] ]
                                                          ]
                                                          (Ty.path "usize")
                                                      ]
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply (Ty.path "slice") [] [ S ],
                                                          "iter",
                                                          []
                                                        |),
                                                        [ M.read (| slice |) ]
                                                      |);
                                                      M.closure
                                                        (fun γ =>
                                                          ltac:(M.monadic
                                                            match γ with
                                                            | [ α0 ] =>
                                                              ltac:(M.monadic
                                                                (M.match_operator (|
                                                                  M.alloc (| α0 |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let s := M.copy (| γ |) in
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [ T ],
                                                                            "len",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::convert::AsRef",
                                                                                B,
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "slice")
                                                                                    []
                                                                                    [ T ]
                                                                                ],
                                                                                "as_ref",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_trait_method (|
                                                                                    "core::borrow::Borrow",
                                                                                    S,
                                                                                    [ B ],
                                                                                    "borrow",
                                                                                    []
                                                                                  |),
                                                                                  [ M.read (| s |) ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)))
                                                                  ]
                                                                |)))
                                                            | _ =>
                                                              M.impossible
                                                                "wrong number of arguments"
                                                            end))
                                                    ]
                                                  |)
                                                |);
                                                M.read (| n |);
                                                M.get_associated_function (|
                                                  Ty.path "usize",
                                                  "checked_add",
                                                  []
                                                |)
                                              ]
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |);
                      M.read (|
                        Value.String "attempt to join into collection with len > usize::MAX"
                      |)
                    ]
                  |)
                |) in
              let~ result :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                      "with_capacity",
                      []
                    |),
                    [ M.read (| reserved_len |) ]
                  |)
                |) 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 [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.ge (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [ T; Ty.path "alloc::alloc::Global" ],
                                                "capacity",
                                                []
                                              |),
                                              [ result ]
                                            |),
                                            M.read (| reserved_len |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.call_closure (|
                                        M.get_function (| "core::panicking::panic", [] |),
                                        [
                                          M.read (|
                                            Value.String
                                              "assertion failed: result.capacity() >= reserved_len"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              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_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                      "extend_from_slice",
                      []
                    |),
                    [
                      result;
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::convert::AsRef",
                          B,
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          "as_ref",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::borrow::Borrow", S, [ B ], "borrow", [] |),
                            [ M.read (| first |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                let~ pos :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ T; Ty.path "alloc::alloc::Global" ],
                        "len",
                        []
                      |),
                      [ result ]
                    |)
                  |) in
                let~ target :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                        "get_unchecked_mut",
                        [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ T; Ty.path "alloc::alloc::Global" ],
                            "spare_capacity_mut",
                            []
                          |),
                          [ result ]
                        |);
                        Value.StructRecord
                          "core::ops::range::RangeTo"
                          [
                            ("end_",
                              BinOp.Wrap.sub (| M.read (| reserved_len |), M.read (| pos |) |))
                          ]
                      ]
                    |)
                  |) in
                let~ sep_uninit :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::raw::from_raw_parts",
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*const") [] [ T ],
                            "cast",
                            [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ T ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| sep |) ]
                            |)
                          ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "len",
                            []
                          |),
                          [ M.read (| sep |) ]
                        |)
                      ]
                    |)
                  |) in
                let~ iter_uninit :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ],
                        [],
                        "map",
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                            ];
                          Ty.function
                            [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                            (Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ T ]
                                  ]
                              ])
                        ]
                      |),
                      [
                        M.read (| iter |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let it := M.copy (| γ |) in
                                          M.read (|
                                            let~ it :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::convert::AsRef",
                                                    B,
                                                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                                    "as_ref",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::borrow::Borrow",
                                                        S,
                                                        [ B ],
                                                        "borrow",
                                                        []
                                                      |),
                                                      [ M.read (| it |) ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::slice::raw::from_raw_parts",
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ T ]
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*const") [] [ T ],
                                                      "cast",
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply (Ty.path "slice") [] [ T ],
                                                          "as_ptr",
                                                          []
                                                        |),
                                                        [ M.read (| it |) ]
                                                      |)
                                                    ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "slice") [] [ T ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ M.read (| it |) ]
                                                  |)
                                                ]
                                              |)
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                let~ remain :=
                  M.alloc (|
                    M.read (|
                      let~ target := M.copy (| target |) in
                      let~ iter := M.copy (| iter_uninit |) in
                      let~ sep_bytes := M.copy (| sep_uninit |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ T ]
                                  ],
                                "len",
                                []
                              |),
                              [ M.read (| sep_uninit |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Integer IntegerKind.Usize 0
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Integer IntegerKind.Usize 1
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Integer IntegerKind.Usize 2
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Integer IntegerKind.Usize 3
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Integer IntegerKind.Usize 4
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))));
                            fun γ =>
                              ltac:(M.monadic
                                (M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::map::Map")
                                            []
                                            [
                                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ S ];
                                              Ty.function
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ S ] ] ]
                                                (Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [ T ]
                                                      ]
                                                  ])
                                            ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [ M.read (| iter |) ]
                                      |)
                                    |),
                                    [
                                      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::iter::adapters::map::Map")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ S ];
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [ Ty.apply (Ty.path "&") [] [ S ]
                                                                  ]
                                                              ]
                                                              (Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ 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 s := M.copy (| γ0_0 |) in
                                                        let~ len :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| sep_bytes |) ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ T ]
                                                                  ],
                                                                "split_at_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| target |);
                                                                M.read (| len |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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 head := M.copy (| γ0_0 |) in
                                                                let tail := M.copy (| γ0_1 |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "copy_from_slice",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| head |);
                                                                        M.read (| sep_bytes |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  M.write (|
                                                                    target,
                                                                    M.read (| tail |)
                                                                  |) in
                                                                let~ content_bytes :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::convert::AsRef",
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ T ]
                                                                            ]
                                                                        ],
                                                                        "as_ref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::borrow::Borrow",
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                                  []
                                                                                  [ T ]
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                                    []
                                                                                    [ T ]
                                                                                ]
                                                                            ],
                                                                            "borrow",
                                                                            []
                                                                          |),
                                                                          [ M.read (| s |) ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |) in
                                                                let~ len :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| content_bytes |) ]
                                                                    |)
                                                                  |) in
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ T ]
                                                                          ],
                                                                        "split_at_mut",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| target |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    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 head :=
                                                                          M.copy (| γ0_0 |) in
                                                                        let tail :=
                                                                          M.copy (| γ0_1 |) in
                                                                        let~ _ :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ T ]
                                                                                  ],
                                                                                "copy_from_slice",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| head |);
                                                                                M.read (|
                                                                                  content_bytes
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            target,
                                                                            M.read (| tail |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |))))
                          ]
                        |) in
                      target
                    |)
                  |) in
                let~ result_len :=
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.read (| reserved_len |),
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                          "len",
                          []
                        |),
                        [ M.read (| remain |) ]
                      |)
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ T; Ty.path "alloc::alloc::Global" ],
                        "set_len",
                        []
                      |),
                      [ result; M.read (| result_len |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              result
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_join_generic_copy : M.IsFunction "alloc::str::join_generic_copy" join_generic_copy.
  
  Module Impl_core_borrow_Borrow_str_for_alloc_string_String.
    Definition Self : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn borrow(&self) -> &str {
            &self[..]
        }
    *)
    Definition borrow (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::Index",
              Ty.path "alloc::string::String",
              [ Ty.path "core::ops::range::RangeFull" ],
              "index",
              []
            |),
            [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::borrow::Borrow"
        Self
        (* Trait polymorphic types *) [ (* Borrowed *) Ty.path "str" ]
        (* Instance *) [ ("borrow", InstanceField.Method borrow) ].
  End Impl_core_borrow_Borrow_str_for_alloc_string_String.
  
  Module Impl_core_borrow_BorrowMut_str_for_alloc_string_String.
    Definition Self : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn borrow_mut(&mut self) -> &mut str {
            &mut self[..]
        }
    *)
    Definition borrow_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::IndexMut",
              Ty.path "alloc::string::String",
              [ Ty.path "core::ops::range::RangeFull" ],
              "index_mut",
              []
            |),
            [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::borrow::BorrowMut"
        Self
        (* Trait polymorphic types *) [ (* Borrowed *) Ty.path "str" ]
        (* Instance *) [ ("borrow_mut", InstanceField.Method borrow_mut) ].
  End Impl_core_borrow_BorrowMut_str_for_alloc_string_String.
  
  Module Impl_alloc_borrow_ToOwned_for_str.
    Definition Self : Ty.t := Ty.path "str".
    
    (*     type Owned = String; *)
    Definition _Owned : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn to_owned(&self) -> String {
            unsafe { String::from_utf8_unchecked(self.as_bytes().to_owned()) }
        }
    *)
    Definition to_owned (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "alloc::string::String",
              "from_utf8_unchecked",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "alloc::borrow::ToOwned",
                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                  [],
                  "to_owned",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| self |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_into(&self, target: &mut String) {
            target.clear();
            target.push_str(self);
        }
    *)
    Definition clone_into (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; target ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let target := M.alloc (| target |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "clear", [] |),
                  [ M.read (| target |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "push_str", [] |),
                  [ M.read (| target |); M.read (| self |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "alloc::borrow::ToOwned"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Owned", InstanceField.Ty _Owned);
          ("to_owned", InstanceField.Method to_owned);
          ("clone_into", InstanceField.Method clone_into)
        ].
  End Impl_alloc_borrow_ToOwned_for_str.
  
  Module Impl_str.
    Definition Self : Ty.t := Ty.path "str".
    
    (*
        pub fn into_boxed_bytes(self: Box<str>) -> Box<[u8]> {
            self.into()
        }
    *)
    Definition into_boxed_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::convert::Into",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "str"; Ty.path "alloc::alloc::Global" ],
              [
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ]; Ty.path "alloc::alloc::Global" ]
              ],
              "into",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_boxed_bytes :
      M.IsAssociatedFunction Self "into_boxed_bytes" into_boxed_bytes.
    
    (*
        pub fn replace<P: Pattern>(&self, from: P, to: &str) -> String {
            let mut result = String::new();
            let mut last_end = 0;
            for (start, part) in self.match_indices(from) {
                result.push_str(unsafe { self.get_unchecked(last_end..start) });
                result.push_str(to);
                last_end = start + part.len();
            }
            result.push_str(unsafe { self.get_unchecked(last_end..self.len()) });
            result
        }
    *)
    Definition replace (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ self; from; to ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let from := M.alloc (| from |) in
          let to := M.alloc (| to |) in
          M.read (|
            let~ result :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "new", [] |),
                  []
                |)
              |) in
            let~ last_end := M.alloc (| Value.Integer IntegerKind.Usize 0 |) 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 "core::str::iter::MatchIndices") [] [ P ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "str", "match_indices", [ P ] |),
                          [ M.read (| self |); M.read (| from |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    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::str::iter::MatchIndices") [] [ P ],
                                      [],
                                      "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let start := M.copy (| γ1_0 |) in
                                      let part := M.copy (| γ1_1 |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [
                                              result;
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "str",
                                                  "get_unchecked",
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ]
                                                  ]
                                                |),
                                                [
                                                  M.read (| self |);
                                                  Value.StructRecord
                                                    "core::ops::range::Range"
                                                    [
                                                      ("start", M.read (| last_end |));
                                                      ("end_", M.read (| start |))
                                                    ]
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [ result; M.read (| to |) ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          last_end,
                                          BinOp.Wrap.add (|
                                            M.read (| start |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "str",
                                                "len",
                                                []
                                              |),
                                              [ M.read (| part |) ]
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "push_str", [] |),
                  [
                    result;
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "str",
                        "get_unchecked",
                        [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
                      |),
                      [
                        M.read (| self |);
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", M.read (| last_end |));
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "str", "len", [] |),
                                [ M.read (| self |) ]
                              |))
                          ]
                      ]
                    |)
                  ]
                |)
              |) in
            result
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replace : M.IsAssociatedFunction Self "replace" replace.
    
    (*
        pub fn replacen<P: Pattern>(&self, pat: P, to: &str, count: usize) -> String {
            // Hope to reduce the times of re-allocation
            let mut result = String::with_capacity(32);
            let mut last_end = 0;
            for (start, part) in self.match_indices(pat).take(count) {
                result.push_str(unsafe { self.get_unchecked(last_end..start) });
                result.push_str(to);
                last_end = start + part.len();
            }
            result.push_str(unsafe { self.get_unchecked(last_end..self.len()) });
            result
        }
    *)
    Definition replacen (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ self; pat; to; count ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let pat := M.alloc (| pat |) in
          let to := M.alloc (| to |) in
          let count := M.alloc (| count |) in
          M.read (|
            let~ result :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "alloc::string::String",
                    "with_capacity",
                    []
                  |),
                  [ Value.Integer IntegerKind.Usize 32 ]
                |)
              |) in
            let~ last_end := M.alloc (| Value.Integer IntegerKind.Usize 0 |) 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 "core::iter::adapters::take::Take")
                          []
                          [ Ty.apply (Ty.path "core::str::iter::MatchIndices") [] [ P ] ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply (Ty.path "core::str::iter::MatchIndices") [] [ P ],
                            [],
                            "take",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "match_indices", [ P ] |),
                              [ M.read (| self |); M.read (| pat |) ]
                            |);
                            M.read (| count |)
                          ]
                        |)
                      ]
                    |)
                  |),
                  [
                    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::iter::adapters::take::Take")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "core::str::iter::MatchIndices")
                                            []
                                            [ P ]
                                        ],
                                      [],
                                      "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let start := M.copy (| γ1_0 |) in
                                      let part := M.copy (| γ1_1 |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [
                                              result;
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "str",
                                                  "get_unchecked",
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ]
                                                  ]
                                                |),
                                                [
                                                  M.read (| self |);
                                                  Value.StructRecord
                                                    "core::ops::range::Range"
                                                    [
                                                      ("start", M.read (| last_end |));
                                                      ("end_", M.read (| start |))
                                                    ]
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [ result; M.read (| to |) ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          last_end,
                                          BinOp.Wrap.add (|
                                            M.read (| start |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "str",
                                                "len",
                                                []
                                              |),
                                              [ M.read (| part |) ]
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "push_str", [] |),
                  [
                    result;
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "str",
                        "get_unchecked",
                        [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
                      |),
                      [
                        M.read (| self |);
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", M.read (| last_end |));
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "str", "len", [] |),
                                [ M.read (| self |) ]
                              |))
                          ]
                      ]
                    |)
                  ]
                |)
              |) in
            result
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replacen : M.IsAssociatedFunction Self "replacen" replacen.
    
    (*
        pub fn to_lowercase(&self) -> String {
            let (mut s, rest) = convert_while_ascii(self, u8::to_ascii_lowercase);
    
            let prefix_len = s.len();
    
            for (i, c) in rest.char_indices() {
                if c == 'Σ' {
                    // Σ maps to σ, except at the end of a word where it maps to ς.
                    // This is the only conditional (contextual) but language-independent mapping
                    // in `SpecialCasing.txt`,
                    // so hard-code it rather than have a generic "condition" mechanism.
                    // See https://github.com/rust-lang/rust/issues/26035
                    let sigma_lowercase = map_uppercase_sigma(self, prefix_len + i);
                    s.push(sigma_lowercase);
                } else {
                    match conversions::to_lower(c) {
                        [a, '\0', _] => s.push(a),
                        [a, b, '\0'] => {
                            s.push(a);
                            s.push(b);
                        }
                        [a, b, c] => {
                            s.push(a);
                            s.push(b);
                            s.push(c);
                        }
                    }
                }
            }
            return s;
    
            fn map_uppercase_sigma(from: &str, i: usize) -> char {
                // See https://www.unicode.org/versions/Unicode7.0.0/ch03.pdf#G33992
                // for the definition of `Final_Sigma`.
                debug_assert!('Σ'.len_utf8() == 2);
                let is_word_final = case_ignorable_then_cased(from[..i].chars().rev())
                    && !case_ignorable_then_cased(from[i + 2..].chars());
                if is_word_final { 'ς' } else { 'σ' }
            }
    
            fn case_ignorable_then_cased<I: Iterator<Item = char>>(iter: I) -> bool {
                use core::unicode::{Case_Ignorable, Cased};
                match iter.skip_while(|&c| Case_Ignorable(c)).next() {
                    Some(c) => Cased(c),
                    None => false,
                }
            }
        }
    *)
    Definition to_lowercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.never_to_any (|
                M.read (|
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "alloc::str::convert_while_ascii", [] |),
                        [
                          M.read (| self |);
                          (* ReifyFnPointer *)
                          M.pointer_coercion
                            (M.get_associated_function (| Ty.path "u8", "to_ascii_lowercase", [] |))
                        ]
                      |)
                    |),
                    [
                      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 s := M.copy (| γ0_0 |) in
                          let rest := M.copy (| γ0_1 |) in
                          let~ prefix_len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "alloc::string::String",
                                  "len",
                                  []
                                |),
                                [ s ]
                              |)
                            |) in
                          let~ _ :=
                            M.use
                              (M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::collect::IntoIterator",
                                      Ty.path "core::str::iter::CharIndices",
                                      [],
                                      "into_iter",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "str",
                                          "char_indices",
                                          []
                                        |),
                                        [ M.read (| rest |) ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  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.path "core::str::iter::CharIndices",
                                                    [],
                                                    "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 γ1_0 :=
                                                      M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                                    let γ1_1 :=
                                                      M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                                    let i := M.copy (| γ1_0 |) in
                                                    let c := M.copy (| γ1_1 |) in
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.eq (|
                                                                    M.read (| c |),
                                                                    Value.UnicodeChar 931
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            let~ sigma_lowercase :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Self,
                                                                    "map_uppercase_sigma.to_lowercase",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| self |);
                                                                    BinOp.Wrap.add (|
                                                                      M.read (| prefix_len |),
                                                                      M.read (| i |)
                                                                    |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let~ _ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "alloc::string::String",
                                                                    "push",
                                                                    []
                                                                  |),
                                                                  [ s; M.read (| sigma_lowercase |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::unicode::unicode_data::conversions::to_lower",
                                                                    []
                                                                  |),
                                                                  [ M.read (| c |) ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        0
                                                                      |) in
                                                                    let γ0_1 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        1
                                                                      |) in
                                                                    let γ0_2 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        2
                                                                      |) in
                                                                    let a := M.copy (| γ0_0 |) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ0_1 |),
                                                                        Value.UnicodeChar 0
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "alloc::string::String",
                                                                          "push",
                                                                          []
                                                                        |),
                                                                        [ s; M.read (| a |) ]
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        0
                                                                      |) in
                                                                    let γ0_1 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        1
                                                                      |) in
                                                                    let γ0_2 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        2
                                                                      |) in
                                                                    let a := M.copy (| γ0_0 |) in
                                                                    let b := M.copy (| γ0_1 |) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ0_2 |),
                                                                        Value.UnicodeChar 0
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "alloc::string::String",
                                                                            "push",
                                                                            []
                                                                          |),
                                                                          [ s; M.read (| a |) ]
                                                                        |)
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "alloc::string::String",
                                                                            "push",
                                                                            []
                                                                          |),
                                                                          [ s; M.read (| b |) ]
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        0
                                                                      |) in
                                                                    let γ0_1 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        1
                                                                      |) in
                                                                    let γ0_2 :=
                                                                      M.SubPointer.get_slice_index (|
                                                                        γ,
                                                                        2
                                                                      |) in
                                                                    let a := M.copy (| γ0_0 |) in
                                                                    let b := M.copy (| γ0_1 |) in
                                                                    let c := M.copy (| γ0_2 |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "alloc::string::String",
                                                                            "push",
                                                                            []
                                                                          |),
                                                                          [ s; M.read (| a |) ]
                                                                        |)
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "alloc::string::String",
                                                                            "push",
                                                                            []
                                                                          |),
                                                                          [ s; M.read (| b |) ]
                                                                        |)
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "alloc::string::String",
                                                                            "push",
                                                                            []
                                                                          |),
                                                                          [ s; M.read (| c |) ]
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |)))
                                                      ]
                                                    |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                      |)))
                                ]
                              |)) in
                          M.return_ (| M.read (| s |) |)))
                    ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_lowercase : M.IsAssociatedFunction Self "to_lowercase" to_lowercase.
    
    (*
        pub fn to_uppercase(&self) -> String {
            let (mut s, rest) = convert_while_ascii(self, u8::to_ascii_uppercase);
    
            for c in rest.chars() {
                match conversions::to_upper(c) {
                    [a, '\0', _] => s.push(a),
                    [a, b, '\0'] => {
                        s.push(a);
                        s.push(b);
                    }
                    [a, b, c] => {
                        s.push(a);
                        s.push(b);
                        s.push(c);
                    }
                }
            }
            s
        }
    *)
    Definition to_uppercase (ε : 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.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "alloc::str::convert_while_ascii", [] |),
                  [
                    M.read (| self |);
                    (* ReifyFnPointer *)
                    M.pointer_coercion
                      (M.get_associated_function (| Ty.path "u8", "to_ascii_uppercase", [] |))
                  ]
                |)
              |),
              [
                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 s := M.copy (| γ0_0 |) in
                    let rest := M.copy (| γ0_1 |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.path "core::str::iter::Chars",
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "str", "chars", [] |),
                                  [ M.read (| rest |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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.path "core::str::iter::Chars",
                                              [],
                                              "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 c := M.copy (| γ0_0 |) in
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::unicode::unicode_data::conversions::to_upper",
                                                      []
                                                    |),
                                                    [ M.read (| c |) ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_slice_index (| γ, 0 |) in
                                                      let γ0_1 :=
                                                        M.SubPointer.get_slice_index (| γ, 1 |) in
                                                      let γ0_2 :=
                                                        M.SubPointer.get_slice_index (| γ, 2 |) in
                                                      let a := M.copy (| γ0_0 |) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ0_1 |),
                                                          Value.UnicodeChar 0
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "alloc::string::String",
                                                            "push",
                                                            []
                                                          |),
                                                          [ s; M.read (| a |) ]
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_slice_index (| γ, 0 |) in
                                                      let γ0_1 :=
                                                        M.SubPointer.get_slice_index (| γ, 1 |) in
                                                      let γ0_2 :=
                                                        M.SubPointer.get_slice_index (| γ, 2 |) in
                                                      let a := M.copy (| γ0_0 |) in
                                                      let b := M.copy (| γ0_1 |) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ0_2 |),
                                                          Value.UnicodeChar 0
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "alloc::string::String",
                                                              "push",
                                                              []
                                                            |),
                                                            [ s; M.read (| a |) ]
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "alloc::string::String",
                                                              "push",
                                                              []
                                                            |),
                                                            [ s; M.read (| b |) ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_slice_index (| γ, 0 |) in
                                                      let γ0_1 :=
                                                        M.SubPointer.get_slice_index (| γ, 1 |) in
                                                      let γ0_2 :=
                                                        M.SubPointer.get_slice_index (| γ, 2 |) in
                                                      let a := M.copy (| γ0_0 |) in
                                                      let b := M.copy (| γ0_1 |) in
                                                      let c := M.copy (| γ0_2 |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "alloc::string::String",
                                                              "push",
                                                              []
                                                            |),
                                                            [ s; M.read (| a |) ]
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "alloc::string::String",
                                                              "push",
                                                              []
                                                            |),
                                                            [ s; M.read (| b |) ]
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "alloc::string::String",
                                                              "push",
                                                              []
                                                            |),
                                                            [ s; M.read (| c |) ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    s))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_uppercase : M.IsAssociatedFunction Self "to_uppercase" to_uppercase.
    
    (*
        pub fn into_string(self: Box<str>) -> String {
            let slice = Box::<[u8]>::from(self);
            unsafe { String::from_utf8_unchecked(slice.into_vec()) }
        }
    *)
    Definition into_string (ε : 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~ slice :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply
                      (Ty.path "alloc::boxed::Box")
                      []
                      [
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.apply
                        (Ty.path "alloc::boxed::Box")
                        []
                        [ Ty.path "str"; Ty.path "alloc::alloc::Global" ]
                    ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "alloc::string::String",
                  "from_utf8_unchecked",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "into_vec",
                      [ Ty.path "alloc::alloc::Global" ]
                    |),
                    [ M.read (| slice |) ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_string : M.IsAssociatedFunction Self "into_string" into_string.
    
    (*
        pub fn repeat(&self, n: usize) -> String {
            unsafe { String::from_utf8_unchecked(self.as_bytes().repeat(n)) }
        }
    *)
    Definition repeat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; n ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let n := M.alloc (| n |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "alloc::string::String",
              "from_utf8_unchecked",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                  "repeat",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| self |) ]
                  |);
                  M.read (| n |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_repeat : M.IsAssociatedFunction Self "repeat" repeat.
    
    (*
        pub fn to_ascii_uppercase(&self) -> String {
            let mut s = self.to_owned();
            s.make_ascii_uppercase();
            s
        }
    *)
    Definition to_ascii_uppercase (ε : 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~ s :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "alloc::borrow::ToOwned",
                    Ty.path "str",
                    [],
                    "to_owned",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "make_ascii_uppercase", [] |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::DerefMut",
                        Ty.path "alloc::string::String",
                        [],
                        "deref_mut",
                        []
                      |),
                      [ s ]
                    |)
                  ]
                |)
              |) in
            s
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_ascii_uppercase :
      M.IsAssociatedFunction Self "to_ascii_uppercase" to_ascii_uppercase.
    
    (*
        pub fn to_ascii_lowercase(&self) -> String {
            let mut s = self.to_owned();
            s.make_ascii_lowercase();
            s
        }
    *)
    Definition to_ascii_lowercase (ε : 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~ s :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "alloc::borrow::ToOwned",
                    Ty.path "str",
                    [],
                    "to_owned",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "make_ascii_lowercase", [] |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::DerefMut",
                        Ty.path "alloc::string::String",
                        [],
                        "deref_mut",
                        []
                      |),
                      [ s ]
                    |)
                  ]
                |)
              |) in
            s
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_ascii_lowercase :
      M.IsAssociatedFunction Self "to_ascii_lowercase" to_ascii_lowercase.
  End Impl_str.
  
  (*
  pub unsafe fn from_boxed_utf8_unchecked(v: Box<[u8]>) -> Box<str> {
      unsafe { Box::from_raw(Box::into_raw(v) as *mut str) }
  }
  *)
  Definition from_boxed_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_associated_function (|
            Ty.apply
              (Ty.path "alloc::boxed::Box")
              []
              [ Ty.path "str"; Ty.path "alloc::alloc::Global" ],
            "from_raw",
            []
          |),
          [
            M.rust_cast
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::boxed::Box")
                    []
                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ]; Ty.path "alloc::alloc::Global"
                    ],
                  "into_raw",
                  []
                |),
                [ M.read (| v |) ]
              |))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_boxed_utf8_unchecked :
    M.IsFunction "alloc::str::from_boxed_utf8_unchecked" from_boxed_utf8_unchecked.
  
  (*
  pub fn convert_while_ascii(s: &str, convert: fn(&u8) -> u8) -> (String, &str) {
      // Process the input in chunks of 16 bytes to enable auto-vectorization.
      // Previously the chunk size depended on the size of `usize`,
      // but on 32-bit platforms with sse or neon is also the better choice.
      // The only downside on other platforms would be a bit more loop-unrolling.
      const N: usize = 16;
  
      let mut slice = s.as_bytes();
      let mut out = Vec::with_capacity(slice.len());
      let mut out_slice = out.spare_capacity_mut();
  
      let mut ascii_prefix_len = 0_usize;
      let mut is_ascii = [false; N];
  
      while slice.len() >= N {
          // SAFETY: checked in loop condition
          let chunk = unsafe { slice.get_unchecked(..N) };
          // SAFETY: out_slice has at least same length as input slice and gets sliced with the same offsets
          let out_chunk = unsafe { out_slice.get_unchecked_mut(..N) };
  
          for j in 0..N {
              is_ascii[j] = chunk[j] <= 127;
          }
  
          // Auto-vectorization for this check is a bit fragile, sum and comparing against the chunk
          // size gives the best result, specifically a pmovmsk instruction on x86.
          // See https://github.com/llvm/llvm-project/issues/96395 for why llvm currently does not
          // currently recognize other similar idioms.
          if is_ascii.iter().map(|x| *x as u8).sum::<u8>() as usize != N {
              break;
          }
  
          for j in 0..N {
              out_chunk[j] = MaybeUninit::new(convert(&chunk[j]));
          }
  
          ascii_prefix_len += N;
          slice = unsafe { slice.get_unchecked(N..) };
          out_slice = unsafe { out_slice.get_unchecked_mut(N..) };
      }
  
      // handle the remainder as individual bytes
      while slice.len() > 0 {
          let byte = slice[0];
          if byte > 127 {
              break;
          }
          // SAFETY: out_slice has at least same length as input slice
          unsafe {
              *out_slice.get_unchecked_mut(0) = MaybeUninit::new(convert(&byte));
          }
          ascii_prefix_len += 1;
          slice = unsafe { slice.get_unchecked(1..) };
          out_slice = unsafe { out_slice.get_unchecked_mut(1..) };
      }
  
      unsafe {
          // SAFETY: ascii_prefix_len bytes have been initialized above
          out.set_len(ascii_prefix_len);
  
          // SAFETY: We have written only valid ascii to the output vec
          let ascii_string = String::from_utf8_unchecked(out);
  
          // SAFETY: we know this is a valid char boundary
          // since we only skipped over leading ascii bytes
          let rest = core::str::from_utf8_unchecked(slice);
  
          (ascii_string, rest)
      }
  }
  *)
  Definition convert_while_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ s; convert ] =>
      ltac:(M.monadic
        (let s := M.alloc (| s |) in
        let convert := M.alloc (| convert |) in
        M.read (|
          let~ slice :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                [ M.read (| s |) ]
              |)
            |) in
          let~ out :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  "with_capacity",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "len",
                      []
                    |),
                    [ M.read (| slice |) ]
                  |)
                ]
              |)
            |) in
          let~ out_slice :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  "spare_capacity_mut",
                  []
                |),
                [ out ]
              |)
            |) in
          let~ ascii_prefix_len := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
          let~ is_ascii :=
            M.alloc (| repeat (| Value.Bool false, Value.Integer IntegerKind.Usize 16 |) |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ge (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |),
                                M.read (|
                                  M.get_constant (| "alloc::str::convert_while_ascii::N" |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ chunk :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "get_unchecked",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeTo")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeTo"
                                  [
                                    ("end_",
                                      M.read (|
                                        M.get_constant (| "alloc::str::convert_while_ascii::N" |)
                                      |))
                                  ]
                              ]
                            |)
                          |) in
                        let~ out_chunk :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ Ty.path "u8" ]
                                  ],
                                "get_unchecked_mut",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeTo")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| out_slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeTo"
                                  [
                                    ("end_",
                                      M.read (|
                                        M.get_constant (| "alloc::str::convert_while_ascii::N" |)
                                      |))
                                  ]
                              ]
                            |)
                          |) 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 "core::ops::range::Range")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::str::convert_while_ascii::N"
                                            |)
                                          |))
                                      ]
                                  ]
                                |)
                              |),
                              [
                                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::ops::range::Range")
                                                    []
                                                    [ Ty.path "usize" ],
                                                  [],
                                                  "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 j := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_array_field (|
                                                        is_ascii,
                                                        j
                                                      |),
                                                      BinOp.le (|
                                                        M.read (|
                                                          M.SubPointer.get_array_field (|
                                                            M.read (| chunk |),
                                                            j
                                                          |)
                                                        |),
                                                        Value.Integer IntegerKind.U8 127
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ne (|
                                          M.rust_cast
                                            (M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path "core::iter::adapters::map::Map")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ Ty.path "bool" ];
                                                    Ty.function
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [ Ty.path "bool" ]
                                                          ]
                                                      ]
                                                      (Ty.path "u8")
                                                  ],
                                                [],
                                                "sum",
                                                [ Ty.path "u8" ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ Ty.path "bool" ],
                                                    [],
                                                    "map",
                                                    [
                                                      Ty.path "u8";
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "bool" ]
                                                            ]
                                                        ]
                                                        (Ty.path "u8")
                                                    ]
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.path "bool" ],
                                                        "iter",
                                                        []
                                                      |),
                                                      [ is_ascii ]
                                                    |);
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ α0 ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| α0 |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let x := M.copy (| γ |) in
                                                                      M.rust_cast
                                                                        (M.read (|
                                                                          M.read (| x |)
                                                                        |))))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              ]
                                            |)),
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::str::convert_while_ascii::N"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) 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 "core::ops::range::Range")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::str::convert_while_ascii::N"
                                            |)
                                          |))
                                      ]
                                  ]
                                |)
                              |),
                              [
                                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::ops::range::Range")
                                                    []
                                                    [ Ty.path "usize" ],
                                                  [],
                                                  "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 j := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| out_chunk |),
                                                        j
                                                      |),
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [ Ty.path "u8" ],
                                                          "new",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.read (| convert |),
                                                            [
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| chunk |),
                                                                j
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ _ :=
                          let β := ascii_prefix_len in
                          M.write (|
                            β,
                            BinOp.Wrap.add (|
                              M.read (| β |),
                              M.read (| M.get_constant (| "alloc::str::convert_while_ascii::N" |) |)
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            slice,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "get_unchecked",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [
                                    ("start",
                                      M.read (|
                                        M.get_constant (| "alloc::str::convert_while_ascii::N" |)
                                      |))
                                  ]
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            out_slice,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ Ty.path "u8" ]
                                  ],
                                "get_unchecked_mut",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| out_slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [
                                    ("start",
                                      M.read (|
                                        M.get_constant (| "alloc::str::convert_while_ascii::N" |)
                                      |))
                                  ]
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ byte :=
                          M.copy (|
                            M.SubPointer.get_array_field (|
                              M.read (| slice |),
                              M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| byte |),
                                          Value.Integer IntegerKind.U8 127
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          let~ _ :=
                            M.write (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ Ty.path "u8" ]
                                    ],
                                  "get_unchecked_mut",
                                  [ Ty.path "usize" ]
                                |),
                                [ M.read (| out_slice |); Value.Integer IntegerKind.Usize 0 ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ],
                                  "new",
                                  []
                                |),
                                [ M.call_closure (| M.read (| convert |), [ byte ] |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |) in
                        let~ _ :=
                          let β := ascii_prefix_len in
                          M.write (|
                            β,
                            BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                          |) in
                        let~ _ :=
                          M.write (|
                            slice,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "get_unchecked",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [ ("start", Value.Integer IntegerKind.Usize 1) ]
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            out_slice,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ Ty.path "u8" ]
                                  ],
                                "get_unchecked_mut",
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                              |),
                              [
                                M.read (| out_slice |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [ ("start", Value.Integer IntegerKind.Usize 1) ]
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  "set_len",
                  []
                |),
                [ out; M.read (| ascii_prefix_len |) ]
              |)
            |) in
          let~ ascii_string :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "alloc::string::String",
                  "from_utf8_unchecked",
                  []
                |),
                [ M.read (| out |) ]
              |)
            |) in
          let~ rest :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::str::converts::from_utf8_unchecked", [] |),
                [ M.read (| slice |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [ M.read (| ascii_string |); M.read (| rest |) ] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_convert_while_ascii :
    M.IsFunction "alloc::str::convert_while_ascii" convert_while_ascii.
  
  Module convert_while_ascii.
    Definition value_N : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 16 |))).
  End convert_while_ascii.
End str.
