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

Module fmt.
  Module float.
    (* Trait *)
    (* Empty module 'GeneralFormat' *)
    
    Module Impl_core_fmt_float_GeneralFormat_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                  fn already_rounded_value_should_use_exponential(&self) -> bool {
                      let abs = $t::abs_private( *self);
                      (abs != 0.0 && abs < 1e-4) || abs >= 1e+16
                  }
      *)
      Definition already_rounded_value_should_use_exponential
          (ε : 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~ abs :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "f32", "abs_private", [] |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |) in
              M.alloc (|
                LogicalOp.or (|
                  LogicalOp.and (|
                    BinOp.ne (| M.read (| abs |), M.read (| UnsupportedLiteral |) |),
                    ltac:(M.monadic
                      (BinOp.lt (| M.read (| abs |), M.read (| UnsupportedLiteral |) |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.ge (| M.read (| abs |), M.read (| UnsupportedLiteral |) |)))
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::float::GeneralFormat"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("already_rounded_value_should_use_exponential",
              InstanceField.Method already_rounded_value_should_use_exponential)
          ].
    End Impl_core_fmt_float_GeneralFormat_for_f32.
    
    Module Impl_core_fmt_float_GeneralFormat_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                  fn already_rounded_value_should_use_exponential(&self) -> bool {
                      let abs = $t::abs_private( *self);
                      (abs != 0.0 && abs < 1e-4) || abs >= 1e+16
                  }
      *)
      Definition already_rounded_value_should_use_exponential
          (ε : 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~ abs :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "f64", "abs_private", [] |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |) in
              M.alloc (|
                LogicalOp.or (|
                  LogicalOp.and (|
                    BinOp.ne (| M.read (| abs |), M.read (| UnsupportedLiteral |) |),
                    ltac:(M.monadic
                      (BinOp.lt (| M.read (| abs |), M.read (| UnsupportedLiteral |) |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.ge (| M.read (| abs |), M.read (| UnsupportedLiteral |) |)))
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::float::GeneralFormat"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("already_rounded_value_should_use_exponential",
              InstanceField.Method already_rounded_value_should_use_exponential)
          ].
    End Impl_core_fmt_float_GeneralFormat_for_f64.
    
    (*
    fn float_to_decimal_common_exact<T>(
        fmt: &mut Formatter<'_>,
        num: &T,
        sign: flt2dec::Sign,
        precision: usize,
    ) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        let mut buf: [MaybeUninit<u8>; 1024] = [MaybeUninit::uninit(); 1024]; // enough for f32 and f64
        let mut parts: [MaybeUninit<numfmt::Part<'_>>; 4] = [MaybeUninit::uninit(); 4];
        let formatted = flt2dec::to_exact_fixed_str(
            flt2dec::strategy::grisu::format_exact,
            *num,
            sign,
            precision,
            &mut buf,
            &mut parts,
        );
        // SAFETY: `to_exact_fixed_str` and `format_exact` produce only ASCII characters.
        unsafe { fmt.pad_formatted_parts(&formatted) }
    }
    *)
    Definition float_to_decimal_common_exact
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num; sign; precision ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          let sign := M.alloc (| sign |) in
          let precision := M.alloc (| precision |) in
          M.read (|
            let~ buf :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 1024
                |)
              |) in
            let~ parts :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                        []
                        [ Ty.path "core::num::fmt::Part" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 4
                |)
              |) in
            let~ formatted :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::num::flt2dec::to_exact_fixed_str",
                    [
                      T;
                      Ty.function
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "core::num::flt2dec::decoder::Decoded" ];
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ]
                            ];
                          Ty.path "i16"
                        ]
                        (Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                            Ty.path "i16"
                          ])
                    ]
                  |),
                  [
                    M.get_function (| "core::num::flt2dec::strategy::grisu::format_exact", [] |);
                    M.read (| M.read (| num |) |);
                    M.read (| sign |);
                    M.read (| precision |);
                    buf;
                    parts
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "pad_formatted_parts",
                  []
                |),
                [ M.read (| fmt |); formatted ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_decimal_common_exact :
      M.IsFunction "core::fmt::float::float_to_decimal_common_exact" float_to_decimal_common_exact.
    
    (*
    fn float_to_decimal_common_shortest<T>(
        fmt: &mut Formatter<'_>,
        num: &T,
        sign: flt2dec::Sign,
        precision: usize,
    ) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        // enough for f32 and f64
        let mut buf: [MaybeUninit<u8>; flt2dec::MAX_SIG_DIGITS] =
            [MaybeUninit::uninit(); flt2dec::MAX_SIG_DIGITS];
        let mut parts: [MaybeUninit<numfmt::Part<'_>>; 4] = [MaybeUninit::uninit(); 4];
        let formatted = flt2dec::to_shortest_str(
            flt2dec::strategy::grisu::format_shortest,
            *num,
            sign,
            precision,
            &mut buf,
            &mut parts,
        );
        // SAFETY: `to_shortest_str` and `format_shortest` produce only ASCII characters.
        unsafe { fmt.pad_formatted_parts(&formatted) }
    }
    *)
    Definition float_to_decimal_common_shortest
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num; sign; precision ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          let sign := M.alloc (| sign |) in
          let precision := M.alloc (| precision |) in
          M.read (|
            let~ buf :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 17
                |)
              |) in
            let~ parts :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                        []
                        [ Ty.path "core::num::fmt::Part" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 4
                |)
              |) in
            let~ formatted :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::num::flt2dec::to_shortest_str",
                    [
                      T;
                      Ty.function
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "core::num::flt2dec::decoder::Decoded" ];
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ]
                            ]
                        ]
                        (Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                            Ty.path "i16"
                          ])
                    ]
                  |),
                  [
                    M.get_function (| "core::num::flt2dec::strategy::grisu::format_shortest", [] |);
                    M.read (| M.read (| num |) |);
                    M.read (| sign |);
                    M.read (| precision |);
                    buf;
                    parts
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "pad_formatted_parts",
                  []
                |),
                [ M.read (| fmt |); formatted ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_decimal_common_shortest :
      M.IsFunction
        "core::fmt::float::float_to_decimal_common_shortest"
        float_to_decimal_common_shortest.
    
    (*
    fn float_to_decimal_display<T>(fmt: &mut Formatter<'_>, num: &T) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        let force_sign = fmt.sign_plus();
        let sign = match force_sign {
            false => flt2dec::Sign::Minus,
            true => flt2dec::Sign::MinusPlus,
        };
    
        if let Some(precision) = fmt.precision {
            float_to_decimal_common_exact(fmt, num, sign, precision)
        } else {
            let min_precision = 0;
            float_to_decimal_common_shortest(fmt, num, sign, min_precision)
        }
    }
    *)
    Definition float_to_decimal_display (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          M.read (|
            let~ force_sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Formatter", "sign_plus", [] |),
                  [ M.read (| fmt |) ]
                |)
              |) in
            let~ sign :=
              M.copy (|
                M.match_operator (|
                  force_sign,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool false |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::Minus" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::MinusPlus" [] |)))
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.SubPointer.get_struct_record_field (|
                        M.read (| fmt |),
                        "core::fmt::Formatter",
                        "precision"
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let precision := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::fmt::float::float_to_decimal_common_exact",
                          [ T ]
                        |),
                        [
                          M.read (| fmt |);
                          M.read (| num |);
                          M.read (| sign |);
                          M.read (| precision |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let~ min_precision := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::fmt::float::float_to_decimal_common_shortest",
                          [ T ]
                        |),
                        [
                          M.read (| fmt |);
                          M.read (| num |);
                          M.read (| sign |);
                          M.read (| min_precision |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_decimal_display :
      M.IsFunction "core::fmt::float::float_to_decimal_display" float_to_decimal_display.
    
    (*
    fn float_to_exponential_common_exact<T>(
        fmt: &mut Formatter<'_>,
        num: &T,
        sign: flt2dec::Sign,
        precision: usize,
        upper: bool,
    ) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        let mut buf: [MaybeUninit<u8>; 1024] = [MaybeUninit::uninit(); 1024]; // enough for f32 and f64
        let mut parts: [MaybeUninit<numfmt::Part<'_>>; 6] = [MaybeUninit::uninit(); 6];
        let formatted = flt2dec::to_exact_exp_str(
            flt2dec::strategy::grisu::format_exact,
            *num,
            sign,
            precision,
            upper,
            &mut buf,
            &mut parts,
        );
        // SAFETY: `to_exact_exp_str` and `format_exact` produce only ASCII characters.
        unsafe { fmt.pad_formatted_parts(&formatted) }
    }
    *)
    Definition float_to_exponential_common_exact
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num; sign; precision; upper ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          let sign := M.alloc (| sign |) in
          let precision := M.alloc (| precision |) in
          let upper := M.alloc (| upper |) in
          M.read (|
            let~ buf :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 1024
                |)
              |) in
            let~ parts :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                        []
                        [ Ty.path "core::num::fmt::Part" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 6
                |)
              |) in
            let~ formatted :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::num::flt2dec::to_exact_exp_str",
                    [
                      T;
                      Ty.function
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "core::num::flt2dec::decoder::Decoded" ];
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ]
                            ];
                          Ty.path "i16"
                        ]
                        (Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                            Ty.path "i16"
                          ])
                    ]
                  |),
                  [
                    M.get_function (| "core::num::flt2dec::strategy::grisu::format_exact", [] |);
                    M.read (| M.read (| num |) |);
                    M.read (| sign |);
                    M.read (| precision |);
                    M.read (| upper |);
                    buf;
                    parts
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "pad_formatted_parts",
                  []
                |),
                [ M.read (| fmt |); formatted ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_exponential_common_exact :
      M.IsFunction
        "core::fmt::float::float_to_exponential_common_exact"
        float_to_exponential_common_exact.
    
    (*
    fn float_to_exponential_common_shortest<T>(
        fmt: &mut Formatter<'_>,
        num: &T,
        sign: flt2dec::Sign,
        upper: bool,
    ) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        // enough for f32 and f64
        let mut buf: [MaybeUninit<u8>; flt2dec::MAX_SIG_DIGITS] =
            [MaybeUninit::uninit(); flt2dec::MAX_SIG_DIGITS];
        let mut parts: [MaybeUninit<numfmt::Part<'_>>; 6] = [MaybeUninit::uninit(); 6];
        let formatted = flt2dec::to_shortest_exp_str(
            flt2dec::strategy::grisu::format_shortest,
            *num,
            sign,
            (0, 0),
            upper,
            &mut buf,
            &mut parts,
        );
        // SAFETY: `to_shortest_exp_str` and `format_shortest` produce only ASCII characters.
        unsafe { fmt.pad_formatted_parts(&formatted) }
    }
    *)
    Definition float_to_exponential_common_shortest
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num; sign; upper ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          let sign := M.alloc (| sign |) in
          let upper := M.alloc (| upper |) in
          M.read (|
            let~ buf :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 17
                |)
              |) in
            let~ parts :=
              M.alloc (|
                repeat (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                        []
                        [ Ty.path "core::num::fmt::Part" ],
                      "uninit",
                      []
                    |),
                    []
                  |),
                  Value.Integer IntegerKind.Usize 6
                |)
              |) in
            let~ formatted :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::num::flt2dec::to_shortest_exp_str",
                    [
                      T;
                      Ty.function
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "core::num::flt2dec::decoder::Decoded" ];
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ]
                            ]
                        ]
                        (Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                            Ty.path "i16"
                          ])
                    ]
                  |),
                  [
                    M.get_function (| "core::num::flt2dec::strategy::grisu::format_shortest", [] |);
                    M.read (| M.read (| num |) |);
                    M.read (| sign |);
                    Value.Tuple
                      [ Value.Integer IntegerKind.I16 0; Value.Integer IntegerKind.I16 0 ];
                    M.read (| upper |);
                    buf;
                    parts
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "pad_formatted_parts",
                  []
                |),
                [ M.read (| fmt |); formatted ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_exponential_common_shortest :
      M.IsFunction
        "core::fmt::float::float_to_exponential_common_shortest"
        float_to_exponential_common_shortest.
    
    (*
    fn float_to_exponential_common<T>(fmt: &mut Formatter<'_>, num: &T, upper: bool) -> Result
    where
        T: flt2dec::DecodableFloat,
    {
        let force_sign = fmt.sign_plus();
        let sign = match force_sign {
            false => flt2dec::Sign::Minus,
            true => flt2dec::Sign::MinusPlus,
        };
    
        if let Some(precision) = fmt.precision {
            // 1 integral digit + `precision` fractional digits = `precision + 1` total digits
            float_to_exponential_common_exact(fmt, num, sign, precision + 1, upper)
        } else {
            float_to_exponential_common_shortest(fmt, num, sign, upper)
        }
    }
    *)
    Definition float_to_exponential_common
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num; upper ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          let upper := M.alloc (| upper |) in
          M.read (|
            let~ force_sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Formatter", "sign_plus", [] |),
                  [ M.read (| fmt |) ]
                |)
              |) in
            let~ sign :=
              M.copy (|
                M.match_operator (|
                  force_sign,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool false |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::Minus" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::MinusPlus" [] |)))
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.SubPointer.get_struct_record_field (|
                        M.read (| fmt |),
                        "core::fmt::Formatter",
                        "precision"
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let precision := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::fmt::float::float_to_exponential_common_exact",
                          [ T ]
                        |),
                        [
                          M.read (| fmt |);
                          M.read (| num |);
                          M.read (| sign |);
                          BinOp.Wrap.add (|
                            M.read (| precision |),
                            Value.Integer IntegerKind.Usize 1
                          |);
                          M.read (| upper |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::fmt::float::float_to_exponential_common_shortest",
                          [ T ]
                        |),
                        [ M.read (| fmt |); M.read (| num |); M.read (| sign |); M.read (| upper |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_exponential_common :
      M.IsFunction "core::fmt::float::float_to_exponential_common" float_to_exponential_common.
    
    (*
    fn float_to_general_debug<T>(fmt: &mut Formatter<'_>, num: &T) -> Result
    where
        T: flt2dec::DecodableFloat + GeneralFormat,
    {
        let force_sign = fmt.sign_plus();
        let sign = match force_sign {
            false => flt2dec::Sign::Minus,
            true => flt2dec::Sign::MinusPlus,
        };
    
        if let Some(precision) = fmt.precision {
            // this behavior of {:.PREC?} predates exponential formatting for {:?}
            float_to_decimal_common_exact(fmt, num, sign, precision)
        } else {
            // since there is no precision, there will be no rounding
            if num.already_rounded_value_should_use_exponential() {
                let upper = false;
                float_to_exponential_common_shortest(fmt, num, sign, upper)
            } else {
                let min_precision = 1;
                float_to_decimal_common_shortest(fmt, num, sign, min_precision)
            }
        }
    }
    *)
    Definition float_to_general_debug (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ fmt; num ] =>
        ltac:(M.monadic
          (let fmt := M.alloc (| fmt |) in
          let num := M.alloc (| num |) in
          M.read (|
            let~ force_sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Formatter", "sign_plus", [] |),
                  [ M.read (| fmt |) ]
                |)
              |) in
            let~ sign :=
              M.copy (|
                M.match_operator (|
                  force_sign,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool false |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::Minus" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::num::flt2dec::Sign::MinusPlus" [] |)))
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.SubPointer.get_struct_record_field (|
                        M.read (| fmt |),
                        "core::fmt::Formatter",
                        "precision"
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let precision := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::fmt::float::float_to_decimal_common_exact",
                          [ T ]
                        |),
                        [
                          M.read (| fmt |);
                          M.read (| num |);
                          M.read (| sign |);
                          M.read (| precision |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::fmt::float::GeneralFormat",
                                      T,
                                      [],
                                      "already_rounded_value_should_use_exponential",
                                      []
                                    |),
                                    [ M.read (| num |) ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ upper := M.alloc (| Value.Bool false |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::fmt::float::float_to_exponential_common_shortest",
                                  [ T ]
                                |),
                                [
                                  M.read (| fmt |);
                                  M.read (| num |);
                                  M.read (| sign |);
                                  M.read (| upper |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let~ min_precision :=
                              M.alloc (| Value.Integer IntegerKind.Usize 1 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::fmt::float::float_to_decimal_common_shortest",
                                  [ T ]
                                |),
                                [
                                  M.read (| fmt |);
                                  M.read (| num |);
                                  M.read (| sign |);
                                  M.read (| min_precision |)
                                ]
                              |)
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_float_to_general_debug :
      M.IsFunction "core::fmt::float::float_to_general_debug" float_to_general_debug.
    
    Module Impl_core_fmt_Debug_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_general_debug(fmt, self)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (| "core::fmt::float::float_to_general_debug", [ Ty.path "f32" ] |),
              [ M.read (| fmt |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_f32.
    
    Module Impl_core_fmt_Display_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_decimal_display(fmt, self)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (| "core::fmt::float::float_to_decimal_display", [ Ty.path "f32" ] |),
              [ M.read (| fmt |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_f32.
    
    Module Impl_core_fmt_LowerExp_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_exponential_common(fmt, self, false)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (|
                "core::fmt::float::float_to_exponential_common",
                [ Ty.path "f32" ]
              |),
              [ M.read (| fmt |); M.read (| self |); Value.Bool false ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::LowerExp"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_LowerExp_for_f32.
    
    Module Impl_core_fmt_UpperExp_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_exponential_common(fmt, self, true)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (|
                "core::fmt::float::float_to_exponential_common",
                [ Ty.path "f32" ]
              |),
              [ M.read (| fmt |); M.read (| self |); Value.Bool true ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::UpperExp"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_UpperExp_for_f32.
    
    Module Impl_core_fmt_Debug_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_general_debug(fmt, self)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (| "core::fmt::float::float_to_general_debug", [ Ty.path "f64" ] |),
              [ M.read (| fmt |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_f64.
    
    Module Impl_core_fmt_Display_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_decimal_display(fmt, self)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (| "core::fmt::float::float_to_decimal_display", [ Ty.path "f64" ] |),
              [ M.read (| fmt |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_f64.
    
    Module Impl_core_fmt_LowerExp_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_exponential_common(fmt, self, false)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (|
                "core::fmt::float::float_to_exponential_common",
                [ Ty.path "f64" ]
              |),
              [ M.read (| fmt |); M.read (| self |); Value.Bool false ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::LowerExp"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_LowerExp_for_f64.
    
    Module Impl_core_fmt_UpperExp_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                  fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
                      float_to_exponential_common(fmt, self, true)
                  }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_function (|
                "core::fmt::float::float_to_exponential_common",
                [ Ty.path "f64" ]
              |),
              [ M.read (| fmt |); M.read (| self |); Value.Bool true ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::UpperExp"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_UpperExp_for_f64.
    
    Module Impl_core_fmt_Debug_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*
          fn fmt(&self, f: &mut Formatter<'_>) -> Result {
              write!(f, "{:#06x}", self.to_bits())
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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", "write_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Arguments",
                    "new_v1_formatted",
                    []
                  |),
                  [
                    M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_lower_hex",
                              [ Ty.path "u16" ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "f16", "to_bits", [] |),
                                  [ M.read (| M.read (| self |) |) ]
                                |)
                              |)
                            ]
                          |)
                        ]
                    |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Placeholder",
                              "new",
                              []
                            |),
                            [
                              Value.Integer IntegerKind.Usize 0;
                              Value.UnicodeChar 32;
                              Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                              Value.Integer IntegerKind.U32 12;
                              Value.StructTuple "core::fmt::rt::Count::Implied" [];
                              Value.StructTuple
                                "core::fmt::rt::Count::Is"
                                [ Value.Integer IntegerKind.Usize 6 ]
                            ]
                          |)
                        ]
                    |);
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::rt::UnsafeArg", "new", [] |),
                      []
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_f16.
    
    Module Impl_core_fmt_Debug_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*
          fn fmt(&self, f: &mut Formatter<'_>) -> Result {
              write!(f, "{:#034x}", self.to_bits())
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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", "write_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Arguments",
                    "new_v1_formatted",
                    []
                  |),
                  [
                    M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_lower_hex",
                              [ Ty.path "u128" ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "f128", "to_bits", [] |),
                                  [ M.read (| M.read (| self |) |) ]
                                |)
                              |)
                            ]
                          |)
                        ]
                    |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Placeholder",
                              "new",
                              []
                            |),
                            [
                              Value.Integer IntegerKind.Usize 0;
                              Value.UnicodeChar 32;
                              Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                              Value.Integer IntegerKind.U32 12;
                              Value.StructTuple "core::fmt::rt::Count::Implied" [];
                              Value.StructTuple
                                "core::fmt::rt::Count::Is"
                                [ Value.Integer IntegerKind.Usize 34 ]
                            ]
                          |)
                        ]
                    |);
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::rt::UnsafeArg", "new", [] |),
                      []
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_f128.
  End float.
End fmt.
