changing registerRef to UpperCamelCase

src/sail_lean_backend/Sail/Sail.lean

@@ -33,7 +33,7 @@ def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo +
 end BitVec
 end Sail
 
-structure registerRef (regstate regval a : Type) where
+structure RegisterRef (regstate regval a : Type) where
   name : String
   read_from : regstate -> a
   write_to : a -> regstate -> regstate

src/sail_lean_backend/pretty_print_lean.ml

@@ -138,7 +138,8 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) =
   | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) ->
       string "Int" (* TODO This probably has to be generalized *)
   | Typ_app (Id_aux (Id "register", _), t_app) ->
-      string "registerRef Unit Unit " (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app
+      string "RegisterRef Unit Unit "
+      (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) 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_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts)

test/lean/bitfield.expected.lean

@@ -16,7 +16,7 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 :=
 def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits (HSub.hSub 8 1) 0 x)}
 
-def _set_cr_type_bits (r_ref : registerRef Unit Unit cr_type) (v : BitVec 8) : Unit :=
+def _set_cr_type_bits (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 8) : Unit :=
   sorry
 
 def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
@@ -25,7 +25,7 @@ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
 def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits 7 4 x)}
 
-def _set_cr_type_CR0 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 4) : Unit :=
+def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 4) : Unit :=
   sorry
 
 def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
@@ -34,7 +34,7 @@ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
 def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits 3 2 x)}
 
-def _set_cr_type_CR1 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit :=
+def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit :=
   sorry
 
 def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
@@ -43,7 +43,7 @@ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
 def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits 1 0 x)}
 
-def _set_cr_type_CR3 (r_ref : registerRef Unit Unit cr_type) (v : BitVec 2) : Unit :=
+def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 2) : Unit :=
   sorry
 
 def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
@@ -52,7 +52,7 @@ def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
 def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits 6 6 x)}
 
-def _set_cr_type_GT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit :=
+def _set_cr_type_GT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit :=
   sorry
 
 def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
@@ -61,7 +61,7 @@ def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
 def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.updateSubrange v.bits 7 7 x)}
 
-def _set_cr_type_LT (r_ref : registerRef Unit Unit cr_type) (v : BitVec 1) : Unit :=
+def _set_cr_type_LT (r_ref : RegisterRef Unit Unit cr_type) (v : BitVec 1) : Unit :=
   sorry
 
 def initialize_registers : Unit :=