1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory ArchStructures_H
12imports
13  "Lib.Lib"
14  "../Types_H"
15  Hardware_H
16begin
17
18context Arch begin global_naming X64_H
19
20#INCLUDE_SETTINGS keep_constructor=asidpool
21#INCLUDE_SETTINGS keep_constructor=arch_tcb
22
23#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H decls_only
24#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H instanceproofs
25#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H bodies_only
26
27datatype arch_kernel_object_type =
28    PDET
29  | PTET
30  | PDPTET
31  | PML4ET
32  | ASIDPoolT
33
34primrec
35  archTypeOf :: "arch_kernel_object \<Rightarrow> arch_kernel_object_type"
36where
37  "archTypeOf (KOPDE e) = PDET"
38| "archTypeOf (KOPTE e) = PTET"
39| "archTypeOf (KOPDPTE e) = PDPTET"
40| "archTypeOf (KOPML4E e) = PML4ET"
41| "archTypeOf (KOASIDPool e) = ASIDPoolT"
42
43end
44end
45