feat: Float is no longer opaque (#14091)

This PR changes the definition of the `Float` and `Float32` types to
wrap the `Float.Model` type introduced in #14079.

We then redefine `add`, `sub`, `mul`, `div`, `sqrt`, `abs`, `neg`,
`isNaN`, `isInf`, `isFinite`, `le`, `lt`, `beq`, `ofInt`, `ofNat`,
`ofIntX`, `ofUIntX`, `toIntX`, `toUIntX` on `Float`/`Float32` to
delegate to their `Float.Model` counterparts. This does not change
anything about compiled code; compiled code uses the accelerated
functions from the runtime as before.

Minor adjustments to the compiler are necessary for proper handling of
the `Float.toModel` and `Float.ofModel` functions.

A small breaking change: `Float.lt` and `Float.le` now are `Float ->
Float -> Bool` instead of `Float -> Float -> Prop`. This is unlikely to
affect anyone as hopefully everyone was using the `LE`/`LT` instances
instead.

Note that this will *not* grow into a fully-featured float library.
Instead, the idea is to make it technically possible for users to
connect up our `Float` type to downstream fully-featured float
libraries, so that theorems about `Float` can be deduced by transporting
lemmas from those libraries. The material about
`Float.Model`/`UnpackedFloat` should also not be used as a starting
point for such downstream libraries; they are simply not designed for
that purpose. Instead, downstream libraries should start from scratch
with whatever development of floating-point numbers they deem
appropriate and then show equivalence between `Float.Model` and their
64-bit float type afterwards.

Author: TwoFX

src/Init/Data/Float/Float.lean

@@ -100,6 +100,9 @@ Negate a `Float.Model`.
 def neg (a : Float.Model) : Float.Model :=
   pack a.unpack.neg
 
+instance : Neg Float.Model where
+  neg a := a.neg
+
 /--
 Return a `Float.Model` with positive sign.
 -/
@@ -292,4 +295,7 @@ Converts a `Float.Model` to an `ISize`, truncating after the decimal point, send
 -/
 def toISize (f : Float.Model) : ISize := f.unpack.toISize
 
+instance : Inhabited Float.Model where
+  default := ofNat 0
+
 end Float.Model

src/Init/Data/Float/Float32.lean

@@ -103,6 +103,9 @@ Negate a `Float32.Model`.
 def neg (a : Float32.Model) : Float32.Model :=
   pack a.unpack.neg
 
+instance : Neg Float32.Model where
+  neg a := a.neg
+
 /--
 Return a `Float32.Model` with positive sign.
 -/
@@ -295,4 +298,7 @@ Converts a `Float32.Model` to an `ISize`, truncating after the decimal point, se
 -/
 def toISize (f : Float32.Model) : ISize := f.unpack.toISize
 
+instance : Inhabited Float32.Model where
+  default := ofNat 0
+
 end Float32.Model

src/Init/Data/Float/Model/Float.lean

@@ -290,6 +290,28 @@ partial def casesStringToMono (c : Cases .pure) (_ : c.typeName == ``String) : T
   let k ← k.toMono
   return .let decl k
 
+/-- Eliminate `cases` for `Float`. -/
+partial def casesFloatToMono (c : Cases .pure) (_ : c.typeName == ``Float) : ToMonoM (Code .pure) := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``Float.toModel [] #[.fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
+/-- Eliminate `cases` for `Float32`. -/
+partial def casesFloat32ToMono (c : Cases .pure) (_ : c.typeName == ``Float32) : ToMonoM (Code .pure) := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``Float32.toModel [] #[.fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
 /-- Eliminate `cases` for `Thunk. -/
 partial def casesThunkToMono (c : Cases .pure) (_ : c.typeName == ``Thunk) : ToMonoM (Code .pure) := do
   assert! c.alts.size == 1
@@ -373,6 +395,10 @@ partial def Code.toMono (code : Code .pure) : ToMonoM (Code .pure) := do
       casesFloatArrayToMono c h
     else if h : c.typeName == ``String then
       casesStringToMono c h
+    else if h : c.typeName == ``Float then
+      casesFloatToMono c h
+    else if h : c.typeName == ``Float32 then
+      casesFloat32ToMono c h
     else if h : c.typeName == ``Thunk then
       casesThunkToMono c h
     else if h : c.typeName == ``Task then

src/Init/Data/Float/Model/Float32.lean

@@ -75,9 +75,27 @@ def tst3 (xs : List Float) (y : Float) : IO Unit :=
 def tst4 (xs : List Float) : IO Unit :=
   IO.println (fMap (fun x => x.abs) xs)
 
+/--
+`Float.ofModel`/`Float.toModel` behave correctly: the triangle relating the two
+`toBits` functions commutes (`Float.toBits = Float.Model.toBits ∘ Float.toModel`),
+and round-tripping a `Float` through its `Float.Model` reproduces it bit-for-bit.
+-/
+def checkModel (f : Float) : Bool :=
+  -- the two ways of obtaining the bits agree
+  (f.toBits == f.toModel.toBits) &&
+  -- `Float.ofModel ∘ Float.toModel = id`, bit-for-bit
+  ((Float.ofModel f.toModel).toBits == f.toBits)
+
+def tst5 : IO Unit := do
+  let samples : List Float :=
+    [0.0, -0.0, 1.0, -1.0, 3.14, -2.5, 1e308, 1e-308, 1 / 0, -1 / 0, 0 / 0]
+  IO.println (samples.all checkModel)
+
 def main : IO Unit := do
   tst1
   IO.println "-----"
   tst2 7
   tst3 [3, 4, 7, 8, 9, 11] 2
   tst4 [3, -3, 0, -0, -1 / 0, -0 / 0]
+  IO.println "-----"
+  tst5

src/Lean/Compiler/LCNF/ToMono.lean

@@ -46,3 +46,5 @@ true
 3.500000
 [1.500000, 2.000000, 3.500000, 4.000000, 4.500000, 5.500000]
 [3.000000, 3.000000, 0.000000, 0.000000, inf, NaN]
+-----
+true

tests/compile/float.lean

@@ -0,0 +1,122 @@
+/-!
+Check that the compiler correctly deals with `Float` in various situations.
+-/
+
+-- If the output of `trace.Compiler.result` turns out to be too unstable, we'll have to
+-- assert this some other way.
+
+set_option trace.Compiler.result true
+
+namespace F
+
+/--
+trace: [Compiler.result] size: 1
+    def F.f x.1 : UInt64 :=
+      let toModel.2 := Float.toModel x.1;
+      return toModel.2
+[Compiler.result] size: 4
+    def F.f._boxed x.1 : obj :=
+      let x.10.boxed := unbox x.1;
+      dec[ref] x.1;
+      let res := F.f x.10.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def f : Float → UInt64
+  | ⟨model⟩ => model.toBits
+
+/--
+trace: [Compiler.result] size: 1
+    def F.g x.1 : Float :=
+      let _x.2 := Float.ofModel x.1;
+      return _x.2
+[Compiler.result] size: 4
+    def F.g._boxed x.1 : obj :=
+      let x.4.boxed := unbox x.1;
+      dec[ref] x.1;
+      let res := F.g x.4.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def g : Float.Model → Float
+  | a => ⟨a⟩
+
+structure Foo where
+  foo : Float
+
+/--
+trace: [Compiler.result] size: 0
+    def F.h x.1 : Float :=
+      return x.1
+[Compiler.result] size: 4
+    def F.h._boxed x.1 : obj :=
+      let x.4.boxed := unbox x.1;
+      dec[ref] x.1;
+      let res := F.h x.4.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def h : Float → Foo
+  | a => ⟨a⟩
+
+end F
+
+namespace F32
+
+/--
+trace: [Compiler.result] size: 1
+    def F32.f x.1 : UInt32 :=
+      let toModel.2 := Float32.toModel x.1;
+      return toModel.2
+[Compiler.result] size: 4
+    def F32.f._boxed x.1 : tobj :=
+      let x.10.boxed := unbox x.1;
+      dec[ref] x.1;
+      let res := F32.f x.10.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def f : Float32 → UInt32
+  | ⟨model⟩ => model.toBits
+
+/--
+trace: [Compiler.result] size: 1
+    def F32.g x.1 : Float32 :=
+      let _x.2 := Float32.ofModel x.1;
+      return _x.2
+[Compiler.result] size: 4
+    def F32.g._boxed x.1 : obj :=
+      let x.4.boxed := unbox x.1;
+      dec x.1;
+      let res := F32.g x.4.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def g : Float32.Model → Float32
+  | a => ⟨a⟩
+
+structure Foo where
+  foo : Float32
+
+/--
+trace: [Compiler.result] size: 0
+    def F32.h x.1 : Float32 :=
+      return x.1
+[Compiler.result] size: 4
+    def F32.h._boxed x.1 : obj :=
+      let x.4.boxed := unbox x.1;
+      dec[ref] x.1;
+      let res := F32.h x.4.boxed;
+      let r := box res;
+      return r
+-/
+#guard_msgs in
+def h : Float32 → Foo
+  | a => ⟨a⟩
+
+end F32

tests/compile/float.lean.out.expected

@@ -0,0 +1,16 @@
+/-!
+Checks that `Float.ofModel` and `Float.toModel` behave correctly at elaboration
+time via `#guard`: the triangle relating the two `toBits` functions commutes
+(`Float.toBits = Float.Model.toBits ∘ Float.toModel`), and round-tripping a
+`Float` through its `Float.Model` reproduces it bit-for-bit.
+-/
+
+-- The `toBits` triangle commutes for a single value.
+#guard (1.0 : Float).toBits == (1.0 : Float).toModel.toBits
+
+-- `Float.ofModel ∘ Float.toModel = id`, bit-for-bit.
+#guard (Float.ofModel (3.14 : Float).toModel).toBits == (3.14 : Float).toBits
+
+-- Both properties hold across normals, signed zeroes, infinities, and `NaN`.
+#guard [0.0, -0.0, 1.0, -1.0, 3.14, -2.5, 1e308, 1e-308, 1 / 0, -1 / 0, 0 / 0].all
+  fun f => f.toBits == f.toModel.toBits && (Float.ofModel f.toModel).toBits == f.toBits