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_word64"
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_word64"
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_word64"
32
33end
34