source: src/ERTL/ERTL.ma @ 745

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

Changes from yesterday. Slowly implementing the functorized imperative code from ERTL :(

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