open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail_instr_kinds
open import Sail_values

type register_name = string
type address = list bitU

type monad 'regval 'a 'e =
  | Done of 'a
  (* Read a number of bytes from memory, returned in little endian order *)
  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
  (* Read the tag of a memory address *)
  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
  (* Tell the system a write is imminent, at address lifted, of size nat *)
  | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
  (* Request the result of store-exclusive *)
  | Excl_res of (bool -> monad 'regval 'a 'e)
  (* Request to write memory at last signalled address. Memory value should be 8
     times the size given in ea signal, given in little endian order *)
  | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
  (* Request to write the tag at given address. *)
  | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
  (* Tell the system to dynamically recalculate dependency footprint *)
  | Footprint of monad 'regval 'a 'e
  (* Request a memory barrier *)
  | Barrier of barrier_kind * monad 'regval 'a 'e
  (* Request to read register, will track dependency when mode.track_values *)
  | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
  (* Request to write register *)
  | Write_reg of register_name * 'regval * monad 'regval 'a 'e
  | Undefined of (bool -> monad 'regval 'a 'e)
  (* Print debugging or tracing information *)
  | Print of string * monad 'regval 'a 'e
  (*Result of a failed assert with possible error message to report*)
  | Fail of string
  (* Exception of type 'e *)
  | Exception of 'e

val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
let return a = Done a

val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
let rec bind m f = match m with
  | Done a -> f a
  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
  | Read_tag a k ->       Read_tag a       (fun v -> bind (k v) f)
  | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
  | Write_tag a t k ->    Write_tag a t    (fun v -> bind (k v) f)
  | Read_reg descr k ->   Read_reg descr   (fun v -> bind (k v) f)
  | Excl_res k ->         Excl_res         (fun v -> bind (k v) f)
  | Undefined k ->        Undefined        (fun v -> bind (k v) f)
  | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
  | Footprint k ->        Footprint        (bind k f)
  | Barrier bk k ->       Barrier bk       (bind k f)
  | Write_reg r v k ->    Write_reg r v    (bind k f)
  | Print msg k ->        Print msg        (bind k f)
  | Fail descr ->         Fail descr
  | Exception e ->        Exception e
end

val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
let exit () = Fail "exit"

val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
let undefined_bool () = Undefined return

val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
let assert_exp exp msg = if exp then Done () else Fail msg

val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e
let throw e = Exception e

val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
let rec try_catch m h = match m with
  | Done a ->             Done a
  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
  | Read_tag a k ->       Read_tag a       (fun v -> try_catch (k v) h)
  | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
  | Write_tag a t k ->    Write_tag a t    (fun v -> try_catch (k v) h)
  | Read_reg descr k ->   Read_reg descr   (fun v -> try_catch (k v) h)
  | Excl_res k ->         Excl_res         (fun v -> try_catch (k v) h)
  | Undefined k ->        Undefined        (fun v -> try_catch (k v) h)
  | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
  | Footprint k ->        Footprint        (try_catch k h)
  | Barrier bk k ->       Barrier bk       (try_catch k h)
  | Write_reg r v k ->    Write_reg r v    (try_catch k h)
  | Print msg k ->        Print msg        (try_catch k h)
  | Fail descr ->         Fail descr
  | Exception e ->        h e
end

(* For early return, we abuse exceptions by throwing and catching
   the return value. The exception type is "either 'r 'e", where "Right e"
   represents a proper exception and "Left r" an early return of value "r". *)
type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e)

val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e
let early_return r = throw (Left r)

val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e
let catch_early_return m =
  try_catch m
    (function
      | Left a -> return a
      | Right e -> throw e
     end)

(* Lift to monad with early return by wrapping exceptions *)
val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e
let liftR m = try_catch m (fun e -> throw (Right e))

(* Catch exceptions in the presence of early returns *)
val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) ->  monadR 'rv 'a 'r 'e2
let try_catchR m h =
  try_catch m
    (function
      | Left r -> throw (Left r)
      | Right e -> h e
     end)

val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e
let maybe_fail msg = function
  | Just a -> return a
  | Nothing -> Fail msg
end

val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
let read_mem_bytes rk addr sz =
  Read_mem rk (bits_of addr) (nat_of_int sz) return

val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
let read_mem rk addr sz =
  bind
    (read_mem_bytes rk addr sz)
    (fun bytes ->
       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))

val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
let read_tag addr = Read_tag (bits_of addr) return

val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
let excl_result () =
  let k successful = (return successful) in
  Excl_res k

val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())

val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
let write_mem_val v = match mem_bytes_of_bits v with
  | Just v -> Write_memv v return
  | Nothing -> Fail "write_mem_val"
end

val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
let write_tag addr b = Write_tag (bits_of addr) b return

val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
let read_reg reg =
  let k v =
    match reg.of_regval v with
      | Just v -> Done v
      | Nothing -> Fail "read_reg: unrecognised value"
    end
  in
  Read_reg reg.name k

(* TODO
val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
let read_reg_range reg i j =
  read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))

let read_reg_bit reg i =
  read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
  return (extract_only_element v)

let read_reg_field reg regfield =
  read_reg_aux (external_reg_field_whole reg regfield)

let read_reg_bitfield reg regfield =
  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
  return (extract_only_element v)*)

let reg_deref = read_reg

val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e
let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())

(* TODO
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 (nat_of_int i,nat_of_int j)) v
let write_reg_pos reg i v =
  let iN = nat_of_int 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 (nat_of_int i,nat_of_int 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*)

val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
let barrier bk = Barrier bk (Done ())

val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
let footprint _ = Footprint (Done ())