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

Module num.
  Module dec2flt.
    Module slow.
      (*
      pub(crate) fn parse_long_mantissa<F: RawFloat>(s: &[u8]) -> BiasedFp {
          const MAX_SHIFT: usize = 60;
          const NUM_POWERS: usize = 19;
          const POWERS: [u8; 19] =
              [0, 3, 6, 9, 13, 16, 19, 23, 26, 29, 33, 36, 39, 43, 46, 49, 53, 56, 59];
      
          let get_shift = |n| {
              if n < NUM_POWERS { POWERS[n] as usize } else { MAX_SHIFT }
          };
      
          let fp_zero = BiasedFp::zero_pow2(0);
          let fp_inf = BiasedFp::zero_pow2(F::INFINITE_POWER);
      
          let mut d = parse_decimal(s);
      
          // Short-circuit if the value can only be a literal 0 or infinity.
          if d.num_digits == 0 || d.decimal_point < -324 {
              return fp_zero;
          } else if d.decimal_point >= 310 {
              return fp_inf;
          }
          let mut exp2 = 0_i32;
          // Shift right toward (1/2 ... 1].
          while d.decimal_point > 0 {
              let n = d.decimal_point as usize;
              let shift = get_shift(n);
              d.right_shift(shift);
              if d.decimal_point < -Decimal::DECIMAL_POINT_RANGE {
                  return fp_zero;
              }
              exp2 += shift as i32;
          }
          // Shift left toward (1/2 ... 1].
          while d.decimal_point <= 0 {
              let shift = if d.decimal_point == 0 {
                  match d.digits[0] {
                      digit if digit >= 5 => break,
                      0 | 1 => 2,
                      _ => 1,
                  }
              } else {
                  get_shift((-d.decimal_point) as _)
              };
              d.left_shift(shift);
              if d.decimal_point > Decimal::DECIMAL_POINT_RANGE {
                  return fp_inf;
              }
              exp2 -= shift as i32;
          }
          // We are now in the range [1/2 ... 1] but the binary format uses [1 ... 2].
          exp2 -= 1;
          while (F::MINIMUM_EXPONENT + 1) > exp2 {
              let mut n = ((F::MINIMUM_EXPONENT + 1) - exp2) as usize;
              if n > MAX_SHIFT {
                  n = MAX_SHIFT;
              }
              d.right_shift(n);
              exp2 += n as i32;
          }
          if (exp2 - F::MINIMUM_EXPONENT) >= F::INFINITE_POWER {
              return fp_inf;
          }
          // Shift the decimal to the hidden bit, and then round the value
          // to get the high mantissa+1 bits.
          d.left_shift(F::MANTISSA_EXPLICIT_BITS + 1);
          let mut mantissa = d.round();
          if mantissa >= (1_u64 << (F::MANTISSA_EXPLICIT_BITS + 1)) {
              // Rounding up overflowed to the carry bit, need to
              // shift back to the hidden bit.
              d.right_shift(1);
              exp2 += 1;
              mantissa = d.round();
              if (exp2 - F::MINIMUM_EXPONENT) >= F::INFINITE_POWER {
                  return fp_inf;
              }
          }
          let mut power2 = exp2 - F::MINIMUM_EXPONENT;
          if mantissa < (1_u64 << F::MANTISSA_EXPLICIT_BITS) {
              power2 -= 1;
          }
          // Zero out all the bits above the explicit mantissa bits.
          mantissa &= (1_u64 << F::MANTISSA_EXPLICIT_BITS) - 1;
          BiasedFp { f: mantissa, e: power2 }
      }
      *)
      Definition parse_long_mantissa (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ F ], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ get_shift :=
                    M.alloc (|
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let n := M.copy (| γ |) in
                                        M.read (|
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.lt (|
                                                          M.read (| n |),
                                                          M.read (|
                                                            M.get_constant (|
                                                              "core::num::dec2flt::slow::parse_long_mantissa::NUM_POWERS"
                                                            |)
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.rust_cast
                                                      (M.read (|
                                                        M.SubPointer.get_array_field (|
                                                          M.get_constant (|
                                                            "core::num::dec2flt::slow::parse_long_mantissa::POWERS"
                                                          |),
                                                          n
                                                        |)
                                                      |))
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.get_constant (|
                                                    "core::num::dec2flt::slow::parse_long_mantissa::MAX_SHIFT"
                                                  |)))
                                            ]
                                          |)
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |) in
                  let~ fp_zero :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::common::BiasedFp",
                          "zero_pow2",
                          []
                        |),
                        [ Value.Integer IntegerKind.I32 0 ]
                      |)
                    |) in
                  let~ fp_inf :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::common::BiasedFp",
                          "zero_pow2",
                          []
                        |),
                        [
                          M.read (|
                            M.get_constant (|
                              "core::num::dec2flt::float::RawFloat::INFINITE_POWER"
                            |)
                          |)
                        ]
                      |)
                    |) in
                  let~ d :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::num::dec2flt::decimal::parse_decimal", [] |),
                        [ M.read (| s |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.or (|
                                    BinOp.eq (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          d,
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.lt (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            d,
                                            "core::num::dec2flt::decimal::Decimal",
                                            "decimal_point"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.I32 (-324)
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| fp_zero |) |) |) |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                d,
                                                "core::num::dec2flt::decimal::Decimal",
                                                "decimal_point"
                                              |)
                                            |),
                                            Value.Integer IntegerKind.I32 310
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (| M.return_ (| M.read (| fp_inf |) |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |)))
                      ]
                    |) in
                  let~ exp2 := M.alloc (| Value.Integer IntegerKind.I32 0 |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.gt (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            d,
                                            "core::num::dec2flt::decimal::Decimal",
                                            "decimal_point"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.I32 0
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ n :=
                                  M.alloc (|
                                    M.rust_cast
                                      (M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          d,
                                          "core::num::dec2flt::decimal::Decimal",
                                          "decimal_point"
                                        |)
                                      |))
                                  |) in
                                let~ shift :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::function::Fn",
                                        Ty.function
                                          [ Ty.tuple [ Ty.path "usize" ] ]
                                          (Ty.path "usize"),
                                        [ Ty.tuple [ Ty.path "usize" ] ],
                                        "call",
                                        []
                                      |),
                                      [ get_shift; Value.Tuple [ M.read (| n |) ] ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::num::dec2flt::decimal::Decimal",
                                        "right_shift",
                                        []
                                      |),
                                      [ d; M.read (| shift |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      d,
                                                      "core::num::dec2flt::decimal::Decimal",
                                                      "decimal_point"
                                                    |)
                                                  |),
                                                  UnOp.neg (|
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::num::dec2flt::decimal::DECIMAL_POINT_RANGE"
                                                      |)
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (| M.return_ (| M.read (| fp_zero |) |) |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  let β := exp2 in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      M.rust_cast (M.read (| shift |))
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.le (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            d,
                                            "core::num::dec2flt::decimal::Decimal",
                                            "decimal_point"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.I32 0
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ shift :=
                                  M.copy (|
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.eq (|
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        d,
                                                        "core::num::dec2flt::decimal::Decimal",
                                                        "decimal_point"
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.I32 0
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.match_operator (|
                                              M.SubPointer.get_array_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  d,
                                                  "core::num::dec2flt::decimal::Decimal",
                                                  "digits"
                                                |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let digit := M.copy (| γ |) in
                                                    let γ :=
                                                      M.alloc (|
                                                        BinOp.ge (|
                                                          M.read (| digit |),
                                                          Value.Integer IntegerKind.U8 5
                                                        |)
                                                      |) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (| M.read (| M.break (||) |) |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.find_or_pattern (|
                                                      γ,
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Integer IntegerKind.U8 0
                                                              |) in
                                                            Value.Tuple []));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Integer IntegerKind.U8 1
                                                              |) in
                                                            Value.Tuple []))
                                                      ],
                                                      M.closure
                                                        (fun γ =>
                                                          ltac:(M.monadic
                                                            match γ with
                                                            | [] =>
                                                              ltac:(M.monadic
                                                                (M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)))
                                                            | _ =>
                                                              M.impossible
                                                                "wrong number of arguments"
                                                            end))
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.alloc (|
                                                      Value.Integer IntegerKind.Usize 1
                                                    |)))
                                              ]
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::Fn",
                                                  Ty.function
                                                    [ Ty.tuple [ Ty.path "usize" ] ]
                                                    (Ty.path "usize"),
                                                  [ Ty.tuple [ Ty.path "usize" ] ],
                                                  "call",
                                                  []
                                                |),
                                                [
                                                  get_shift;
                                                  Value.Tuple
                                                    [
                                                      M.rust_cast
                                                        (UnOp.neg (|
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              d,
                                                              "core::num::dec2flt::decimal::Decimal",
                                                              "decimal_point"
                                                            |)
                                                          |)
                                                        |))
                                                    ]
                                                ]
                                              |)
                                            |)))
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::num::dec2flt::decimal::Decimal",
                                        "left_shift",
                                        []
                                      |),
                                      [ d; M.read (| shift |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.gt (|
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      d,
                                                      "core::num::dec2flt::decimal::Decimal",
                                                      "decimal_point"
                                                    |)
                                                  |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::num::dec2flt::decimal::DECIMAL_POINT_RANGE"
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (| M.return_ (| M.read (| fp_inf |) |) |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  let β := exp2 in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.sub (|
                                      M.read (| β |),
                                      M.rust_cast (M.read (| shift |))
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  let~ _ :=
                    let β := exp2 in
                    M.write (|
                      β,
                      BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.I32 1 |)
                    |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.gt (|
                                        BinOp.Wrap.add (|
                                          M.read (|
                                            M.get_constant (|
                                              "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.I32 1
                                        |),
                                        M.read (| exp2 |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ n :=
                                  M.alloc (|
                                    M.rust_cast
                                      (BinOp.Wrap.sub (|
                                        BinOp.Wrap.add (|
                                          M.read (|
                                            M.get_constant (|
                                              "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.I32 1
                                        |),
                                        M.read (| exp2 |)
                                      |))
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.gt (|
                                                  M.read (| n |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::num::dec2flt::slow::parse_long_mantissa::MAX_SHIFT"
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              n,
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::slow::parse_long_mantissa::MAX_SHIFT"
                                                |)
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::num::dec2flt::decimal::Decimal",
                                        "right_shift",
                                        []
                                      |),
                                      [ d; M.read (| n |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  let β := exp2 in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      M.rust_cast (M.read (| n |))
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    BinOp.Wrap.sub (|
                                      M.read (| exp2 |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                                        |)
                                      |)
                                    |),
                                    M.read (|
                                      M.get_constant (|
                                        "core::num::dec2flt::float::RawFloat::INFINITE_POWER"
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| fp_inf |) |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::decimal::Decimal",
                          "left_shift",
                          []
                        |),
                        [
                          d;
                          BinOp.Wrap.add (|
                            M.read (|
                              M.get_constant (|
                                "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                              |)
                            |),
                            Value.Integer IntegerKind.Usize 1
                          |)
                        ]
                      |)
                    |) in
                  let~ mantissa :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::decimal::Decimal",
                          "round",
                          []
                        |),
                        [ d ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (| mantissa |),
                                    BinOp.Wrap.shl (|
                                      Value.Integer IntegerKind.U64 1,
                                      BinOp.Wrap.add (|
                                        M.read (|
                                          M.get_constant (|
                                            "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::num::dec2flt::decimal::Decimal",
                                    "right_shift",
                                    []
                                  |),
                                  [ d; Value.Integer IntegerKind.Usize 1 ]
                                |)
                              |) in
                            let~ _ :=
                              let β := exp2 in
                              M.write (|
                                β,
                                BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.I32 1 |)
                              |) in
                            let~ _ :=
                              M.write (|
                                mantissa,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::num::dec2flt::decimal::Decimal",
                                    "round",
                                    []
                                  |),
                                  [ d ]
                                |)
                              |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            BinOp.Wrap.sub (|
                                              M.read (| exp2 |),
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                                                |)
                                              |)
                                            |),
                                            M.read (|
                                              M.get_constant (|
                                                "core::num::dec2flt::float::RawFloat::INFINITE_POWER"
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (| M.return_ (| M.read (| fp_inf |) |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ power2 :=
                    M.alloc (|
                      BinOp.Wrap.sub (|
                        M.read (| exp2 |),
                        M.read (|
                          M.get_constant (|
                            "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                          |)
                        |)
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (|
                                    M.read (| mantissa |),
                                    BinOp.Wrap.shl (|
                                      Value.Integer IntegerKind.U64 1,
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                        |)
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              let β := power2 in
                              M.write (|
                                β,
                                BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.I32 1 |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    let β := mantissa in
                    M.write (|
                      β,
                      BinOp.bit_and
                        (M.read (| β |))
                        (BinOp.Wrap.sub (|
                          BinOp.Wrap.shl (|
                            Value.Integer IntegerKind.U64 1,
                            M.read (|
                              M.get_constant (|
                                "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                              |)
                            |)
                          |),
                          Value.Integer IntegerKind.U64 1
                        |))
                    |) in
                  M.alloc (|
                    Value.StructRecord
                      "core::num::dec2flt::common::BiasedFp"
                      [ ("f", M.read (| mantissa |)); ("e", M.read (| power2 |)) ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_parse_long_mantissa :
        M.IsFunction "core::num::dec2flt::slow::parse_long_mantissa" parse_long_mantissa.
      
      Module parse_long_mantissa.
        Definition value_MAX_SHIFT : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 60 |))).
        
        Definition value_NUM_POWERS : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 19 |))).
        
        Definition value_POWERS : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                Value.Array
                  [
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 13;
                    Value.Integer IntegerKind.U8 16;
                    Value.Integer IntegerKind.U8 19;
                    Value.Integer IntegerKind.U8 23;
                    Value.Integer IntegerKind.U8 26;
                    Value.Integer IntegerKind.U8 29;
                    Value.Integer IntegerKind.U8 33;
                    Value.Integer IntegerKind.U8 36;
                    Value.Integer IntegerKind.U8 39;
                    Value.Integer IntegerKind.U8 43;
                    Value.Integer IntegerKind.U8 46;
                    Value.Integer IntegerKind.U8 49;
                    Value.Integer IntegerKind.U8 53;
                    Value.Integer IntegerKind.U8 56;
                    Value.Integer IntegerKind.U8 59
                  ]
              |))).
      End parse_long_mantissa.
    End slow.
  End dec2flt.
End num.
