open import Pervasives
open import State
open import Sail_values

let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l

let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v

let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l

let wMem_Val_NORMAL (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return ()
let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O

let DataMemoryBarrier_Reads () = return ()
let DataMemoryBarrier_Writes () = return ()
let DataMemoryBarrier_All () = return ()
let DataSynchronizationBarrier_Reads () = return ()
let DataSynchronizationBarrier_Writes () = return ()
let DataSynchronizationBarrier_All () = return ()
let InstructionSynchronizationBarrier () = return ()