source: src/LIN/JointLTLLIN.ma @ 1132

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

reunified ltl and lin instruction type, removing lifting in ltl and lin and simplifying the ertl > ertl passes

File size: 1.5 KB
Line 
1include "ASM/String.ma".
2include "ASM/I8051.ma".
3include "common/CostLabel.ma".
4include "common/Graphs.ma".
5include "common/AST.ma".
6include "common/Registers.ma".
7
8inductive joint_instruction (globals: list ident): Type[0] ≝
9  | joint_instr_comment: String → joint_instruction globals
10  | joint_instr_cost_label: costlabel → joint_instruction globals
11  | joint_instr_int: Register → Byte → joint_instruction globals
12  | joint_instr_pop: joint_instruction globals
13  | joint_instr_push: joint_instruction globals
14  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
15  | joint_instr_from_acc: Register → joint_instruction globals
16  | joint_instr_to_acc: Register → joint_instruction globals
17  | joint_instr_opaccs: OpAccs → joint_instruction globals
18  | joint_instr_op1: Op1 → joint_instruction globals
19  | joint_instr_op2: Op2 → Register → joint_instruction globals
20  | joint_instr_clear_carry: joint_instruction globals
21  | joint_instr_set_carry: joint_instruction globals
22  | joint_instr_load: joint_instruction globals
23  | joint_instr_store: joint_instruction globals
24  | joint_instr_call_id: ident → joint_instruction globals
25  | joint_instr_cond_acc: label → joint_instruction globals.
26
27inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
28  | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
29  | joint_st_goto: label → joint_statement A globals
30  | joint_st_return: joint_statement A globals.
Note: See TracBrowser for help on using the repository browser.