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