open import Pervasives_extra
open import Sail_impl_base
open import Vector
open import Sail_values
open import Arch

val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a
let return a = Done a

val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b
let rec bind m f = match m with
  | Done a ->              f a 
  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s  in (bind o f,opt))
  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s  in (bind o f,opt))
  | Footprint o_s ->       Footprint        (let (o,opt) = o_s  in (bind o f,opt))
  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s  in (bind o f,opt))
  | Escape o_s  ->         Escape o_s
end


type M 'e 'a = Sail_impl_base.outcome unit 'e 'a

let (>>=) = bind
val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
let (>>) m n = m >>= fun _ -> n

val exit : forall 'a 'e. 'e -> M 'e 'a
let exit e = Escape (Just (return e,Nothing))

val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU)
let read_memory rk addr sz =
  let addr = address_lifted_of_bitv addr in
  let sz = natFromInteger sz in
  let k memory_value =
    let bitv = bitv_of_byte_lifteds memory_value in
    (Done bitv,Nothing) in
  Read_mem (rk,addr,sz) k

val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer  -> M 'e unit
let write_memory_ea wk addr sz =
  let addr = address_lifted_of_bitv addr in
  let sz = natFromInteger sz in
  Write_ea (wk,addr,sz) (Done (),Nothing)

val write_memory_val : forall 'e. vector bitU -> M 'e bool
let write_memory_val v =
  let v = byte_lifteds_of_bitv v in
  let k successful = (return successful,Nothing) in
  Write_memv v k


val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU)
let read_reg_range reg i j =
  let (i,j) = (natFromInteger i,natFromInteger j) in
  let start = natFromInteger (start_index_reg reg) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  let k register_value =
    let v = bitvFromRegisterValue register_value in
    (Done v,Nothing) in
  Read_reg reg k

val read_reg_bit : forall 'e. register -> integer -> M 'e bitU
let read_reg_bit reg i = 
  read_reg_range reg i i >>= fun v -> return (access v i)

val read_reg : forall 'e. register -> M 'e (vector bitU)
let read_reg reg =
  let start = natFromInteger (start_index_reg reg) in
  let sz = natFromInteger (length_reg reg) in
  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
  let k register_value =
    let v = bitvFromRegisterValue register_value in
    (Done v,Nothing) in
  Read_reg reg k

val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU)
let read_reg_field reg rfield = 
  let (i,j) =
    let (i,j) = field_indices rfield in
    (natFromInteger i,natFromInteger j) in
  let start = natFromInteger (start_index_reg reg) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  let k register_value =
    let v = bitvFromRegisterValue register_value in
    (Done v,Nothing) in
  Read_reg reg k

val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bitU
let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)



val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit
let write_reg_range reg i j v =
  let rv = registerValueFromBitv v reg in
  let start = natFromInteger (start_index_reg reg) in
  let (i,j) = (natFromInteger i,natFromInteger j) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  Write_reg (reg,rv) (Done (),Nothing)

val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit
let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)

val write_reg : forall 'e. register -> vector bitU -> M 'e unit
let write_reg reg v =
  let rv = registerValueFromBitv v reg in
  let start = natFromInteger (start_index_reg reg) in
  let sz = natFromInteger (length_reg reg) in
  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
  Write_reg (reg,rv) (Done (),Nothing)

val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit
let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)

val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> M 'e unit
let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)


val barrier : forall 'e. barrier_kind -> M 'e unit
let barrier bk = Barrier bk (Done (), Nothing)


val footprint : forall 'e. M 'e unit
let footprint = Footprint (Done (),Nothing)


val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
let rec foreachM_inc (i,stop,by) vars body = 
  if i <= stop
  then
    body i vars >>= fun vars ->
    foreachM_inc (i + by,stop,by) vars body
  else return vars


val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
let rec foreachM_dec (i,stop,by) vars body = 
  if i >= stop
  then
    body i vars >>= fun vars ->
    foreachM_dec (i - by,stop,by) vars body
  else return vars


let write_two_regs r1 r2 vec =
  let size = length_reg r1 in
  let start = get_start vec in
  let vsize = length vec in
  let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
  let r2_v =
    (slice vec)
      (if defaultDir then size - start else start - size)
      (if defaultDir then vsize - start else start - vsize) in
  write_reg r1 r1_v >> write_reg r2 r2_v