diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 8 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 8 | ||||
| -rw-r--r-- | riscv/riscv_extras_sequential.lem | 8 |
3 files changed, 18 insertions, 6 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 412dcfc7..9ec1d86d 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -217,7 +217,7 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val print = "prerr_endline" : string -> unit +val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit @@ -402,9 +402,9 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) -val print_int = "prerr_int" : (string, int) -> unit -val print_bits = "prerr_bits" : forall 'n. (string, bits('n)) -> unit -val print_string = "prerr_string" : (string, string) -> unit +val print_int = "print_int" : (string, int) -> unit +val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit +val print_string = "print_string" : (string, string) -> unit val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index b29fe545..b3d84df6 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -101,7 +101,13 @@ val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvecto let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit -let print_string msg s = prerr_endline (msg ^ s) +let print_string msg s = print_endline (msg ^ s) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem index b29fe545..b3d84df6 100644 --- a/riscv/riscv_extras_sequential.lem +++ b/riscv/riscv_extras_sequential.lem @@ -101,7 +101,13 @@ val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvecto let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit -let print_string msg s = prerr_endline (msg ^ s) +let print_string msg s = print_endline (msg ^ s) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) |