1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory; 4 5val _ = new_theory "ppc_coretypes"; 6 7 8(* ---------------------------------------------------------------------------------- *> 9 10 This theory defines the types and operations over these types for the PowerPC model. 11 12<* ---------------------------------------------------------------------------------- *) 13 14(* used by the AST *) 15 16val _ = type_abbrev("ireg",``:word5``); 17val _ = type_abbrev("freg",``:word5``); 18val _ = type_abbrev("ppc_constant",``:word16``); 19val _ = type_abbrev("crbit",``:word2``); 20 21(* used elsewhere *) 22 23val _ = Hol_datatype ` 24 ppc_bit = PPC_CARRY (* carry bit of the status register *) 25 | PPC_CR0 of word2 (* bit i of the condition register *)`; 26 27val _ = Hol_datatype ` 28 ppc_reg = PPC_IR of word5 (* integer registers *) 29 | PPC_LR (* link register (return address) *) 30 | PPC_CTR (* count register, used for some branches *) 31 | PPC_PC (* program counter *)`; 32 33val _ = Hol_datatype `iiid = <| proc : num ; program_order_index : num |>`; 34 35 36val _ = export_theory (); 37