Reading floats

Stream: lean4

[Ramon Fernandez Mir]

I need to read the value of floats to convert it to a rational or some structure I can reason about. If I'm not mistaken, the only way to do that right now is to convert it to string and do something like:

def readFloat (f : Float) : Option (Int × Nat) :=
  match Lean.Json.Parser.num f.toString.mkIterator with
    | Lean.Parsec.ParseResult.success _ res =>
      some (res.mantissa, res.exponent)
    | _ => none

Or I could also multiply by a big number, then convert it to int and get some approximation. But I guess that could lead to problems for big floats.

Instead, what I've currently done is I've changed Lean to be able to get the bit representation and from there I can extract the values I need. So I've added:

/* In lean.h */
 static inline uint64_t lean_float_to_bits(double a) {
    union { double f; uint64_t u; } fu = { .f = a }; return fu.u;
 }

-- In Float.lean
@[extern "lean_float_to_bits"] constant Float.toBits : Float → UInt64

There's no way to do that without changing Lean, right? Would it make sense to have this function or a similar one in Lean? Thanks

[Henrik Böving]

Oh of course there is a way, you can add FFI extensions to Lean as a user yourself without touching the compiler, example for how to do this with a lake project: https://github.com/leanprover/lake/tree/master/examples/ffi

[Ramon Fernandez Mir]

I see. So that would be an option. But last time I tried using the FFI, I couldn't really make it work interactively. Has that been solved now?

[Henrik Böving]

I don't know that from the top of my head its been a while since I've touched the FFI since it's not the main focus right now and will get some more love after mathlib4 is ported.

[James Gallicchio]

Ramon Fernandez Mir said:

I see. So that would be an option. But last time I tried using the FFI, I couldn't really make it work interactively. Has that been solved now?

Do you mean with #eval commands? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.23eval.20with.20native.20functions

[Ramon Fernandez Mir]

I see, yes, that worked nicely, thank you! All I needed was

moreServerArgs := #["--load-dynlib=extern/build/lib/FloatExt.dylib"]

in my Lake file.