- Timestamp:
- Sep 2, 2011, 11:36:15 AM (10 years ago)
- Location:
- src/LIN
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LIN.ma
r1167 r1168 1 include "Joint/JointLTLLIN.ma". 2 3 inductive pre_lin_statement (globals: list ident): Type[0] ≝ 4 | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals. 1 include "joint/Joint.ma". 2 3 definition lin_params: params ≝ 4 mk_params unit unit unit unit registers_move Register. 5 6 definition pre_lin_statement ≝ 7 λglobals: list ident. joint_statement unit lin_params globals. 5 8 6 9 definition lin_statement ≝ -
src/LIN/LINToASM.ma
r1149 r1168 35 35 match instr' with 36 36 [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 37 | joint_instr_cond _acclbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)37 | joint_instr_cond lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 38 38 | _ ⇒ set_empty ? 39 39 ]
Note: See TracChangeset
for help on using the changeset viewer.