source: src/LIN/JointLTLLIN.ma @ 733

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

Fixed partial commit.

File size: 1.4 KB
Line 
1include "ASM/String.ma".
2include "ASM/I8051.ma".
3include "common/AST.ma".
4
5inductive 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
23inductive 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.