fix parentheses around Vector

rems-project · Feb 3, 2025 · a5dbda8 · a5dbda8
1 parent a8621bd
commit a5dbda8
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -199,7 +199,7 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
   match t with
   | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp m, _); A_aux (A_typ elem_typ, _)]) ->
       (* TODO: remove duplication with exists, below *)
-      string "Vector" ^^ space ^^ parens (doc_typ ctx elem_typ) ^^ space ^^ doc_nexp ctx m
+      nest 2 (parens (flow space [string "Vector"; doc_typ ctx elem_typ; doc_nexp ctx m]))
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
   | Typ_id (Id_aux (Id "int", _)) -> string "Int"
   | Typ_app (Id_aux (Id "atom_bool", _), _) | Typ_id (Id_aux (Id "bool", _)) -> string "Bool"
@@ -210,7 +210,7 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
       parens (string "BitVec " ^^ doc_nexp ctx m)
   | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int"
   | Typ_app (Id_aux (Id "register", _), t_app) ->
-      string "RegisterRef RegisterType " ^^ separate_map comma (doc_typ_app ctx) t_app
+      parens (string "RegisterRef RegisterType " ^^ separate_map comma (doc_typ_app ctx) t_app)
   | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) ->
       underscore (* TODO check if the type of implicit arguments can really be always inferred *)
   | Typ_app (Id_aux (Id "option", _), [A_aux (A_typ typ, _)]) -> parens (string "Option " ^^ doc_typ ctx typ)

diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
@@ -29,7 +29,7 @@ def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) :=
 def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x)
 
-def _set_cr_type_bits (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 8)) : SailM Unit := do
+def _set_cr_type_bits (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 8)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_bits r v)
 
@@ -39,7 +39,7 @@ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) :=
 def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v 7 4 x)
 
-def _set_cr_type_CR0 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 4)) : SailM Unit := do
+def _set_cr_type_CR0 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 4)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_CR0 r v)
 
@@ -49,7 +49,7 @@ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) :=
 def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v 3 2 x)
 
-def _set_cr_type_CR1 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do
+def _set_cr_type_CR1 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 2)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_CR1 r v)
 
@@ -59,7 +59,7 @@ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) :=
 def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v 1 0 x)
 
-def _set_cr_type_CR3 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do
+def _set_cr_type_CR3 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 2)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_CR3 r v)
 
@@ -69,7 +69,7 @@ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) :=
 def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v 6 6 x)
 
-def _set_cr_type_GT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do
+def _set_cr_type_GT (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 1)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_GT r v)
 
@@ -79,7 +79,7 @@ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) :=
 def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
   (Sail.BitVec.updateSubrange v 7 7 x)
 
-def _set_cr_type_LT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do
+def _set_cr_type_LT (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 1)) : SailM Unit := do
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_LT r v)
 

diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
@@ -79,7 +79,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
   default := .Reg _PC
 abbrev SailM := PreSailM RegisterType
 
-def GPRs : Vector (RegisterRef RegisterType (BitVec 64)) 31 :=
+def GPRs : (Vector (RegisterRef RegisterType (BitVec 64)) 31) :=
   #v[Reg R30, Reg R29, Reg R28, Reg R27, Reg R26, Reg R25, Reg R24, Reg R23, Reg R22, Reg R21,
     Reg R20, Reg R19, Reg R18, Reg R17, Reg R16, Reg R15, Reg R14, Reg R13, Reg R12, Reg R11,
     Reg R10, Reg R9, Reg R8, Reg R7, Reg R6, Reg R5, Reg R4, Reg R3, Reg R2, Reg R1, Reg R0]