diff options
Diffstat (limited to 'snapshots/isabelle/riscv/Riscv_extras.thy')
| -rw-r--r-- | snapshots/isabelle/riscv/Riscv_extras.thy | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/snapshots/isabelle/riscv/Riscv_extras.thy b/snapshots/isabelle/riscv/Riscv_extras.thy index 8e371170..0a4528fe 100644 --- a/snapshots/isabelle/riscv/Riscv_extras.thy +++ b/snapshots/isabelle/riscv/Riscv_extras.thy @@ -1,16 +1,16 @@ -chapter \<open>Generated by Lem from riscv_extras.lem.\<close> +chapter \<open>Generated by Lem from \<open>riscv_extras.lem\<close>.\<close> theory "Riscv_extras" -imports - Main - "Lem_pervasives" - "Lem_pervasives_extra" - "Sail2_instr_kinds" - "Sail2_values" - "Sail2_operators_mwords" - "Sail2_prompt_monad" - "Sail2_prompt" +imports + Main + "LEM.Lem_pervasives" + "LEM.Lem_pervasives_extra" + "Sail.Sail2_instr_kinds" + "Sail.Sail2_values" + "Sail.Sail2_operators_mwords" + "Sail.Sail2_prompt_monad" + "Sail.Sail2_prompt" begin @@ -122,10 +122,10 @@ definition MEMr_reserved_strong_acquire :: " int \<Rightarrow> int \<Rightarrow (*val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => - integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e*) -definition write_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('rv,(unit),'e)monad " where + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e*) +definition write_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('rv,(bool),'e)monad " where " write_ram addrsize size1 hexRAM address value1 = ( - write_mem_val instance_Sail2_values_Bitvector_Machine_word_mword_dict value1 \<bind> (\<lambda>x . (case x of _ => return () )) )" + write_mem_val instance_Sail2_values_Bitvector_Machine_word_mword_dict value1 )" (*val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => |