open import Pervasives
open import Pervasives_extra
open import Sail_instr_kinds
open import Sail_values
open import Sail_operators_mwords
open import Prompt_monad
open import Prompt

type bitvector 'a = mword 'a

let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
let MEM_fence_i     () = barrier Barrier_RISCV_i

val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e

let MEMea addr size                      = write_mem_ea Write_plain addr size
let MEMea_release addr size              = write_mem_ea Write_RISCV_release addr size
let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_release addr size
let MEMea_conditional addr size          = write_mem_ea Write_RISCV_conditional addr size
let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_release addr size
let MEMea_conditional_strong_release addr size
                                          = write_mem_ea Write_RISCV_conditional_strong_release addr size

val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e
let write_ram addrsize size hexRAM address value =
  write_mem_ea Write_plain address size >>
  write_mem_val value >>= fun _ ->
  return ()

val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
  integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
let read_ram addrsize size hexRAM address =
  read_mem Read_plain address size

let speculate_conditional_success () = excl_result ()

val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
let get_slice_int len n lo =
  (* TODO: Is this the intended behaviour? *)
  let hi = lo + len - 1 in
  let bits = bits_of_int (hi + 1) n in
  of_bits_failwith (subrange_list false bits hi lo)

val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_right v m = shiftr v (uint m)
val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
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)

val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))