source: src/joint/JointLTLLIN.ma @ 1166

Last change on this file since 1166 was 1166, checked in by mulligan, 10 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.