Adding a mk_struct test

rems-project · Jan 16, 2025 · 662fa50 · 662fa50
1 parent e75d960
commit 662fa50
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 1 deletion.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -284,7 +284,7 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
       nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e
   | E_struct fexps ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (separate comma args)
+      braces (separate (comma ^^ space) args)
   | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id
   | E_struct_update (exp, fexps) ->
       let args = List.map (doc_fexp ctxt) fexps in

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -14,6 +14,10 @@ def struct_field2 (s : My_struct) : (BitVec 1) :=
 def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
   {s with field2 := b}
 
+/-- Type quantifiers: i : Int -/
+def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
+  {field1 := i, field2 := b}
+
 def initialize_registers : Unit :=
   ()
 
diff --git a/test/lean/struct.sail b/test/lean/struct.sail
@@ -15,4 +15,12 @@ function struct_field2(s) = {
 val struct_update_field2 : (My_struct, bit) -> My_struct
 function struct_update_field2(s, b) = {
   { s with field2 = b }
+}
+
+val mk_struct : (int, bit) -> My_struct
+function mk_struct(i, b) = {
+  struct { 
+    field1 = i,
+    field2 = b
+  }
 }