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

Module num.
  Module dec2flt.
    Module common.
      (* Trait *)
      (* Empty module 'ByteSlice' *)
      
      Module Impl_core_num_dec2flt_common_ByteSlice_for_slice_u8.
        Definition Self : Ty.t := Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ].
        
        (*
            fn read_u64(&self) -> u64 {
                let mut tmp = [0; 8];
                tmp.copy_from_slice(&self[..8]);
                u64::from_le_bytes(tmp)
            }
        *)
        Definition read_u64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ tmp :=
                  M.alloc (|
                    repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "copy_from_slice",
                        []
                      |),
                      [
                        tmp;
                        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::RangeTo") [] [ Ty.path "usize" ]
                            ],
                            "index",
                            []
                          |),
                          [
                            M.read (| self |);
                            Value.StructRecord
                              "core::ops::range::RangeTo"
                              [ ("end_", Value.Integer IntegerKind.Usize 8) ]
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "from_le_bytes", [] |),
                    [ M.read (| tmp |) ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn write_u64(&mut self, value: u64) {
                self[..8].copy_from_slice(&value.to_le_bytes())
            }
        *)
        Definition write_u64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; value ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let value := M.alloc (| value |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                  "copy_from_slice",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::IndexMut",
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                      "index_mut",
                      []
                    |),
                    [
                      M.read (| self |);
                      Value.StructRecord
                        "core::ops::range::RangeTo"
                        [ ("end_", Value.Integer IntegerKind.Usize 8) ]
                    ]
                  |);
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "u64", "to_le_bytes", [] |),
                      [ M.read (| value |) ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn offset_from(&self, other: &Self) -> isize {
                other.len() as isize - self.len() as isize
            }
        *)
        Definition offset_from (ε : 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
              BinOp.Wrap.sub (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "len",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)),
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "len",
                      []
                    |),
                    [ M.read (| self |) ]
                  |))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn parse_digits(&self, mut func: impl FnMut(u8)) -> &Self {
                let mut s = self;
        
                while let Some((c, s_next)) = s.split_first() {
                    let c = c.wrapping_sub(b'0');
                    if c < 10 {
                        func(c);
                        s = s_next;
                    } else {
                        break;
                    }
                }
        
                s
            }
        *)
        Definition parse_digits (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ impl_FnMut_u8_ ], [ self; func ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let func := M.alloc (| func |) in
              M.read (|
                let~ s := M.copy (| self |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (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" ],
                                      "split_first",
                                      []
                                    |),
                                    [ M.read (| s |) ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                              let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                              let c := M.copy (| γ1_0 |) in
                              let s_next := M.copy (| γ1_1 |) in
                              let~ c :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "u8",
                                      "wrapping_sub",
                                      []
                                    |),
                                    [ M.read (| M.read (| c |) |); M.read (| UnsupportedLiteral |) ]
                                  |)
                                |) in
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.lt (|
                                              M.read (| c |),
                                              Value.Integer IntegerKind.U8 10
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnMut",
                                              impl_FnMut_u8_,
                                              [ Ty.tuple [ Ty.path "u8" ] ],
                                              "call_mut",
                                              []
                                            |),
                                            [ func; Value.Tuple [ M.read (| c |) ] ]
                                          |)
                                        |) in
                                      let~ _ := M.write (| s, M.read (| s_next |) |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)))
                                ]
                              |)));
                          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
                M.alloc (| M.read (| s |) |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::num::dec2flt::common::ByteSlice"
            Self
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("read_u64", InstanceField.Method read_u64);
              ("write_u64", InstanceField.Method write_u64);
              ("offset_from", InstanceField.Method offset_from);
              ("parse_digits", InstanceField.Method parse_digits)
            ].
      End Impl_core_num_dec2flt_common_ByteSlice_for_slice_u8.
      
      (*
      pub(crate) fn is_8digits(v: u64) -> bool {
          let a = v.wrapping_add(0x4646_4646_4646_4646);
          let b = v.wrapping_sub(0x3030_3030_3030_3030);
          (a | b) & 0x8080_8080_8080_8080 == 0
      }
      *)
      Definition is_8digits (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ v ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            M.read (|
              let~ a :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                    [ M.read (| v |); Value.Integer IntegerKind.U64 5063812098665367110 ]
                  |)
                |) in
              let~ b :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "wrapping_sub", [] |),
                    [ M.read (| v |); Value.Integer IntegerKind.U64 3472328296227680304 ]
                  |)
                |) in
              M.alloc (|
                BinOp.eq (|
                  BinOp.bit_and
                    (BinOp.bit_or (M.read (| a |)) (M.read (| b |)))
                    (Value.Integer IntegerKind.U64 9259542123273814144),
                  Value.Integer IntegerKind.U64 0
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_is_8digits : M.IsFunction "core::num::dec2flt::common::is_8digits" is_8digits.
      
      (* StructRecord
        {
          name := "BiasedFp";
          const_params := [];
          ty_params := [];
          fields := [ ("f", Ty.path "u64"); ("e", Ty.path "i32") ];
        } *)
      
      Module Impl_core_fmt_Debug_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (* 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_field2_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "BiasedFp" |);
                  M.read (| Value.String "f" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::dec2flt::common::BiasedFp",
                    "f"
                  |);
                  M.read (| Value.String "e" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::num::dec2flt::common::BiasedFp",
                      "e"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_common_BiasedFp.
      
      Module Impl_core_marker_Copy_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_core_num_dec2flt_common_BiasedFp.
      
      Module Impl_core_clone_Clone_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (* 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 (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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_common_BiasedFp.
      
      Module Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_common_BiasedFp.
      
      Module Impl_core_cmp_PartialEq_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (* 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
              LogicalOp.and (|
                BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::num::dec2flt::common::BiasedFp",
                      "f"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::num::dec2flt::common::BiasedFp",
                      "f"
                    |)
                  |)
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::num::dec2flt::common::BiasedFp",
                        "e"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "core::num::dec2flt::common::BiasedFp",
                        "e"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => 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_common_BiasedFp.
      
      Module Impl_core_cmp_Eq_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (* 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.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_common_BiasedFp.
      
      Module Impl_core_default_Default_for_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "core::num::dec2flt::common::BiasedFp"
                [
                  ("f",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "u64",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("e",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "i32",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_core_num_dec2flt_common_BiasedFp.
      
      Module Impl_core_num_dec2flt_common_BiasedFp.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::common::BiasedFp".
        
        (*
            pub const fn zero_pow2(e: i32) -> Self {
                Self { f: 0, e }
            }
        *)
        Definition zero_pow2 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ e ] =>
            ltac:(M.monadic
              (let e := M.alloc (| e |) in
              Value.StructRecord
                "core::num::dec2flt::common::BiasedFp"
                [ ("f", Value.Integer IntegerKind.U64 0); ("e", M.read (| e |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_zero_pow2 : M.IsAssociatedFunction Self "zero_pow2" zero_pow2.
      End Impl_core_num_dec2flt_common_BiasedFp.
    End common.
  End dec2flt.
End num.
