open import Pervasives_extra
open import Vector
open import Arch

let compose f g x = f (g x)

type end_flag =
  | E_big_endian
  | E_little_endian

type direction = 
  | D_increasing
  | D_decreasing

type register_value = <| 
    rv_bits: list bit (* MSB first, smallest index number *); 
    rv_dir: direction; 
    rv_start: nat ;
    rv_start_internal: nat; 
    (*when dir is increasing, rv_start = rv_start_internal. 
      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
    |>

type byte = list bit (* of length 8 *)  (*MSB first everywhere*)

type address = integer
type address_lifted = address

type memory_value = list byte
(* the list is of length >=1 *)
(* for both big-endian (Power) and little-endian (ARM), the head of the
     list is the byte stored at the lowest address *)
(* for big-endian Power the head of the list is the most-significant
   byte, in both the interpreter and machineDef* code. *)
(* For little-endian ARM, the head of the list is the
   least-significant byte in machineDef* code and the
   most-significant byte in interpreter code, with the switch over
   (a list-reverse) being done just inside the interpreter interface*)
(* In other words, in the machineDef* code the lowest-address byte is first,
   and in the interpreter code the most-significant byte is first *)

type opcode = Opcode of list byte (* of length 4 *)

type read_kind =
  (* common reads *)
  | Read_plain
  (* Power reads *)
  | Read_reserve
  (* AArch64 reads *)
  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream

type write_kind =
  (* common writes *)
  | Write_plain
  (* Power writes *)
  | Write_conditional
  (* AArch64 writes *)
  | Write_release | Write_exclusive | Write_exclusive_release

type barrier_kind =
  (* Power barriers *)
  | Sync | LwSync | Eieio | Isync
  (* AArch64 barriers *)
  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 

type slice = (nat * nat)

type reg_name = 
  (* Name of the register, accessing the entire register, the start and size of this register, 
   * and its direction *)
  | Reg of string * nat * nat * direction
                                  
  (* Name of the register, accessing from the bit indexed by the first
   * to the bit indexed by the second integer of the slice, inclusive. For
   * machineDef* the first is a smaller number or equal to the second.  *)
  | Reg_slice of string * nat * direction * slice 
                                              
  (* Name of the register, start and direction, and name of the field of the register
   * accessed. The slice specifies where this field is in the register*)
  | Reg_field of string * nat * direction * string * slice 

  (* The first four components are as in Reg_field; the final slice
   * specifies a part of the field, indexed w.r.t. the register as a whole *)
  | Reg_f_slice of string * nat * direction * string * slice * slice 

type outcome 'e 'a =
  (* Request to read memory, value is location to read followed by registers that location depended 
   * on when mode.track_values, integer is size to read, followed by registers that were used in 
   * computing that size *)
  (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
  | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *
                  (memory_value -> outcome 'a)
                    
  (* Request to write memory, first value and dependent registers is location, second is the value 
   * to write *)
  | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value *
                   maybe (list reg_name) * (bool -> outcome 'a)
                                             
  (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
  | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'a
                                                                              
  (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
   * ea signal *)
  | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'a)
                                                           
  (* Request a memory barrier *)
  (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
   * need that *)
  | Barrier of barrier_kind * outcome 'a
                                
  (* Tell the system to dynamically recalculate dependency footprint *)
  | Footprint of outcome 'a
                   
  (* Request to read register *)
  | Read_reg of reg_name * (register_value -> outcome 'a)
                             
  (* Request to write register *)
  | Write_reg of reg_name * register_value * outcome 'a
                                               
  (* List of instruction states to be run in parrallel, any order permitted.
     Expects concurrency model to choose an order: a permutation of the original list *)
  | Nondet_choice of list (outcome unit) * (list (outcome unit) -> outcome 'a)
                                                
  (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
   * provide a handler. *)
  | Escape 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)

  (* Stop for incremental stepping, function can be used to display function call data *)
  | Done of 'a

type M 'e 'a = outcome 'e 'a

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

val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c)

val (>>) : forall 'b. M unit -> (unit -> M 'b) -> M 'b
let (>>) m n = m >>= fun _ -> n

let rec (>>=) m f = match m with
  | Done a -> f a
  | Read_mem rk addr sz rs k ->        Read_mem rk addr sz rs        (fun v -> (k v) >>= f)
  | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> (k b) >>= f)
  | Write_ea wk addr sz rs k ->        Write_ea wk addr sz rs        (k >>= f)
  | Write_memv v rs k ->               Write_memv v rs               (fun b -> (k b) >>= f)
  | Barrier bk k ->                    Barrier bk                    (k >>= f)
  | Footprint k ->                     Footprint                     (k >>= f)
  | Read_reg reg k ->                  Read_reg reg                  (fun v -> (k v) >>= f)
  | Write_reg reg v k ->               Write_reg reg v               (k >>= f)
  | Nondet_choice actions k ->         Nondet_choice actions         (fun c -> (k c) >>= f)
  | Escape -> Escape
  end

val exit : forall 'a 'e. 'e -> M 'a
let exit _ = Escape

val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
let rec byte_chunks n list = match (n,list) with
  | (0,_) -> []
  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
  | _ -> failwith "byte_chunks not given enough bits"
end

val bitvFromBytes : list byte -> vector bit
let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir

let dir is_inc = if is_inc then D_increasing else D_decreasing

val bitvFromRegisterValue : register_value -> vector bit
let bitvFromRegisterValue v =
  V (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)

val registerValueFromBitv : vector bit -> register -> register_value
let registerValueFromBitv (V bits start is_inc) reg = 
  let start = natFromInteger start in
  <| rv_bits = bits;
     rv_dir = dir is_inc;
     rv_start_internal = start;
     rv_start = start+1 - (natFromInteger (length_reg reg)) |>

val read_memory : read_kind -> integer -> integer -> M (vector bit)
let read_memory rk addr sz =
  let sz = natFromInteger sz in
  Read_mem rk addr sz Nothing (compose Done bitvFromBytes)

val write_memory : write_kind -> integer -> integer -> vector bit -> M bool
let write_memory wk addr sz (V v _ _) =
  let sz = natFromInteger sz in
  Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done

val read_reg_range : register -> (integer * integer) -> M (vector bit)
let read_reg_range reg (i,j) =
  let (i,j) = (natFromInteger i,natFromInteger j) in
  let start = natFromInteger (start_index_reg reg) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  Read_reg reg (compose Done bitvFromRegisterValue)

val write_reg_range : register -> (integer * integer) -> vector bit -> M unit
let write_reg_range reg (i,j) v =
  let rv = registerValueFromBitv v reg in
  let start = natFromInteger (start_index_reg reg) in
  let (i,j) = (natFromInteger i,natFromInteger j) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  Write_reg reg rv (Done ())

val read_reg_bit : register -> integer -> M bit
let read_reg_bit reg i = 
  let i = natFromInteger i in
  let start = natFromInteger (start_index_reg reg) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
  Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))

val write_reg_bit : register -> integer -> bit -> M unit
let write_reg_bit reg i bit = write_reg_range reg (i,i) (V [bit] 0 true)

val read_reg : register -> M (vector bit)
let read_reg reg =
  let start = natFromInteger (start_index_reg reg) in
  let sz = natFromInteger (length_reg reg) in
  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
  Read_reg reg (compose Done bitvFromRegisterValue)

val write_reg : register -> vector bit -> M unit
let write_reg reg v =
  let rv = registerValueFromBitv v reg in
  let start = natFromInteger (start_index_reg reg) in
  let sz = natFromInteger (length_reg reg) in
  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
  Write_reg reg rv (Done ())

val read_reg_field : register -> register_field -> M (vector bit)
let read_reg_field reg rfield = 
  let (i,j) =
    let (i,j) = field_indices rfield in
    (natFromInteger i,natFromInteger j) in
  let start = natFromInteger (start_index_reg reg) in
  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
  Read_reg reg (compose Done bitvFromRegisterValue)

val write_reg_field : register -> register_field -> vector bit -> M unit
let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)

val read_reg_bitfield : register -> register_bitfield -> M bit
let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)

val write_reg_bitfield : register -> register_bitfield -> bit -> M unit
let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)

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


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