source: src/ERTL/ERTL.ma @ 735

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

Changes from today

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