Lean: Small fixes for the RISC-V model

lib/flow.sail

@@ -58,7 +58,7 @@ therefore be included in just about every Sail specification.
 val eq_unit = pure { lean : "BEq.beq", _ : "eq_unit" } : (unit, unit) -> bool(true)
 function eq_unit(_, _) = true
 
-val eq_bit = pure { lem : "eq", lean : "Eq", _ : "eq_bit" } : (bit, bit) -> bool
+val eq_bit = pure { lem : "eq", lean : "BEq.beq", _ : "eq_bit" } : (bit, bit) -> bool
 
 val not_bool = pure {coq: "negb", lean: "Bool.not", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
 /* NB: There are special cases in Sail for effectful uses of and_bool and

lib/vector.sail

@@ -208,7 +208,7 @@ val bitvector_update = pure {
   interpreter: "update",
   lem: "update_vec_dec",
   coq: "update_vec_dec",
-  lean: "bitvectorUpdate",
+  lean: "BitVec.update",
   _: "vector_update"
 } : forall 'n 'm, 0 <= 'm < 'n. (bits('n), int('m), bit) -> bits('n)
 $else

src/sail_lean_backend/Sail/Sail.lean

@@ -44,6 +44,8 @@ def append' (x : BitVec n) (y : BitVec m) {mn}
     (hmn : mn = n + m := by (conv => rhs; dsimp); try rfl) : BitVec mn :=
   hmn ▸ x.append y
 
+def update (x : BitVec m) (n : Nat) (b : BitVec 1) := updateSubrange' x n _ b
+
 def toBin {w : Nat} (x : BitVec w) : String :=
   List.asString (List.map (fun c => if c then '1' else '0') (List.ofFn (BitVec.getMsb' x)))
 
@@ -199,8 +201,6 @@ def reg_deref (reg_ref : @RegisterRef Register RegisterType α) : PreSailM Regis
 
 def vectorAccess [Inhabited α] (v : Vector α m) (n : Nat) := v[n]!
 
-def bitvectorUpdate (v : BitVec m) (n : Nat) (b : Bool) := v[n]! = b
-
 def vectorUpdate (v : Vector α m) (n : Nat) (a : α) := v.set! n a
 
 def assert (p : Bool) (s : String) : PreSailM RegisterType c ue Unit :=
@@ -326,7 +326,6 @@ def main_of_sail_main (initialState : SequentialState RegisterType c) (main : Un
   | .error e _ => do
     IO.println s!"Error while running the sail program!: {e.print}"
 
-
 section Loops
 
 def foreach_' (from' to step : Nat) (vars : Vars) (body : Nat -> Vars -> Vars) : Vars := Id.run do

src/sail_lean_backend/pretty_print_lean.ml

@@ -515,11 +515,13 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       if Env.is_register id env then wrap_with_left_arrow (not as_monadic) (string "readReg " ^^ doc_id_ctor id)
       else wrap_with_pure as_monadic (doc_id_ctor id)
   | E_lit l -> wrap_with_pure as_monadic (doc_lit l)
-  | E_app (Id_aux (Id "None", _), _) -> string "none"
+  | E_app (Id_aux (Id "None", _), _) -> wrap_with_pure as_monadic (string "none")
   | E_app (Id_aux (Id "Some", _), args) ->
-      let d_id = string "some" in
-      let d_args = List.map d_of_arg args in
-      nest 2 (parens (flow (break 1) (d_id :: d_args)))
+      wrap_with_pure as_monadic
+        (let d_id = string "some" in
+         let d_args = List.map d_of_arg args in
+         nest 2 (parens (flow (break 1) (d_id :: d_args)))
+        )
   | E_app (Id_aux (Id "foreach#", _), args) -> begin
       let doc_loop_var (E_aux (e, (l, _)) as exp) =
         match e with
@@ -608,8 +610,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
   | E_vector vals ->
       string "#v" ^^ wrap_with_pure as_monadic (brackets (nest 2 (flow (comma ^^ break 1) (List.map d_of_arg vals))))
   | E_typ (typ, e) ->
-      if effectful (effect_of e) then
-        parens (separate space [doc_exp as_monadic ctx e; colon; string "SailM"; doc_typ ctx typ])
+      if effectful (effect_of e) then doc_exp as_monadic ctx e
       else wrap_with_pure as_monadic (parens (separate space [doc_exp false ctx e; colon; doc_typ ctx typ]))
   | E_tuple es -> wrap_with_pure as_monadic (parens (separate_map (comma ^^ space) d_of_arg es))
   | E_internal_plet (lpat, lexp, e) | E_let (LB_aux (LB_val (lpat, lexp), _), e) ->