(*Generated by Lem from handwritten_support/0.11/mem_metadata.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory lem_pervasives_extraTheory sail2_instr_kindsTheory sail2_valuesTheory sail2_prompt_monadTheory sail2_operators_mwordsTheory sail2_promptTheory;

val _ = numLib.prefer_num();



val _ = new_theory "mem_metadata"

(*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*)
val _ = Define `
 ((write_ram:write_kind -> 'a words$word -> int -> 'n words$word -> unit -> 'rv sail2_state_monad$sequential_state ->(((bool),'e)sail2_state_monad$result#'rv sail2_state_monad$sequential_state)set) wk addr width data meta=
   (sail2_state_monad$write_memS 
  instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict 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*)
val _ = Define `
 ((read_ram:read_kind -> 'a words$word -> int -> bool -> 'rv sail2_state_monad$sequential_state ->((('n words$word#unit),'e)sail2_state_monad$result#'rv sail2_state_monad$sequential_state)set) rk addr width read_tag=  (sail2_state_monad$bindS
  (sail2_state_monad$read_memS 
  instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict rk ()  addr width) (\ (data :  'n words$word) . 
  sail2_state_monad$returnS (data, () ))))`;

val _ = export_theory()