| 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.
