- Timestamp:
- Aug 31, 2011, 6:24:03 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/JointLTLLIN.ma
r1132 r1161 6 6 include "common/Registers.ma". 7 7 8 inductive 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. 8 inductive joint_instruction 9 (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) 10 (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0]) 11 (pair_reg: Type[0]): Type[0] ≝ 12 | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 13 | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 14 | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 15 | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 16 | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 17 | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 18 | joint_instr_hdw_to_hdw: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 19 | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 20 | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 21 | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 22 | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 23 | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 24 | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 25 | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 26 | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 27 | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg. 26 28 27 inductive 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. 29 inductive joint_statement 30 (A: Type[0]) (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) 31 (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0]) (pair_reg: Type[0]): Type[0] ≝ 32 | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 33 | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg 34 | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
Note: See TracChangeset
for help on using the changeset viewer.