feat: add Float.{toRatParts, toStringFull} (leanprover-community#282)

Std.lean

@@ -71,6 +71,7 @@ import Std.Lean.Command
 import Std.Lean.CoreM
 import Std.Lean.Delaborator
 import Std.Lean.Expr
+import Std.Lean.Float
 import Std.Lean.Format
 import Std.Lean.HashMap
 import Std.Lean.HashSet

Std/Lean/Float.lean

@@ -0,0 +1,60 @@
+/-
+ Copyright (c) 2023 Mario Carneiro. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Authors: Mario Carneiro
+-/
+
+namespace Float
+
+/-- Returns `v, exp` integers such that `f = v * 2^exp`.
+(`e` is not minimal, but `v.abs` will be at most `2^53 - 1`.)
+Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`). -/
+def toRatParts (f : Float) : Option (Int × Int) :=
+  if f.isFinite then
+    let (f', exp) := f.frExp
+    let x := (2^53:Nat).toFloat * f'
+    let v := if x < 0 then
+      (-(-x).floor.toUInt64.toNat : Int)
+    else
+      (x.floor.toUInt64.toNat : Int)
+    some (v, exp - 53)
+  else none
+
+/-- Returns `v, exp` integers such that `f = v * 2^exp`.
+Like `toRatParts`, but `e` is guaranteed to be minimal (`n` is always odd), unless `n = 0`.
+`n.abs` will be at most `2^53 - 1` because `Float` has 53 bits of precision.
+Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`). -/
+partial def toRatParts' (f : Float) : Option (Int × Int) :=
+  f.toRatParts.map fun (n, e) =>
+    if n == 0 then (0, 0) else
+      let neg : Bool := n < 0
+      let v := n.natAbs.toUInt64
+      let c := trailingZeros v 0
+      let v := (v >>> c.toUInt64).toNat
+      (if neg then -v else v, e + c.toNat)
+where
+  /-- Calculates the number of trailing bits in a `UInt64`. Requires `v ≠ 0`. -/
+  -- Note: it's a bit dumb to be using a loop here, but it is hopefully written
+  -- such that LLVM can tell we are computing trailing bits and do good things to it
+  -- TODO: prove termination under suitable assumptions (only relevant if `Float` is not opaque)
+  trailingZeros (v : UInt64) (c : UInt8) :=
+    if v &&& 1 == 0 then trailingZeros (v >>> 1) (c + 1) else c
+
+/-- Converts `f` to a string, including all decimal digits. -/
+def toStringFull (f : Float) : String :=
+  if let some (v, exp) := toRatParts f then
+    let v' := v.natAbs
+    let s := if exp ≥ 0 then
+      Nat.repr (v' * (2^exp.toNat:Nat))
+    else
+      let e := (-exp).toNat
+      let intPart := v' / 2^e
+      let rem := v' % 2^e
+      if rem == 0 then
+        Nat.repr intPart
+      else
+        let rem := Nat.repr ((2^e + v' % 2^e) * 5^e)
+        let rem := rem.dropRightWhile (· == '0')
+        s!"{intPart}.{rem.extract ⟨1⟩ rem.endPos}"
+    if v < 0 then s!"-{s}" else s
+  else f.toString -- inf, -inf, nan

Std/Tactic/GuardExpr.lean

@@ -231,10 +231,12 @@ expression equals `true`. -/
 elab "#guard " e:term : command =>
   Lean.Elab.Command.liftTermElabM do
     let e ← Term.elabTermEnsuringType e (mkConst ``Bool)
-    Term.synthesizeSyntheticMVarsUsingDefault
+    Term.synthesizeSyntheticMVarsNoPostponing
     let e ← instantiateMVars e
-    if e.hasMVar then
-      throwError "expression{indentExpr e}\nhas metavariables"
-    let v ← unsafe (evalExpr Bool (mkConst ``Bool) e)
-    unless v do
-      throwError "expression{indentExpr e}\ndid not evaluate to `true`"
+    let mvars ← getMVars e
+    if mvars.isEmpty then
+      let v ← unsafe evalExpr Bool (mkConst ``Bool) e
+      unless v do
+        throwError "expression{indentExpr e}\ndid not evaluate to `true`"
+    else
+      _ ← Term.logUnassignedUsingErrorInfos mvars

test/float.lean

@@ -0,0 +1,44 @@
+import Std.Tactic.GuardExpr
+import Std.Lean.Float
+
+#guard 0.0.toRatParts == some (0, -53)
+#guard (2^(-1000):Float).toRatParts == some (4503599627370496, -1052)
+#guard (2^(-30):Float).toRatParts == some (4503599627370496, -82)
+#guard 0.1.toRatParts == some (7205759403792794, -56)
+#guard 0.5.toRatParts == some (4503599627370496, -53)
+#guard 5.0.toRatParts == some (5629499534213120, -50)
+#guard (-5.0).toRatParts == some (-5629499534213120, -50)
+#guard 5.5.toRatParts == some (6192449487634432, -50)
+#guard 500000000000000.5.toRatParts == some (8000000000000008, -4)
+#guard 5000000000000000.5.toRatParts == some (5000000000000000, 0)
+#guard 1e1000.toRatParts == none
+#guard (-1e1000).toRatParts == none
+#guard (-0/0:Float).toRatParts == none
+
+#guard 0.0.toRatParts' == some (0, 0)
+#guard (2^(-1000):Float).toRatParts' == some (1, -1000)
+#guard (2^(-30):Float).toRatParts' == some (1, -30)
+#guard 0.1.toRatParts' == some (3602879701896397, -55)
+#guard 0.5.toRatParts' == some (1, -1)
+#guard 5.0.toRatParts' == some (5, 0)
+#guard (-5.0).toRatParts' == some (-5, 0)
+#guard 5.5.toRatParts' == some (11, -1)
+#guard 500000000000000.5.toRatParts' == some (1000000000000001, -1)
+#guard 5000000000000000.5.toRatParts' == some (152587890625, 15)
+#guard 1e1000.toRatParts' == none
+#guard (-1e1000).toRatParts' == none
+#guard (-0/0:Float).toRatParts' == none
+
+#guard 0.0.toStringFull == "0"
+#guard (2^(-1000):Float).toStringFull.length == 1002
+#guard (2^(-30):Float).toStringFull == "0.000000000931322574615478515625"
+#guard 0.1.toStringFull == "0.1000000000000000055511151231257827021181583404541015625"
+#guard 0.5.toStringFull == "0.5"
+#guard 5.0.toStringFull == "5"
+#guard (-5.0).toStringFull == "-5"
+#guard 5.5.toStringFull == "5.5"
+#guard 500000000000000.5.toStringFull == "500000000000000.5"
+#guard 5000000000000000.5.toStringFull == "5000000000000000"
+#guard 1e1000.toStringFull == "inf"
+#guard (-1e1000).toStringFull == "-inf"
+#guard (-0/0:Float).toStringFull == "NaN"