source: src/joint/JointLTLLIN.ma @ 1166

Last change on this file since 1166 was 1166, checked in by mulligan, 8 years ago

moved joint ltl lin files into their own directory. more changes to ltl and lin passes to help type checker in ertl pass

File size: 3.1 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 registers_move: Type[0] ≝
9  | from_acc: Register → registers_move
10  | to_acc: Register → registers_move.
11
12inductive joint_instruction
13  (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
14  (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
15  | joint_instr_comment: String → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
16  | joint_instr_cost_label: costlabel → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
17  | joint_instr_int: generic_reg → Byte → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
18  | joint_instr_move: pair_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
19  | joint_instr_pop: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
20  | joint_instr_push: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
21  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
22  | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
23  | joint_instr_op1: Op1 → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
24  | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
25  | joint_instr_clear_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
26  | joint_instr_set_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
27  | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
28  | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
29  | joint_instr_call_id: ident → nat → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
30  | joint_instr_cond: acc_a_reg → label → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
31
32inductive joint_statement
33  (A: Type[0]) (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
34  (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
35  | joint_st_sequential: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals → A → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
36  | joint_st_goto: label → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
37  | joint_st_return: joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
Note: See TracBrowser for help on using the repository browser.