blob: b90d93e29379c38ac5d505198dd66490160c01e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(*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()
|
