open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail_values
open import Prompt_monad
open import Prompt
open import State_monad
open import {isabelle} `State_monad_extras`

(* State monad wrapper around prompt monad *)

val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
let rec liftState _ (Done a)          = returnS a
and liftState ra (Read_mem rk a sz k) = bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
and liftState ra (Write_memv descr k) = bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
and liftState ra (Read_reg descr k)   = bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
and liftState ra (Excl_res k)         = bindS (excl_resultS ())       (fun v -> liftState ra (k v))
and liftState ra (Write_ea wk a sz k) = seqS (write_mem_eaS wk a sz)  (liftState ra k)
and liftState ra (Write_reg r v k)    = seqS (write_regvalS ra r v)   (liftState ra k)
and liftState ra (Barrier _ k)        = liftState ra k
and liftState _  (Fail descr)         = failS descr
and liftState _  (Error descr)        = failS descr
and liftState _  (Exception e)        = throwS e


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

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

val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs '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 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs '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 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_PM vars cond body s =
  if cond vars then
    bind (body vars) (fun vars s' -> while_PM vars cond body s') s
  else return vars s

val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                ('vars -> 'vars) -> M 'regs 'vars 'e
let rec while_MP vars cond body s =
  bind
    (cond vars)
    (fun cond_val s' ->
      if cond_val then while_MP (body vars) cond body s' else return vars s') s

val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_MM vars cond body s =
  bind
    (cond vars)
    (fun cond_val s' ->
      if cond_val then
        bind
          (body vars)
          (fun vars s'' -> while_MM vars cond body s'') s'
      else return vars s') s

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 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_PM vars cond body s =
  bind
    (body vars)
    (fun vars s' ->
      if (cond vars) then return vars s' else until_PM vars cond body s') s

val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                ('vars -> 'vars) -> M 'regs 'vars 'e
let rec until_MP vars cond body s =
  let vars = body vars in
  bind
    (cond vars)
    (fun cond_val s' ->
      if cond_val then return vars s' else until_MP vars cond body s') s

val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_MM vars cond body s =
  bind
    (body vars)
    (fun vars s' ->
      bind
        (cond vars)
        (fun cond_val s''->
          if cond_val then return vars s'' else until_MM vars cond body s'') s') s
*)