Merge pull request #1784 from cryspen/lean-floats

[Lean] Add basic support for floats

Author: abentkamp

CHANGELOG.md

@@ -32,6 +32,7 @@ Changes to the Lean backend:
  - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
  - Add support for shift-left (#1785)
  - Add support for default methods of traits (#1777)
+ - Add support for floats (#1784)
  - Add support for pattern matching on constant literals (#1789)
  - Add support for binding subpatterns in match constructs (#1790)
 

hax-lib/proof-libs/lean/Hax/Float.lean

@@ -0,0 +1,27 @@
+import Hax.Lib
+import Hax.Integers.Ops
+
+abbrev f32 := Float32
+abbrev f64 := Float
+
+macro "declare_float_ops" typeName:ident : command =>
+  `(
+    namespace $typeName
+
+    instance : HaxAdd $typeName where
+      add := fun x y => x + y
+
+    instance : HaxSub $typeName where
+      sub := fun x y => x - y
+
+    instance : HaxMul $typeName where
+      mul := fun x y => x * y
+
+    instance : HaxDiv $typeName where
+      div := fun x y => x / y
+
+    end $typeName
+  )
+
+declare_float_ops f32
+declare_float_ops f64

hax-lib/proof-libs/lean/Hax/Rust_primitives.lean

@@ -1,2 +1,3 @@
 import Hax.Integers.Ops
 import Hax.Integers.Spec
+import Hax.Float

rust-engine/src/backends/lean.rs

@@ -431,9 +431,6 @@ set_option linter.unusedVariables false
 
         fn expr(&self, Expr { kind, ty, meta: _ }: &Expr) -> DocBuilder<A> {
             match &**kind {
-                ExprKind::Literal(int_lit @ Literal::Int { .. }) => {
-                    docs![int_lit, reflow!(" : "), ty].parens().group()
-                }
                 ExprKind::If {
                     condition,
                     then,
@@ -478,6 +475,9 @@ set_option linter.unusedVariables false
                         }
                     }
                 }
+                ExprKind::Literal(numeric_lit @ (Literal::Float { .. } | Literal::Int { .. })) => {
+                    docs![numeric_lit, reflow!(" : "), ty].parens().group()
+                }
                 ExprKind::Literal(literal) => docs![literal],
                 ExprKind::Array(exprs) => docs![
                     "#v[",
@@ -788,7 +788,11 @@ set_option linter.unusedVariables false
                     negative,
                     kind: _,
                 } => format!("{}{value}", if *negative { "-" } else { "" }),
-                Literal::Float { .. } => emit_error!(issue 1715, "Unsupported Float literal"),
+                Literal::Float {
+                    value,
+                    negative,
+                    kind: _,
+                } => format!("{}{value}", if *negative { "-" } else { "" }),
             }]
         }
 
@@ -805,7 +809,7 @@ set_option linter.unusedVariables false
             match primitive_ty {
                 PrimitiveTy::Bool => docs!["Bool"],
                 PrimitiveTy::Int(int_kind) => docs![int_kind],
-                PrimitiveTy::Float(_) => emit_error!(issue 1715, "Unsupported Float type"),
+                PrimitiveTy::Float(float_kind) => docs![float_kind],
                 PrimitiveTy::Char => docs!["Char"],
                 PrimitiveTy::Str => docs!["String"],
             }
@@ -828,6 +832,14 @@ set_option linter.unusedVariables false
             }]
         }
 
+        fn float_kind(&self, float_kind: &FloatKind) -> DocBuilder<A> {
+            docs![match float_kind {
+                FloatKind::F32 => "f32",
+                FloatKind::F64 => "f64",
+                _ => emit_error!(issue 1787, "The only supported float types are `f32` and `f64`."),
+            }]
+        }
+
         fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A> {
             match generic_value {
                 GenericValue::Ty(ty) => docs![ty],
@@ -1248,10 +1260,6 @@ set_option linter.unusedVariables false
             unreachable_by_invariant!(Drop_references)
         }
 
-        fn float_kind(&self, _float_kind: &FloatKind) -> DocBuilder<A> {
-            emit_error!(issue 1715, "floats are unsupported")
-        }
-
         fn dyn_trait_goal(&self, _dyn_trait_goal: &DynTraitGoal) -> DocBuilder<A> {
             emit_error!(issue 1708, "`dyn` traits are unsupported")
         }

test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

@@ -654,6 +654,20 @@ def Lean_tests.Loops.Errors.loop4
     | (Core.Ops.Control_flow.ControlFlow.Continue e)
       => (pure (Core.Result.Result.Ok (Rust_primitives.Hax.Tuple2.mk e e)))
 
+def Lean_tests.Floats.N : f32 := RustM.of_isOk (do (pure (1.0 : f32))) (by rfl)
+
+def Lean_tests.Floats.test
+  (_ : Rust_primitives.Hax.Tuple0)
+  : RustM Rust_primitives.Hax.Tuple0
+  := do
+  let l0 : f64 := (1.0 : f64);
+  let l1 : f64 := (0.9 : f64);
+  let l2 : f32 := (5.0 : f32);
+  let l5 : f32 := Lean_tests.Floats.N;
+  (pure Rust_primitives.Hax.Tuple0.mk)
+
+def Lean_tests.Floats.f (x : f64) (y : f32) : RustM f32 := do (pure y)
+
 inductive Lean_tests.Enums.E : Type
 | V1 : Lean_tests.Enums.E
 | V2 : Lean_tests.Enums.E

tests/lean-tests/src/floats.rs

@@ -0,0 +1,16 @@
+// Tests on floats
+#![allow(dead_code)]
+#![allow(unused_variables)]
+
+const N: f32 = 1.0;
+
+fn test() {
+    let l0 = 1.0;
+    let l1 = 0.9;
+    let l2 = 5.0f32;
+    let l5 = N;
+}
+
+fn f(x: f64, y: f32) -> f32 {
+    y
+}

tests/lean-tests/src/lib.rs

@@ -4,6 +4,7 @@
 pub mod comments;
 pub mod constants;
 pub mod enums;
+pub mod floats;
 pub mod ite;
 pub mod loops;
 pub mod matching;