ToExpr Float

Stream: lean4

[Tomas Skrivan]

Are there somewhere ToExpr Float and ToExpr Float32 instances? Or has anyone done this before? Or what would be the best approach to implement it? Should I just manually hack out mantisa and exponent and then build expresion with ofScientific?

[Robin Arnez]

Here's a prototype (which is probably pretty slow but whatever):

import Mathlib

open Lean Qq

def Float.toScientificParts (f : Float) : Bool × Nat × Int :=
  let bits := f.toBits
  let expPart : UInt64 := (bits >>> 52) &&& 0x7ff
  let mantPart : UInt64 := bits &&& ((1 : UInt64) <<< 52 - 1)
  if expPart = 0 ∧ mantPart = 0 then
    (bits >>> 63 != 0, 0, -1)
  else
    let exp : Int := (if expPart = 0 then (-0x3fe : Int) else expPart.toNat - 0x3ff) - 52
    let mant : Nat := if expPart = 0 then mantPart.toNat else mantPart.toNat + 1 <<< 52
    let qval : Rat := mant * 2^exp
    let log10 : Int := Int.log 10 qval
    let value : Nat := ⌊qval * 10^(17 - log10)⌋₊
    let (value, log10) := removeUnnecessaryDigits f.abs value (log10 - 17)
    (bits >>> 63 != 0, value, log10)
where
  removeUnnecessaryDigits (f : Float) (mant : Nat) (exp : Int) : Nat × Int :=
    if mant ≥ 10 ∧ exp ≠ -1 ∧ Float.ofScientific ((mant + 5) / 10) (exp < 0) (exp + 1).natAbs == f then
      removeUnnecessaryDigits f ((mant + 5) / 10) (exp + 1)
    else
      (mant, exp)

instance : ToExpr Float where
  toExpr x :=
    if x.isFinite then
      let (isNeg, mant, exp) := Float.toScientificParts x
      let mantE : Q(Nat) := mkRawNatLit mant
      let esign : Q(Bool) := if exp < 0 then q(true) else q(false)
      let expE : Q(Nat) := mkRawNatLit exp.natAbs
      let fval : Q(Float) := q(OfScientific.ofScientific $mantE $esign $expE)
      if isNeg then q(-$fval) else fval
    else if x.isNaN then
      q(Float.nan)
    else if 0 < x then
      q(Float.inf)
    else
      q(-Float.inf)
  toTypeExpr := mkConst ``Float

/-- info: 0.30000000000000004 -/
#guard_msgs in
#eval 0.1 + 0.2

[Tomas Skrivan]

Nice! works pretty well!