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

Module escape.
  Definition value_HEX_DIGITS : Value.t :=
    M.run
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [
                Ty.apply
                  (Ty.path "&")
                  []
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 16 ]
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                  ]
              ],
            "unwrap",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ],
                "as_ascii",
                []
              |),
              [ M.read (| UnsupportedLiteral |) ]
            |)
          ]
        |))).
  
  (*
  const fn backslash<const N: usize>(a: ascii::Char) -> ([ascii::Char; N], Range<u8>) {
      const { assert!(N >= 2) };
  
      let mut output = [ascii::Char::Null; N];
  
      output[0] = ascii::Char::ReverseSolidus;
      output[1] = a;
  
      (output, 0..2)
  }
  *)
  Definition backslash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [], [ a ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        M.read (|
          let~ _ := M.get_constant (| "core::escape::backslash_discriminant" |) in
          let~ output :=
            M.alloc (|
              repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
              |),
              Value.StructTuple "core::ascii::ascii_char::AsciiChar::ReverseSolidus" []
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 1 |)
              |),
              M.read (| a |)
            |) in
          M.alloc (|
            Value.Tuple
              [
                M.read (| output |);
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.U8 0);
                    ("end_", Value.Integer IntegerKind.U8 2)
                  ]
              ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_backslash : M.IsFunction "core::escape::backslash" backslash.
  
  (*
  const fn escape_ascii<const N: usize>(byte: u8) -> ([ascii::Char; N], Range<u8>) {
      const { assert!(N >= 4) };
  
      match byte {
          b'\t' => backslash(ascii::Char::SmallT),
          b'\r' => backslash(ascii::Char::SmallR),
          b'\n' => backslash(ascii::Char::SmallN),
          b'\\' => backslash(ascii::Char::ReverseSolidus),
          b'\'' => backslash(ascii::Char::Apostrophe),
          b'\"' => backslash(ascii::Char::QuotationMark),
          byte => {
              let mut output = [ascii::Char::Null; N];
  
              if let Some(c) = byte.as_ascii()
                  && !byte.is_ascii_control()
              {
                  output[0] = c;
                  (output, 0..1)
              } else {
                  let hi = HEX_DIGITS[(byte >> 4) as usize];
                  let lo = HEX_DIGITS[(byte & 0xf) as usize];
  
                  output[0] = ascii::Char::ReverseSolidus;
                  output[1] = ascii::Char::SmallX;
                  output[2] = hi;
                  output[3] = lo;
  
                  (output, 0..4)
              }
          }
      }
  }
  "
  *)
  Definition escape_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [], [ byte ] =>
      ltac:(M.monadic
        (let byte := M.alloc (| byte |) in
        M.read (|
          let~ _ := M.get_constant (| "core::escape::escape_ascii_discriminant" |) in
          M.match_operator (|
            byte,
            [
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 9
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallT" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 13
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallR" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 10
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallN" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 92
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::ReverseSolidus" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 39
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::Apostrophe" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.U8 34
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::escape::backslash", [] |),
                      [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::QuotationMark" [] ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let byte := M.copy (| γ |) in
                  let~ output :=
                    M.alloc (|
                      repeat (|
                        Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [],
                        N
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "u8", "as_ascii", [] |),
                                [ byte ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let c := M.copy (| γ0_0 |) in
                          let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "u8",
                                      "is_ascii_control",
                                      []
                                    |),
                                    [ byte ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                output,
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                              |),
                              M.read (| c |)
                            |) in
                          M.alloc (|
                            Value.Tuple
                              [
                                M.read (| output |);
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", Value.Integer IntegerKind.U8 0);
                                    ("end_", Value.Integer IntegerKind.U8 1)
                                  ]
                              ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ hi :=
                            M.copy (|
                              M.SubPointer.get_array_field (|
                                M.get_constant (| "core::escape::HEX_DIGITS" |),
                                M.alloc (|
                                  M.rust_cast
                                    (BinOp.Wrap.shr (|
                                      M.read (| byte |),
                                      Value.Integer IntegerKind.I32 4
                                    |))
                                |)
                              |)
                            |) in
                          let~ lo :=
                            M.copy (|
                              M.SubPointer.get_array_field (|
                                M.get_constant (| "core::escape::HEX_DIGITS" |),
                                M.alloc (|
                                  M.rust_cast
                                    (BinOp.bit_and
                                      (M.read (| byte |))
                                      (Value.Integer IntegerKind.U8 15))
                                |)
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                output,
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                              |),
                              Value.StructTuple
                                "core::ascii::ascii_char::AsciiChar::ReverseSolidus"
                                []
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                output,
                                M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                              |),
                              Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallX" []
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                output,
                                M.alloc (| Value.Integer IntegerKind.Usize 2 |)
                              |),
                              M.read (| hi |)
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                output,
                                M.alloc (| Value.Integer IntegerKind.Usize 3 |)
                              |),
                              M.read (| lo |)
                            |) in
                          M.alloc (|
                            Value.Tuple
                              [
                                M.read (| output |);
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", Value.Integer IntegerKind.U8 0);
                                    ("end_", Value.Integer IntegerKind.U8 4)
                                  ]
                              ]
                          |)))
                    ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_escape_ascii : M.IsFunction "core::escape::escape_ascii" escape_ascii.
  
  (*
  const fn escape_unicode<const N: usize>(c: char) -> ([ascii::Char; N], Range<u8>) {
      const { assert!(N >= 10 && N < u8::MAX as usize) };
  
      let c = c as u32;
  
      // OR-ing `1` ensures that for `c == 0` the code computes that
      // one digit should be printed.
      let start = (c | 1).leading_zeros() as usize / 4 - 2;
  
      let mut output = [ascii::Char::Null; N];
      output[3] = HEX_DIGITS[((c >> 20) & 15) as usize];
      output[4] = HEX_DIGITS[((c >> 16) & 15) as usize];
      output[5] = HEX_DIGITS[((c >> 12) & 15) as usize];
      output[6] = HEX_DIGITS[((c >> 8) & 15) as usize];
      output[7] = HEX_DIGITS[((c >> 4) & 15) as usize];
      output[8] = HEX_DIGITS[((c >> 0) & 15) as usize];
      output[9] = ascii::Char::RightCurlyBracket;
      output[start + 0] = ascii::Char::ReverseSolidus;
      output[start + 1] = ascii::Char::SmallU;
      output[start + 2] = ascii::Char::LeftCurlyBracket;
  
      (output, (start as u8)..(N as u8))
  }
  *)
  Definition escape_unicode (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [], [ c ] =>
      ltac:(M.monadic
        (let c := M.alloc (| c |) in
        M.read (|
          let~ _ := M.get_constant (| "core::escape::escape_unicode_discriminant" |) in
          let~ c := M.alloc (| M.rust_cast (M.read (| c |)) |) in
          let~ start :=
            M.alloc (|
              BinOp.Wrap.sub (|
                BinOp.Wrap.div (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "u32", "leading_zeros", [] |),
                      [ BinOp.bit_or (M.read (| c |)) (Value.Integer IntegerKind.U32 1) ]
                    |)),
                  Value.Integer IntegerKind.Usize 4
                |),
                Value.Integer IntegerKind.Usize 2
              |)
            |) in
          let~ output :=
            M.alloc (|
              repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 3 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 20 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 4 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 16 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 5 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 12 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 6 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 8 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 7 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 4 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 8 |)
              |),
              M.read (|
                M.SubPointer.get_array_field (|
                  M.get_constant (| "core::escape::HEX_DIGITS" |),
                  M.alloc (|
                    M.rust_cast
                      (BinOp.bit_and
                        (BinOp.Wrap.shr (| M.read (| c |), Value.Integer IntegerKind.I32 0 |))
                        (Value.Integer IntegerKind.U32 15))
                  |)
                |)
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (| Value.Integer IntegerKind.Usize 9 |)
              |),
              Value.StructTuple "core::ascii::ascii_char::AsciiChar::RightCurlyBracket" []
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (|
                  BinOp.Wrap.add (| M.read (| start |), Value.Integer IntegerKind.Usize 0 |)
                |)
              |),
              Value.StructTuple "core::ascii::ascii_char::AsciiChar::ReverseSolidus" []
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (|
                  BinOp.Wrap.add (| M.read (| start |), Value.Integer IntegerKind.Usize 1 |)
                |)
              |),
              Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallU" []
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                output,
                M.alloc (|
                  BinOp.Wrap.add (| M.read (| start |), Value.Integer IntegerKind.Usize 2 |)
                |)
              |),
              Value.StructTuple "core::ascii::ascii_char::AsciiChar::LeftCurlyBracket" []
            |) in
          M.alloc (|
            Value.Tuple
              [
                M.read (| output |);
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", M.rust_cast (M.read (| start |)));
                    ("end_",
                      M.rust_cast
                        (M.read (| M.get_constant (| "core::escape::escape_unicode::N" |) |)))
                  ]
              ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_escape_unicode : M.IsFunction "core::escape::escape_unicode" escape_unicode.
  
  (* StructRecord
    {
      name := "EscapeIterInner";
      const_params := [ "N" ];
      ty_params := [];
      fields :=
        [
          ("data",
            Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ]);
          ("alive", Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_core_escape_EscapeIterInner_N.
    Definition Self (N : Value.t) : Ty.t :=
      Ty.apply (Ty.path "core::escape::EscapeIterInner") [ N ] [].
    
    (* Clone *)
    Definition clone (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::escape::EscapeIterInner"
            [
              ("data",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "array")
                      [ N ]
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::escape::EscapeIterInner",
                      "data"
                    |)
                  ]
                |));
              ("alive",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::escape::EscapeIterInner",
                      "alive"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self N)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone N)) ].
  End Impl_core_clone_Clone_for_core_escape_EscapeIterInner_N.
  
  Module Impl_core_fmt_Debug_for_core_escape_EscapeIterInner_N.
    Definition Self (N : Value.t) : Ty.t :=
      Ty.apply (Ty.path "core::escape::EscapeIterInner") [ N ] [].
    
    (* Debug *)
    Definition fmt (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "EscapeIterInner" |);
              M.read (| Value.String "data" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::escape::EscapeIterInner",
                "data"
              |);
              M.read (| Value.String "alive" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::escape::EscapeIterInner",
                  "alive"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self N)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt N)) ].
  End Impl_core_fmt_Debug_for_core_escape_EscapeIterInner_N.
  
  Module Impl_core_escape_EscapeIterInner_N.
    Definition Self (N : Value.t) : Ty.t :=
      Ty.apply (Ty.path "core::escape::EscapeIterInner") [ N ] [].
    
    (*
        pub const fn backslash(c: ascii::Char) -> Self {
            let (data, range) = backslash(c);
            Self { data, alive: range }
        }
    *)
    Definition backslash (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ c ] =>
        ltac:(M.monadic
          (let c := M.alloc (| c |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::escape::backslash", [] |),
                  [ M.read (| c |) ]
                |)
              |),
              [
                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 data := M.copy (| γ0_0 |) in
                    let range := M.copy (| γ0_1 |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::escape::EscapeIterInner"
                        [ ("data", M.read (| data |)); ("alive", M.read (| range |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_backslash :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "backslash" (backslash N).
    
    (*
        pub const fn ascii(c: u8) -> Self {
            let (data, range) = escape_ascii(c);
            Self { data, alive: range }
        }
    *)
    Definition ascii (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ c ] =>
        ltac:(M.monadic
          (let c := M.alloc (| c |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::escape::escape_ascii", [] |),
                  [ M.read (| c |) ]
                |)
              |),
              [
                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 data := M.copy (| γ0_0 |) in
                    let range := M.copy (| γ0_1 |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::escape::EscapeIterInner"
                        [ ("data", M.read (| data |)); ("alive", M.read (| range |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_ascii :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "ascii" (ascii N).
    
    (*
        pub const fn unicode(c: char) -> Self {
            let (data, range) = escape_unicode(c);
            Self { data, alive: range }
        }
    *)
    Definition unicode (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ c ] =>
        ltac:(M.monadic
          (let c := M.alloc (| c |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::escape::escape_unicode", [] |),
                  [ M.read (| c |) ]
                |)
              |),
              [
                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 data := M.copy (| γ0_0 |) in
                    let range := M.copy (| γ0_1 |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::escape::EscapeIterInner"
                        [ ("data", M.read (| data |)); ("alive", M.read (| range |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unicode :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "unicode" (unicode N).
    
    (*
        pub const fn empty() -> Self {
            Self { data: [ascii::Char::Null; N], alive: 0..0 }
        }
    *)
    Definition empty (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::escape::EscapeIterInner"
            [
              ("data",
                repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |));
              ("alive",
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.U8 0);
                    ("end_", Value.Integer IntegerKind.U8 0)
                  ])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_empty :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "empty" (empty N).
    
    (*
        pub fn as_ascii(&self) -> &[ascii::Char] {
            // SAFETY: `self.alive` is guaranteed to be a valid range for indexing `self.data`.
            unsafe {
                self.data.get_unchecked(usize::from(self.alive.start)..usize::from(self.alive.end))
            }
        }
    *)
    Definition as_ascii (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "slice") [] [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
              "get_unchecked",
              [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::escape::EscapeIterInner",
                "data"
              |);
              Value.StructRecord
                "core::ops::range::Range"
                [
                  ("start",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::From",
                        Ty.path "usize",
                        [ Ty.path "u8" ],
                        "from",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::escape::EscapeIterInner",
                              "alive"
                            |),
                            "core::ops::range::Range",
                            "start"
                          |)
                        |)
                      ]
                    |));
                  ("end_",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::From",
                        Ty.path "usize",
                        [ Ty.path "u8" ],
                        "from",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::escape::EscapeIterInner",
                              "alive"
                            |),
                            "core::ops::range::Range",
                            "end"
                          |)
                        |)
                      ]
                    |))
                ]
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ascii :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "as_ascii" (as_ascii N).
    
    (*
        pub fn as_str(&self) -> &str {
            self.as_ascii().as_str()
        }
    *)
    Definition as_str (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "slice") [] [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
              "as_str",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::escape::EscapeIterInner") [ N ] [],
                  "as_ascii",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_str :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "as_str" (as_str N).
    
    (*
        pub fn len(&self) -> usize {
            usize::from(self.alive.end - self.alive.start)
        }
    *)
    Definition len (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::convert::From",
              Ty.path "usize",
              [ Ty.path "u8" ],
              "from",
              []
            |),
            [
              BinOp.Wrap.sub (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::escape::EscapeIterInner",
                      "alive"
                    |),
                    "core::ops::range::Range",
                    "end"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::escape::EscapeIterInner",
                      "alive"
                    |),
                    "core::ops::range::Range",
                    "start"
                  |)
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_len :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "len" (len N).
    
    (*
        pub fn next(&mut self) -> Option<u8> {
            let i = self.alive.next()?;
    
            // SAFETY: `i` is guaranteed to be a valid index for `self.data`.
            unsafe { Some(self.data.get_unchecked(usize::from(i)).to_u8()) }
        }
    *)
    Definition next (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ i :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ],
                                [],
                                "next",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::escape::EscapeIterInner",
                                  "alive"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "u8" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "core::convert::Infallible" ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.StructTuple
                    "core::option::Option::Some"
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ascii::ascii_char::AsciiChar",
                          "to_u8",
                          []
                        |),
                        [
                          M.read (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                "get_unchecked",
                                [ Ty.path "usize" ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::escape::EscapeIterInner",
                                  "data"
                                |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.path "usize",
                                    [ Ty.path "u8" ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| i |) ]
                                |)
                              ]
                            |)
                          |)
                        ]
                      |)
                    ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_next :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "next" (next N).
    
    (*
        pub fn next_back(&mut self) -> Option<u8> {
            let i = self.alive.next_back()?;
    
            // SAFETY: `i` is guaranteed to be a valid index for `self.data`.
            unsafe { Some(self.data.get_unchecked(usize::from(i)).to_u8()) }
        }
    *)
    Definition next_back (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ i :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::double_ended::DoubleEndedIterator",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ],
                                [],
                                "next_back",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::escape::EscapeIterInner",
                                  "alive"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "u8" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "core::convert::Infallible" ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.StructTuple
                    "core::option::Option::Some"
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ascii::ascii_char::AsciiChar",
                          "to_u8",
                          []
                        |),
                        [
                          M.read (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                "get_unchecked",
                                [ Ty.path "usize" ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::escape::EscapeIterInner",
                                  "data"
                                |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.path "usize",
                                    [ Ty.path "u8" ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| i |) ]
                                |)
                              ]
                            |)
                          |)
                        ]
                      |)
                    ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_next_back :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "next_back" (next_back N).
    
    (*
        pub fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
            self.alive.advance_by(n)
        }
    *)
    Definition advance_by (N : Value.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self; n ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let n := M.alloc (| n |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ],
              [],
              "advance_by",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::escape::EscapeIterInner",
                "alive"
              |);
              M.read (| n |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_advance_by :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "advance_by" (advance_by N).
    
    (*
        pub fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
            self.alive.advance_back_by(n)
        }
    *)
    Definition advance_back_by
        (N : Value.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N in
      match ε, τ, α with
      | [], [], [ self; n ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let n := M.alloc (| n |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::double_ended::DoubleEndedIterator",
              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "u8" ],
              [],
              "advance_back_by",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::escape::EscapeIterInner",
                "alive"
              |);
              M.read (| n |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_advance_back_by :
      forall (N : Value.t),
      M.IsAssociatedFunction (Self N) "advance_back_by" (advance_back_by N).
  End Impl_core_escape_EscapeIterInner_N.
End escape.
