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