open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_bitlists
open import Sail2_prompt_monad
open import Sail2_prompt

type ty512
instance (Size ty512) let size = 512 end
declare isabelle target_rep type ty512 = `512`
type ty1024
instance (Size ty1024) let size = 1024 end
declare isabelle target_rep type ty1024 = `1024`
type ty2048
instance (Size ty2048) let size = 2048 end
declare isabelle target_rep type ty2048 = `2048`

let hexchar_to_bool_list c =
  if c = #'0' then      Just ([false;false;false;false])
  else if c = #'1' then Just ([false;false;false;true ])
  else if c = #'2' then Just ([false;false;true; false])
  else if c = #'3' then Just ([false;false;true; true ])
  else if c = #'4' then Just ([false;true; false;false])
  else if c = #'5' then Just ([false;true; false;true ])
  else if c = #'6' then Just ([false;true; true; false])
  else if c = #'7' then Just ([false;true; true; true ])
  else if c = #'8' then Just ([true; false;false;false])
  else if c = #'9' then Just ([true; false;false;true ])
  else if c = #'A' then Just ([true; false;true; false])
  else if c = #'a' then Just ([true; false;true; false])
  else if c = #'B' then Just ([true; false;true; true ])
  else if c = #'b' then Just ([true; false;true; true ])
  else if c = #'C' then Just ([true; true; false;false])
  else if c = #'c' then Just ([true; true; false;false])
  else if c = #'D' then Just ([true; true; false;true ])
  else if c = #'d' then Just ([true; true; false;true ])
  else if c = #'E' then Just ([true; true; true; false])
  else if c = #'e' then Just ([true; true; true; false])
  else if c = #'F' then Just ([true; true; true; true ])
  else if c = #'f' then Just ([true; true; true; true ])
  else Nothing

let hexstring_to_bools s =
  match (toCharList s) with
    | z :: x :: hs ->
       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
    | _ -> Nothing
  end

val hex_slice : forall 'rv 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
let hex_slice v len lo =
  match hexstring_to_bools v with
    | Just bs ->
       let hi = len + lo - 1 in
       let bs = ext_list false (len + lo) bs in
       return (of_bools (subrange_list false bs hi lo))
    | Nothing -> Fail "hex_slice"
  end

(* Use constants for undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)
val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
let undefined_vector len u = return (repeat [u] len)
val undefined_bitvector : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
let undefined_bitvector len = return (of_bools (repeat [false] len))
val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
let undefined_bits = undefined_bitvector
let undefined_bit () = return B0
let undefined_real () = return (realFromFrac 0 1)
let undefined_range i j = return i
let undefined_atom i = return i
let undefined_nat () = return (0:ii)

val write_ram : forall 'rv 'e.
  integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e
let write_ram addrsize size hexRAM address value =
  write_mem_ea Write_plain address size >>
  write_mem Write_plain address size value >>= fun _ ->
  return ()

val read_ram : forall 'rv 'e.
  integer -> integer -> list bitU -> list bitU -> monad 'rv (list bitU) 'e
let read_ram addrsize size hexRAM address =
  read_mem Read_plain address size

val elf_entry : unit -> integer
let elf_entry () = 0
declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`