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