Lean: fix parantheses around negative integer literals (#926)

rems-project · Jan 30, 2025 · 9383224 · 9383224
1 parent e7f1262
commit 9383224
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -116,9 +116,11 @@ let string_of_nexp_con (Nexp_aux (n, l)) =
   | Nexp_neg _ -> "Nexp_neg"
   | Nexp_exp _ -> "Nexp_exp"
 
+let doc_big_int i = if i >= Z.zero then string (Big_int.to_string i) else parens (string (Big_int.to_string i))
+
 let doc_nexp ctx (Nexp_aux (n, l) as nexp) =
   match n with
-  | Nexp_constant i -> string (Big_int.to_string i)
+  | Nexp_constant i -> doc_big_int i
   | Nexp_var ki -> doc_kid ctx ki
   | _ -> failwith ("NExp " ^ string_of_nexp_con nexp ^ " " ^ string_of_nexp nexp ^ " not translatable yet.")
 
@@ -220,9 +222,7 @@ let doc_lit (L_aux (lit, l)) =
   | L_one -> string "1#1"
   | L_false -> string "false"
   | L_true -> string "true"
-  | L_num i ->
-      let s = Big_int.to_string i in
-      string s
+  | L_num i -> doc_big_int i
   | L_hex n -> utf8string ("0x" ^ n)
   | L_bin n -> utf8string ("0b" ^ n)
   | L_undef -> utf8string "(Fail \"undefined value of unsupported type\")"

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -8,7 +8,7 @@ def extern_add : Int :=
   (Int.add 5 4)
 
 def extern_sub : Int :=
-  (Int.sub 5 4)
+  (Int.sub 5 (-4))
 
 def extern_tdiv : Int :=
   (Int.tdiv 5 4)
@@ -20,10 +20,10 @@ def extern_tmod_positive : Int :=
   (Int.tmod 5 4)
 
 def extern_negate : Int :=
-  (Int.neg 5)
+  (Int.neg (-5))
 
 def extern_mult : Int :=
-  (Int.mul 5 4)
+  (Int.mul 5 (-4))
 
 def extern_and : Bool :=
   (Bool.and true false)

diff --git a/test/lean/extern.sail b/test/lean/extern.sail
@@ -7,7 +7,7 @@ function extern_add() -> int = {
 }
 
 function extern_sub() -> int = {
-  return sub_int(5, 4)
+  return sub_int(5, -4)
 }
 
 function extern_tdiv() -> int = {
@@ -23,11 +23,11 @@ function extern_tmod_positive() -> int = {
 }
 
 function extern_negate() -> int = {
-  return negate_int(5)
+  return negate_int(-5)
 }
 
 function extern_mult() -> int = {
-  return mult_int(5, 4)
+  return mult_int(5, -4)
 }
 
 function extern_and() -> bool = {