extract float from string?

Stream: lean4

[Robert]

hey everyone! How do we extract a float value from the string? Theres functions like "String.toInt?" but i dont see a similar one for float?

[Jovan Gerbscheid]

I guess the best you can do is use docs#OfScientific.ofScientific, and parse the exact numbers from the String yourself.

[Mario Carneiro]

there is definitely a float parser in core, it is needed in JSON parsing

[Mario Carneiro]

It produces JsonNumber but it's not too hard to adapt it

import Lean.Data.Json.Parser
import Batteries.Lean.Float

def String.toFloat? (s : String) : Option Float := do
  let { mantissa, exponent } ← (Lean.Json.Parser.num.run s).toOption
  return Int.divFloat mantissa (10 ^ exponent)

/-- info: some 2.000000 -/
#guard_msgs in #eval String.toFloat? "2.0"
/-- info: some 0.000023 -/
#guard_msgs in #eval String.toFloat? "2.333333e-5"
/-- info: none -/
#guard_msgs in #eval String.toFloat? "hello"

[Kim Morrison]

Perhaps someone could refactor that flip the dependency (i.e. keep the same logic, but in a new Float.fromString? and have the json parser call that?

[Mario Carneiro]

well you probably wouldn't want to have json route through floats directly as the process is lossy

[Mario Carneiro]

currently it's being parsed into JsonNumber which can represent decimal fractions losslessly

[Mario Carneiro]

but you could have a more agnostic basic function which returns the mantissa/exponent components without committing to the JsonNumber type

[Mario Carneiro]

(Note also that I used a function from batteries here (Int.divFloat), which as you can tell from the module name I'm :+1: on upstreaming)