- Timestamp:
- Sep 1, 2011, 4:53:01 PM (10 years ago)
- Location:
- src/LIN
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/JointLTLLIN.ma
r1163 r1164 6 6 include "common/Registers.ma". 7 7 8 inductive registers_move: Type[0] ≝ 9 | from_acc: Register → registers_move 10 | to_acc: Register → registers_move. 11 8 12 inductive joint_instruction 9 ( globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])10 (dp l_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝11 | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg12 | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg13 | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg14 | joint_instr_move: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg15 | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg16 | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg17 | 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 pair_reg generic_reg18 | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg19 | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg20 | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg21 | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg22 | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg23 | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg24 | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg25 | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg26 | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.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. 27 31 28 32 inductive joint_statement 29 (A: Type[0]) ( globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])30 (dp l_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝31 | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg32 | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg33 | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.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. -
src/LIN/LIN.ma
r1163 r1164 2 2 3 3 definition pre_lin_statement ≝ 4 λglobals. 5 joint_statement unit globals Register Register 4 joint_statement unit Register Register 6 5 Register Register Register 7 (Register × Register).6 registers_move. 8 7 9 8 definition lin_statement ≝
Note: See TracChangeset
for help on using the changeset viewer.