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

Module num.
  Module flt2dec.
    Module estimator.
      (*
      pub fn estimate_scaling_factor(mant: u64, exp: i16) -> i16 {
          // 2^(nbits-1) < mant <= 2^nbits if mant > 0
          let nbits = 64 - (mant - 1).leading_zeros() as i64;
          // 1292913986 = floor(2^32 * log_10 2)
          // therefore this always underestimates (or is exact), but not much.
          (((nbits + exp as i64) * 1292913986) >> 32) as i16
      }
      *)
      Definition estimate_scaling_factor
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ mant; exp ] =>
          ltac:(M.monadic
            (let mant := M.alloc (| mant |) in
            let exp := M.alloc (| exp |) in
            M.read (|
              let~ nbits :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    Value.Integer IntegerKind.I64 64,
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "u64", "leading_zeros", [] |),
                        [ BinOp.Wrap.sub (| M.read (| mant |), Value.Integer IntegerKind.U64 1 |) ]
                      |))
                  |)
                |) in
              M.alloc (|
                M.rust_cast
                  (BinOp.Wrap.shr (|
                    BinOp.Wrap.mul (|
                      BinOp.Wrap.add (| M.read (| nbits |), M.rust_cast (M.read (| exp |)) |),
                      Value.Integer IntegerKind.I64 1292913986
                    |),
                    Value.Integer IntegerKind.I32 32
                  |))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_estimate_scaling_factor :
        M.IsFunction
          "core::num::flt2dec::estimator::estimate_scaling_factor"
          estimate_scaling_factor.
    End estimator.
  End flt2dec.
End num.
