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
11(*
12   Types visible in the API.
13*)
14
15chapter "Arch-dependant Types visible in the API"
16
17theory ArchTypes_H
18imports
19  State_H
20  Hardware_H
21  "Lib.Lib"
22begin
23
24#INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits
25
26context Arch begin global_naming X64_H
27
28#INCLUDE_HASKELL SEL4/API/Types/X64.lhs CONTEXT X64_H
29
30end
31
32text {* object\_type instance proofs *}
33
34qualify X64_H (in Arch)
35instantiation X64_H.object_type :: enum
36begin
37interpretation Arch .
38definition
39  enum_object_type: "enum_class.enum \<equiv>
40    map APIObjectType (enum_class.enum :: apiobject_type list) @
41     [PDPointerTableObject,
42      PML4Object,
43      HugePageObject,
44      SmallPageObject,
45      LargePageObject,
46      PageTableObject,
47      PageDirectoryObject
48    ]"
49
50definition
51  "enum_class.enum_all (P :: object_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
52
53definition
54  "enum_class.enum_ex (P :: object_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
55
56  instance
57    apply intro_classes
58     apply (safe, simp)
59     apply (case_tac x)
60    apply (simp_all add: enum_object_type)
61    apply (auto intro: distinct_map_enum
62                 simp: enum_all_object_type_def enum_ex_object_type_def)
63    done
64end
65
66
67instantiation X64_H.object_type :: enum_alt
68begin
69interpretation Arch .
70definition
71  enum_alt_object_type: "enum_alt \<equiv>
72    alt_from_ord (enum :: object_type list)"
73instance ..
74end
75
76instantiation X64_H.object_type :: enumeration_both
77begin
78interpretation Arch .
79instance by (intro_classes, simp add: enum_alt_object_type)
80end
81
82context begin interpretation Arch .
83requalify_types object_type
84end
85
86end
87