1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ArchSetup 8imports 9 "CLib.CTranslationNICTA" 10begin 11 12abbreviation (input) 13 "(arch_load_machine_word 14 (load_word32 :: word32 mem_read) 15 (load_word64 :: word64 mem_read) 16 :: machine_word mem_read) 17 \<equiv> load_word32" 18 19abbreviation (input) 20 "(arch_store_machine_word 21 (store_word32 :: word32 mem_upd) 22 (store_word64 :: word64 mem_upd) 23 :: machine_word mem_upd) 24 \<equiv> store_word32" 25 26abbreviation (input) 27 "(arch_machine_word_constructor 28 (from_word32 :: word32 \<Rightarrow> 'a) 29 (from_word64 :: word64 \<Rightarrow> 'a) 30 :: machine_word \<Rightarrow> 'a) 31 \<equiv> from_word32" 32 33end 34