diff options
Diffstat (limited to 'handwritten_support/0.11/mem_metadata.lem')
| -rw-r--r-- | handwritten_support/0.11/mem_metadata.lem | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem deleted file mode 100644 index 8a8c070..0000000 --- a/handwritten_support/0.11/mem_metadata.lem +++ /dev/null @@ -1,16 +0,0 @@ -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, ())) |