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