From cbb2d05e0db6bedf9d6844f29ee25b95429b994c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 16 Oct 2023 11:06:46 +0200
Subject: Improve formatting of scalars in Lean

---
 compiler/Extract.ml | 33 ++++++++++-----------------------
 1 file changed, 10 insertions(+), 23 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 99ea14a4..b56d8c51 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -912,11 +912,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | Scalar sv -> (
         match !backend with
         | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
-        | Coq | HOL4 ->
+        | Coq | HOL4 | Lean ->
             let print_brackets = inside && !backend = HOL4 in
             if print_brackets then F.pp_print_string fmt "(";
             (match !backend with
-            | Coq -> ()
+            | Coq | Lean -> ()
             | HOL4 ->
                 F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty);
                 F.pp_print_space fmt ()
@@ -924,30 +924,17 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             (* We need to add parentheses if the value is negative *)
             if sv.PV.value >= Z.of_int 0 then
               F.pp_print_string fmt (Z.to_string sv.PV.value)
-            else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
+            else
+              F.pp_print_string fmt
+                ("(" ^ Z.to_string sv.PV.value
+                ^ if !backend = Lean then ":Int" else "" ^ ")");
             (match !backend with
-            | Coq -> F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty)
+            | Coq | Lean ->
+                let iname = String.lowercase_ascii (int_name sv.PV.int_ty) in
+                F.pp_print_string fmt ("%" ^ iname)
             | HOL4 -> ()
             | _ -> raise (Failure "Unreachable"));
-            if print_brackets then F.pp_print_string fmt ")"
-        | Lean ->
-            F.pp_print_string fmt "(";
-            F.pp_print_string fmt (int_name sv.int_ty);
-            F.pp_print_string fmt ".ofInt ";
-            (* Something very annoying: negated values like `-3` are
-               ambiguous in Lean because of conversions, so we have to
-               be extremely explicit with negative numbers.
-            *)
-            if Z.lt sv.value Z.zero then (
-              F.pp_print_string fmt "(";
-              F.pp_print_string fmt "-";
-              F.pp_print_string fmt "(";
-              Z.pp_print fmt (Z.neg sv.value);
-              F.pp_print_string fmt ":Int";
-              F.pp_print_string fmt ")";
-              F.pp_print_string fmt ")")
-            else Z.pp_print fmt sv.value;
-            F.pp_print_string fmt ")")
+            if print_brackets then F.pp_print_string fmt ")")
     | Bool b ->
         let b =
           match !backend with
-- 
cgit v1.2.3