Line | |
---|
1 | include "ASM/String.ma". |
---|
2 | include "ASM/I8051.ma". |
---|
3 | include "common/AST.ma". |
---|
4 | |
---|
5 | inductive JointInstruction (globals: list Identifier): Type[0] ≝ |
---|
6 | | Joint_Instr_Comment: String → JointInstruction globals |
---|
7 | | Joint_Instr_CostLabel: Identifier → JointInstruction globals |
---|
8 | | Joint_Instr_Int: Register → Byte → JointInstruction globals |
---|
9 | | Joint_Instr_Pop: JointInstruction globals |
---|
10 | | Joint_Instr_Push: JointInstruction globals |
---|
11 | | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals |
---|
12 | | Joint_Instr_FromAcc: Register → JointInstruction globals |
---|
13 | | Joint_Instr_ToAcc: Register → JointInstruction globals |
---|
14 | | Joint_Instr_OpAccs: OpAccs → JointInstruction globals |
---|
15 | | Joint_Instr_Op1: Op1 → JointInstruction globals |
---|
16 | | Joint_Instr_Op2: Op2 → Register → JointInstruction globals |
---|
17 | | Joint_Instr_ClearCarry: JointInstruction globals |
---|
18 | | Joint_Instr_Load: JointInstruction globals |
---|
19 | | Joint_Instr_Store: JointInstruction globals |
---|
20 | | Joint_Instr_CallId: Identifier → JointInstruction globals |
---|
21 | | Joint_Instr_CondAcc: Identifier → JointInstruction globals. |
---|
22 | |
---|
23 | inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝ |
---|
24 | | Joint_St_Sequential: JointInstruction globals → A → JointStatement A globals |
---|
25 | | Joint_St_Goto: Identifier → JointStatement A globals |
---|
26 | | Joint_St_Return: JointStatement A globals. |
---|
Note: See
TracBrowser
for help on using the repository browser.