open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail_values
open import Prompt_monad
open import {isabelle} `Prompt_monad_extras`

val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv 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 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
let iteri f xs = iter_aux 0 f xs

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


val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                ('vars -> 'vars) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                ('vars -> 'vars) -> monad 'rv 'vars 'e
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 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
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*)