open import Pervasives_extra
open import Sail_impl_base
open import Sail_values

type MR 'a 'r = outcome_r 'a 'r
type M 'a = outcome 'a

val return : forall 'a 'r. 'a -> MR 'a 'r
let return a = Done a

val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
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))
  | Excl_res k ->          Excl_res         (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 descr ->        Escape descr
  | Fail descr ->          Fail descr
  | Error descr ->         Error descr
  | Return a ->            Return a
  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
end


let inline (>>=) = bind
val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
let inline (>>) m n = m >>= fun _ -> n

val exit : forall 'a 'b. 'b -> M 'a
let exit s = Fail Nothing

val assert_exp : bool -> string -> M unit
let assert_exp exp msg = if exp then Done () else Fail (Just msg)

val early_return : forall 'r. 'r -> MR unit 'r
let early_return r = Return r

val liftR : forall 'a 'r. M 'a -> MR 'a 'r
let rec liftR m = match m with
  | Done a ->              Done a
  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (liftR o,opt))
  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (liftR o,opt))
  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (liftR o,opt))
  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (liftR o,opt))
  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (liftR o,opt))
  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (liftR o,opt))
  | Escape descr ->        Escape descr
  | Fail descr ->          Fail descr
  | Error descr ->         Error descr
  | Return _ ->            Error "uncaught early return"
end

val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
let rec catch_early_return m = match m with
  | Done a ->              Done a
  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (catch_early_return o,opt))
  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (catch_early_return o,opt))
  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (catch_early_return o,opt))
  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (catch_early_return o,opt))
  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (catch_early_return o,opt))
  | Escape descr ->        Escape descr
  | Fail descr ->          Fail descr
  | Error descr ->         Error descr
  | Return a ->            Done a
end

val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b
let read_mem dir rk addr sz =
  let addr = address_lifted_of_bitv (bits_of addr) in
  let sz = natFromInteger sz in
  let k memory_value =
    let bitv = of_bits (internal_mem_value dir memory_value) in
    (Done bitv,Nothing) in
  Read_mem (rk,addr,sz) k

val excl_result : unit -> M bool
let excl_result () =
  let k successful = (return successful,Nothing) in
  Excl_res k

val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit
let write_mem_ea wk addr sz =
  let addr = address_lifted_of_bitv (bits_of addr) in
  let sz = natFromInteger sz in
  Write_ea (wk,addr,sz) (Done (),Nothing)

val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool
let write_mem_val v =
  let v = external_mem_value (bits_of v) in
  let k successful = (return successful,Nothing) in
  Write_memv v k

val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a
let read_reg_aux reg = 
  let k reg_value =
    let v = of_bits (internal_reg_value reg_value) in
    (Done v,Nothing) in
  Read_reg reg k

let read_reg reg =
  read_reg_aux (external_reg_whole reg)
let read_reg_range reg i j =
  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
let read_reg_bit reg i =
  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
  return (extract_only_element v)
let read_reg_field reg regfield =
  read_reg_aux (external_reg_field_whole reg regfield.field_name)
let read_reg_bitfield reg regfield =
  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
  return (extract_only_element v)

let reg_deref = read_reg

val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit
let write_reg_aux reg_name v =
  let regval = external_reg_value reg_name (bits_of v) in
  Write_reg (reg_name,regval) (Done (), Nothing)

let write_reg reg v =
  write_reg_aux (external_reg_whole reg) v
let write_reg_range reg i j v =
  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
let write_reg_pos reg i v =
  let iN = natFromInteger i in
  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
let write_reg_bit = write_reg_pos
let write_reg_field reg regfield v =
  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
(*let write_reg_field_bit reg regfield bit =
  write_reg_aux (external_reg_field_whole reg regfield.field_name)
                (Vector [bit] 0 (is_inc_of_reg reg))*)
let write_reg_field_range reg regfield i j v =
  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
let write_reg_field_pos reg regfield i v =
  write_reg_field_range reg regfield i i [v]
let write_reg_field_bit = write_reg_field_pos

let write_reg_ref (reg, v) = write_reg reg v

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


val footprint : M unit
let footprint = Footprint (Done (),Nothing)


val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
let rec iter_aux i f xs = match xs with
  | x :: xs -> f i x >> iter_aux (i + 1) f xs
  | [] -> return ()
  end

val iteri : forall 'regs 'e 'a. (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
let iteri f xs = iter_aux 0 f xs

val iter : forall 'regs 'e 'a. ('a -> MR unit 'e) -> list 'a -> MR unit 'e
let iter f xs = iteri (fun _ x -> f x) xs


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


val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
let rec foreachM_dec (i,stop,by) vars body =
  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
  then
    body i vars >>= fun vars ->
    foreachM_dec (i - by,stop,by) vars body
  else return vars

val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec while_PP vars cond body =
  if cond vars then while_PP (body vars) cond body else vars

val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
                ('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec while_PM vars cond body =
  if cond vars then
    body vars >>= fun vars -> while_PM vars cond body
  else return vars

val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
                ('vars -> 'vars) -> MR 'vars 'r
let rec while_MP vars cond body =
  cond vars >>= fun cond_val ->
  if cond_val then while_MP (body vars) cond body else return vars

val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
                ('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec while_MM vars cond body =
  cond vars >>= fun cond_val ->
  if cond_val then
    body vars >>= fun vars -> while_MM vars cond body
  else return vars

val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec until_PP vars cond body =
  let vars = body vars in
  if (cond vars) then vars else until_PP (body vars) cond body

val until_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
                ('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec until_PM vars cond body =
  body vars >>= fun vars ->
  if (cond vars) then return vars else until_PM vars cond body

val until_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
                ('vars -> 'vars) -> MR 'vars 'r
let rec until_MP vars cond body =
  let vars = body vars in
  cond vars >>= fun cond_val ->
  if cond_val then return vars else until_MP vars cond body

val until_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
                ('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec until_MM vars cond body =
  body vars >>= fun vars ->
  cond vars >>= fun cond_val ->
  if cond_val then return vars else until_MM vars cond body

(*let write_two_regs r1 r2 vec =
  let is_inc =
    let is_inc_r1 = is_inc_of_reg r1 in
    let is_inc_r2 = is_inc_of_reg r2 in
    let () = ensure (is_inc_r1 = is_inc_r2)
                    "write_two_regs called with vectors of different direction" in
    is_inc_r1 in

  let (size_r1 : integer) = size_of_reg r1 in
  let (start_vec : integer) = get_start vec in
  let size_vec = length vec in
  let r1_v =
    if is_inc
    then slice vec start_vec (size_r1 - start_vec - 1)
    else slice vec start_vec (start_vec - size_r1 - 1) in
  let r2_v =
    if is_inc
    then slice vec (size_r1 - start_vec) (size_vec - start_vec)
    else slice vec (start_vec - size_r1) (start_vec - size_vec) in
  write_reg r1 r1_v >> write_reg r2 r2_v*)