From 11d722f8d35e7ce95c7a33d678285b03ce4a5dd7 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Thu, 31 Oct 2024 11:50:49 +0100
Subject: [PATCH] be able to translate operation tests on bit vectors (#755)

---
 lib/vector.sail                            |  1 +
 src/sail_lean_backend/pretty_print_lean.ml | 10 ++++++++--
 test/lean/extern_bitvec.expected.lean      |  9 +++++++++
 test/lean/extern_bitvec.sail               | 12 ++++++++++++
 4 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 test/lean/extern_bitvec.expected.lean
 create mode 100644 test/lean/extern_bitvec.sail

diff --git a/lib/vector.sail b/lib/vector.sail
index aa1caf059..88fc77c7a 100644
--- a/lib/vector.sail
+++ b/lib/vector.sail
@@ -198,6 +198,7 @@ val add_bits = pure {
   interpreter: "add_vec",
   lem: "add_vec",
   coq: "add_vec",
+  lean: "Add.add",
   _: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index b63a4f8f9..4bfe95ea3 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -64,10 +64,14 @@ let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
   | _, [typ] -> ([(pat, typ)], identity)
   | _, _ -> unreachable l __POS__ "Unexpected pattern/type combination"
 
+let doc_nexp (Nexp_aux (n, l) as nexp) =
+  match n with Nexp_constant i -> string (Big_int.to_string i) | _ -> failwith "NExp not translatable yet."
+
 let doc_typ (Typ_aux (t, _) as typ) =
   match t with
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
   | Typ_id (Id_aux (Id "int", _)) -> string "Int"
+  | Typ_app (Id_aux (Id "bitvector", _), [A_aux (A_nexp m, _)]) -> string "BitVec " ^^ doc_nexp m
   | _ -> failwith "Type not translatable yet."
 
 let lean_escape_string s = Str.global_replace (Str.regexp "\"") "\"\"" s
@@ -82,8 +86,8 @@ let doc_lit (L_aux (lit, l)) =
   | L_num i ->
       let s = Big_int.to_string i in
       string s
-  | L_hex n -> utf8string ("Ox" ^ n)
-  | L_bin n -> utf8string ("Ob" ^ n)
+  | L_hex n -> utf8string ("0x" ^ n)
+  | L_bin n -> utf8string ("0b" ^ n)
   | L_undef -> utf8string "(Fail \"undefined value of unsupported type\")"
   | L_string s -> utf8string ("\"" ^ lean_escape_string s ^ "\"")
   | L_real s -> utf8string s (* TODO test if this is really working *)
@@ -99,6 +103,8 @@ let rec doc_exp (E_aux (e, (l, annot)) as full_exp) =
       in
       let d_args = List.map doc_exp args in
       nest 2 (parens (flow (break 1) (d_id :: d_args)))
+  | E_vector vals -> failwith "vector found"
+  | E_typ (typ, e) -> parens (separate space [doc_exp e; colon; doc_typ typ])
   | _ -> failwith "Expression not translatable yet"
 
 let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) =
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
new file mode 100644
index 000000000..55c5ff288
--- /dev/null
+++ b/test/lean/extern_bitvec.expected.lean
@@ -0,0 +1,9 @@
+def extern_const : BitVec 64 :=
+  (0xFFFF000012340000 : BitVec 64)
+
+def extern_add : BitVec 16 :=
+  (Add.add (0xFFFF : BitVec 16) (0x1234 : BitVec 16))
+
+def initialize_registers : Unit :=
+  ()
+
diff --git a/test/lean/extern_bitvec.sail b/test/lean/extern_bitvec.sail
new file mode 100644
index 000000000..92dcf62a5
--- /dev/null
+++ b/test/lean/extern_bitvec.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+function extern_const() -> bitvector(64) = {
+  return 0xFFFF_0000_1234_0000
+}
+
+function extern_add() -> bitvector(16) = {
+  return 0xFFFF + 0x1234
+}
+