Fix Lem generation for RISC-V

2 files changed, 16 insertions, 2 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index f77994d6..dacde107 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -378,10 +378,10 @@ function vector64 n = __raw_GetSlice_int(64, n, 0)
 
 function break () : unit -> unit = ()
 
-val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o.
+val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
-val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o.
+val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
   (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
 
 overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem
index ba00defb..044b2aa3 100644
--- a/riscv/riscv_extras_embed_sequential.lem
+++ b/riscv/riscv_extras_embed_sequential.lem
@@ -41,3 +41,17 @@ let zero_extend v len = extz_vec len v
 
 let shift_bits_right v m = shiftr v (unsigned m)
 let shift_bits_left v m = shiftl v (unsigned m)
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))