open import Pervasives
open import Vector
open import Arch

(* 'a is result type, 'e is error type *)
type M 's 'e 'a = 's -> (either 'a 'e * 's)

val return : forall 's 'e 'a. 'a -> M 's 'e 'a
let return a s = (Left a,s)

val bind : forall 's 'e 'a 'b. M 's 'e 'a -> ('a -> M 's 'e 'b) -> M 's 'e 'b
let bind m f s = match m s with
  | (Left a,s') -> f a s'
  | (Right error,s') -> (Right error,s')
  end

val exit : forall 's 'e 'a. 'e -> M 's 'e 'a
let exit e s = (Right e,s)

let (>>=) = bind
let (>>) m n = m >>= fun _ -> n

val read_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> M state 'e (vector bit)
let read_reg_range reg (i,j) s =
  let v = slice (read_regstate s reg) i j in
  (Left v,s)

val read_reg_bit : forall 'e. register -> integer (*nat*) -> M state 'e bit
let read_reg_bit reg i s =
  let v = access (read_regstate s reg) i in
  (Left v,s)

val write_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> vector bit -> M state 'e unit
let write_reg_range (reg : register) (i,j) (v : vector bit) s =
  let v' = update (read_regstate s reg) i j v in
  let s' = write_regstate s reg v' in
  (Left (),s')

val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> M state 'e unit
let write_reg_bit reg i bit s =
  let v = read_regstate s reg in
  let v' = update_pos v i bit in
  let s' = write_regstate s reg v' in
  (Left (),s')

val read_reg : forall 'e. register -> M state 'e (vector bit)
let read_reg reg s =
  let v = read_regstate s reg in
  (Left v,s)

val write_reg : forall 'e. register -> vector bit -> M state 'e unit
let write_reg reg v s =
  let s' = write_regstate s reg v in
  (Left (),s')
    

val foreach_inc :  forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
let rec foreach_inc (i,stop,by) vars body = 
  if i <= stop
  then
    let (_,vars) = body i vars in
    foreach_inc (i + by,stop,by) vars body
  else ((),vars)


val foreach_dec : forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
let rec foreach_dec (i,stop,by) vars body = 
  if i >= stop
  then
    let (_,vars) = body i vars in
    foreach_dec (i - by,stop,by) vars body
  else ((),vars)


val foreachM_inc : forall 's 'e 'vars. (nat * nat * nat) -> 'vars ->
                  (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * '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 's 'e 'vars. (nat * nat * nat) -> 'vars ->
                  (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * '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)

val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit)
let read_reg_field reg rfield = read_reg_range reg (field_indices rfield)

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

val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit
let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)

val write_reg_field_bit : forall 'e. register -> register_field_bit -> bit -> M state 'e unit
let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)


let length l = integerFromNat (length l)

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