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

Module num.
  Module dec2flt.
    Module Impl_core_str_traits_FromStr_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Err = ParseFloatError; *)
      Definition _Err : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (*
                  fn from_str(src: &str) -> Result<Self, ParseFloatError> {
                      dec2flt(src)
                  }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ src ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            M.call_closure (|
              M.get_function (| "core::num::dec2flt::dec2flt", [ Ty.path "f32" ] |),
              [ M.read (| src |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_f32.
    
    Module Impl_core_str_traits_FromStr_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Err = ParseFloatError; *)
      Definition _Err : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (*
                  fn from_str(src: &str) -> Result<Self, ParseFloatError> {
                      dec2flt(src)
                  }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ src ] =>
          ltac:(M.monadic
            (let src := M.alloc (| src |) in
            M.call_closure (|
              M.get_function (| "core::num::dec2flt::dec2flt", [ Ty.path "f64" ] |),
              [ M.read (| src |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_f64.
    
    (* StructRecord
      {
        name := "ParseFloatError";
        const_params := [];
        ty_params := [];
        fields := [ ("kind", Ty.path "core::num::dec2flt::FloatErrorKind") ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (* Debug *)
      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",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "ParseFloatError" |);
                M.read (| Value.String "kind" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::dec2flt::ParseFloatError",
                    "kind"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_core_num_dec2flt_ParseFloatError.
    
    Module Impl_core_clone_Clone_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::num::dec2flt::ParseFloatError"
              [
                ("kind",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "core::num::dec2flt::FloatErrorKind",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::num::dec2flt::ParseFloatError",
                        "kind"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_num_dec2flt_ParseFloatError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_ParseFloatError.
    
    Module Impl_core_cmp_PartialEq_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::num::dec2flt::FloatErrorKind",
                [ Ty.path "core::num::dec2flt::FloatErrorKind" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::num::dec2flt::ParseFloatError",
                  "kind"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::num::dec2flt::ParseFloatError",
                  "kind"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_num_dec2flt_ParseFloatError.
    
    Module Impl_core_cmp_Eq_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_num_dec2flt_ParseFloatError.
    
    (*
    Enum FloatErrorKind
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Empty";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Invalid";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_core_num_dec2flt_FloatErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::FloatErrorKind".
      
      (* Debug *)
      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_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::num::dec2flt::FloatErrorKind::Empty"
                            |) in
                          M.alloc (| M.read (| Value.String "Empty" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::num::dec2flt::FloatErrorKind::Invalid"
                            |) in
                          M.alloc (| M.read (| Value.String "Invalid" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_core_num_dec2flt_FloatErrorKind.
    
    Module Impl_core_clone_Clone_for_core_num_dec2flt_FloatErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::FloatErrorKind".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "core::num::dec2flt::FloatErrorKind::Empty" |) in
                      M.alloc (|
                        Value.StructTuple "core::num::dec2flt::FloatErrorKind::Empty" []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "core::num::dec2flt::FloatErrorKind::Invalid" |) in
                      M.alloc (|
                        Value.StructTuple "core::num::dec2flt::FloatErrorKind::Invalid" []
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_num_dec2flt_FloatErrorKind.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_FloatErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::FloatErrorKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_FloatErrorKind.
    
    Module Impl_core_cmp_PartialEq_for_core_num_dec2flt_FloatErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::FloatErrorKind".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::num::dec2flt::FloatErrorKind" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::num::dec2flt::FloatErrorKind" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_num_dec2flt_FloatErrorKind.
    
    Module Impl_core_cmp_Eq_for_core_num_dec2flt_FloatErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::FloatErrorKind".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_num_dec2flt_FloatErrorKind.
    
    Module Impl_core_error_Error_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (*
          fn description(&self) -> &str {
              match self.kind {
                  FloatErrorKind::Empty => "cannot parse float from empty string",
                  FloatErrorKind::Invalid => "invalid float literal",
              }
          }
      *)
      Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::num::dec2flt::ParseFloatError",
                  "kind"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::dec2flt::FloatErrorKind::Empty" |) in
                      M.alloc (|
                        M.read (| Value.String "cannot parse float from empty string" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::dec2flt::FloatErrorKind::Invalid" |) in
                      M.alloc (| M.read (| Value.String "invalid float literal" |) |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("description", InstanceField.Method description) ].
    End Impl_core_error_Error_for_core_num_dec2flt_ParseFloatError.
    
    Module Impl_core_fmt_Display_for_core_num_dec2flt_ParseFloatError.
      Definition Self : Ty.t := Ty.path "core::num::dec2flt::ParseFloatError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              #[allow(deprecated)]
              self.description().fmt(f)
          }
      *)
      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_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::error::Error",
                    Ty.path "core::num::dec2flt::ParseFloatError",
                    [],
                    "description",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| f |)
              ]
            |)))
        | _, _, _ => 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_core_num_dec2flt_ParseFloatError.
    
    (*
    pub(super) fn pfe_empty() -> ParseFloatError {
        ParseFloatError { kind: FloatErrorKind::Empty }
    }
    *)
    Definition pfe_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::num::dec2flt::ParseFloatError"
            [ ("kind", Value.StructTuple "core::num::dec2flt::FloatErrorKind::Empty" []) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_pfe_empty : M.IsFunction "core::num::dec2flt::pfe_empty" pfe_empty.
    
    (*
    pub fn pfe_invalid() -> ParseFloatError {
        ParseFloatError { kind: FloatErrorKind::Invalid }
    }
    *)
    Definition pfe_invalid (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::num::dec2flt::ParseFloatError"
            [ ("kind", Value.StructTuple "core::num::dec2flt::FloatErrorKind::Invalid" []) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_pfe_invalid : M.IsFunction "core::num::dec2flt::pfe_invalid" pfe_invalid.
    
    (*
    fn biased_fp_to_float<T: RawFloat>(x: BiasedFp) -> T {
        let mut word = x.f;
        word |= (x.e as u64) << T::MANTISSA_EXPLICIT_BITS;
        T::from_u64_bits(word)
    }
    *)
    Definition biased_fp_to_float (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ x ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          M.read (|
            let~ word :=
              M.copy (|
                M.SubPointer.get_struct_record_field (|
                  x,
                  "core::num::dec2flt::common::BiasedFp",
                  "f"
                |)
              |) in
            let~ _ :=
              let β := word in
              M.write (|
                β,
                BinOp.bit_or
                  (M.read (| β |))
                  (BinOp.Wrap.shl (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          x,
                          "core::num::dec2flt::common::BiasedFp",
                          "e"
                        |)
                      |)),
                    M.read (|
                      M.get_constant (|
                        "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                      |)
                    |)
                  |))
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::num::dec2flt::float::RawFloat",
                  T,
                  [],
                  "from_u64_bits",
                  []
                |),
                [ M.read (| word |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_biased_fp_to_float :
      M.IsFunction "core::num::dec2flt::biased_fp_to_float" biased_fp_to_float.
    
    (*
    pub fn dec2flt<F: RawFloat>(s: &str) -> Result<F, ParseFloatError> {
        let mut s = s.as_bytes();
        let c = if let Some(&c) = s.first() {
            c
        } else {
            return Err(pfe_empty());
        };
        let negative = c == b'-';
        if c == b'-' || c == b'+' {
            s = &s[1..];
        }
        if s.is_empty() {
            return Err(pfe_invalid());
        }
    
        let mut num = match parse_number(s) {
            Some(r) => r,
            None if let Some(value) = parse_inf_nan(s, negative) => return Ok(value),
            None => return Err(pfe_invalid()),
        };
        num.negative = negative;
        if !cfg!(feature = "optimize_for_size") {
            if let Some(value) = num.try_fast_path::<F>() {
                return Ok(value);
            }
        }
    
        // If significant digits were truncated, then we can have rounding error
        // only if `mantissa + 1` produces a different result. We also avoid
        // redundantly using the Eisel-Lemire algorithm if it was unable to
        // correctly round on the first pass.
        let mut fp = compute_float::<F>(num.exponent, num.mantissa);
        if num.many_digits && fp.e >= 0 && fp != compute_float::<F>(num.exponent, num.mantissa + 1) {
            fp.e = -1;
        }
        // Unable to correctly round the float using the Eisel-Lemire algorithm.
        // Fallback to a slower, but always correct algorithm.
        if fp.e < 0 {
            fp = parse_long_mantissa::<F>(s);
        }
    
        let mut float = biased_fp_to_float::<F>(fp);
        if num.negative {
            float = -float;
        }
        Ok(float)
    }
    *)
    Definition dec2flt (ε : 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~ s :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                      [ M.read (| s |) ]
                    |)
                  |) in
                let~ c :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "first",
                                    []
                                  |),
                                  [ M.read (| s |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let c := M.copy (| γ0_0 |) in
                            c));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [
                                        M.call_closure (|
                                          M.get_function (| "core::num::dec2flt::pfe_empty", [] |),
                                          []
                                        |)
                                      ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ negative :=
                  M.alloc (| BinOp.eq (| M.read (| c |), M.read (| UnsupportedLiteral |) |) |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  BinOp.eq (| M.read (| c |), M.read (| UnsupportedLiteral |) |),
                                  ltac:(M.monadic
                                    (BinOp.eq (|
                                      M.read (| c |),
                                      M.read (| UnsupportedLiteral |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              s,
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::index::Index",
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  [
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeFrom")
                                      []
                                      [ Ty.path "usize" ]
                                  ],
                                  "index",
                                  []
                                |),
                                [
                                  M.read (| s |);
                                  Value.StructRecord
                                    "core::ops::range::RangeFrom"
                                    [ ("start", Value.Integer IntegerKind.Usize 1) ]
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "is_empty",
                                    []
                                  |),
                                  [ M.read (| s |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_function (| "core::num::dec2flt::pfe_invalid", [] |),
                                        []
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ num :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::num::dec2flt::parse::parse_number", [] |),
                          [ M.read (| s |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let r := M.copy (| γ0_0 |) in
                            r));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::num::dec2flt::parse::parse_inf_nan",
                                    [ F ]
                                  |),
                                  [ M.read (| s |); M.read (| negative |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let value := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Ok"
                                      [ M.read (| value |) ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::num::dec2flt::pfe_invalid",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      num,
                      "core::num::dec2flt::number::Number",
                      "negative"
                    |),
                    M.read (| negative |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| UnOp.not (| Value.Bool false |) |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::num::dec2flt::number::Number",
                                          "try_fast_path",
                                          [ F ]
                                        |),
                                        [ num ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let value := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [ M.read (| value |) ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ fp :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::num::dec2flt::lemire::compute_float", [ F ] |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            num,
                            "core::num::dec2flt::number::Number",
                            "exponent"
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            num,
                            "core::num::dec2flt::number::Number",
                            "mantissa"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  LogicalOp.and (|
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        num,
                                        "core::num::dec2flt::number::Number",
                                        "many_digits"
                                      |)
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.ge (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            fp,
                                            "core::num::dec2flt::common::BiasedFp",
                                            "e"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.I32 0
                                      |)))
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "core::num::dec2flt::common::BiasedFp",
                                        [ Ty.path "core::num::dec2flt::common::BiasedFp" ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        fp;
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::num::dec2flt::lemire::compute_float",
                                              [ F ]
                                            |),
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  num,
                                                  "core::num::dec2flt::number::Number",
                                                  "exponent"
                                                |)
                                              |);
                                              BinOp.Wrap.add (|
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    num,
                                                    "core::num::dec2flt::number::Number",
                                                    "mantissa"
                                                  |)
                                                |),
                                                Value.Integer IntegerKind.U64 1
                                              |)
                                            ]
                                          |)
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                fp,
                                "core::num::dec2flt::common::BiasedFp",
                                "e"
                              |),
                              Value.Integer IntegerKind.I32 (-1)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) 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 (|
                                      fp,
                                      "core::num::dec2flt::common::BiasedFp",
                                      "e"
                                    |)
                                  |),
                                  Value.Integer IntegerKind.I32 0
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              fp,
                              M.call_closure (|
                                M.get_function (|
                                  "core::num::dec2flt::slow::parse_long_mantissa",
                                  [ F ]
                                |),
                                [ M.read (| s |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ float :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::num::dec2flt::biased_fp_to_float", [ F ] |),
                      [ M.read (| fp |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.SubPointer.get_struct_record_field (|
                                num,
                                "core::num::dec2flt::number::Number",
                                "negative"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              float,
                              M.call_closure (|
                                M.get_trait_method (| "core::ops::arith::Neg", F, [], "neg", [] |),
                                [ M.read (| float |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| float |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_dec2flt : M.IsFunction "core::num::dec2flt::dec2flt" dec2flt.
  End dec2flt.
End num.
