diff options
Diffstat (limited to 'handwritten_support/mem_metadata.lem')
| -rw-r--r-- | handwritten_support/mem_metadata.lem | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem new file mode 100644 index 0000000..8a8c070 --- /dev/null +++ b/handwritten_support/mem_metadata.lem @@ -0,0 +1,16 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e +let write_ram wk addr width data meta = + write_mem wk () addr width data + +val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +let read_ram rk addr width read_tag = + read_mem rk () addr width >>= (fun (data : mword 'n) -> + return (data, ())) |