diff options
Diffstat (limited to 'riscv/riscv_extras_embed_sequential.lem')
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 14 |
1 files changed, 14 insertions, 0 deletions
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))) |