source: src/ERTL/ERTL.ma @ 733

Last change on this file since 733 was 733, checked in by mulligan, 10 years ago

Fixed partial commit.

File size: 2.6 KB
Line 
1include "ASM/I8051.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "utilities/IdentifierTools.ma".
4include "common/Graphs.ma".
5
6definition Registers ≝ list Register.
7
8definition AbstractRegister ≝ nat.
9
10inductive ERTLStatement: Type[0] ≝
11  | ERTL_St_Skip: Identifier → ERTLStatement
12  | ERTL_St_Comment: String → Identifier → ERTLStatement
13  | ERTL_St_Cost: Identifier → Identifier → ERTLStatement
14  | ERTL_St_Get_Hdw: Register → AbstractRegister → Identifier → ERTLStatement
15  | ERTL_St_Set_Hdw: AbstractRegister → Register → Identifier → ERTLStatement
16  | ERTL_St_Hdw_To_Hdw: Register → Register → Identifier → ERTLStatement
17  | ERTL_St_NewFrame: Identifier → ERTLStatement
18  | ERTL_St_DelFrame: Identifier → ERTLStatement
19  | ERTL_St_FrameSize: AbstractRegister → Identifier → ERTLStatement
20  | ERTL_St_Pop: AbstractRegister → Identifier → ERTLStatement
21  | ERTL_St_Push: AbstractRegister → Identifier → ERTLStatement
22  | ERTL_St_AddrH: AbstractRegister → Identifier → Identifier → ERTLStatement
23  | ERTL_St_AddrL: AbstractRegister → Identifier → Identifier → ERTLStatement
24  | ERTL_St_Int: AbstractRegister → Byte → Identifier → ERTLStatement
25  | ERTL_St_Move: AbstractRegister → AbstractRegister → Identifier → ERTLStatement
26  | ERTL_St_Opaccs: OpAccs → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
27  | ERTL_St_Op1: Op1 → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
28  | ERTL_St_Op2: Op2 → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
29  | ERTL_St_ClearCarry: Identifier → ERTLStatement
30  | ERTL_St_Load: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
31  | ERTL_St_Store: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
32  | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement.
33
34definition ERTLStatementGraph ≝ graph ERTLStatement.
35
36record ERTLInternalFunction: Type[0] ≝
37{
38  ERTL_IF_LUniverse: Universe;
39  ERTL_IF_RUniverse: Universe;
40  ERTL_IF_Params: Byte;
41  ERTL_IF_Locals: BitVectorTrieSet 16;
42  ERTL_IF_Graph: ERTLStatementGraph;
43  ERTL_IF_Entry: Identifier;
44  ERTL_IF_Exit: Identifier
45}.
46
47inductive ERTLFunction: Type[0] ≝
48  | ERTL_Fu_Internal: ERTLInternalFunction → ERTLFunction
49  | ERTL_Fu_External: ExternalFunction → ERTLFunction.
50 
51record ERTLProgram: Type[0] ≝
52{
53  ERTL_Pr_Vars: list (Identifier × nat);
54  ERTL_Pr_Funcs: list (Identifier × ERTLFunction);
55  ERTL_Pr_Main: option Identifier
56}.
Note: See TracBrowser for help on using the repository browser.